Universal vs existential quantifier proof computation

Stream: new members

[Plamen Dimitrov]

Hi all, why is the computational structure for dependent function types preserved in Lean but the one for pairs isn't? If I have a proof h : ∀ x : α, P x I can apply it to data x to produce a proof of the proposition P xbut if I instead have a proof h : ∃ x : α, P xI need a noncomputable h.choose to extract the witness. Axiom of choice and classical reasoning aside, I assume the problem boils down to not allowing eliminating from the Prop universe into a Type universe which would differentiate the second from the first case? Because if one has already made the effort to construct the witness x and thus construct an existential proof h then why won't they be able to reuse their own constriction from within the proof term?

[Aaron Liu]

Because of definitional proof irrelevance, you can't be allowed to project data from proofs

[Kevin Buzzard]

Because it's unsound if you can use the witness. Any two proofs of a proposition are equal in lean so in particular different witnesses give the same proof

[Aaron Liu]

if the exists statement is the existence of a proof, then you can project it out, so if P is a proposition and h : ∃ x : P, Q x then h.1 : P and h.2 : Q h.1

[Niels Voss]

Please see https://leanprover-community.github.io/extras/pitfalls.html#trying-to-extract-data-from-proofs-of-propositions. I think what you might be confused about is why you can seemingly extract data from hf : ∀ x : α, P x, but not from he : ∃ x : α, P x, despite them both being proofs of propositions. The reason for this is that when you apply x to hf, you don't get data, you get a proof, which is perfectly fine. Likewise, you are actually allowed to extract an x from he without choice using Exists.elim provided that this x is only used to produce a proof of a proposition. The only thing that requires using choice is extracting an x from he and then using it to construct an element of some type in Type or above.

[Plamen Dimitrov]

First of all, thanks all for replying and the clarifications you added!

I think what you might be confused about is why you can seemingly extract data from hf : ∀ x : α, P x, but not from he : ∃ x : α, P x, despite them both being proofs of propositions.

Exactly, it seemed strange they are treated differently at first.

Likewise, you are actually allowed to extract an x from he without choice using Exists.elim provided that this x is only used to produce a proof of a proposition.

Good clarification, it must explain why we can eliminate in proofs but not outside of them.

The only thing that requires using choice is extracting an x from he and then using it to construct an element of some type in Type or above.

This matches with my suggested assumption above: "I assume the problem boils down to not allowing eliminating from the Prop universe into a Type universe which would differentiate the second from the first case."

Because it's unsound if you can use the witness. Any two proofs of a proposition are equal in lean so in particular different witnesses give the same proof.

I see, so in one sentence because of the design choice of proof irrelevance so that we cannot project two witnesses that might compute differently from the same proof. Or in a validated example:

def he1 : ∃ x, x = 0  := ⟨0, rfl⟩
def he2 : ∃ x, x = 0  := ⟨0 + 0, rfl⟩

def P : Prop := ∃ x, x = 0
def proof_irrelevance : ∀ (p q : P), p = q := sorry

def irrelevant_proofs : he1 = he2 := proof_irrelevance he1 he2
#check he1.1 = he2.1
/-
Invalid projection: Cannot project a value of non-propositional type
  Nat
from the expression
  he1
which has propositional type
  ∃ x, x = 0
-/

if the exists statement is the existence of a proof, then you can project it out, so if P is a proposition and h : ∃ x : P, Q x then h.1 : P and h.2 : Q h.1

Which makes the behavior consistent in allowing exploiting the computational structure of the two proofs as long as the result of this is a proof, i.e. remains in the Prop universe. Just to add a validated example for everyone else that might end up reading this:

def P: Prop := sorry
def Q (x: P): Prop := sorry

def h : ∃ x : P, Q x := sorry

#check h.1 -- : P
#check h.2 -- : Q h.1

Thanks all!