bool.bxor_iff_eq

Stream: new members

[Donald Sebastian Leung]

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]

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]

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]

in short, make everything a prop as soon as possible

[Mario Carneiro]

Also, every theorem about bool can be proven by dec_trivial

[Patrick Massot]

by \neg you mean \not, right?

[Mario Carneiro]

yes

[Mario Carneiro]

they both work

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

why would you need a unicode hotkey for -?

[Mario Carneiro]

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

[Patrick Massot]

No idea.

[Patrick Massot]

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

[Mario Carneiro]

vscode says I could just use \n

[Mario Carneiro]

which neatly avoids the abbreviation question