Proof

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

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.

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

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

<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>