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

Paolo Giarrusso (Feb 12 2022 at 15:49):

(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 ?

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

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: Oct 13 2024 at 01:02 UTC