exactly one of the following holds

Stream: general

[Shreyas Srinivas]

How does one canonically state theorems of the form “exactly one of the following statements is true”. One trick I can have tried is to define an inductive Type (not Prop ) in which constructors hold each of the individual props. Is this correct/ideal?

[Chris Henson]

Something similar to docs#List.TFAE maybe?

[Shreyas Srinivas]

My propositions are not equivalent

[Shreyas Srinivas]

Quite the opposite

[Shreyas Srinivas]

If any of the propositions are true, the others are not.

[Shreyas Srinivas]

And one of them is necessarily true

[Chris Henson]

Yes I understand, I said similar. The condition would be that any proposition in the list being true implies the negation of the others.

[Chris Henson]

You however asked for canonical, I am not aware of an existing definition for this.

[James E Hanson]

I don't think there's a canonical choice, and I don't know if this is the optimal way to do it, but this would work:

def ExactlyOne (ps : List Prop) : Prop
  := ∃! n : ℕ, ps[n]?.getD False

[Thomas Murrills]

I could have sworn I remember something like "EOTF" being discussed/proposed somewhere, but I can't find it... :thinking:

[Thomas Murrills]

There is this from 2022: #Is there code for X? > "exactly one of the following is true", which has some ideas!

[Thomas Murrills]

Ah, I think I'm thinking of a discussion from the discord! It was spelled EOFT there, if you'd like to search—but I think you were part of that discussion anyway, so maybe you've already taken it into account. :grinning_face_with_smiling_eyes:

[Thomas Murrills]

My feeling is that (the lean4 version) of @Eric Wieser's suggestion in that thread above is the most similar in nature to the existing TFAE, and lets you avoid having a new inductive:

def EOTF : List Prop → Prop
  | [] => False
  | P :: l => P ∧ (∀ Q ∈ l, ¬Q) ∨ ¬ P ∧ EOTF l

[Shreyas Srinivas]

I actually wonder if a Finvec version is better

[Shreyas Srinivas]

Then we can use fin cases over the indices

[Shreyas Srinivas]

The extra inductive structure from lists seems unnecessary

[Snir Broshi]

James E Hanson said:

I don't think there's a canonical choice, and I don't know if this is the optimal way to do it, but this would work:

def ExactlyOne (ps : List Prop) : Prop
  := ∃! n : ℕ, ps[n]?.getD False

Why not

def ExactlyOne (ps : List Prop) : Prop :=
  ∃! p ∈ ps, p

[Snir Broshi]

Or generalized to support other list-ish containers:

def ExactlyOne {α : Type*} (ps : α) [Membership Prop α] : Prop :=
  ∃! p ∈ ps, p

works with List/Set/Finset/Multiset/Array
(doesn't generalize to finvec though)

[Robin Arnez]

Snir Broshi schrieb:

Why not

def ExactlyOne (ps : List Prop) : Prop :=
  ∃! p ∈ ps, p

import Mathlib

def ExactlyOne (ps : List Prop) : Prop :=
  ∃! p ∈ ps, p

example : ExactlyOne [True, True] := by
  rw [ExactlyOne]
  use True, ⟨List.mem_cons_self, trivial⟩
  simp

[Alex Meiburg]

This could still be suitably generalized with GetElem? though.

[Thomas Murrills]

Shreyas Srinivas said:

I actually wonder if a Finvec version is better

Hmm, yeah, that's interesting! It's a lot nicer for access too (P i); in some personal notes I have on TFAE I explore something similar, but over a general index set I instead of some Fin n. Fin/FinVec likely have some nice API around them that would actually make such a thing more practical, I imagine?

So, maybe it's worth experimenting with Fin.TFAE (or Fun.TFAE.{u} {I:Sort u} (P : I → Prop) : Prop := ∀ i j : I, P i ↔ P j!). The issue of course is compositionality...maps J → I give us TFAE subsets very nicely, but putting TFAE's together requires dealing with ⊕ or spans. But, the FinVec case might conceivably have nice operations for concatenating vectors? I'm not familiar with the API.

[Shreyas Srinivas]

Finvec has nice notation though I would like to see bulleted lists for this particular use case.

[Thomas Murrills]

Aside: In a P : I → Prop-centered description, TFAE P could be phrased as the fact that P factors through the unique function I → Unit, while EOTF P expresses that the constant map fun _ => True : Unit → Prop factors uniquely through P. Though, these representations don't lend themselves to very ergonomic formalizations in Lean, as far as I know. :)

Note: for symmetry, we might want to insist that TFAE P means that P factors uniquely through the unique function I → Unit. This is harmless when I is nonempty, but does conflict with Mathlib's definition when I is empty. Mathlib effectively drops the uniqueness and allows List.tfae_nil. Also, the alternative "factors uniquely" configurations among P and Unit are unfortunately trivial.

[Shreyas Srinivas]

Or maybe even named item lists so we get to talk about the individual hypothesis by names we pick.

[Thomas Murrills]

Shreyas Srinivas said:

Finvec has nice notation though I would like to see bulleted lists for this particular use case.

I would even like to go a step further and use numbered lists with optional names! :)

