coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>
- To: Cedric Auger <sedrikov AT gmail.com>
- Cc: Pierre Courtieu <pierre.courtieu AT gmail.com>, Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] What problem does an extracted function solve?
- Date: Mon, 4 Nov 2013 20:39:51 +0000
- Accept-language: en-GB, en-US
Thanks to you both for your comments. It hadn't occurred to me to use a front end to filter out bad contexts. Is this what normally happens in practice?
I'd be grateful if someone would point me to a non-trivial example of an extracted function that has been packaged up in this or some other way. Thanks.
Regards,
Jeff.
On 4 Nov 2013, at 13:49, Cedric Auger wrote:
2013/11/4 Pierre Courtieu <pierre.courtieu AT gmail.com>
Hi Jeff,
Short answer: t computes, given a positive integer, a positive
integer. It is not very interesting but you must admit that the
property you extracted was not very interesting from the start. :-)
If you had extracted a proof of (forall x : nat, x > 0 -> {y : nat | y
> x /\ prime(x) }) then you would have obtained a function that given
an integer x greater than 3, return a prime integer above x. That
would have been maybe more interesting.
I would add, that it is also a good thing to define a "front end module", that is a module which would extract each type to identity and would describe a set of entry points to your work, and black-list the other extracted modules to avoid using it in a bad context.
For instance, you could define a "nat -> option nat" function as:
Definition frontend (n : nat) :=
match n with
| O => None
| S _ => projT1 (T n …)
end.
Lemma main : forall x, x>0 -> match frontend x with Some y => y > 0 | None => False end.
…
This way, frontend can be safely called from the outside, and your main lemma says that each positive input is mapped to a positive output via "frontend" (which has exactly the same signature in the extracted code).
Longer answer: Remember that "extraction" means "extract the
computation part of the proof term". On the coq side, T is a function
that takes two arguments: x and H, and returns an exitential proof. If
you remove the non computational part (i.e. things that have a type in
Prop), then T is a function taking only x as argument, and returning
only the witness y used to prove the existential. In this particular
proof you chose to give x itself as a witness of the existance of y.
So the extracted function is the identity.
I would avoid the "proof term" and "existential proof" as they can be confusing (for me this denotes stuff in Prop, and in this sense, this remark is wrong).
If you chose instead this proof:
fun (x : nat) (H : x > 0) => exist (fun y : nat => y > 0) (x+3) H
then the extracted function would be another witness computation,
namely let t x = x + 3.
If you don't see how the existential proof is extracted into only a
witness, you should have a look at the definition of ex (the coq
constant hidden behind "exists"). It is a actually pair (y, P y), the
first componenet is computational, the second is not. So extraction is
straigthforward here: it is a simple projection.
Well, not exactly straight forward. It is a P. Letouzey optimization to remove the constructor.
In fact,
Inductive sig (t:Type) (P:t->Prop) : Type :=
| Exist : forall x, P x -> sig t P.
should be extracted as
type sig 'a = Exist of 'a
but to remove overhead, it is extracted as
type sig 'a = 'a
Hope this helps,
Pierre
2013/11/4 Terrell, Jeffrey <jeffrey.terrell AT kcl.ac.uk>:
> It's easy to show that
>
> T =
> fun (x : nat) (H : x > 0) => exist (fun y : nat => y > 0) x H
> : forall x : nat, x > 0 -> {y : nat | y > 0}
>
> Clearly, T cannot produce an output unless it is given a nat x and a proof that x > 0. However, I'm not sure what to make of the function extracted from T, i.e.
>
> let t x =
> x
>
> because t can produce an output for all values of x, not only x > 0. On the face of it, t appears to solve a different problem than T. How should one view the relationship between t and T?
>
> Regards,
> Jeff.
--
.../Sedrikov\...
- [Coq-Club] What problem does an extracted function solve?, Terrell, Jeffrey, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Pierre Courtieu, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Cedric Auger, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Terrell, Jeffrey, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Pierre Letouzey, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Terrell, Jeffrey, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Cedric Auger, 11/04/2013
- Re: [Coq-Club] What problem does an extracted function solve?, Pierre Courtieu, 11/04/2013
Archive powered by MHonArc 2.6.18.