Theorem for "finite choice"?

Stream: Is there code for X?

[Yiming Xu]

I hope it is a quick question. Do we have a theorem saying "any surjection to a finite set has a section" without using the axiom of choice formalized somewhere? If it exists, could you please tell me where it is?

[Kenny Lau]

I don't think mathlib has put a lot of effort in eliminating "axiom of choice" from the axioms

[Kyle Miller]

It's good to ask questions with a #mwe so that there's no guessing about the exact formulation you want. Here's my guess:

import Mathlib

def sec {α β} [Fintype β] (f : α → β) (h : Function.Surjective f) : β → α := sorry

-- and then a theorem that `sec` is a right inverse of `f`

I don't see any way to construct such a function without using the axiom of choice.

[Ruben Van de Velde]

It's possible if you have an order on beta, I think

[Edward van de Meent]

the above mwe probably not; there is no constructive way to get an element of α

[Ruben Van de Velde]

Oh yeah, I was confusing alpha and beta

[Yiming Xu]

Thanks for all these swift answers, and it is all my bad for not being explicit enough.

I just mean proving the existence of the function by induction on the cardinality of $\beta$. I do not need a function that eats a surjection and gives a section.

So I want something like

lemma sec_ex {α β} [Fintype β] (f : α → β) (h : \forall b: β, \exists a : α, f a = b) : \exists s :β → α.  f o s = id β  := sorry

The argument I expect is by induction on the cardinality of β.

[Terence Tao]

This is (essentially) Lemma 3.5.12 of my Analysis I textbook, formalized at https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_3_5.lean#L276

It does unfortunately use the axiom of (unique) choice at one point, which in Lean forces one to open Classical at one point. But that is in part because I am using a custom version of the natural numbers here that is not an inductive type, but rather one coming from Zermelo-Frankel set theory.

[Yiming Xu]

I see... A bit of unexpected. I should aware that the induction only works under the framework of ZF, so it is something to do with the implementation of Lean.

[Yiming Xu]

Many thanks though! Let me add a reference provided by @Kyod of how to do finite choice in Rcoq.
https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Logic.ConstructiveEpsilon.html
I would be interested to know if it is ported into Lean.

[Terence Tao]

I think this works:

import Mathlib.Tactic

