The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 19 Nov 2013 22:03:16 +0100,
Robbert Krebbers 
<mailinglists AT robbertkrebbers.nl>
 a écrit :

> On 11/19/2013 08:27 PM, David MENTRÉ wrote:
> >   * Curry-Howard isomorphism: a very simple Coq theorem (on Boolean
> > or integers) with associated proof, from which I could also
> > generate OCaml code and show the Coq type.
> What about something simple like:
> 
> Lemma minus : forall x y : nat, y <= x -> { z | x = y + z }.
> Proof.
>    induction x as [|x IH].
>    { exists 0. omega. }
>    intros [|y] ?.
>    { exists (S x). omega. }
>    destruct (IH y) as [z Hz]. omega. exists z. omega.
> Defined.
> 
> Extraction minus.
> (*
> (** val minus : nat -> nat -> nat **)
> 
> let rec minus n y =
>    match n with
>    | O -> O
>    | S n0 ->
>      (match y with
>       | O -> S n0
>       | S y0 -> minus n0 y0)
> *)

Be careful, Extraction is not Curry Howard isomorphism! (Well, it is
not an isomorphism at all.)