not xor

Stream: Is there code for X?

[Andrew Yang]

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]

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]

I suppose xor is for Props?
At least #check tells me that xor : Prop → Prop → Prop.

[Yaël Dillies]

Oh wait. There's a xor for Props? Well then yeah those lemmas are nice.

[Ruben Van de Velde]

bxor is for booleans, apparently

[Yaël Dillies]

Probably belong in logic.basic.