Precisely one of these holds

Stream: mathlib4

[Michael Rothgang]

What's the idiomatic mathlib spelling for "exactly one of these conditions holds"?
(Case in point is #9343: the result is "either condition A xor condition B holds". The current solution is a lemma $\lnot A$ iff $B$, which is slightly cumbersome to prove.)

[Yury G. Kudryashov]

See docs#Xor'

[Yury G. Kudryashov]

IMHO, we should define an instance of docs#Xor for docs#Prop and docs#Bool, then use the ^^^ notation.

[Yaël Dillies]

No, you should use docs#symmDiff instead

[Johan Commelin]

I'm not sure... We also don't use $\cup$ and $\cap$ instead of $\lor$ and $\land$...

[Eric Rodriguez]

we can make some nice notation for symmdiff. I'm surprised we haven't ran into this much before; I think many, many of the Ors written in mathlib right now are of this form

[Adam Topaz]

Personally I think we should set something up similar to docs#List.TFAE for this.

[Johan Commelin]

X1OTFIT = "exactly one of the following is true"

[Adam Topaz]

List.ExactlyOne

[Yury G. Kudryashov]

We can have both a List and a binary version. I think that the operation on Prop should be called xor in theorem names. I don't care which notation does it use.

[Michael Rothgang]

Thanks for all the pointers! I've gone with Xor for now - if there's consensus to use otherwise or a reviewer objects, this can be changed easily.

[Wrenna Robson]

I think it probably shouldn't use ^^^ because we have a different symbol for "Boolean and" and ∧, right?

[Wrenna Robson]

Unfortunately this operation is quite an overloaded one, semantically. But I think @Yaël Dillies is right: ∆ is good.

[Wrenna Robson]

It is worth thinking about what you'd actually do with such statements, mind. And and Or decompose easily enough.

[Eric Wieser]

∆ is no good for the n-ary statement

[Wrenna Robson]

good point

[Wrenna Robson]

But then, again, it isn't clear to me (from a structural point of view) how you should use such a proposition.

For A_i, I suppose what you have is a) a proof of A_1 or A_2.. or A_n, and b) a proof that A_i -> not (A_j) for i \ne j.

[Wrenna Robson]

It's a little bit like being pairwise disjoint, actually.

[Wrenna Robson]

That is probably the analogous n-ary statement on sets.

[Wrenna Robson]

What you probably want is a symbol for "at most one of these is true", which is that. And then or covers "at least one of these is true".

[Wrenna Robson]

Any two of them imply False.

[Kevin Buzzard]

Eric Wieser said:

∆ is no good for the n-ary statement

I guess ∆ is great for "an odd number of these statements are true" :-)

[Wrenna Robson]

example (ι : Type*) (p : ι → Prop) : Prop := Pairwise (fun i j => ¬ (p i) ∨ ¬ (p j)) ∧ ∃ i, p i

[Wrenna Robson]

Something like this?

[Wrenna Robson]

example (ι : Type*) (p : ι → Prop) : Prop := Pairwise (Or on (Not ∘ p)) ∧ ∃ i, p i

or this, if you want to be cute.

[Eric Wieser]

∃! i, p i seems like the obvious spelling

[Wrenna Robson]

Yes I was about to say, if you want to bundle everything together, that is the one.

[Wrenna Robson]

But in practice I think you will, I'm prepared to say 99% of the time, prove that by proving the left and the right there.

[Wrenna Robson]

Incidentally, where is ∃! defined? Docs search isn't giving me it.

[Wrenna Robson]

nvm got it.
ExistsUnique p = ∃ (x : α), p x ∧ ∀ (y : α), p y → y = x

[Wrenna Robson]

Not sure if that's easier or harder to work with in practice.

[Wrenna Robson]

like I can imagine in some cases wanting to split the proof of "at most one" and "at least one", and here, you show "at most one" and then "any others are that one"

[Yaël Dillies]

Wrenna Robson said:

It's a little bit like being pairwise disjoint, actually.

It is exactly being a partition of True.

[Yury G. Kudryashov]

BTW, do we have (∃! b : Bool, p b) <-> Xor' (p true) (p false)?