Proof
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.
You are encouraged to solve this task according to the task description, using any language you may know.
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>
Go
Relevant WP article Peano axioms. <lang go>package main
import "fmt"
// dependent types, as suggested on the talk page, only exist in Go when // one interface is a proper subset of another. type number interface {
successor() number hasSuccessor() (number, bool) add(number) number
}
type even interface {
number // this includes number methods as a proper subset of even methods. evenSuccessor() even hasEvenSuccessor() (even, bool) addEven(even) even normalize() number
}
// underlying types, implementations of interfaces. type peanoNumber struct {
pred *peanoNumber
}
type evenPeano struct {
pn *peanoNumber prpr *evenPeano
}
var ns = make(map[*peanoNumber]*peanoNumber) // see axiom 8, below var es = make(map[*evenPeano]*evenPeano)
// definition: zero is even var e0 = &evenPeano{&peanoNumber{}, nil}
// peano axiom 1: zero is a number var zero number = e0.pn // see axiom 5, below.
// peano axioms 2-4, relexive, symetric, and transitive properties, // let's say, are implemented by the compiler's == operator, // based on the following phrase from the language reference, // // "Pointer values are equal if they point to the same location or if // both are nil." // // and based on the common meaning of the word "same" and trust that // new() never returns a value the same as an existing referenced pointer.
// axiom 5, closure, relies also on the language reference phrase, // // "the first operand must be assignable to the type of // the second operand, or vice versa." // // and also the section on assignability. That section describes several // cases of assignability, the only one applicable for type number being, // // "[x is assignable to T when] x's type is identical to T. // // Note that to reduce assignability and therefore closure, to type identity, // nil must be excluded from the set of valid "numbers."
// axiom 6: every number has a successor // axiom 8: s(n) == s(m) where n == m func (n *peanoNumber) successor() number {
s := ns[n] if s == nil { s = &peanoNumber{n} ns[n] = s } return s
}
// axiom 7: zero is the not the successor of any number. func (s *peanoNumber) hasSuccessor() (n number, ok bool) {
if number(s) == zero { return nil, false } return s.pred, true
}
// second order function: addition, defined over the set of numbers. func (a *peanoNumber) add(b number) number {
p, ok := b.hasSuccessor() if !ok { return a } return a.successor().add(p)
}
// evenPeano implementation of number methods func (n *evenPeano) successor() number {
return n.pn.successor()
}
func (s *evenPeano) hasSuccessor() (n number, ok bool) {
return s.pn.hasSuccessor()
}
func (a *evenPeano) add(b number) number {
return a.pn.add(b)
}
// evenSuccessor, combined with the definition of e0 as even, // represent the definition of "even numbers" func (n *evenPeano) evenSuccessor() even {
s := es[n] if s == nil { s = &evenPeano{n.pn.successor().successor().(*peanoNumber), n} es[n] = s } return s
}
// corellary of axiom 7 func (s *evenPeano) hasEvenSuccessor() (even, bool) {
if s.normalize() == zero { return nil, false } return s.prpr, true
}
// same addition definition, just partitioned by second successor. // note no type conversions, no type assertions, no tests except the // null case terminating recursion. This compiles completes the proof. func (a *evenPeano) addEven(b even) even {
p, ok := b.hasEvenSuccessor() if !ok { return a } return a.evenSuccessor().addEven(p)
}
// kind of quirky: evenPeanos have their cannonical peanoNumber as a field, // so an interface on one compares != to an interface on the other, even // though they represent the same number. normalize returns the field so // that conversion to an interface will compare ==. func (n *evenPeano) normalize() number {
return n.pn
}
// arithmetic demonstration, just for fun func main() {
// e0 is zero fmt.Println(e0.normalize() == zero)
// two = 2 two := e0.evenSuccessor() fmt.Println(two.normalize() == zero.successor().successor())
// two + two = 1 + 3 fmt.Println(two.addEven(two).normalize() == zero.successor().add(zero.successor().successor().successor()))
}</lang> Output:
true true true
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>