Why is choice more powerful than exists hypothesis?

Stream: new members

[Dan Abramov]

I'm trying to understand patterns for dealing with existence and choice.

I have this little example:

import Mathlib.Tactic

def PairSet := Nat → Nat → Prop
def IsFunctional (s : PairSet) : Prop := ∀ x, (∃ y, s x y) ∧ (∀ y₁ y₂, (s x) y₁ → s x y₂ → y₁ = y₂)
def funToPairSet (f : Nat → Nat) : PairSet := fun x y ↦ y = f x

noncomputable def y_exists (s : PairSet) (h : IsFunctional s) (x : Nat) : ∃ y, s x y :=
  (h x).1

noncomputable def pairSetToFun (s : PairSet) (h : IsFunctional s) : Nat → Nat := fun x ↦
  (y_exists s h x).choose

lemma pairSetToFun_spec (s : PairSet) (h : IsFunctional s) (x : Nat) :
    s x (pairSetToFun s h x) :=
  (y_exists s h x).choose_spec

theorem funToPairSet_functional (f : Nat → Nat) : IsFunctional (funToPairSet f) := by
  unfold IsFunctional
  intro x
  constructor
  · unfold funToPairSet
    use f x
  intro y1 y2 hf1 hf2
  unfold funToPairSet at *
  rw [hf1, hf2]

theorem pairSetToFun_funToPairSet_eq (f : Nat → Nat) :
    pairSetToFun (funToPairSet f) (funToPairSet_functional f) = f := by
  ext x
  let hyex := y_exists _ (funToPairSet_functional f) x
  have ⟨y, hy⟩ := hyex
  have hy' := hyex.choose_spec
  exact hy'

My question is, why does hy' satisfy the last lemma, but hy doesn't?
How to think about this?

The proof state is:

f : ℕ → ℕ
x : ℕ
hyex : ∃ y, funToPairSet f x y := y_exists (funToPairSet f) (funToPairSet_functional f) x
y : ℕ
hy : funToPairSet f x y
hy' : funToPairSet f x hyex.choose
⊢ pairSetToFun (funToPairSet f) ⋯ x = f x

I'm honestly confused why hy' satisfies the goal at all — the goal and hy' read different to me.

What am I missing?

[Kyle Miller]

(Note that your first noncomputable def should be theorem)

[Kyle Miller]

Maybe this helps?

theorem pairSetToFun_funToPairSet_eq (f : Nat → Nat) :
    pairSetToFun (funToPairSet f) (funToPairSet_functional f) = f := by
  ext x
  let hyex := y_exists _ (funToPairSet_functional f) x
  have ⟨y, hy⟩ := hyex
  have hy' := hyex.choose_spec
  unfold funToPairSet at hy' ⊢
  unfold pairSetToFun
  exact hy'

[Kyle Miller]

Notice that hy' and the goal are both Exists.choose applied to a proof. Since they're proofs, for them to be the same, they just need to have equivalent types (by proof irrelevance).

[Kyle Miller]

In one case you have ∃ y, funToPairSet f x y and in the other you have ∃ y, y = f x, and by definition of funToPairSet these are the same.

[Kyle Miller]

(Side note: there's always going to be a bit of an "impedance mismatch" here, between native functions and functions-as-a-set-of-pairs, because native functions have some kind of computational content, but the set-of-pairs perspective doesn't actually say what the value is for a given input. It doesn't matter in the end for reasoning, but it's an interesting difference.)

[Dan Abramov]

OK, mechanically I think this makes sense.

Is there also a conceptual way to think about this? Like, how do I make sense of the fact that the same existential has two different ways to obtain "a value with a hypothesis" out of it, but only choice works in this case?

[Kenny Lau]

@Dan Abramov it's because choose is a function

[Kenny Lau]

a function is required to give the same output every time

[Kenny Lau]

so even though it's arbitrary, it's a fixed arbitrary choice

[Dan Abramov]

Ah, so we're kind of lifting the existential "up" to a point if multiple places in code share access to it, they can also obtain a stronger result (choice would give us same value for it). Whereas if the pairSetToFun function wasn't defined via that choosing existential, we wouldn't have that way to coordinate later?

[Kenny Lau]

it seems like your interpretation of choice is the opposite of mine

[Kenny Lau]

your pairSetToFun was defined using the same choose as the hyex.choose_spec in your proof

[Kenny Lau]

same choose on same proof gives same result

[Kenny Lau]

(yes, it's the same proof, because all proofs are the same)

[Kyle Miller]

Do you like continuation-passing style / callbacks @Dan Abramov?

When you're in a proof, you can think of the pattern matching notation as setting up a callback, rather than "actually" getting any values out. The rest of the proof from that point is the callback, and it says "if someone were to give us a witness, then this is why the conclusion follows", but that doesn't mean that there is a witness in hand.

Maybe: proofs are evidence that a proposition is true, but the proofs themselves are opaque objects that we don't inspect. (With Exists.intro we provide a witness to provide the evidence that the existential is true, but we've thrown that witness into the void and never expect to "read" it ever again.)

[Kyle Miller]

If we want to "actually" get the value, which is what a top-level definition must be, an actual value, then we can't use this callback approach. We need the value now, not in the imagined later point in time when someone gives us a witness.

The choice function makes a choice ahead of time for a witness, that way we "actually" have one when we need it.

[Dan Abramov]

same choose on same proof gives same result

Right, so I think that's what I meant... Let me try to rephase it.

If I got it right, when you just "read" an existential, each "read" is independent and nothing "ties" those reads together. So if you want multiple "reads" to be coordinated, you have to "read" ahead of time, and choice is a way to do that. Everybody doing choice on the same existential will "read" the same value. So it would be possible to use that fact when reducing expressions that have the same choice on both sides.

