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