Exists elimination

Stream: Type theory

[Nico Beck]

I have read that the kernel of Lean 3 works proof irrelevant. All proofs of a theorem are judgmentally equal. Does that mean that if I have constructed a proof p : exists x, P x where P : A -> Prop, A : Type, then there is no way to extract an actual w : A from p for which P w is true?

Is it possible to extract witnesses from existence proofs in Lean 2? I really like this feature of (intuitionistic) type theory, and I would like to use it. How is the situation in Coq?

[Karl Palmskog]

Coq extraction (to OCaml/Haskell/Scheme) removes all occurrences of terms in Prop. That is, if you want to get witnesses, you have to define them in the Set or Type sorts. People usually do this with sigma types, e.g., they write { x : nat | prime x} as the type of a "fancy" existence proof of a primality checker that should extract well (and you can also easily get the proof of primality inside Coq when you need it).

To my knowledge, Lean doesn't have a similar extraction like Coq's to OCaml etc., but others may know more about the closest functionality.

[Johan Commelin]

@Nico Beck In Lean you would have to use the axiom of choice to pull out a witness.

[Johan Commelin]

But again, if you have a term of the subtype {x : A // P x}, then you can of course get the witness constructively.

[Nico Beck]

@Johan Commelin I have learned that in intuitionistic logic a proof of \exists x : A, P x is the same as a pair (x, p) where x : A and p : P x. (I.e. exists is just a Sigma-type). If exists is implemented like this, then I shouldn't need the axiom of choice to extract a witness from a proof.

I have tried to use Sigma types in Lean, but I can not form \Sigma x : A, P x if P is of type P: A \to Prop. I can only do it if P is of type P : A\to Type. My question is basically if there is a version of Lean where exists is implemented as a \Sigma type (maybe I am misunderstanding something). What about the HoTT version of Lean 2? Can I use \Sigma x : A, P x : Prop in HoTT?

[Johan Commelin]

You are exactly looking for {x : A // P x}.

[Johan Commelin]

But not that this is not necessarily a subsingleton.

[Johan Commelin]

If you want that, then you could stick a trunc in front of it.

[Nico Beck]

Okay, thank you :) Where can I read about {x : A // P x }? Is it in the 'theorem proving in Lean' book?

[Johan Commelin]

Probably. It's notation for docs#subtype

[bottine]

If I may: what's the difference between sigma and subtype?

[Johan Commelin]

subtype is for P : X → Prop as opposed to P : X → Type u.

[bottine]

OK, and is there a reason for the distinction? I understand (or somehow am OK) with the distinction between Exists and Sigma: Exists behaves as the subsingleton truncation of Sigma (right?), but wouldn't Sigma subsume subtype?

[Johan Commelin]

It probably has to do with Prop being impredicative. But I really don't know. I've never really thought about these issues.

[bottine]

OK, thanks!

[bottine]

By the way, is there a kind of "LEAN book" reference mirroring the HoTT book: somewhere explaining the type theory underlying LEAN and how things are built on it?

[Johan Commelin]

There is #leantt and #tpil

[bottine]

These are good references, indeed :)

[Karl Palmskog]

here is the explanation for why Coq distinguishes sigma types: https://cstheory.stackexchange.com/questions/21836/why-does-coq-have-prop

[Reid Barton]

Karl Palmskog said:

To my knowledge, Lean doesn't have a similar extraction like Coq's to OCaml etc., but others may know more about the closest functionality.

The closest analogue is the Lean interpreter (or in Lean 4, the compiler). Interpreted/compiled code also has no runtime representation for p : Prop. Functions that use constants like choice in ways that are relevant for computation (e.g., not just inside proofs) are marked noncomputable and the interpreter/compiler won't generate code for them.

[Eric Wieser]

docs#subtype and docs#sigma are both special cases of docs#psigma.