Proof: Difference between revisions
Content added Content deleted
No edit summary |
|||
Line 3: | Line 3: | ||
Define a type of even numbers (0, 2, 4, 6, ...) then prove that the addition of any two even numbers is even. |
Define a type of even numbers (0, 2, 4, 6, ...) then prove that the addition of any two even numbers is even. |
||
=={{header| |
=={{header|Coq}}== |
||
<font color="#a020f0">Inductive</font> <font color="#0000ff">nat</font> : <font color="#228b22">Set</font> := |
|||
| O : nat |
|||
This is technically not a proof that even numbers sum to even numbers. |
|||
| S : nat -> nat. |
|||
Natural is a pre-defined subtype for Ada. |
|||
<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 |
|||
<font color="#a020f0">Fixpoint</font> <font color="#0000ff">plus</font> (<font color="#b8860b">n m</font>:nat) {<font color="#228b22">struct</font> n} : nat := |
|||
--------- |
|||
<font color="#228b22">match</font> n <font color="#228b22">with</font> |
|||
-- "+" -- |
|||
| O => m |
|||
| S p => S (p + m) |
|||
<font color="#228b22">end</font> |
|||
where <font "string">"n + m"</font> := (plus n m) : nat_scope. |
|||
function "+" (Left, Right : Even_Number) return Even_Number is |
|||
begin |
|||
return (Value => Left.Value + Right.Value); |
|||
end "+"; |
|||
--------- |
|||
-- "-" -- |
|||
--------- |
|||
<font color="#a020f0">Inductive</font> <font color="#0000ff">even</font> : nat -> <font color="#228b22">Set</font> := |
|||
function "-" (Left, Right : Even_Number) return Even_Number is |
|||
| even_O : even O |
|||
begin |
|||
| even_SSn : <font color="#228b22">forall</font> n:nat, |
|||
return (Value => Left.Value - Right.Value); |
|||
even n -> even (S (S n)). |
|||
end "-"; |
|||
--------- |
|||
-- "*" -- |
|||
--------- |
|||
<font color="#a020f0">Theorem</font> <font color="#0000ff">even_plus_even</font> : <font color="#228b22">forall</font> n m:nat, |
|||
function "*" (Left, Right : Even_Number) return Even_Number is |
|||
even n -> even m -> even (n + m). |
|||
begin |
|||
<font color="#a020f0">Proof</font>. |
|||
return (Value => Left.Value * Right.Value); |
|||
<font color="#00008b">intros</font> n m H H0. |
|||
end "*"; |
|||
<font color="#00008b">elim</font> H. |
|||
--------- |
|||
<font color="#00008b">trivial</font>. |
|||
-- "/" -- |
|||
<font color="#00008b">intros</font>. |
|||
<font color="#00008b">simpl</font>. |
|||
function "/" (Left, Right : Even_Number) return Natural is |
|||
<font color="#00008b">case</font> even_SSn. |
|||
return Left.Value / Right.Value; |
|||
<font color="#00008b">intros</font>. |
|||
end "/"; |
|||
<font color="#00008b">apply</font> even_SSn; <font color="#00008b">assumption</font>. |
|||
----------- |
|||
<font color="#00008b">assumption</font>. |
|||
-- Image -- |
|||
<font color="#a020f0">Qed</font>. |
|||
----------- |
|||
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;</ada> |
|||
=={{header|Agda2}}== |
|||
<pre> |
|||
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) |
|||
</pre> |
|||
=={{header|Coq}}== |
|||
<pre> |
|||
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. |
|||
</pre> |
|||
=={{header|Omega}}== |
=={{header|Omega}}== |
||
Line 170: | Line 55: | ||
even_plus (ES em) en = ES (even_plus em en) |
even_plus (ES em) en = ES (even_plus em en) |
||
=={{header| |
=={{header|Agda2}}== |
||
<font color="#cd6600">module</font> <font color="#a020f0">Arith</font> <font color="#cd6600">where</font> |
|||
<pre> |
|||
nat : type. |
|||
z : nat. |
|||
<font color="#cd6600">data</font> <font color="#006400">Nat</font> <font color="#404040">:</font> <font color="#0000cd">Set</font> <font color="#cd6600">where</font> |
|||
s : nat -> nat. |
|||
<font color="#008b00">zero</font> <font color="#404040">:</font> <font color="#006400">Nat</font> |
|||
<font color="#008b00">suc</font> <font color="#404040">:</font> <font color="#006400">Nat</font> <font color="#404040">-></font> <font color="#006400">Nat</font> |
|||
<font color="#0000ee">_+_</font> <font color="#404040">:</font> <font color="#006400">Nat</font> <font color="#404040">-></font> <font color="#006400">Nat</font> <font color="#404040">-></font> <font color="#006400">Nat</font> |
|||
<font color="#008b00">zero</font> <font "agda2-highlight-operator"><font color="#0000ee">+</font></font> <font "agda2-highlight-bound-variable">n</font> <font color="#404040">=</font> <font "agda2-highlight-bound-variable">n</font> |
|||
<font color="#008b00">suc</font> <font "agda2-highlight-bound-variable">m</font> <font "agda2-highlight-operator"><font color="#0000ee">+</font></font> <font "agda2-highlight-bound-variable">n</font> <font color="#404040">=</font> <font color="#008b00">suc</font> <font color="#404040">(</font><font "agda2-highlight-bound-variable">m</font> <font "agda2-highlight-operator"><font color="#0000ee">+</font></font> <font "agda2-highlight-bound-variable">n</font><font color="#404040">)</font> |
|||
<font color="#cd6600">data</font> <font color="#006400">Even</font> <font color="#404040">:</font> <font color="#006400">Nat</font> <font color="#404040">-></font> <font color="#0000cd">Set</font> <font color="#cd6600">where</font> |
|||
<font color="#008b00">even_zero</font> <font color="#404040">:</font> <font color="#006400">Even</font> <font color="#008b00">zero</font> |
|||
<font color="#008b00">even_suc_suc</font> <font color="#404040">:</font> <font color="#404040">{</font><font "agda2-highlight-bound-variable">n</font> <font color="#404040">:</font> <font color="#006400">Nat</font><font color="#404040">}</font> <font color="#404040">-></font> <font color="#006400">Even</font> <font "agda2-highlight-bound-variable">n</font> <font color="#404040">-></font> <font color="#006400">Even</font> <font color="#404040">(</font><font color="#008b00">suc</font> <font color="#404040">(</font><font color="#008b00">suc</font> <font "agda2-highlight-bound-variable">n</font><font color="#404040">))</font> |
|||
<font color="#0000ee">_even+_</font> <font color="#404040">:</font> <font color="#404040">{</font><font "agda2-highlight-bound-variable">m</font> <font "agda2-highlight-bound-variable">n</font> <font color="#404040">:</font> <font color="#006400">Nat</font><font color="#404040">}</font> <font color="#404040">-></font> <font color="#006400">Even</font> <font "agda2-highlight-bound-variable">m</font> <font color="#404040">-></font> <font color="#006400">Even</font> <font "agda2-highlight-bound-variable">n</font> <font color="#404040">-></font> <font color="#006400">Even</font> <font color="#404040">(</font><font "agda2-highlight-bound-variable">m</font> <font "agda2-highlight-operator"><font color="#0000ee">+</font></font> <font "agda2-highlight-bound-variable">n</font><font color="#404040">)</font> |
|||
<font color="#008b00">even_zero</font> <font "agda2-highlight-operator"><font color="#0000ee">even+</font></font> <font "agda2-highlight-bound-variable">en</font> <font color="#404040">=</font> <font "agda2-highlight-bound-variable">en</font> |
|||
<font color="#008b00">even_suc_suc</font> <font "agda2-highlight-bound-variable">em</font> <font "agda2-highlight-operator"><font color="#0000ee">even+</font></font> <font "agda2-highlight-bound-variable">en</font> <font color="#404040">=</font> <font color="#008b00">even_suc_suc</font> <font color="#404040">(</font><font "agda2-highlight-bound-variable">em</font> <font "agda2-highlight-operator"><font color="#0000ee">even+</font></font> <font "agda2-highlight-bound-variable">en</font><font color="#404040">)</font> |
|||
=={{header|Twelf}}== |
|||
plus : nat -> nat -> nat -> type. |
|||
<font color="#b22222">nat</font> : <font color="#000000">type</font>. |
|||
plus-z : plus z N2 N2. |
|||
<font color="#b22222">z</font> : nat. |
|||
plus-s : plus (s N1) N2 (s N3) |
|||
<font color="#b22222">s</font> : nat <font color="#000000">-></font> nat. |
|||
<- plus N1 N2 N3. |
|||
<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>. |
|||
%% declare totality assertion |
|||
<font color="#b22222">plus-z</font> : plus z <font color="#0000ff">N2</font> <font color="#0000ff">N2</font>. |
|||
%mode plus +N1 +N2 -N3. |
|||
<font color="#b22222">plus-s</font> : plus (s <font color="#0000ff">N1</font>) <font color="#0000ff">N2</font> (s <font color="#0000ff">N3</font>) |
|||
%worlds () (plus _ _ _). |
|||
<font color="#000000"><-</font> plus <font color="#0000ff">N1</font> <font color="#0000ff">N2</font> <font color="#0000ff">N3</font>. |
|||
%% check totality assertion |
|||
%total N1 (plus N1 _ _). |
|||
<font color="#b22222">%% declare totality assertion</font> |
|||
<font color="#9370db">%mode</font> plus +N1 +N2 -N3. |
|||
<font color="#9370db">%worlds</font> () (plus <font color="#000000">_</font> <font color="#000000">_</font> <font color="#000000">_</font>). |
|||
even : nat -> type. |
|||
<font color="#b22222">%% check totality assertion</font> |
|||
even-z : even z. |
|||
<font color="#9370db">%total</font> <font color="#0000ff">N1</font> (plus <font color="#0000ff">N1</font> <font color="#000000">_</font> <font color="#000000">_</font>). |
|||
even-s : even (s (s N)) |
|||
<- even N. |
|||
<font color="#b22222">even</font> : nat <font color="#000000">-></font> <font color="#000000">type</font>. |
|||
sum-evens : even N1 -> even N2 -> plus N1 N2 N3 -> even N3 -> type. |
|||
<font color="#b22222">even-z</font> : even z. |
|||
%mode sum-evens +D1 +D2 +Dplus -D3. |
|||
<font color="#b22222">even-s</font> : even (s (s <font color="#0000ff">N</font>)) |
|||
<font color="#000000"><-</font> even <font color="#0000ff">N</font>. |
|||
sez : sum-evens |
|||
even-z |
|||
(DevenN2 : even N2) |
|||
<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>. |
|||
(plus-z : plus z N2 N2) |
|||
<font color="#9370db">%mode</font> sum-evens +D1 +D2 +Dplus -D3. |
|||
DevenN2. |
|||
<font color="#b22222">sez</font> : sum-evens |
|||
even-z |
|||
(DevenN2 : even N2) |
(<font color="#0000ff">DevenN2</font> : even <font color="#0000ff">N2</font>) |
||
(plus-z : plus z <font color="#0000ff">N2</font> <font color="#0000ff">N2</font>) |
|||
<font color="#0000ff">DevenN2</font>. |
|||
(even-s DevenN3') |
|||
<- sum-evens DevenN1' DevenN2 Dplus DevenN3'. |
|||
<font color="#b22222">ses</font> : sum-evens |
|||
( (even-s <font color="#0000ff">DevenN1'</font>) : even (s (s <font color="#0000ff">N1'</font>))) |
|||
%worlds () (sum-evens _ _ _ _). |
|||
(<font color="#0000ff">DevenN2</font> : even <font color="#0000ff">N2</font>) |
|||
%total D (sum-evens D _ _ _). |
|||
( (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>))) |
|||
</pre> |
|||
(even-s <font color="#0000ff">DevenN3'</font>) |
|||
<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>. |
|||
<font color="#9370db">%worlds</font> () (sum-evens <font color="#000000">_</font> <font color="#000000">_</font> <font color="#000000">_</font> <font color="#000000">_</font>). |
|||
<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>). |
Revision as of 20:18, 10 August 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.
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)
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 _ _ _).