Zulip Chat Archive

Stream: new members

Topic: bool.bxor_iff_eq


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:44):

in short, make everything a prop as soon as possible

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:44):

Also, every theorem about bool can be proven by dec_trivial

view this post on Zulip Patrick Massot (Jun 10 2020 at 13:44):

by \neg you mean \not, right?

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:44):

yes

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:45):

they both work

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:46):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 10 2020 at 13:49):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:51):

why would you need a unicode hotkey for -?

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:51):

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

view this post on Zulip Patrick Massot (Jun 10 2020 at 13:55):

No idea.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:59):

vscode says I could just use \n

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:59):

which neatly avoids the abbreviation question


Last updated: May 14 2021 at 00:42 UTC