The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT univ-grenoble-alpes.fr>]

Hello,

Here is a simple example.

Inductive even : nat -> Prop :=
| E0 : even 0
| E2 : forall n, even n -> even (S (S n)).

Definition ev2 : even 2 := E2 0 E0.
Definition ev4 : even 4 := E2 2 ev2.

(* An explicit proof term for the following *)
Definition even_plus : forall n m, even n -> even m -> even (n + m) :=
  fun n m evn evm  =>
    (fix fxp n (e : even n) {struct e} : even(n+m) :=
       match e in even n return even (n+m) with
       | E0 => evm
       | E2 n' en' => E2 (n'+m) (fxp  n' en')
       end) n evn.

Compute (even_plus 4 2 ev4 ev2 : even 6).
(* =  E2 4 (E2 2 (E2 0 E0)) *)

Hope this helps,
Jean-Francois

On Wed, Oct 27, 2021 at 01:18:34PM +0400, Frederic Mesnard wrote:
>    Hi all,
> 
>    I am reading the CACM paper "Propositions as Types" written by Philip
>    Wadler.
>    With Coq, I can easily observe "propositions as types" and "proofs as
>    programs".
>    Can I also observe "simplification of proofs as evaluation of programs"
>    within Coq?
>    Where can I find examples?
> 
>    Thanks in advance!
>    Fred

-- 
Jean-Francois Monin
Verimag
Universite Grenoble Alpes