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 ?

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)

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`

?

Ah. I thought the goal was to extract `wit_N`

... which I think is hidden by (a) `sigW`

(b) `Qed`

?

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
*)
```

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 *)
```

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.

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.
```

Okay, nope — `xchoose`

is axiom-free, but the computational content is sealed anyway.

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`

?

@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`

.

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.

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.

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

?

yes

if you close `lim_extract'`

with `Qed`

, then `Eval vm_compute in proj1_sig lim_extract'.`

will get stuck as well.

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

).

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.

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

and this begs the question: how on Earth can `sigW`

work? Does it extract the witness of its argument anyway? Well, no.

so `sigW`

is just to switch between `Prop`

and `Types `

?

what purpose does `sigW`

serve specifically ?

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

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)

basically, the input asserts there exists an `x : T`

such that `P x`

holds, but does not actually provide any such `x`

.

`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}`

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

and this is only possible for certain `T`

and `P`

where this magic can be performed :-)

what do you mean by certain `T`

and `P`

?

what are the restrictions on `T`

and `P`

?

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.

ah okay. Thanks !!

also regarding the subtleties between `Qed`

and `Defined`

, do you have pointers to sources were I could refer to for more such subtleties ? Thanks !

@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

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

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

Last updated: Oct 05 2023 at 02:01 UTC