[Shreyas Srinivas]

Technically a finmap can achieve this. So take a finite type (for example an inductive type with 3 no argument constructors for naming 3 hypothesis

[Shreyas Srinivas]

And then, since you are only using the constructors as indices, why not just put the props with their indexing constructors. And suddenly you have the inductive type solution I mentioned above.

[Thomas Murrills]

The example notation I've been thinking about is something like

TFAE
  1. z ∈ Metric.sphere 0 1
  2 UnitNorm. ‖z‖ = 1
  3. ‖z‖ ^ 2 = 1

but the optional naming is a bit awkward.

[Thomas Murrills]

Shreyas Srinivas said:

And then, since you are only using the constructors as indices, why not just put the props with their indexing constructors. And suddenly you have the inductive type solution I mentioned above.

I feel like that might be load-bearing "just". :grinning_face_with_smiling_eyes: Doesn't this mean I can't have a uniform TFAE API that works across all such TFAE-like types, because each TFAE must apply to a different type which it knows nothing about? Or I need to have some kind of TFAE-API instance that I can apply with deriving?

[Shreyas Srinivas]

You put the api in a typeclass

[Shreyas Srinivas]

Anyway, I think life is simpler without one more typeclass. Finvec fits the bill neatly

[Thomas Murrills]

The other thing I would worry about with a typeclass-on-custom-type model is that it could make it harder to make TFAE's on the fly, mid-proof.

[Thomas Murrills]

I do wonder if it's worth having some way to actually store the name in the expression somehow by modifying the index type somehow; I think putting the Prop inside the index type might be rough, but I'm curious if we could allow naming via being a bit more flexible on our index type somehow.

Another solution is metadata somewhere, but this is liable to be erased; another is asking for Fin n → Prop × Name and just working around that, but that jettisons many nice properties (but, it keeps the name with the Prop even if the index changes, which is nice); another is an extension that tries to store indices or Props locally and guides an elaborator.

Every approach feels a little bit wrong, somehow...my inclination, if I had to give one, though, is that this is really an elaboration feature, and so should live in the elaborator somehow, not in the semantics of the expression.

[Shreyas Srinivas]

I think that's a nice ambition. For now I am going to go ahead with Finvecs

[Jihoon Hyun]

How about defining 'at most one is true' and 'at least one is true', as if we define singleton with exists and subsingleton?

[Shreyas Srinivas]

import Mathlib

def ExactlyOne {n} (propVec : Fin n → Prop) := ∃! i, propVec i

def AtLeastOne {n} (propVec : Fin n → Prop) := ∃ i, propVec i

def AtmostOne {n} (propVec : Fin n → Prop) := (∀ i, ¬ propVec i) ∨ ExactlyOne propVec

[Aaron Liu]

ahh it's not constructively correct

[Aaron Liu]

def AtmostOne {n} (propVec : Fin n → Prop) := ∀ i, propVec i → ∀ j, propVec j → i = j

[Snir Broshi]

import Mathlib
open Cardinal

def ExactlyOne {n} (propVec : Fin n → Prop) := #(propVec ⁻¹' {True}) = 1

:sunglasses:

[Johan Commelin]

You can use ExistsUnique and pass it a Fin n indexed vector using the ![prop 1, prop2, prop 3] notation.

[Johan Commelin]

Ooh, I see that's also in Shreyas's latest message.