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.

Ada

Natural is a pre-defined subtype for Ada.

package Evens is
   type Even_Number is private;
   function "+"(Left, Right : Even_Number) return Even_Number;
   function "-"(Left, Right : Even_Number) return Even_Number;
   function "*"(Left, Right : Even_Number) return Even_Number;
   function "/"(Left, Right : Even_Number) return Natural;
   function Image(Item : Even_Number) return String;
   function To_Even(Item : Natural) return Even_Number;
   function To_Natural(Item : Even_Number) return Natural;
   Constraint_Error : exception;
private
   type Even_Number is record
      Value : Natural := 0;
   end record;
end Evens;

package body Evens is

   ---------
   -- "+" --
   ---------

   function "+" (Left, Right : Even_Number) return Even_Number is
      Temp : Even_Number;
   begin
      Temp.Value := Left.Value + Right.Value;
      return Temp;
   end "+"; 

   ---------
   -- "-" --
   ---------

   function "-" (Left, Right : Even_Number) return Even_Number is
      Temp : Even_Number;
   begin
      if Right.Value > Left.Value then
         raise Constraint_Error;
      end if;
      Temp.Value := Left.Value - Right.Value;
      return Temp;
   end "-";

   ---------
   -- "*" --
   ---------

   function "*" (Left, Right : Even_Number) return Even_Number is
      Temp : Even_Number;
   begin
      Temp.Value := Left.Value * Right.Value;
      return Temp;
   end "*";

   ---------
   -- "/" --
   ---------

   function "/" (Left, Right : Even_Number) return Natural is
      Temp : Natural := Left.Value / Right.Value;
   begin
      return Temp;
   end "/"; 

   -----------
   -- Image --
   ----------- 

   function Image (Item : Even_Number) return String is
   begin
      return Natural'Image(Item.Value);
   end Image;

   -------------
   -- To_Even --
   -------------

   function To_Even (Item : Natural) return Even_Number is
      Temp : Even_Number;
   begin
      if Item mod 2 /= 0 then
         raise Constraint_Error;
      end if;
      Temp.Value := Item;
      return Temp;
   end To_Even;

   ----------------
   -- To_Natural --
   ----------------

   function To_Natural (Item : Even_Number) return Natural is
   begin
      return Item.Value;
   end To_Natural; 

end Evens;

Coq

<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. </coq>

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

<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) </agda2>

Twelf

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