get the witness of `∃!`?

Stream: new members

[Yusuke Inoue]

In first order logic, when we have a ∃! prop, we can define a new constant representing the only witness of prop.
Logically, I think it could be done in Lean, but actually not.
Here are two ways I know and why I don't think they're good:

• using a type in Type instead : that requires much stronger premise
• using Classical.choose : in FOL AC isn't needed to do that
  The witness of a ∃! prop is actually 'subsingle', so maybe allow getting the witness from that a prop wouldn't lead to inconsistency?

[Aaron Liu]

If you allow eliminating out the witness such that elim (mk x proof) = x definitionally then it makes definitional equality undecidable

[Aaron Liu]

well, even more undecidable (it was undecidable already because of a similar problem with Acc.rec)

[Aaron Liu]

this is the same problem as #Type theory > Can `Squash.mk x = Squash.mk y` be made true by definition? @ 💬 but with ExistsUnique instead of Squash

[Kyle Miller]

My rough understanding here is that to be able to get the witness, you need to have some sort of computational interpretation of proofs for it all to work out (since you'll need to be able to compute with that witness in reductions; I think this touches on what Aaron is saying about undecidability).

There is a computational interpretation of proofs, but Lean tends to avoid doing any proof reductions if it can help it. The compiler will erase proofs for example, so you won't be able to use this for programs, without a lot of extra work to figure out how to modify the compiler.

But, the definitional equality problem that Aaron mentions is a problem. Given two witnesses x and y, proof irrelevance means mk x proof1 = mk y proof2 is a definitional equality, so elim (mk x proof1) = elim (mk y proof2) is a definitional equality, and so x = y is a definitional equality. That's not good, because x and y might not directly be definitionally equal (!). I'm not sure this is a very big problem, given that the definitional equality algorithm already isn't transitive, but it certainly won't make the situation better.

[Yusuke Inoue]

Could we simply drop the computational interpretation, making the witness opaque?

[Yusuke Inoue]

just like the way it works in FOL, imo

[Kyle Miller]

May as well use Classical.choose then I think?

[Yusuke Inoue]

eh, I think Classical.choose looks too strong for this purpose.Anyway, in FOL, AC is not needed to do that.

[Kyle Miller]

I believe in type theory "getting the witness from a proof" usually means something like "reduce the proof to weak-head normal form ExistsUnique.mk x proof and then use x". Anything else amounts to adding an axiom, where you don't "really" get a witness, just a purported one that's supposed to exist.

[Kyle Miller]

My understanding is that FOL doesn't have the same sense of constructions as in the Calculus of Constructions. It's a much more stringent requirement to be able to "get" the witness in CoC than FOL, since "getting" the witness means you need to be able to compute with the witness in some way.

[Kyle Miller]

In CoC, you can "get" the witness of even an existential in a more limited sense, using Exists.rec, and that's probably similar to what it means to get a witness in FOL. (I'm no logician though!)

[Yusuke Inoue]

Maybe introducing a way to get a witness can better simulate the feeling of doing FOL when actually using Lean, that's what I think when asking this question

[Aaron Liu]

How do you "get" the witness in FOL, when you're stating the theorem? That is, if I have a proof that ∃! x, P x how do I state that "Q x where x is the unique x such that P x" in FOL? Clearly you need some sort of quantification to contain the x, and then once you start proving that Q x you don't need any choice in the proof, you just unwrap the exists.

[Aaron Liu]

My point is that you can do this in Lean too, it just looks kind of ugly

[Yusuke Inoue]

Yes, but without a way to introduce a constant representing the witness, the sentences will easily be quite long.

[Aaron Liu]

this happens in FOL too

[Yusuke Inoue]

Aaron Liu said:

My point is that you can do this in Lean too, it just looks kind of ugly

Yes that's what I think.

[suhr]

Yusuke Inoue said:

Anyway, in FOL, AC is not needed to do that.

In FOL you just never leave the Prop.

[Kyle Miller]

I think it wouldn't be too hard of a metaprogramming exercise to make an elaborator that eliminates uses of Classical.choice in a Prop context.

[Aaron Liu]

the reason you don't need AC to do this in FOL is because in FOL you have these lengthy sentences that every time they need to reference the unique x that satisfies P they put a quantifier instead and you can do that in Lean too

