Proof

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