Proof

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.

Proof
You are encouraged to solve this task according to the task description, using any language you may know.

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.

Omega

 data Even :: Nat ~> *0 where
    EZ:: Even Z
    ES:: Even n -> Even (S (S n))
 
 plus:: Nat ~> Nat ~> Nat
 {plus Z m} = m
 {plus (S n) m} = S {plus n m}
 
 even_plus:: Even m -> Even n -> Even {plus m n}
 even_plus EZ en = en
 even_plus (ES em) en = ES (even_plus em en)

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 _ _ _).