Evens Sum To Even

From Rosetta Code

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.

[edit] 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.

[edit] 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)

[edit] 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)

[edit] 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 _ _ _).