Proof: Difference between revisions
Content added Content deleted
(Simplified the Ada source code.) |
|||
Line 4: | Line 4: | ||
=={{header|Ada}}== |
=={{header|Ada}}== |
||
This is technically not a proof that even numbers sum to even numbers. |
|||
Natural is a pre-defined subtype for Ada. |
Natural is a pre-defined subtype for Ada. |
||
package Evens is |
package Evens is |
||
Line 14: | Line 17: | ||
function To_Even(Item : Natural) return Even_Number; |
function To_Even(Item : Natural) return Even_Number; |
||
function To_Natural(Item : Even_Number) return Natural; |
function To_Natural(Item : Even_Number) return Natural; |
||
Constraint_Error : exception; |
|||
private |
private |
||
type Even_Number is record |
type Even_Number is record |
||
Value : Natural |
Value : Natural; |
||
end record; |
end record; |
||
end Evens; |
end Evens; |
||
Line 28: | Line 30: | ||
function "+" (Left, Right : Even_Number) return Even_Number is |
function "+" (Left, Right : Even_Number) return Even_Number is |
||
Temp : Even_Number; |
|||
begin |
begin |
||
return (Value => Left.Value + Right.Value); |
|||
⚫ | |||
end "+"; |
end "+"; |
||
Line 39: | Line 39: | ||
function "-" (Left, Right : Even_Number) return Even_Number is |
function "-" (Left, Right : Even_Number) return Even_Number is |
||
Temp : Even_Number; |
|||
begin |
begin |
||
return (Value => Left.Value - Right.Value); |
|||
raise Constraint_Error; |
|||
⚫ | |||
Temp.Value := Left.Value - Right.Value; |
|||
return Temp; |
|||
end "-"; |
end "-"; |
||
Line 53: | Line 48: | ||
function "*" (Left, Right : Even_Number) return Even_Number is |
function "*" (Left, Right : Even_Number) return Even_Number is |
||
Temp : Even_Number; |
|||
begin |
begin |
||
return (Value => Left.Value * Right.Value); |
|||
return Temp; |
|||
end "*"; |
end "*"; |
||
Line 64: | Line 57: | ||
function "/" (Left, Right : Even_Number) return Natural is |
function "/" (Left, Right : Even_Number) return Natural is |
||
Temp : Natural := Left.Value / Right.Value; |
|||
begin |
begin |
||
return |
return Left.Value / Right.Value; |
||
end "/"; |
end "/"; |
||
Line 75: | Line 67: | ||
function Image (Item : Even_Number) return String is |
function Image (Item : Even_Number) return String is |
||
begin |
begin |
||
return Natural'Image(Item.Value); |
return Natural'Image (Item.Value); |
||
end Image; |
end Image; |
||
Line 83: | Line 75: | ||
function To_Even (Item : Natural) return Even_Number is |
function To_Even (Item : Natural) return Even_Number is |
||
Temp : Even_Number; |
|||
begin |
begin |
||
if Item mod 2 |
if Item mod 2 = 0 then |
||
⚫ | |||
⚫ | |||
raise Constraint_Error; |
raise Constraint_Error; |
||
end if; |
end if; |
||
Temp.Value := Item; |
|||
return Temp; |
|||
end To_Even; |
end To_Even; |
||
Revision as of 11:44, 16 March 2008
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 "/"; ----------- -- 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 begin if Item mod 2 = 0 then return (Value => Item); else raise Constraint_Error; end if; end To_Even; ---------------- -- To_Natural -- ---------------- 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 _ _ _).