computing quotient choice

Stream: mathlib4

[Aaron Liu]

docs#Quotient.choice is a version of the axiom of choice. It can be used to decide arbitrary propositions, and therefore has no computational interpretation.

Code to decide arbitrary proposition

import Mathlib.Data.Quot

/--
info: Quotient.choice.{u_3, u_4} {ι : Type u_3} {α : ι → Type u_4} {S : (i : ι) → Setoid (α i)}
  (f : (i : ι) → Quotient (S i)) : Quotient inferInstance
-/
#guard_msgs in
#check Quotient.choice

-- suppose `Quotient.choice` were computable by implementing it as `sorry`
def choice : type_of% @Quotient.choice := sorry
-- we use this equivalent version
nonrec def Trunc.choice {ι : Type*} {α : ι → Type*}
    (f : (i : ι) → Trunc (α i)) : Trunc ((i : ι) → α i) :=
  (choice f).recOnSubsingleton Trunc.mk

def propDecidable (p : Prop) : Decidable p :=
  -- we follow the proof of `Classical.em`
  let S : Setoid Bool :=
    { r x y := x = y ∨ p
      iseqv :=
        { refl _ := .inl rfl
          symm h := h.imp_left Eq.symm
          trans h₁ h₂ := h₂.elim (· ▸ h₁) Or.inr } }
  have f (i : Quotient S) : Trunc { x : Bool // Quotient.mk S x = i } :=
    i.recOnSubsingleton fun x => Trunc.mk ⟨x, rfl⟩
  (Trunc.choice f).recOnSubsingleton fun g =>
    let u : Bool := (g (Quotient.mk S true)).1
    let v : Bool := (g (Quotient.mk S false)).1
    have u_def : u = true ∨ p := Quotient.exact (g (Quotient.mk S true)).2
    have v_def : v = false ∨ p := Quotient.exact (g (Quotient.mk S false)).2
    have not_uv_or_p : u ≠ v ∨ p :=
      match u_def, v_def with
      | Or.inr h, _ => Or.inr h
      | _, Or.inr h => Or.inr h
      | Or.inl hut, Or.inl hvf =>
        have hne : u ≠ v := by simp [hvf, hut]
        Or.inl hne
    have p_implies_uv (hp : p) : u = v :=
      congrArg (fun i => (g i).1) (Quotient.sound (Or.inr hp))
    decidable_of_iff (u = v) ⟨not_uv_or_p.neg_resolve_left, p_implies_uv⟩

In #mathlib4 > A monad for partial computations, there is an implementation for countable choice. The trick to decide arbitrary propositions does not work here because the indexing type is fixed to be Nat. The implementation is included here:
Anthony Vandikas said:

unsafe def Quotient.countableChoice_impl {α : Nat → Type*} {S : ∀ i, Setoid (α i)}
    (f : ∀ i, Quotient (S i)) :
    @Quotient (∀ i, α i) (by infer_instance) :=
  Quotient.lift₂
    (fun z s ↦ ⟦fun | .zero => z | .succ n => s n⟧)
    (fun z₁ s₁ z₂ s₂ h₁ h₂ ↦ by
      apply sound
      rintro ⟨_|n⟩
      · apply h₁
      · apply h₂)
    (f 0)
    (countableChoice_impl (fun n ↦ f n.succ))

@[implemented_by Quotient.countableChoice_impl]
def Quotient.countableChoice {α : Nat → Type*} {S : ∀ i, Setoid (α i)}
    (f : ∀ i, Quotient (S i)) :
    @Quotient (∀ i, α i) (by infer_instance) :=
  Quotient.choice f

So countable choice is implemented using only safe functions, but there is now a termination issue. It's impossible to prove termination. But I don't see how I can get this to run forever either, so maybe it is sound?

There is also an easier way to implement it, like this:

unsafe def Quotient.countableChoice_impl {α : Nat → Type*} {S : ∀ i, Setoid (α i)}
    (f : ∀ i, Quotient (S i)) :
    @Quotient (∀ i, α i) (by infer_instance) :=
  ⟦fun i ↦ (f i).unquot⟧

An analogous implementation is not sound for Quotient.choice. Is this version sound?

What about dependent choice? The statement of dependent choice looks like this:

import Mathlib

def Quotient.dependentChoice {α : Sort*} {s : Setoid α} (f : α → Quotient s) (init : α) :
    Trunc { seq : ℕ → α // seq 0 = init ∧ ∀ n, f (seq n) = Quotient.mk s (seq (n + 1)) } :=
  sorry

This also seems to be implementable. But I also thought Quotient.choice was implementable until I saw a counterexample. So how can I tell if a proposed implementation is sound?

[Eric Wieser]

For what it's worth you can drop the unsafe above with partial:

import Mathlib

instance {α : ℕ → Type u_1} {S : (i : ℕ) → Setoid (α i)} [i : Nonempty ((i : ℕ) → Quotient (S i))] :
    Nonempty (@Quotient (∀ i, α i) inferInstance) := i.map Quotient.choice

partial def Quotient.countableChoice_impl {α : Nat → Type*} {S : ∀ i, Setoid (α i)}
    (f : ∀ i, Quotient (S i)) :
    @Quotient (∀ i, α i) (by infer_instance) :=
  Quotient.lift₂
    (fun z s ↦ ⟦fun | .zero => z | .succ n => s n⟧)
    (fun z₁ s₁ z₂ s₂ h₁ h₂ ↦ by
      apply sound
      rintro ⟨_|n⟩
      · apply h₁
      · apply h₂)
    (f 0)
    (countableChoice_impl (fun n ↦ f n.succ))

@[implemented_by Quotient.countableChoice_impl]
def Quotient.countableChoice {α : Nat → Type*} {S : ∀ i, Setoid (α i)}
    (f : ∀ i, Quotient (S i)) :
    @Quotient (∀ i, α i) (by infer_instance) :=
  Quotient.choice f

[Eric Wieser]

But I couldn't persuade partial_fixpoint to work

[Anthony Vandikas]

Aaron Liu said:

What about dependent choice?

Here is a quick and dirty implementation:

instance {α : Sort*} {s : Setoid α} (f : α → Quotient s) (init : α)
    : Nonempty (Trunc { seq : Nat → α //
        seq 0 = init ∧
        ∀ n, f (seq n) = Quotient.mk s (seq (n + 1)) }) := by
  constructor
  apply Trunc.mk
  use Nat.rec init (fun _ x ↦ (f x).out)
  simp only [Quotient.out_eq, implies_true, and_true]
  rfl

partial def Quotient.dependentChoice {α : Sort*} {s : Setoid α} (f : α → Quotient s) (init : α) :
    Trunc { seq : Nat → α // seq 0 = init ∧ ∀ n, f (seq n) = Quotient.mk s (seq (n + 1)) } :=
  Quotient.recOnSubsingleton (motive := fun a ↦ a = f init → _) (f init) (fun a h ↦
  Quotient.recOnSubsingleton (Quotient.dependentChoice f a) (fun s ↦
    ⟦{
      val
        | 0 => init
        | n + 1 => s.val n
      property := by
        simp only [true_and]
        intro n
        cases n
        · simp only [s.property.1, h]
        · simp only [s.property.2]
    }⟧)) rfl

I have not tested that this actually works, which hinges onrecOnSubsingleton being "compiled away" so that the recursive call is essentially done lazily.

My understanding is that anything partial is guaranteed to be "sound" in the sense that you get runtime type preservation, but not in the sense that also guarantees termination. So as long as you can give a partial implementation of whatever axiom you need and can show (possibly independently of Lean's logic) that it terminates, you are good to go.

(I had originally implemented Quotient.countableChoice_impl using partial. It got changed to unsafe because I copied the body of the partial implementation into the definition of the unsafe one by accident :whoops:)