Proof: Difference between revisions
m (Removed explicit syntax highlighting from Agda2) |
m (Removed explicit syntax highlighting from Twelf) |
||
Line 180: | Line 180: | ||
=={{header|Twelf}}== |
=={{header|Twelf}}== |
||
<twelf> |
|||
<font color="#b22222">nat</font> : <font color="#000000">type</font>. |
|||
nat : type. |
|||
<font color="#b22222">z</font> : nat. |
|||
z : nat. |
|||
<font color="#b22222">s</font> : nat <font color="#000000">-></font> nat. |
|||
s : nat -> nat. |
|||
<font color="#b22222">plus</font> : nat <font color="#000000">-></font> nat <font color="#000000">-></font> nat <font color="#000000">-></font> <font color="#000000">type</font>. |
|||
plus : nat -> nat -> nat -> type. |
|||
<font color="#b22222">plus-z</font> : plus z <font color="#0000ff">N2</font> <font color="#0000ff">N2</font>. |
|||
plus-z : plus z N2 N2. |
|||
<font color="#b22222">plus-s</font> : plus (s <font color="#0000ff">N1</font>) <font color="#0000ff">N2</font> (s <font color="#0000ff">N3</font>) |
|||
plus-s : plus (s N1) N2 (s N3) |
|||
<font color="#000000"><-</font> plus <font color="#0000ff">N1</font> <font color="#0000ff">N2</font> <font color="#0000ff">N3</font>. |
|||
<- plus N1 N2 N3. |
|||
%% declare totality assertion |
|||
%mode plus +N1 +N2 -N3. |
|||
<font color="#9370db">%worlds</font> () (plus <font color="#000000">_</font> <font color="#000000">_</font> <font color="#000000">_</font>). |
|||
%worlds () (plus _ _ _). |
|||
%% check totality assertion |
|||
<font color="#9370db">%total</font> <font color="#0000ff">N1</font> (plus <font color="#0000ff">N1</font> <font color="#000000">_</font> <font color="#000000">_</font>). |
|||
%total N1 (plus N1 _ _). |
|||
<font color="#b22222">even</font> : nat <font color="#000000">-></font> <font color="#000000">type</font>. |
|||
even : nat -> type. |
|||
<font color="#b22222">even-z</font> : even z. |
|||
even-z : even z. |
|||
<font color="#b22222">even-s</font> : even (s (s <font color="#0000ff">N</font>)) |
|||
even-s : even (s (s N)) |
|||
<font color="#000000"><-</font> even <font color="#0000ff">N</font>. |
|||
⚫ | |||
<font color="#b22222">sum-evens</font> : even <font color="#0000ff">N1</font> <font color="#000000">-></font> even <font color="#0000ff">N2</font> <font color="#000000">-></font> plus <font color="#0000ff">N1</font> <font color="#0000ff">N2</font> <font color="#0000ff">N3</font> <font color="#000000">-></font> even <font color="#0000ff">N3</font> <font color="#000000">-></font> <font color="#000000">type</font>. |
|||
sum-evens : even N1 -> even N2 -> plus N1 N2 N3 -> even N3 -> type. |
|||
%mode sum-evens +D1 +D2 +Dplus -D3. |
|||
<font color="#b22222">sez</font> : sum-evens |
|||
sez : sum-evens |
|||
⚫ | |||
even-z |
|||
(<font color="#0000ff">DevenN2</font> : even <font color="#0000ff">N2</font>) |
|||
(DevenN2 : even N2) |
|||
(plus-z : plus z <font color="#0000ff">N2</font> <font color="#0000ff">N2</font>) |
|||
(plus-z : plus z N2 N2) |
|||
<font color="#0000ff">DevenN2</font>. |
|||
DevenN2. |
|||
<font color="#b22222">ses</font> : sum-evens |
|||
ses : sum-evens |
|||
( (even-s <font color="#0000ff">DevenN1'</font>) : even (s (s <font color="#0000ff">N1'</font>))) |
|||
( |
( (even-s DevenN1') : even (s (s N1'))) |
||
(DevenN2 : even N2) |
|||
( (plus-s (plus-s <font color="#0000ff">Dplus</font>)) : plus (s (s <font color="#0000ff">N1'</font>)) <font color="#0000ff">N2</font> (s (s <font color="#0000ff">N3'</font>))) |
|||
( (plus-s (plus-s Dplus)) : plus (s (s N1')) N2 (s (s N3'))) |
|||
(even-s DevenN3') |
|||
<font color="#000000"><-</font> sum-evens <font color="#0000ff">DevenN1'</font> <font color="#0000ff">DevenN2</font> <font color="#0000ff">Dplus</font> <font color="#0000ff">DevenN3'</font>. |
|||
<- sum-evens DevenN1' DevenN2 Dplus DevenN3'. |
|||
<font color="#9370db">%worlds</font> () (sum-evens <font color="#000000">_</font> <font color="#000000">_</font> <font color="#000000">_</font> <font color="#000000">_</font>). |
|||
%worlds () (sum-evens _ _ _ _). |
|||
<font color="#9370db">%total</font> <font color="#0000ff">D</font> (sum-evens <font color="#0000ff">D</font> <font color="#000000">_</font> <font color="#000000">_</font> <font color="#000000">_</font>). |
|||
%total D (sum-evens D _ _ _). |
|||
</twelf> |
Revision as of 01:50, 12 March 2008
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
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; 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
<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. </coq>
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)
Agda2
<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) </agda2>
Twelf
<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 _ _ _). </twelf>