Zulip Chat Archive
Stream: Is there code for X?
Topic: not xor
Andrew Yang (Dec 17 2021 at 12:43):
Do we not have these?
@[simp]
lemma not_xor (P Q : Prop) : ¬ xor P Q ↔ (P ↔ Q) :=
by simpa [xor, not_or_distrib] using (iff_iff_implies_and_implies _ _).symm
lemma xor_iff_not_iff (P Q : Prop) : xor P Q ↔ ¬ (P ↔ Q) :=
by rw [iff_not_comm, not_xor]
I'd also argue that not_xor
should be called by push_neg
, but I'm not sure how to do so.
Yaël Dillies (Dec 17 2021 at 12:52):
You're mixing up the bool
and Prop
worlds in a weird way. We can't prove everything for Prop
, everything for bool
, and everything where both are mixed up in all ways. So I'd argue this lemma should only be about bool
and use bnot
.
Andrew Yang (Dec 17 2021 at 12:54):
I suppose xor
is for Props?
At least #check
tells me that xor : Prop → Prop → Prop
.
Yaël Dillies (Dec 17 2021 at 12:56):
Oh wait. There's a xor
for Props? Well then yeah those lemmas are nice.
Ruben Van de Velde (Dec 17 2021 at 12:57):
bxor
is for booleans, apparently
Yaël Dillies (Dec 17 2021 at 12:57):
Probably belong in logic.basic
.
Last updated: Dec 20 2023 at 11:08 UTC