Proof
Proof
You are encouraged to solve this task according to the task description, using any language you may know.
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
This is technically not a proof that even numbers sum to even numbers.
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; private type Even_Number is record Value : Natural; end record; end Evens;
package body Evens is function "+" (Left, Right : Even_Number) return Even_Number is begin return (Value => Left.Value + Right.Value); end "+"; function "-" (Left, Right : Even_Number) return Even_Number is begin return (Value => Left.Value - Right.Value); end "-"; function "*" (Left, Right : Even_Number) return Even_Number is begin return (Value => Left.Value * Right.Value); end "*"; function "/" (Left, Right : Even_Number) return Natural is begin return Left.Value / Right.Value; end "/"; function Image (Item : Even_Number) return String is begin return Natural'Image (Item.Value); end Image; function To_Even (Item : Natural) return Even_Number is begin if Item mod 2 = 0 then return (Value => Item); else raise Constraint_Error; end if; end To_Even; function To_Natural (Item : Even_Number) return Natural is begin return Item.Value; end To_Natural; end Evens;
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)
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)
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 _ _ _).