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.
|
...never odd or even... 
Awesome. Thank you for posting this. I just learned a little bit of Coq and was wondering how it compared.
Thanks! This is of course a very light comparison- but hopefully useful nonetheless.