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