Proof
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.
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)
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)
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
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 _ _ _).