Stream: Coq users

Topic: explicitly extracting an existential


view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Feb 12 2022 at 15:49):

(deleted)

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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
*)

view this post on Zulip 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 *)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Feb 12 2022 at 16:19):

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

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mohit Tekriwal (Feb 12 2022 at 19:52):

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

view this post on Zulip Paolo Giarrusso (Feb 12 2022 at 19:52):

yes

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Feb 12 2022 at 19:53):

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

view this post on Zulip 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.

view this post on Zulip Mohit Tekriwal (Feb 12 2022 at 19:54):

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

view this post on Zulip 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.

view this post on Zulip Mohit Tekriwal (Feb 12 2022 at 19:56):

so sigW is just to switch between Prop and Types ?

view this post on Zulip Mohit Tekriwal (Feb 12 2022 at 19:57):

what purpose does sigW serve specifically ?

view this post on Zulip Paolo Giarrusso (Feb 12 2022 at 20:00):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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}

view this post on Zulip Mohit Tekriwal (Feb 12 2022 at 20:05):

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

view this post on Zulip Paolo Giarrusso (Feb 12 2022 at 20:05):

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

view this post on Zulip Mohit Tekriwal (Feb 12 2022 at 20:06):

what do you mean by certain T and P ?

view this post on Zulip Mohit Tekriwal (Feb 12 2022 at 20:08):

what are the restrictions on T and P ?

view this post on Zulip 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.

view this post on Zulip Mohit Tekriwal (Feb 12 2022 at 20:10):

ah okay. Thanks !!

view this post on Zulip 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 !

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mohit Tekriwal (Feb 12 2022 at 21:04):

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


Last updated: Feb 08 2023 at 23:03 UTC