The Coq mailing list

[David MENTRE <dmentre AT linux-france.org>]

Hello Robbert and Cédric,

2013/11/20 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)
>> *)

Thanks Robbert, that seems a very fine example.

I had to add "Require Import Omega." to replay the proof. I needed to
remove "{" and "}" characters to replay the proof on Coq 8.3 (no issue
on 8.4).

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

So what would show Curry Howard isomorphism? "Show Proof." (just
before Defined.)?

Best regards,
david