[Kyle Miller]

@Yusuke Inoue Are you familiar with using obtain to get a witness from an existential? That's usually how people do it, rather than using Classical.choose, unless you mean you want to use it inside of other definitions.

[Kyle Miller]

I think it would be very useful to have a #mwe to ground this discussion at this point.

[Yusuke Inoue]

Aaron Liu said:

this happens in FOL too

I read somewhere that when we have a existsunique prop, introducing its witness as a constant is a conservative extension. Maybe in proof assistants based on FOL they allow users to do that (just guessing, so far I've never used them).

[Yusuke Inoue]

Kyle Miller said:

Yusuke Inoue Are you familiar with using obtain to get a witness from an existential? That's usually how people do it, rather than using Classical.choose, unless you mean you want to use it inside of other definitions.

Yes I know obtain

[Yusuke Inoue]

Kyle Miller said:

I think it would be very useful to have a #mwe to ground this discussion at this point.

Good idea. I'll give one

[Terence Tao]

Some relevant recent discussion: #general > crazy idea: "Type" → "Space", "term" → "point" @ 💬 . As observed there, the ability to extract witnesses from an ExistUnique is equivalent to having a choice function for non-empty singletons.

I also wrote some basic API for extracting witnesses (using choice) at https://github.com/teorth/analysis/blob/main/analysis/Analysis/Tools/ExistsUnique.lean (this doesn't directly address your question, but helped with the practical concern of just extracting the constant for use in Lean proofs).

[Yusuke Inoue]

Yusuke Inoue said:

Kyle Miller said:

I think it would be very useful to have a #mwe to ground this discussion at this point.

Good idea. I'll give one

It's from Tao's analysis I.

Exercise 3.5.12. This exercise will establish a rigorous version of Proposition 2.1.16. Let $f : \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ be a function, and let $c$ be a natural number. Show that there exists a function $a : \mathbb{N} \to \mathbb{N}$ such that
$a(0) = c$
$a(n\text{++}) = f(n, a(n)) \quad \text{for all} \quad n \in \mathbb{N},$
and furthermore that this function is unique.

Hint: First show inductively that for every natural number $N$, there exists a unique function $a_N : \{ n \in \mathbb{N} : n \leq N \} \to \mathbb{N}$ such that:
$a_N(0) = c$
$a_N(n\text{++}) = f(n, a_N(n)) \quad \text{for all} \quad n < N$

For an additional challenge: Prove this using only Peano axioms (no ordering properties or Proposition 2.1.16).

Challenge Hint: First show inductively that for every $N$, there exists a unique pair of subsets $A_N, B_N \subseteq \mathbb{N}$ satisfying:
(a) $A_N \cap B_N = \emptyset$
(b) $A_N \cup B_N = \mathbb{N}$
(c) $0 \in A_N$
(d) $N\text{++} \in B_N$
(e) If $n \in B_N$, then $n\text{++} \in B_N$
(f) If $n \in A_N$ and $n \neq N$, then $n\text{++} \in A_N$

Then use $A_N$ as $\{ n \in \mathbb{N} : n \leq N \}$ in the previous argument.

import Mathlib

class PeanoAxioms (N : Type) extends Zero N where
  succ : N -> N
  zero_no_succ : ∀n : N, ¬ succ n = 0
  succ_cancel : ∀a b : N, succ a = succ b → a = b
  induction : ∀f : N → Prop, (f 0 ∧ ∀n : N, f n → f (succ n)) → ∀n : N, f n

postfix:100 "++" => PeanoAxioms.succ

namespace PeanoAxioms

variable {N : Type}[PeanoAxioms N]

lemma unique_set_up_to_n : ∀n, ∃!p : Set N × Set N ,let (a,b) := p;
  a ∩ b = ∅ ∧ a ∪ b = Set.univ ∧ 0 ∈ a ∧ n++ ∈ b ∧
  (∀m, m ∈ b → m++ ∈ b) ∧ (∀m, (m ∈ a ∧ m ≠ n) → m++ ∈ a) := by sorry

lemma unique_fun : ∃!f : N → Set N × Set N,∀n,let (a,b) := f n;
  a ∩ b = ∅ ∧ a ∪ b = Set.univ ∧ 0 ∈ a ∧ n++ ∈ b ∧
  (∀m, m ∈ b → m++ ∈ b) ∧ (∀m, (m ∈ a ∧ m ≠ n) → m++ ∈ a) := by sorry;

def A (n : N) : Set N := (unique_fun |> ExistsUnique.exists |> Classical.choose) n |> Prod.fst

lemma unique_fn_for_n (f : N → N → N) (c : N) : ∀n,∃!a : {m // A n m} → N,
  (∃h : 0 ∈ A n, a ⟨0,h⟩ = c) ∧ ∀m : {m : N // A n m }, ↑m ≠ n → ∃h : (↑m)++ ∈ A n, a ⟨(↑m)++,h⟩ = f (↑m) (a m) := by sorry

Without defining A here, the unique_fn_for_n statement will be quite long.
Defining A using existing axioms in Mathlib requires Classical.choose, which seems too strong.

An additional unique_choice axiom looks appealing to me :upside_down:

[Kyle Miller]

Maybe a unique_choice axiom would be a weaker assumption (at the cost of adding a new axiom!) but practically it's usually best to avoid any kind of choice at all if it's possible to construct the objects under consideration.

Something that's missing from the Peano axioms is a recursion principle, which would let you construct these sets without any need for choice. Here it is mostly worked out for creating the sets a and b, minus the part that shows the sets are unique:

import Mathlib

class PeanoAxioms (N : Type) extends Zero N where
  succ : N -> N
  zero_no_succ : ∀n : N, ¬ succ n = 0
  succ_cancel : ∀a b : N, succ a = succ b → a = b
  induction : ∀f : N → Prop, (f 0 ∧ ∀n : N, f n → f (succ n)) → ∀n : N, f n
  recurse : ∀ (f : N → Type), (f 0) → ((n : N) → f n → f (succ n)) → (n : N) → f n
  recurse_zero : ∀ (f : N → Type) (z : f 0) (s : (n : N) → f n → f (succ n)),
    recurse f z s 0 = z
  recurse_succ : ∀ (f : N → Type) (z : f 0) (s : (n : N) → f n → f (succ n)),
    ∀ (n : N), recurse f z s (succ n) = s n (recurse f z s n)

postfix:100 "++" => PeanoAxioms.succ

namespace PeanoAxioms

variable {N : Type} [PeanoAxioms N]

def A : N → Set N :=
  PeanoAxioms.recurse
    (fun _ => Set N)
    {0}
    (fun m last => insert (m++) last)

def B (n : N) : Set N := Set.univ \ A n

lemma cases (f : N → Prop) (zero : f 0) (succ : ∀ n : N, f (succ n)) : ∀n : N, f n :=
  PeanoAxioms.induction f ⟨zero, fun n _ => succ n⟩

lemma succ_ne_self : ∀ (n : N), ¬ n++ = n := by
  apply PeanoAxioms.induction
  constructor
  · exact PeanoAxioms.zero_no_succ 0
  · intro n hn h
    apply hn
    apply PeanoAxioms.succ_cancel
    exact h

lemma inter_eq_empty (n : N) : A n ∩ B n = ∅ := by simp [A, B]
lemma union_eq_univ (n : N) : A n ∪ B n = Set.univ := by simp [A, B]

lemma zero_mem_a : ∀ n : N, 0 ∈ A n := by
  apply PeanoAxioms.induction
  constructor
  · simp [A, PeanoAxioms.recurse_zero]
  · intro n hn
    rw [A] at hn
    simp [A, PeanoAxioms.recurse_succ, hn]

lemma mem_of_succ_mem_a : ∀ (n m : N), m++ ∈ A n → m ∈ A n := by
  apply PeanoAxioms.induction
  constructor
  · simp [A, PeanoAxioms.recurse_zero]
    intro m h
    exact absurd h (PeanoAxioms.zero_no_succ m)
  · intro n ih m
    simp [A, PeanoAxioms.recurse_succ]
    rintro (h | h)
    · replace h := PeanoAxioms.succ_cancel _ _ h
      subst h
      right
      revert m
      apply PeanoAxioms.cases
      · intro
        simp [PeanoAxioms.recurse_zero]
      · intro m _
        simp [PeanoAxioms.recurse_succ]
    · right
      exact ih m h

lemma self_mem_a : ∀ (n : N), n ∈ A n := by
  apply PeanoAxioms.cases
  · simp [A, PeanoAxioms.recurse_zero]
  · intro n
    simp [A, PeanoAxioms.recurse_succ]

lemma succ_self_not_mem_a : ∀ (n : N), ¬ n++ ∈ A n := by
  apply PeanoAxioms.induction
  constructor
  · simp [A, PeanoAxioms.recurse_zero, zero_no_succ]
  · intro n
    apply mt
    intro h
    rw [A, PeanoAxioms.recurse_succ, ← A] at h
    simp [succ_ne_self] at h
    revert h
    apply mem_of_succ_mem_a

lemma succ_mem_a : ∀ (n m : N), m ∈ A n ∧ m ≠ n → m++ ∈ A n := by
  apply PeanoAxioms.induction
  constructor
  · simp [A, PeanoAxioms.recurse_zero]
  · intro n ih
    rintro m ⟨h1, h2⟩
    revert h1
    rw [A, PeanoAxioms.recurse_succ, ← A]
    simp [h2]
    rw [or_iff_not_imp_left]
    intro h3 h4
    apply ih
    refine ⟨h3, ?_⟩
    contrapose! h4
    rw [h4]

lemma succ_mem_b : ∀ (n : N), n++ ∈ B n := by
  simp [B]
  apply succ_self_not_mem_a

lemma succ_mem_b_of_mem_b (n m : N) : m ∈ B n → m++ ∈ B n := by
  simp [B]
  apply mt
  apply mem_of_succ_mem_a

lemma unique_set_up_to_n : ∀n, ∃!p : Set N × Set N ,let (a,b) := p;
    a ∩ b = ∅ ∧ a ∪ b = Set.univ ∧ 0 ∈ a ∧ n++ ∈ b ∧
    (∀m, m ∈ b → m++ ∈ b) ∧ (∀m, (m ∈ a ∧ m ≠ n) → m++ ∈ a) := by
  intro n
  use (A n, B n)
  dsimp only
  use! inter_eq_empty n, union_eq_univ n, zero_mem_a n, succ_mem_b n, succ_mem_b_of_mem_b n,
    succ_mem_a n
  rintro ⟨a, b⟩
  simp
  sorry -- prove uniqueness

[Kyle Miller]

Kyle Miller said:

I think it wouldn't be too hard of a metaprogramming exercise to make an elaborator that eliminates uses of Classical.choice in a Prop context.

More details about this idea:

I'm imagining that you would be able to define A using Classical.choice, and then your proof would look like

lemma unique_set_up_to_n : ∀n, ∃!p : Set N × Set N ,let (a,b) := p;
    a ∩ b = ∅ ∧ a ∪ b = Set.univ ∧ 0 ∈ a ∧ n++ ∈ b ∧
    (∀m, m ∈ b → m++ ∈ b) ∧ (∀m, (m ∈ a ∧ m ≠ n) → m++ ∈ a) :=
  elim_choice% [A] by
    ... a proof that uses A ...

which would tell it to unfold A while trying to eliminate uses of Classical.choice, which it will be able to do because the goal is a proposition. This would simulate the conservative extension idea you mentioned @Yusuke Inoue, but restricted to a Prop context.

[Yusuke Inoue]

Kyle Miller said:

Maybe a unique_choice axiom would be a weaker assumption (at the cost of adding a new axiom!) but practically it's usually best to avoid any kind of choice at all if it's possible to construct the objects under consideration.

I have just realized that Classical.EM is weaker than Classical.choicebut there's no additional axiom for it, the fact shows that usually 'the cost of adding a new axiom' is seen to be expensive.

[Kyle Miller]

Re this point about a missing recursion principle: it's the Calculus of Constructions, not the Calculus of Things We Proved That Exist :-)

[Kyle Miller]

I want to be clear that I'm not saying anything about whether it's worth studying which axioms are needed for what or not.

You're certainly free to add your own unique choice axiom!

If you want to be safe about it, you could define it as an opaque definition using Classical.choice, and then treat this as an axiom.

[Yusuke Inoue]

Thanks! I think I've got a lot from these replies.