Proof: Difference between revisions
Content added Content deleted
(Added twelf example) |
(→Examples: Added Ada) |
||
Line 7: | Line 7: | ||
=Examples= |
=Examples= |
||
=={{header|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; |
|||
=={{header|Coq}}== |
=={{header|Coq}}== |
||
<font color="#a020f0">Inductive</font> <font color="#0000ff">nat</font> : <font color="#228b22">Set</font> := |
<font color="#a020f0">Inductive</font> <font color="#0000ff">nat</font> : <font color="#228b22">Set</font> := |
Revision as of 04:59, 22 December 2007
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.
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
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.
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)
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 _ _ _).