Proof
Proof
You are encouraged to solve this task according to the task description, using any language you may know.
You are encouraged to solve this task according to the task description, using any language you may know.
Task
Define a type for natural numbers (0, 1, 2, 3, ...) and addition on them. Define a type of even numbers (0, 2, 4, 6, ...) then prove that the addition of any two even numbers is even.
Examples
Coq
Inductive nat : Set := | O : nat | S : nat -> nat. Fixpoint plus (n m:nat) {struct n} : nat := match n with | O => m | S p => S (p + m) end where "n + m" := (plus n m) : nat_scope. Inductive even : nat -> Set := | even_O : even O | even_SSn : forall n:nat, even n -> even (S (S n)). Theorem even_plus_even : forall n m:nat, even n -> even m -> even (n + m). Proof. intros n m H H0. elim H. trivial. intros. simpl. case even_SSn. intros. apply even_SSn; assumption. assumption. Qed.
Agda2
module Arith where data Nat : Set where zero : Nat suc : Nat -> Nat _+_ : Nat -> Nat -> Nat zero + n = n suc m + n = suc (m + n) data Even : Nat -> Set where even_zero : Even zero even_suc_suc : {n : Nat} -> Even n -> Even (suc (suc n)) _even+_ : {m n : Nat} -> Even m -> Even n -> Even (m + n) even_zero even+ en = en even_suc_suc em even+ en = even_suc_suc (em even+ en)
Twelf
nat : type. z : nat. s : nat -> nat. plus : nat -> nat -> nat -> type. plus-z : plus z N2 N2. plus-s : plus (s N1) N2 (s N3) <- plus N1 N2 N3. %% declare totality assertion %mode plus +N1 +N2 -N3. %worlds () (plus _ _ _). %% check totality assertion %total N1 (plus N1 _ _). even : nat -> type. even-z : even z. even-s : even (s (s N)) <- even N. sum-evens : even N1 -> even N2 -> plus N1 N2 N3 -> even N3 -> type. %mode sum-evens +D1 +D2 +Dplus -D3. sez : sum-evens even-z (DevenN2 : even N2) (plus-z : plus z N2 N2) DevenN2. ses : sum-evens ( (even-s DevenN1') : even (s (s N1'))) (DevenN2 : even N2) ( (plus-s (plus-s Dplus)) : plus (s (s N1')) N2 (s (s N3'))) (even-s DevenN3') <- sum-evens DevenN1' DevenN2 Dplus DevenN3'. %worlds () (sum-evens _ _ _ _). %total D (sum-evens D _ _ _).