Proof: Difference between revisions
Content added Content deleted
(Initial upload.) |
(Added Agda2 example) |
||
Line 44: | Line 44: | ||
<font color="#00008b">assumption</font>. |
<font color="#00008b">assumption</font>. |
||
<font color="#a020f0">Qed</font>. |
<font color="#a020f0">Qed</font>. |
||
=={{header|Agda2}}== |
|||
<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> |
Revision as of 20:54, 21 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
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)