The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

For a simple example of the Curry-Howard isomorphism, how about:

Definition or_ind : forall P Q R:Prop, (P -> R) -> (Q -> R) -> (P \/ Q -> R) :=

fun P Q R PimplR QimplR (H : P \/ Q) =>
match H with

| or_introl p => PimplR p

| or_intror q => QimplR q
end.

vs

Definition sum_rect : forall A B C:Type, (A -> C) -> (B -> C) -> (A + B -> C) :=
fun A B C AtoC BtoC (s : A + B) =>
match s with

| inl a => AtoC a

| inr b => BtoC b
end.

On Tue, Nov 19, 2013 at 11:27 AM, David MENTRÉ <dmentre AT linux-france.org> wrote:

Hello,

I am doing some introductory course on formal methods. Amongst them, I tell a few words about Coq and its underlying principles.

To illustrate more concretely this Coq part, would somebody have or point me to some *very* simple Coq examples of:

 * Constructive logic: an example showing a short demonstration that exhibits the mathematical element to prove compared to the same proof made with classical logic;

 * 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.

The shorter the better. If both parts can be combined into the same example, it might be easier to explain.

I have looked on Wikipedia and Google but examples I found were rather complicated (at least not something that can be explained in one slide).

Many thanks in advance for any help.

Best regards,
david