The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Here's just another very simple example to throw out there, in case it's useful:

Fixpoint plus_0_r (n:nat) : n + 0 = n :=
match n return (n + 0 = n) with
| 0 => eq_refl 0
| S m => f_equal S (plus_0_r m)
end.

This defines a proof term of type "forall n:nat, n + 0 = n", and illustrates the equivalence between "proof by induction" and "recursively defined function".  It also points out why Coq's type checking needs to be able to do some reduction of definitions: in the first case, eq_refl 0 is of type "0 = 0" while the match statement expects something of type "0 + 0 = 0".  So the type checker needs to be able to determine that those two types are in fact the same thing, using the definition of plus to reduce "0 + 0" to "0".  Likewise, in the second case, f_equal S (plus_0_r m) is literally of type "S (m + 0) = S m" while the match expects something of type "(S m) + 0 = S m", so again it needs to do partial reduction of the first one, not knowing anything about m, in order to determine that the two types are the same.
--

Daniel Schepler

On Wed, Nov 20, 2013 at 3:37 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

As far as I understand, you can see Curry Howard isomorphism as something to give a common framework to both proofs and computations.
I think it helps to mix them. If you want to do some proofs on programs, you need two languages, one to define programs (and in which you may wish to also express some properties¹), and another to define proofs, and which will have some understanding on the one to define programs. Curry Howard isomorphism allows to use one common framework for both. Furthermore, it allows also to make programs involving proofs (as {x|x>0} type), so we can mix all in a very uniform way (beside the fact that you do not want to extract information from proof, ie. you want proof irrelevance).

¹this wish can be neglected, as a: "div : (a:int) -> int <precondition:a>0> = …" can also be written "div : int -> int" and the precondition added in the proof part (so in the second language), for the theorem to hold.

2013/11/20 David MENTRE <dmentre AT linux-france.org>

Hello Cedric,

2013/11/20 Cedric Auger <sedrikov AT gmail.com>:

> Still, maybe you wanted to do extraction and have proved programs in OCaml
> thanks to it, simply, this is not the Curry Howard isomorphism, it is some
> other interesting theory (but don’t forget, that once extracted, you cannot
> go back to the proof

Yes, I just wanted to illustrate Coq proof, extraction and proved
programs (Robbert example is nice in that regard). You are right that
I misunderstood that the Curry-Howard isomorphism was used for the
extraction mechanism. I thought the extracted program was issued from
the Coq proof (by interpreting the proof as program through
Curry-Howard) after erasing type annotations.

Now a last question: is the Curry-Howard isomorphism used in Coq
internals or not at all? In other words, is this isomorphism needed in
underlying Coq logic or not?


Thank you for your replies,
Best regards,
david

--
.../Sedrikov\...