## Stream: Coq users

### Topic: explicitly extracting an existential

#### Mohit Tekriwal (Feb 12 2022 at 15:23):

Hello,

So I have a proof to define a set of positive naturals:

Lemma lim_extract:
{ N: nat | ltn 0%N N}.
Proof.
apply sigW.
by exists 1%N.
Qed.

To extract an N satisfying the predicate,

I can define the following:
Definition wit_N := proj1_sig lim_extract.

From my understanding, wit_N would be any positive natural.

But, I would like to recover back 1 that I used as a witness in the proof of lim_extract. Is it possible to do so ? or, is it possible to get an explicit witness from an existential proof ?

#### Karl Palmskog (Feb 12 2022 at 15:48):

the `exists` tactic injects something into the `Prop` sort, and once you do that, you can't get that something out of `Prop` (which seems to be what you want). See here for how Coq's Prop works: https://cstheory.stackexchange.com/questions/21836/why-does-coq-have-prop/21878

(deleted)

#### Karl Palmskog (Feb 12 2022 at 15:52):

Paolo, you may be right that it's not the `exists` tactic that's the culprit here, but my interpretation of the question is that the goal is to recover `ltn 0 1`. So I guess the `by` is what technically hides the `1` in `ltn 0 1`?

#### Paolo Giarrusso (Feb 12 2022 at 15:53):

Ah. I thought the goal was to extract `wit_N`... which I think is hidden by (a) `sigW` (b) `Qed`?

#### Paolo Giarrusso (Feb 12 2022 at 15:55):

Concretely, the following variant works:

``````Require Import Lia.
Lemma lim_extract: { N : nat | 0 < N}.
Proof. exists 1; lia. Defined.
Definition wit_N := proj1_sig lim_extract.
Eval cbv in wit_N.
(*
= 1
: nat
*)
``````

#### Paolo Giarrusso (Feb 12 2022 at 16:05):

Uhm, looking closer at `sigW` I suspect you _could_ extract its witness, since it's a constructive proof of the axiom of choice for ssreflect _choice_ types, but something is sealed. Nevertheless, `sigW` seems unnecessary even in the original proof:

``````From mathcomp Require Import ssrbool choice.
From mathcomp Require Import ssrnat ssreflect.

Lemma lim_extract : {N : nat | ltn 0%N N}.
Proof. by exists 1. Defined.
Print Assumptions lim_extract.
(* Closed under the global context *)
Eval vm_compute in proj1_sig lim_extract.
(*
= 1
: nat
*)
Lemma lim_extract' : {N : nat | ltn 0%N N}.
Proof. apply sigW. by exists 1. Defined.

Print Assumptions lim_extract'.
(* Closed under the global context *)

Eval vm_compute in proj1_sig lim_extract'.
(* long output *)
``````

#### Paolo Giarrusso (Feb 12 2022 at 16:06):

and if you have a proof where `sigW` is needed, because you only have an existential in `Prop`, then I expect @Karl Palmskog's answer applies.

#### Paolo Giarrusso (Feb 12 2022 at 16:08):

aah, `xchoose` helps, since `sigW`'s proof is just:

``````Lemma sigW P : (exists x, P x) -> {x | P x}.
Proof. by move=> exP; exists (xchoose exP); apply: xchooseP. Qed.
``````

#### Paolo Giarrusso (Feb 12 2022 at 16:19):

Okay, nope — `xchoose` is axiom-free, but the computational content is sealed anyway.

#### Mohit Tekriwal (Feb 12 2022 at 19:40):

Thanks @Paolo Giarrusso and @Karl Palmskog for your answer. This looks interesting. why is that we are able to extract the witness without `sigW` and not with `sigW` ? Why is it that the computational content is sealed when we use `sigW` ?

#### Paolo Giarrusso (Feb 12 2022 at 19:48):

@Mohit Tekriwal you can't extract computational content from proofs closed with `Qed`, like `sigW`. And AFAICT there are multiple `Qed` in the path to `sigW`.

#### Paolo Giarrusso (Feb 12 2022 at 19:51):

Basically, `Qed` proofs get typechecked (and saved), but are treated as axioms to prevent clients from accidentally depending on details; and computing on axioms gets stuck.

