Proof
You are encouraged to solve this task according to the task description, using any language you may know.
This task only makes sense for dependently-typed languages and proof assistants, or for languages with a type system strong enough to emulate certain dependent types. It does not ask you to implement a theorem prover yourself.
Task:
- Define a countable set of natural numbers {0, 1, 2, 3, ...}.
- Define an addition on that numbers.
- Define a countable set of even natural numbers {0, 2, 4, 6, ...} within the previously defined set of natural numbers.
- Prove that the addition of any two even numbers is even.
- Prove that the addition is always associative.
ACL2
<lang Lisp>(thm (implies (and (evenp x) (evenp y))
(evenp (+ x y))))</lang>
Agda
<lang agda>module Arith where
-- 1. Natural numbers. -- -- ℕ-formation: ℕ is set. -- -- ℕ-introduction: o ∈ ℕ, -- a ∈ ℕ | (1 + a) ∈ ℕ. -- data ℕ : Set where
o : ℕ 1+ : ℕ → ℕ
-- 2. Addition. -- -- via ℕ-elimination. -- infixl 6 _+_ _+_ : ℕ → ℕ → ℕ o + n = n 1+ m + n = 1+ (m + n)
-- 3. Even natural numbers. -- data 2×ℕ : ℕ → Set where
o : 2×ℕ o
2+ : {n : ℕ} → 2×ℕ n → 2×ℕ (1+ (1+ n))
-- 4. Sum of any two even numbers is even. -- even+even≡even : {m n : ℕ} → 2×ℕ m → 2×ℕ n → 2×ℕ (m + n) even+even≡even o n = n even+even≡even (2+ m) n = 2+ (even+even≡even m n)
-- The identity type for natural numbers. -- infix 4 _≡_ data _≡_ (n : ℕ) : ℕ → Set where
refl : n ≡ n
cong : {m n : ℕ} → m ≡ n → 1+ m ≡ 1+ n cong refl = refl
-- 5.1. Direct proof of the associativity of addition. -- +-associative : (m n p : ℕ) → (m + n) + p ≡ m + (n + p) +-associative o _ _ = refl +-associative (1+ m) n p = cong (+-associative m n p)
-- Proof _of_ mathematical induction on the natural numbers. -- -- P 0, ∀ x. P x → P (1 + x) | ∀ x. P x. -- ind : (P : ℕ → Set) → P o → (∀ n → P n → P (1+ n)) → ∀ n → P n ind P P₀ _ o = P₀ ind P P₀ next (1+ n) = next n (ind P P₀ next n)
-- 5.2. Associativity of addition by induction. -- +-associative′ : (m n p : ℕ) → (m + n) + p ≡ m + (n + p) +-associative′ m n p = ind P P₀ is m
where P : ℕ → Set P i = i + n + p ≡ i + (n + p) P₀ : P o P₀ = refl is : ∀ i → P i → P (1+ i) is i Pi = cong Pi
</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
Using GADTs and type families it is possible to write an adaptation of the Agda version:
<lang haskell>{-# LANGUAGE TypeOperators, TypeFamilies, GADTs #-}
module Arith where
-- 1. Natural numbers.
data Z = Z data S n = S n
-- 2. Addition.
infixl 6 :+ type family x :+ y type instance Z :+ n = n type instance (S m) :+ n = S (m :+ n)
-- 3. Even natural numbers.
data En :: * -> * where
Ez :: En Z Es :: En n -> En (S (S n))
-- 4. Sum of any two even numbers is even.
sum_of_even_is_even :: En m -> En n -> En (m :+ n) sum_of_even_is_even Ez n = n sum_of_even_is_even (Es m) n = Es $ sum_of_even_is_even m n
-- The identity type for natural numbers.
infix 4 := data (:=) n :: * -> * where
Refl :: n := n
cong :: m := n -> S m := S n cong Refl = Refl
-- 5. Associativity of addition (via propositional equality).
class AssocAdd m where
proof :: m -> n -> p -> (m :+ n) :+ p := m :+ (n :+ p)
instance AssocAdd Z where
proof Z _ _ = Refl
instance AssocAdd m => AssocAdd (S m) where
proof (S m) n p = cong (proof m n p)
</lang>
See also Proof/Haskell for implementation of a small theorem prover.
J
Given:
<lang j>isEven=: 0 = 2&| isOdd =: 1 = 2&|</lang>
We can easily see that the sum of two even numbers is even:
<lang j> isEven +/~ 2*i.9 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1</lang>
And by induction we can believe that this property holds for all even numbers.
See also: http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf
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>
Salmon
Note that the only current implementation of Salmon is an interpreter that ignores proofs and doesn't try to check them, but in the future when there is an implementation that checks proofs, it should be able to check the proof in this Salmon code.
<lang Salmon>pure function even(x) returns boolean ((x in [0...+oo)) && ((x % 2) == 0)); theorem(forall(x : even, y : even) ((x + y) in even)) proof
{
forall (x : even, y : even)
{
L1:
x in even;
L2:
((x in [0...+oo)) && ((x % 2) == 0)) because type_definition(L1);
L3:
((x % 2) == 0) because simplification(L2);
L4:
y in even;
L5:
((y in [0...+oo)) && ((y % 2) == 0)) because type_definition(L4);
L6:
((y % 2) == 0) because simplification(L5);
L7:
(((x + y) % 2) == (x % 2) + (y % 2)); // axiom of % and +
L8:
(((x + y) % 2) == 0 + (y % 2)) because substitution(L3, L7);
L9:
(((x + y) % 2) == 0 + 0) because substitution(L6, L8);
L10:
(((x + y) % 2) == 0) because simplification(L9);
(x + y) in even because type_definition(even, L10);
};
};</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>