theorem finite_choice {X:Type*} {f:X → ℕ} {N:ℕ} (h: ∀ n < N, ∃ x, f x = n) :
  ∃ g: Fin N → X, ∀ n, f (g n) = n := by
  induction' N with N ih
  . simp
  specialize ih ?a
  . intro n hn; exact h n (by linarith)
  obtain ⟨ g, hg ⟩ := ih
  specialize h N (by linarith); obtain ⟨ x, hx ⟩ := h
  set g' : Fin (N+1) → X := fun n ↦ if h:n.val < N then g ⟨ n.val, h ⟩ else x
  use g'
  intro n; by_cases h:n.val < N
  . simp [g', dif_pos h, hg]
  convert hx
  . simp [g', dif_neg h]
  have := n.isLt; omega

lemma sec_ex {α β:Type*} [Fintype β] (f : α → β) (h : ∀ b: β, ∃ a : α, f a = b) : ∃ s :β → α, f ∘ s = id := by
  set N := Fintype.card β
  let e : β ≃ Fin N := Fintype.equivFinOfCardEq (show Fintype.card β = N by rfl)
  set F: α → ℕ := fun a ↦ (e (f a)).val
  replace h : ∀ n < N, ∃ x, F x = n := by
    intro n hn
    obtain ⟨ a, ha ⟩ := h (e.symm ⟨ n, hn ⟩)
    use a; simp [F, ha]
  obtain ⟨ g, hg ⟩ := finite_choice h; use g ∘ e
  ext b; specialize hg (e b)
  simpa [F, Fin.val_inj] using hg

[Aaron Liu]

This does use choice

[Aaron Liu]

But you can modify it to avoid choice

[Terence Tao]

Where is choice used?

[Terence Tao]

Maybe in the linarith and omega tactics? everything else seems to be choice free

[Terence Tao]

No... I replaced these with explicit lemmas and #print_axioms finite_choice still contains Classical.choice. Is it the if ... then ... else statement? I really can't see any choice-dependent step here

[Aaron Liu]

docs#Fintype.equivFinOfCardEq

[Aaron Liu]

uses choice

[Aaron Liu]

the corresponding exists statement I think does not use choice

[Terence Tao]

OK I will fix this, but there appears to also be a choice dependency in finite_choice:

import Mathlib.Tactic

theorem finite_choice {X:Type*} {f:X → ℕ} {N:ℕ} (h: ∀ n < N, ∃ x, f x = n) :
  ∃ g: Fin N → X, ∀ n, f (g n) = n := by
  induction' N with N ih
  . simp only [IsEmpty.forall_iff, exists_const]
  specialize ih ?_
  . intro n hn; exact h n (Nat.lt_add_right 1 hn)
  obtain ⟨ g, hg ⟩ := ih
  specialize h N (lt_add_one N); obtain ⟨ x, hx ⟩ := h
  set g' : Fin (N+1) → X := fun n ↦ if h:n.val < N then g ⟨ n.val, h ⟩ else x
  use g'
  intro n; by_cases h:n.val < N
  . simp only [g', dif_pos h, hg]
  convert hx
  . simp only [g', dif_neg h]
  have := n.isLt; exact Nat.eq_of_lt_succ_of_not_lt this h

#printaxioms finite_choice -- 'finite_choice' depends on axioms: [propext, Classical.choice, Quot.sound]

[Aaron Liu]

it's linarith

[Aaron Liu]

try your hand at doing those manually

[Aaron Liu]

docs#Nat.lt_add_one

[Aaron Liu]

I think you might also have to add [DecidableEq β] to your hypotheses since otherwise there's no way to constructively distinguish elements of β

[Terence Tao]

I've done all that, but there is still a choice dependency somewhere. Is there a finer tool than #printaxioms to diagnose this?

import Mathlib.Tactic

theorem finite_choice {X:Type*} {f:X → ℕ} {N:ℕ} (h: ∀ n < N, ∃ x, f x = n) :
  ∃ g: Fin N → X, ∀ n, f (g n) = n := by
  induction' N with N ih
  . simp only [IsEmpty.forall_iff, exists_const]
  specialize ih ?_
  . intro n hn; exact h n (Nat.lt_add_right 1 hn)
  obtain ⟨ g, hg ⟩ := ih
  specialize h N (lt_add_one N); obtain ⟨ x, hx ⟩ := h
  set g' : Fin (N+1) → X := fun n ↦ if h:n.val < N then g ⟨ n.val, h ⟩ else x
  use g'
  intro n; by_cases h:n.val < N
  . simp only [g', dif_pos h, hg]
  convert hx
  . simp only [g', dif_neg h]
  have := n.isLt; exact Nat.eq_of_lt_succ_of_not_lt this h

#printaxioms finite_choice -- 'finite_choice' depends on axioms: [propext, Classical.choice, Quot.sound]

lemma sec_ex {α β:Type*} [Fintype β] [DecidableEq β] (f : α → β) (h : ∀ b: β, ∃ a : α, f a = b) : ∃ s :β → α, f ∘ s = id := by
  set N := Fintype.card β
  obtain ⟨ e, _ ⟩ := (Fintype.truncEquivFinOfCardEq (show Fintype.card β = N by rfl)).exists_rep
  set F: α → ℕ := fun a ↦ (e (f a)).val
  replace h : ∀ n < N, ∃ x, F x = n := by
    intro n hn
    obtain ⟨ a, ha ⟩ := h (e.symm ⟨ n, hn ⟩)
    use a; simp [F, ha]
  obtain ⟨ g, hg ⟩ := finite_choice h; use g ∘ e
  ext b; specialize hg (e b)
  simpa [F, Fin.val_inj] using hg

[Ruben Van de Velde]

Seems to be the obtain

[Aaron Liu]

Terence Tao said:

OK I will fix this, but there appears to also be a choice dependency in finite_choice:

import Mathlib.Tactic

theorem finite_choice {X:Type*} {f:X → ℕ} {N:ℕ} (h: ∀ n < N, ∃ x, f x = n) :
  ∃ g: Fin N → X, ∀ n, f (g n) = n := by
  induction' N with N ih
  . simp only [IsEmpty.forall_iff, exists_const]
  specialize ih ?_
  . intro n hn; exact h n (Nat.lt_add_right 1 hn)
  obtain ⟨ g, hg ⟩ := ih
  specialize h N (lt_add_one N); obtain ⟨ x, hx ⟩ := h
  set g' : Fin (N+1) → X := fun n ↦ if h:n.val < N then g ⟨ n.val, h ⟩ else x
  use g'
  intro n; by_cases h:n.val < N
  . simp only [g', dif_pos h, hg]
  convert hx
  . simp only [g', dif_neg h]
  have := n.isLt; exact Nat.eq_of_lt_succ_of_not_lt this h

#printaxioms finite_choice -- 'finite_choice' depends on axioms: [propext, Classical.choice, Quot.sound]

This one is docs#Nat.instStarOrderedRing which is involved in ZeroLEOneClass Nat for docs#lt_add_one, you should use docs#Nat.lt_add_one instead.

[Terence Tao]

Now choice-free!

import Mathlib.Tactic

theorem finite_choice {X:Type*} {f:X → ℕ} {N:ℕ} (h: ∀ n < N, ∃ x, f x = n) :
  ∃ g: Fin N → X, ∀ n, f (g n) = n := by
  induction' N with N ih
  . simp only [IsEmpty.forall_iff, exists_const]
  specialize ih ?_
  . intro n hn; exact h n (Nat.lt_add_right 1 hn)
  obtain ⟨ g, hg ⟩ := ih
  specialize h N (Nat.lt_add_one N); obtain ⟨ x, hx ⟩ := h
  set g' : Fin (N+1) → X := fun n ↦ if h:n.val < N then g ⟨ n.val, h ⟩ else x
  use g'
  intro n; by_cases h:n.val < N
  . simp only [g', dif_pos h, hg]
  convert hx
  . simp only [g', dif_neg h]
  exact Nat.eq_of_lt_succ_of_not_lt n.isLt h

lemma sec_ex {α β:Type*} [Fintype β] [DecidableEq β] (f : α → β) (h : ∀ b: β, ∃ a : α, f a = b) : ∃ s :β → α, f ∘ s = id := by
  set N := Fintype.card β
  obtain ⟨ e, _ ⟩ := (Fintype.truncEquivFinOfCardEq (show Fintype.card β = N by rfl)).exists_rep
  set F: α → ℕ := fun a ↦ (e (f a)).val
  replace h : ∀ n < N, ∃ x, F x = n := by
    intro n hn
    obtain ⟨ a, ha ⟩ := h (e.symm ⟨ n, hn ⟩)
    use a; simp [F, ha]
  obtain ⟨ g, hg ⟩ := finite_choice h; use g ∘ e
  ext b; specialize hg (e b)
  simpa [F, Fin.val_inj] using hg

#printaxioms sec_ex -- 'sec_ex' depends on axioms: [propext, Quot.sound]

[Aaron Liu]

this is what you get for importing everything

[Aaron Liu]

I'm surprised #printaxioms parses, I'm used to writing it like #print axioms

[Aaron Liu]

Terence Tao said:

I've done all that, but there is still a choice dependency somewhere. Is there a finer tool than #printaxioms to diagnose this?

My method is to put stop (that's a tactic) at various points in the proof and see when the choice goes away

[Yiming Xu]

I want to try to follow this: is there any quick explanation on what the role of "DecidableEq" here is and what it has to do with choice?

[Yiming Xu]

Thank you @Terence Tao and now I am picking your theorem for free and using it in my formalization!(feeling a bit guilty...)

[Yiming Xu]

Nice to have it in Mathlib? I kind of do not think I will be the only person who needs that.

[Terence Tao]

I've uploaded it to my analysis repository: https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/FiniteChoice.lean . I'm not sure Mathlib is optimized to hold choice-free theorems, as can already be evidenced by how non-trivial it was to expunge choice from the above proof

[Aaron Liu]

I don't think this will make it into mathlib, since it's essentially a duplicate of docs#Function.Surjective.hasRightInverse. Since, it's constructive, maybe a version that returns a Trunc {s : β → α // Function.RightInverse s f}?

[Yiming Xu]

I see. I just heard today that initially people are dedicated to be constructive on the very beginning stage when developing Lean, and then start taking shortcuts because it is not easy.

[Terence Tao]

Fintype does not directly come with an enumeration by a Fin, to get that enumeration constructively one needs to be able to decidably compare elements of the Fintype with each other

[Yiming Xu]

Terence Tao said:

I've uploaded it to my analysis repository: https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/FiniteChoice.lean . I'm not sure Mathlib is optimized to hold choice-free theorems, as can already be evidenced by how non-trivial it was to expunge choice from the above proof

It also reminds me that I should be aware of tactics with choice if I do not want that.

[Yiming Xu]

I am now a bit afraid that if I do not want choice, I may should avoid using the quotient package in Lean when constructing pushout in the category of finite sets. (It should be doable.)

[Terence Tao]

For what it is worth, here is a Trunc version:

def finite_choice_trunc {X:Type*} {f:X → ℕ} {N:ℕ} (h: ∀ n < N, Trunc {x // f x = n}) :
  Trunc {g: Fin N → X // ∀ n, f (g n) = n} := by
  induction' N with N ih
  . apply Trunc.mk
    refine ⟨ Fin.elim0, ?_ ⟩
    simp only [IsEmpty.forall_iff, exists_const]
  specialize ih ?_
  . intro n hn; exact h n (Nat.lt_add_right 1 hn)
  apply Trunc.bind ih; intro ⟨ g, hg ⟩
  apply Trunc.bind (h N (Nat.lt_add_one N)); intro ⟨ x, hx ⟩
  set g' : Fin (N+1) → X := fun n ↦ if h:n.val < N then g ⟨ n.val, h ⟩ else x
  apply Trunc.mk
  use g'
  intro n; by_cases h:n.val < N
  . simp only [g', dif_pos h, hg]
  convert hx
  . simp only [g', dif_neg h]
  exact Nat.eq_of_lt_succ_of_not_lt n.isLt h

def sec_ex_trunc {α β:Type*} [Fintype β] [DecidableEq β] (f : α → β) (h : ∀ b, Trunc { a // f a = b}) : Trunc { s // f ∘ s = id } := by
  set N := Fintype.card β
  apply Trunc.bind (Fintype.truncEquivFinOfCardEq (show Fintype.card β = N by rfl))
  intro e
  set F: α → ℕ := fun a ↦ (e (f a)).val
  replace h : ∀ n < N, Trunc {x // F x = n} := by
    intro n hn
    apply Trunc.bind (h (e.symm ⟨ n, hn ⟩)); intro ⟨ a, ha ⟩
    apply Trunc.mk; use a; simp only [ha, Equiv.apply_symm_apply, F]
  apply Trunc.bind (finite_choice_trunc h); intro ⟨ g, hg ⟩
  apply Trunc.mk; use g ∘ e; ext b; specialize hg (e b)
  simpa only [Function.comp_apply, id_eq, Fin.val_inj, EmbeddingLike.apply_eq_iff_eq, F] using hg

#print axioms sec_ex_trunc -- 'sec_ex_trunc' depends on axioms: [propext, Quot.sound]

[Kyle Miller]

Yiming Xu said:

then start taking shortcuts because it is not easy

I think it's rather that avoiding choice in proofs was recognized to not have immediate practical applications (practical with respect to the goals of the Lean project). It's interesting avoiding choice, but doing so doesn't unlock any features in Lean at the moment.

@Terence Tao's sec_ex_trunc is more interesting though, since it's actually constructing an (indeterminate) section from a family of (indeterminate) preimages. Constructivism in Lean looks like defs that can be compiled/reduced.

Food for thought: Lean proofs that avoid choice don't necessarily give you witnesses (so can they really be said to be constructive?), but also Lean definitions might use the axiom of choice yet still can be compiled/reduced (so should one really say that such definitions are not constructive?).

[Kyle Miller]

Regarding that first part in the last paragraph: proof irrelevance and "tautological extensionality" (a weaker form of propext) are enough to cause "constructive" proofs to not be computationally meaningful, in the sense that you can't reduce them to extract witnesses, etc. In my naiveté I could be misunderstanding the meaning of the following example (like, maybe there's some reduction order that would normalize?), but what I draw from it is that (1) avoiding the axiom of choice isn't enough to make proofs constructive, and hence (2) there's not much point in avoiding the axiom of choice in Lean proofs, unless you're specifically doing reverse mathematics (but even so, maybe Lean isn't the best platform for that, given all the implicit axioms in the type theory?). The effort might be better spent on making computable definitions.

def True' := ∀ p : Prop, p → p

def om : True' := fun A a =>
   @cast (True' → True') A (propext ⟨fun _ => a, fun _ => id⟩)
   fun z => z (True' → True') id z

def Om : True' := om (True' → True') id om

def foo : And True True := Om _ ⟨trivial, trivial⟩

#print axioms foo
-- 'foo' depends on axioms: [propext]

example : foo.recOn (fun _ _ => 1) = 1 := rfl
--                                        ~~~
-- error: maximum recursion depth has been reached
-- (Reduction of `Om` goes into an infinite loop!)

Paper by Abel and Coquand introducing this issue: https://arxiv.org/abs/1911.08174

Zulip thread where Mario Carneiro found that this can cause normalization failure in Type, not just Prop: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Normalization.20fails.20in.20lean/near/409110365 (the above example is adapted from this)

[Aaron Liu]

first time I've seen an actual infinite loop

[Kenny Lau]

@Yiming Xu i'm afraid you might be, uh, what's the word, following the footsteps of Sisyphus by trying to remove choice from every theorem in mathlib.

[Kenny Lau]

especially when, given proof irrelevance, the "real" difference is at the level of defs, and not at the level of the proofs of theorems

[Kenny Lau]

Lean4 is built with proof irrelevance, which means that the proofs are irrelevant.

[Kenny Lau]

it matters to me much more whether I need to write noncomputable def or def, than whether a theorem depends on the axiom of choice.

[Yiming Xu]

Kenny Lau said:

especially when, given proof irrelevance, the "real" difference is at the level of defs, and not at the level of the proofs of theorems

I see. Good reminder on proof irrelevance. I agree that executability, addressed by computability, matters much more. I will not waste time trying to remove AC. It just happens to me that for the particular proof I want to work with, I would like to confirm we do not need AC to make the proof go through.

I will see clearer how much definitions would I like to make explicit for this proof, to see if it will have any effect on computability...

[Yiming Xu]

Kyle Miller said:

Yiming Xu said:

then start taking shortcuts because it is not easy

I think it's rather that avoiding choice in proofs was recognized to not have immediate practical applications (practical with respect to the goals of the Lean project). It's interesting avoiding choice, but doing so doesn't unlock any features in Lean at the moment.

Terence Tao's sec_ex_trunc is more interesting though, since it's actually constructing an (indeterminate) section from a family of (indeterminate) preimages. Constructivism in Lean looks like defs that can be compiled/reduced.

Food for thought: Lean proofs that avoid choice don't necessarily give you witnesses (so can they really be said to be constructive?), but also Lean definitions might use the axiom of choice yet still can be compiled/reduced (so should one really say that such definitions are not constructive?).

That's reasonable. It just happens that sometimes we do not want something that is not supposed to depend on choice to depend on choice when it comes to formalization. But thanks to the reminder from Kenny Lau, once we have a proof in Lean, by proof irrelevance, we do not care anymore about whether AC is called in the proof.

[Yiming Xu]

Kyle Miller said:

Yiming Xu said:

then start taking shortcuts because it is not easy

I think it's rather that avoiding choice in proofs was recognized to not have immediate practical applications (practical with respect to the goals of the Lean project). It's interesting avoiding choice, but doing so doesn't unlock any features in Lean at the moment.

Terence Tao's sec_ex_trunc is more interesting though, since it's actually constructing an (indeterminate) section from a family of (indeterminate) preimages. Constructivism in Lean looks like defs that can be compiled/reduced.

Food for thought: Lean proofs that avoid choice don't necessarily give you witnesses (so can they really be said to be constructive?), but also Lean definitions might use the axiom of choice yet still can be compiled/reduced (so should one really say that such definitions are not constructive?).

Re:
but also Lean definitions might use the axiom of choice yet still can be compiled/reduced

There are two things to take away from your comment:
-Avoiding AC does not make things computable
-Having AC does not necessarily make things noncomputable.
And this separates AC and computability in Lean into two detached problems.

I am not sure if I get this: i.e. what would be a def that calls AC but still computable? If it happens, do you mean the definition takes a proof, and this proof can be constructed using choice? Is there any mwe to clearify that?

[Robin Arnez]

def test (a : Array Nat) (h : 10 < a.size) : Nat :=
  let a := a.push 5
  a[3]'(by grind)

/-- info: 'test' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms test

/-- info: 4 -/
#guard_msgs in
#reduce test #[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11] (by decide)

Here we use grind to provide the array indexing proof and it happens to use choice, so we get a choice dependency. Runtime doesn't care and reduction doesn't either though because of proof irrelevance.

[Yiming Xu]

So I think I see it confirms my conjecture that the choice is used in a proof taken by a definition. I see. It makes a lots of sense and many thanks!