#### Paolo Giarrusso (Feb 12 2022 at 19:52):

That one, per se, could be fixed by using `Defined` instead of `Qed` in the needed places, which is often a bad idea; doing that for `sigW` is not enough.

#### Mohit Tekriwal (Feb 12 2022 at 19:52):

oh okay, that's why you close the proof with `Defined` ?

yes

#### Paolo Giarrusso (Feb 12 2022 at 19:53):

if you close `lim_extract'` with `Qed`, then `Eval vm_compute in proj1_sig lim_extract'.` will get stuck as well.

#### Paolo Giarrusso (Feb 12 2022 at 19:53):

(try it out; it will still give an output, it just won't be `1`).

#### Paolo Giarrusso (Feb 12 2022 at 19:53):

The other point is that `{x | P x}` lives in `Type` and can have computational content, while ` (exists x, P x)` lives in `Prop` so it does not, as @Karl Palmskog mentioned.

#### Mohit Tekriwal (Feb 12 2022 at 19:54):

ah okay, yeah it doesn't output 1. That's interesting. Thanks a lot !! :)

#### Paolo Giarrusso (Feb 12 2022 at 19:55):

and this begs the question: how on Earth can `sigW` work? Does it extract the witness of its argument anyway? Well, no.

#### Mohit Tekriwal (Feb 12 2022 at 19:56):

so `sigW` is just to switch between `Prop` and `Types ` ?

#### Mohit Tekriwal (Feb 12 2022 at 19:57):

what purpose does `sigW` serve specifically ?

#### Paolo Giarrusso (Feb 12 2022 at 20:00):

In your original example, it's indeed not useful.

#### Paolo Giarrusso (Feb 12 2022 at 20:00):

in general, it's a proof of the axiom of choice, under strong restrictions on its arguments:

``````forall [T : choiceType] [P : pred T], (exists x : T, P x) -> {y : T | P y}
``````

(EDITED for clarity)

#### Paolo Giarrusso (Feb 12 2022 at 20:01):

basically, the input asserts there exists an `x : T` such that `P x` holds, but does not actually provide any such `x`.

#### Paolo Giarrusso (Feb 12 2022 at 20:02):

`sigW` will then compute a (possibly different) witness, let's call it `y : T`, such that `P y` holds, and give you a dependent pair of `y : T` and `P y` — that pair is `{y : T | P y}`

#### Mohit Tekriwal (Feb 12 2022 at 20:05):

ah I see. That's really interesting. Thanks a lot for the clarification @Paolo Giarrusso :)

#### Paolo Giarrusso (Feb 12 2022 at 20:05):

and this is only possible for certain `T` and `P` where this magic can be performed :-)

#### Mohit Tekriwal (Feb 12 2022 at 20:06):

what do you mean by certain `T` and `P` ?

#### Mohit Tekriwal (Feb 12 2022 at 20:08):

what are the restrictions on `T` and `P` ?

#### Paolo Giarrusso (Feb 12 2022 at 20:09):

the statement above takes `T : choiceType` and `P : pred T` — and ssreflect defines `pred T := T -> bool` not `T -> Prop`: so it's a computable predicate.

#### Mohit Tekriwal (Feb 12 2022 at 20:10):

ah okay. Thanks !!

#### Mohit Tekriwal (Feb 12 2022 at 20:12):

also regarding the subtleties between `Qed` and `Defined`, do you have pointers to sources were I could refer to for more such subtleties ? Thanks !

#### Paolo Giarrusso (Feb 12 2022 at 20:15):

@Mohit Tekriwal maybe https://stackoverflow.com/q/25478682/53974 helps? But I suspect http://adam.chlipala.net/cpdt/html/Subset.html#pred_strong4 might give a better treatment

#### Ali Caglayan (Feb 12 2022 at 20:16):

If you are asking about Qed specifically, then the reference manual is the best place to look. However if you want to learn about general Coq know-hows, the following is quite a resourceful list: https://github.com/tchajed/coq-tricks

#### Mohit Tekriwal (Feb 12 2022 at 21:04):

Thanks a lot @Paolo Giarrusso and @Ali Caglayan :)

Last updated: Jun 18 2024 at 21:01 UTC