Proof: Difference between revisions
(→{{header|Twelf}}: PureBasic Omitted) |
(Use lang tags for all of these.) |
||
Line 21: | Line 21: | ||
Prove that the addition of any two even numbers is even, if the result is a member of the type. |
Prove that the addition of any two even numbers is even, if the result is a member of the type. |
||
=={{header| |
=={{header|Agda}}== |
||
Requires version w. |
|||
<font color="#cd6600">module</font> <font color="#a020f0">Arith</font> <font color="#cd6600">where</font> |
|||
<font color="#cd6600">data</font> <font color="#006400">Nat</font> <font color="#404040">:</font> <font color="#0000cd">Set</font> <font color="#cd6600">where</font> |
|||
<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> |
|||
<lang agda>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) |
|||
</lang> |
|||
=={{header|Coq}}== |
=={{header|Coq}}== |
||
<lang coq>Inductive nat : Set := |
|||
| O : nat |
|||
| S : nat -> nat. |
|||
<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. |
|||
<font color="#a020f0">Inductive</font> <font color="#0000ff">even</font> : nat -> <font color="#228b22">Set</font> := |
|||
| even_O : even O |
|||
| even_SSn : <font color="#228b22">forall</font> n:nat, |
|||
even n -> even (S (S n)). |
|||
<font color="#a020f0">Theorem</font> <font color="#0000ff">even_plus_even</font> : <font color="#228b22">forall</font> n m:nat, |
|||
even n -> even m -> even (n + m). |
|||
<font color="#a020f0">Proof</font>. |
|||
<font color="#00008b">intros</font> n m H H0. |
|||
<font color="#00008b">elim</font> H. |
|||
<font color="#00008b">trivial</font>. |
|||
<font color="#00008b">intros</font>. |
|||
<font color="#00008b">simpl</font>. |
|||
<font color="#00008b">case</font> even_SSn. |
|||
<font color="#00008b">intros</font>. |
|||
<font color="#00008b">apply</font> even_SSn; <font color="#00008b">assumption</font>. |
|||
<font color="#00008b">assumption</font>. |
|||
<font color="#a020f0">Qed</font>. |
|||
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. |
|||
</lang> |
|||
=={{header|Haskell}}== |
=={{header|Haskell}}== |
||
Line 85: | Line 87: | ||
=={{header|Omega}}== |
=={{header|Omega}}== |
||
<lang 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) |
|||
</lang> |
|||
=={{header|Tcl}}== |
=={{header|Tcl}}== |
||
Line 184: | Line 187: | ||
=={{header|Twelf}}== |
=={{header|Twelf}}== |
||
<font color="#b22222">nat</font> : <font color="#000000">type</font>. |
|||
<lang twelf>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. |
|||
<font color="#b22222">%% declare totality assertion</font> |
|||
%% declare totality assertion |
|||
<font color="#9370db">%mode</font> plus +N1 +N2 -N3. |
|||
%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 _ _ _). |
|||
<font color="#b22222">%% check totality assertion</font> |
|||
%% 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>. |
|||
<- even N. |
|||
<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. |
|||
<font color="#9370db">%mode</font> sum-evens +D1 +D2 +Dplus -D3. |
|||
%mode sum-evens +D1 +D2 +Dplus -D3. |
|||
<font color="#b22222">sez</font> : sum-evens |
|||
sez : sum-evens |
|||
even-z |
|||
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 <font color="#0000ff">DevenN3'</font>) |
|||
(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 _ _ _). |
|||
</lang> |
|||
{{omit from|PureBasic}} |
{{omit from|PureBasic}} |
Revision as of 19:09, 3 December 2010
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, ...) representable by a computer, and addition on them. Define a type of even numbers (0, 2, 4, 6, ...) within the previously defined range of natural numbers. Prove that the addition of any two even numbers is even, if the result is a member of the type.
Agda
Requires version w.
<lang agda>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) </lang>
Coq
<lang 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. </lang>
Haskell
See Proof/Haskell.
Omega
<lang 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) </lang>
Tcl
Using the datatype
package from the Pattern Matching task...
<lang tcl>package require datatype datatype define Int = Zero | Succ val datatype define EO = Even | Odd
proc evenOdd val {
global environment datatype match $val {
case Zero -> { Even } case [Succ [Succ x]] -> { evenOdd $x } case t -> { set term [list evenOdd $t] if {[info exists environment($term)]} { return $environment($term) } elseif {[info exists environment($t)]} { return [evenOdd $environment($t)] } else { return $term } }
}
}
proc add {a b} {
global environment datatype match $a {
case Zero -> { return $b } case [Succ x] -> { Succ [add $x $b] } case t -> { datatype match $b { case Zero -> { return $t } case [Succ x] -> { Succ [add $t $x] } case t2 -> { set term [list add $t $t2] if {[info exists environment($term)]} { return $environment($term) } elseif {[info exists environment($t)]} { return [add $environment($t) $t2] } elseif {[info exists environment($t2)]} { return [add $t $environment($t2)] } else { return $term } } } }
}
}
puts "BASE CASE" puts "evenOdd Zero = [evenOdd Zero]" puts "evenOdd \[add Zero Zero\] = [evenOdd [add Zero Zero]]"
puts "\nITERATIVE CASE" set environment([list evenOdd p]) Even puts "if evenOdd p = Even..." puts "\tevenOdd \[Succ \[Succ p\]\] = [evenOdd [Succ [Succ p]]]" unset environment puts "if evenOdd \[add p q\] = Even..." set environment([list evenOdd [add p q]]) Even foreach {a b} {
p q {Succ {Succ p}} q p {Succ {Succ q}} {Succ {Succ p}} {Succ {Succ q}}
} {
puts "\tevenOdd \[[list add $a $b]\] = [evenOdd [add $a $b]]"
}</lang> Output:
BASE CASE evenOdd Zero = Even evenOdd [add Zero Zero] = Even ITERATIVE CASE if evenOdd p = Even... evenOdd [Succ [Succ p]] = Even if evenOdd [add p q] = Even... evenOdd [add p q] = Even evenOdd [add {Succ {Succ p}} q] = Even evenOdd [add p {Succ {Succ q}}] = Even evenOdd [add {Succ {Succ p}} {Succ {Succ q}}] = Even
It is up to the caller to take the output of this program and interpret it as a proof.
Twelf
<lang 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 _ _ _). </lang>