Stream: new members

Topic: bool.bxor_iff_eq

Donald Sebastian Leung (Jun 10 2020 at 13:38):

In data.bool, there is a lemma bool.bxor_iff_ne which states that bxor x y = bool.tt ↔ x ≠ y for all x, y; however, there doesn't seem to be bool.bxor_iff_eq stating that bxor x y = bool.ff ↔ x = y. Did I miss something?

Patrick Massot (Jun 10 2020 at 13:41):

I'm not too surprised that bool misses lemmas. Either you're proving stuff and work with Prop or you're programming and work with bool without needing lemmas.

Mario Carneiro (Jun 10 2020 at 13:43):

I would rather see this lemma proven by rewriting bxor x y = bool.ff to \neg \u (bxor x y) and from there to \neg (x != y) and then x = y

Mario Carneiro (Jun 10 2020 at 13:44):

in short, make everything a prop as soon as possible

Mario Carneiro (Jun 10 2020 at 13:44):

Also, every theorem about bool can be proven by dec_trivial

Patrick Massot (Jun 10 2020 at 13:44):

by \neg you mean \not, right?

yes

they both work

Mario Carneiro (Jun 10 2020 at 13:46):

it's also the actual LaTeX AFAIR so that's what my fingers know

Patrick Massot (Jun 10 2020 at 13:48):

Oh I see, they both triggered the same unicode translation. I though that you were saying -tt works.

Patrick Massot (Jun 10 2020 at 13:49):

It's a bit unfortunate since neg is lemma names means something completely different.

Mario Carneiro (Jun 10 2020 at 13:51):

why would you need a unicode hotkey for -?

Mario Carneiro (Jun 10 2020 at 13:51):

unless you are on a non-english keyboard that makes - hard to hit

No idea.

Patrick Massot (Jun 10 2020 at 13:56):

Why would you need a unicode hotkey for \not that would be anything other than \not or \non

Mario Carneiro (Jun 10 2020 at 13:59):

vscode says I could just use \n

Mario Carneiro (Jun 10 2020 at 13:59):

which neatly avoids the abbreviation question

Last updated: May 14 2021 at 00:42 UTC