Does that make sense?

[Kyle Miller]

Dan Abramov said:

when you just "read" an existential, each "read" is independent and nothing "ties" those reads together.

That's a way I've thought about it before as well, and it gives you all the intuition you need.

[Dan Abramov]

Hm would it be a reasonable analogy to say that destructuring an existential is like chaining a then(val => ...) to some Promise (i.e. monadically adding more computation to it) while choice is like actually like getting a reference to that Promise so you can pass it around? Not sure if I'm stretching the analogy too far.

[Dan Abramov]

I guess I'm struggling to imagine what choice would mean in the CPS world — usually if you do CPS, you don't have the option of "actually" getting the value

[Kyle Miller]

Yes, it's exactly like chaining promises.

The choice function though is giving the actual value that some promise resolves to. Not necessarily this Exists.

[Dan Abramov]

Interesting, so I guess choice is like a loophole that forces the collapse. And for consistency it must collapse the same way for everyone

[Kyle Miller]

And it collapses in the same way for everyone because it's a function, so equal inputs means equal outputs.

[Aaron Liu]

Dan Abramov said:

I guess I'm struggling to imagine what choice would mean in the CPS world — usually if you do CPS, you don't have the option of "actually" getting the value

Choice is a way of magically spawning in a value since there's no other way to "actually" get it out

[Kyle Miller]

Re chaining promises, if you look at the type of Exists.casesOn, the intro argument is the continuation argument:

set_option pp.proofs true
#check Exists.casesOn
-- Exists.casesOn.{u} {α : Sort u} {p : α → Prop} {motive : Exists p → Prop} (t : Exists p)
--  (intro : ∀ (w : α) (h : p w), motive (Exists.intro w h)) : motive t

I mentioned in your other thread that this type can be simplified to something equivalent but easier to read:

Exists.casesOn'.{u} {α : Sort u} {p : α → Prop} {motive : Prop} (t : Exists p)
  (intro : ∀ (w : α) (h : p w), motive) : motive

(No need for the value returned by the continuation to depend on t.)

[Kyle Miller]

That's to say, the have ⟨w,h⟩ := t; b is the same as t.casesOn fun w h => b

[Kyle Miller]

(Hopefully this last line connects it up to Promise well enough.)

[Kyle Miller]

I'm reminded that I've heard that continuation-passing style is somehow related to classical logic.

If we had call-with-current-continuation, then we could use Exists.casesOn to extract a witness:

call_with_cc fun cont =>
  t.casesOn fun w h => cont w

So, I suppose it must be at least as powerful as Classical.choice.

[Dan Abramov]

OK yeah this is very helpful, thank you!

A big aha moment tbh.

[Dan Abramov]

In a sense, is choice strictly more powerful than destructuring? Are there any things I can prove with destructuring but not with choice for the same existential?

[Kyle Miller]

Oh, neat, call-with-cc can be made to actually work here (which by the way is Pierce's law):

noncomputable def call_with_cc {α β : Sort _} (f : (α → β) → α) : α :=
  Classical.choice <| by
    obtain h | h := isEmpty_or_nonempty α
    · exact ⟨f h.elim'⟩
    · exact h

def Exists.choose' {α : Sort _} {p : α → Prop} (t : ∃ x, p x) : α :=
  call_with_cc fun cont =>
    t.casesOn fun w _ => cont w

[Kyle Miller]

Dan Abramov said:

In a sense, is choice strictly more powerful than destructuring?

I believe choice is strictly more powerful.

Destructuring is just the mechanism that's built into the theory of inductive types. It's also the "natural" one (e.g. it's the elimination rule for natural deduction)

[Kyle Miller]

(Oops, I got tricked with my _'s. This is a purely Prop version... I leave it as an exercise to make a version that actually works, if that's possible! Especially one that does the Exists version of Classical.indefiniteDescription.)

[Kyle Miller]

Fixed it:

noncomputable def call_with_cc {α β : Sort _} (f : (α → β) → Nonempty α) : α :=
  Classical.choice <| by
    obtain h | h := isEmpty_or_nonempty α
    · exact f h.elim'
    · exact h

noncomputable def Exists.indefiniteDescription {α : Sort _} {p : α → Prop} (t : ∃ x, p x) :
    { x : α // p x } :=
  call_with_cc fun ret =>
    t.casesOn fun w h => ret ⟨w, h⟩

noncomputable def Exists.choose' {α : Sort*} {p : α → Prop} (t : ∃ x, p x) : α :=
  t.indefiniteDescription.1

theorem Exists.choose_spec' {α : Sort _} {p : α → Prop} (t : ∃ x, p x) :
    p (Exists.choose' t) := by
  -- unfold Exists.choose' indefiniteDescription call_with_cc
  exact Subtype.property _

[Dan Abramov]

To summarize it for myself, here's how I would explain it.

  have y_exists := ((funToPairSet_functional f) x).1 -- ∃ y, ...

  -- Option 1: Destructuring
  let ⟨y1, hy1⟩ := y_exists
  let ⟨y2, hy2⟩ := y_exists
  have : y1 = y2 := by sorry -- not provable (who said they're equal?)

  -- Option 2: Choice
  let y1' := y_exists.choose
  let hy1' := y_exists.choose_spec
  let y2' := y_exists.choose
  let hy2' := y_exists.choose_spec
  have : y1' = y2' := by rfl -- trivially true! "canonical" rabbit for this hat

[Dan Abramov]

with a caveat that uniqueness would make the first case provable