**Note from 23rd August, 2017**

I found this draft blog post lying around, written in the spring of 2015 while I was working at Imperial College London as a Research Associate in the Mobility Reading Group with Nobuko Yoshida. This was the fruit of a discussion with Tiago Cogumbreiro where we were comparing Coq and Agda for theorem proving. I believe we had a few more “side-by-side” comparisons written down, but this is all I have here: simple code for showing that addition of two even numbers yields an even number. It might prove to be a useful reference for someone else (at the time, I had a hard time remembering Coq syntax as I didn’t use it very often, and Tiago kindly gave me some pointers) so I have posted it “as is” now, over two years later.

Agda | Coq |
---|---|

data Nat : Set where zero : Nat succ : Nat -> Nat data Even : Nat -> Set where even_base : Even zero even_step : forall {n} -> Even n -> Even (succ (succ n)) |
Inductive Nat := | zero : Nat | succ : Nat -> Nat. Inductive Even: Nat -> Prop := | even_base : Even zero | even_step : forall n, Even n -> Even (succ (succ n)). |

_+_ : Nat -> Nat -> Nat zero + n = n (succ n) + m = succ (n + m) |
Fixpoint add (n:Nat) (m:Nat) := match n with | zero => m | succ n' => succ (add n' m) end. |

even_sum : forall {n m} -> Even n -> Even m -> Even (n + m) even_sum even_base x = x even_sum (even_step x) y = even_step (even_sum x y) |
Lemma add_succ: forall n m, add (succ n) m = succ (add n m). Proof. auto. Qed. Lemma even_sum : forall n m, Even n -> Even m -> Even (add n m). Proof. intros n m even_n even_m. induction even_n. (* case even_base *) - simpl. assumption. (* case even_step *) - repeat (rewrite add_succ). apply even_step. assumption. Qed. |