609 lines
22 KiB
Text
609 lines
22 KiB
Text
-- {{{ Logic/general definitions
|
||
|
||
-- import basic logic definitions from <logic.pg>
|
||
|
||
@include logic.pg
|
||
|
||
-- }}}
|
||
|
||
-- {{{ Axioms
|
||
|
||
-- Now we can define the Peano axioms. Unlike with equality, perga is not
|
||
-- powerful enough to construct the natural numbers (or at least to prove the
|
||
-- Peano axioms as theorems from a definition constructible in perga). However,
|
||
-- working with axioms is extremely common in math. As such, perga has a system
|
||
-- for doing just that, namely the ★axiom★ system.
|
||
--
|
||
-- In a definition, rather than give a value for the term, we can give it the
|
||
-- value axiom, in which case a type ascription is mandatory. Perga will then
|
||
-- trust our type ascription, and assume going forward that the identifier we
|
||
-- defined is a value of the asserted type. For example, we will use the axiom
|
||
-- system to assert the existence of a type of natural numbers
|
||
|
||
axiom nat : ★;
|
||
|
||
-- As you can imagine, this can be risky. For instance, there's nothing stopping
|
||
-- us from saying
|
||
-- uh_oh : false := axiom;
|
||
-- or stipulating more subtly contradictory axioms. As such, as in mathematics,
|
||
-- axioms should be used with care.
|
||
--
|
||
-- There's another problem with axioms, namely that perga cannot do any
|
||
-- computations with axioms. The more you can define within perga natively, the
|
||
-- better, as computations done without axioms can be utilized by perga. For
|
||
-- example, in <computation.pg>, we define the natural numbers as Church
|
||
-- numerals entirely within perga. There, the proof that 1 + 1 = 2 is just
|
||
-- eq_refl, since they reduce to the same thing. Here, 1 + 1 = 2 will
|
||
-- require a proof, since perga is unable to do computations with things defined
|
||
-- as axioms.
|
||
--
|
||
-- With these warnings in place, the Peano axioms are proven to be consistent,
|
||
-- so we should be fine. I'm formalizing the second order axioms given in the
|
||
-- wikipedia article on the Peano axioms
|
||
-- (https://en.wikipedia.org/wiki/Peano_axioms).
|
||
|
||
-- axiom 1: 0 is a natural number
|
||
axiom zero : nat;
|
||
|
||
-- axiom 6: For every n, S n is a natural number.
|
||
axiom suc (n : nat) : nat;
|
||
|
||
-- axiom 7: If S n = S m, then n = m.
|
||
axiom suc_inj : forall (n m : nat), eq nat (suc n) (suc m) → eq nat n m;
|
||
|
||
-- axiom 8: No successor of any natural number is zero.
|
||
axiom suc_nonzero : forall (n : nat), not (eq nat (suc n) zero);
|
||
|
||
-- axiom 9: Induction! For any proposition P on natural numbers, if P(0) holds,
|
||
-- and if for every natural number n, P(n) ⇒ P(S n), then P holds for all n.
|
||
axiom nat_ind : forall (P : nat → ★), P zero → (forall (n : nat), P n → P (suc n))
|
||
→ forall (n : nat), P n;
|
||
|
||
-- }}}
|
||
|
||
-- {{{ Basic Definitions
|
||
|
||
-- Now that we have stipulated these axioms, we are free to use them to make
|
||
-- definitions, prove theorems, etc.
|
||
--
|
||
-- Our first theorem, as a warm up, is to prove that every natural number is
|
||
-- either 0 or the successor of another natural number.
|
||
--
|
||
-- First, we will make a bunch of abbreviations, since these terms get really
|
||
-- long and complicated really quickly.
|
||
|
||
-- Some abbreviations for common numbers.
|
||
def one : nat := suc zero;
|
||
def two : nat := suc one;
|
||
def three : nat := suc two;
|
||
def four : nat := suc three;
|
||
def five : nat := suc four;
|
||
|
||
-- A nice infix abbreviation for equality on natural numbers
|
||
def = (n m : nat) := eq nat n m;
|
||
infixl 11 =;
|
||
|
||
-- First, the predecessor of n is m if n = suc m.
|
||
def pred (n m : nat) : ★ := n = suc m;
|
||
|
||
-- Our claim is a disjunction, whose first option is that n = 0.
|
||
def szc_l (n : nat) := n = zero;
|
||
|
||
-- The second option is that n has a predecessor.
|
||
def szc_r (n : nat) := exists nat (pred n);
|
||
|
||
-- So the claim we are trying to prove is that either one of the above options
|
||
-- holds for every n.
|
||
def szc (n : nat) := szc_l n ∨ szc_r n;
|
||
|
||
-- And here's our proof!
|
||
def suc_or_zero : forall (n : nat), szc n :=
|
||
-- We will prove this by induction.
|
||
nat_ind szc
|
||
-- For the base case, the first option holds, i.e. 0 = 0
|
||
(or_intro_l (szc_l zero) (szc_r zero) (eq_refl nat zero))
|
||
|
||
-- For the inductive case, suppose the theorem holds for n.
|
||
(fun (n : nat) (_ : szc n) =>
|
||
-- Then the right option holds for suc n, since suc n is the
|
||
-- successor of n
|
||
or_intro_r (szc_l (suc n)) (szc_r (suc n))
|
||
(exists_intro nat (pred (suc n)) n (eq_refl nat (suc n))));
|
||
|
||
-- }}}
|
||
|
||
-- {{{ Recursive Definitions
|
||
|
||
-- The next step would normally be to define addition and prove properties of
|
||
-- addition. However, we need to take a very long and difficult detour in order
|
||
-- to be able to define addition in the first place. The normal way addition is
|
||
-- defined is by the following two equations:
|
||
--
|
||
-- 1) n + 0 = n
|
||
-- 2) n + (suc m) = suc (n + m)
|
||
--
|
||
-- It is clear that this definition is ok, since m gets smaller with every
|
||
-- application of equation 2, until m reaches zero, whereupon we can use
|
||
-- equation 1. This argument, while perfectly reasonable, is deceptively
|
||
-- difficult to formalize. It turns out that this structure of recursively
|
||
-- defining a function by two equations similar to 1 and 2 is extremely common.
|
||
-- So, we will take the time to prove the following theorem.
|
||
--
|
||
-- Theorem (recursive definitions):
|
||
-- For every type A, element z : A, and function fS : nat → A → A, there
|
||
-- exists a unique function f : nat → A satisfying
|
||
-- 1) f 0 = z
|
||
-- 2) forall n : nat, f (suc n) = fS n (f n)
|
||
--
|
||
-- Once we've proved this theorem, we can easily define addition such that,
|
||
-- i.e. that for any fixed n : nat, "n+" is the unique function satisfying
|
||
-- 1) n + 0 = n
|
||
-- 2) forall m : nat, n + (suc m) = suc (n + m)
|
||
-- Notice that this is the exact form we need in order to apply the theorem.
|
||
--
|
||
-- However, proving this theorem is *extremely long and difficult*. I would
|
||
-- recommend skipping this section and coming back to it after you are much
|
||
-- more used to perga. As such, I will go into a lot less detail on each of
|
||
-- these proofs than in the later sections.
|
||
--
|
||
-- Here's our game plan. We will define a relation R : nat → A → ★ such that
|
||
-- R x y iff for every relation Q : nat → A → ★ satisfying
|
||
-- 1) Q 0 z and
|
||
-- 2) forall (x : nat) (y : A), Q x y → Q (suc x) (fS x y),
|
||
-- Q x y.
|
||
-- In more mathy lingo, we take R to be the intersection of every relation
|
||
-- satisfying 1 and 2. From there we will, with much effort, prove that R is
|
||
-- actually a function satisfying the equations we want it to.
|
||
|
||
section RecursiveDefs
|
||
|
||
-- First, fix an A, z : A, and fS : nat → A → A
|
||
variable (A : ★) (z : A) (fS : nat → A → A);
|
||
|
||
-- {{{ Defining R
|
||
-- Here is condition 1 formally expressed in perga.
|
||
def cond1 (Q : nat → A → ★) := Q zero z;
|
||
|
||
-- Likewise for condition 2.
|
||
def cond2 (Q : nat → A → ★) :=
|
||
forall (n : nat) (y : A), Q n y → Q (suc n) (fS n y);
|
||
|
||
-- From here we can define R.
|
||
def rec_rel (x : nat) (y : A) :=
|
||
forall (Q : nat → A → ★), cond1 Q → cond2 Q → Q x y;
|
||
-- }}}
|
||
|
||
-- {{{ R is total
|
||
def total (A B : ★) (R : A → B → ★) := forall (a : A), exists B (R a);
|
||
|
||
def rec_rel_cond1 : cond1 rec_rel :=
|
||
fun (Q : nat → A → ★) (h1 : cond1 Q) (h2 : cond2 Q) => h1;
|
||
|
||
def rec_rel_cond2 : cond2 rec_rel :=
|
||
fun (n : nat) (y : A) (h : rec_rel n y)
|
||
(Q : nat → A → ★) (h1 : cond1 Q) (h2 : cond2 Q) =>
|
||
h2 n y (h Q h1 h2);
|
||
|
||
def rec_rel_total : total nat A rec_rel :=
|
||
let (P (x : nat) := exists A (rec_rel x)) in
|
||
nat_ind P
|
||
(exists_intro A (rec_rel zero) z rec_rel_cond1)
|
||
(fun (n : nat) (IH : P n) =>
|
||
exists_elim A (P (suc n)) (rec_rel n) IH
|
||
(fun (y0 : A) (hy : rec_rel n y0) =>
|
||
exists_intro A (rec_rel (suc n)) (fS n y0) (rec_rel_cond2 n y0 hy)))
|
||
end;
|
||
|
||
-- }}}
|
||
|
||
-- {{{ Defining R2
|
||
def alt_cond1 (x : nat) (y : A) :=
|
||
x = zero ∧ eq A y z;
|
||
|
||
def cond_y2 (x : nat) (y : A)
|
||
(x2 : nat) (y2 : A) :=
|
||
(eq A y (fS x2 y2)) ∧ (rec_rel x2 y2);
|
||
|
||
def cond_x2 (x : nat) (y : A) (x2 : nat) :=
|
||
pred x x2 ∧ exists A (cond_y2 x y x2);
|
||
|
||
def alt_cond2 (x : nat) (y : A) := exists nat (cond_x2 x y);
|
||
|
||
def rec_rel_alt (x : nat) (y : A) := alt_cond1 x y ∨ alt_cond2 x y;
|
||
-- }}}
|
||
|
||
-- {{{ R = R2
|
||
|
||
-- {{{ R2 ⊆ R
|
||
def R2_sub_R_case1 (x : nat) (y : A) : alt_cond1 x y → rec_rel x y :=
|
||
fun (case1 : alt_cond1 x y) =>
|
||
let (x0 := and_elim_l (x = zero) (eq A y z) case1)
|
||
(yz := and_elim_r (x = zero) (eq A y z) case1)
|
||
(a1 := (eq_sym A y z yz) (rec_rel zero) rec_rel_cond1)
|
||
in
|
||
(eq_sym nat x zero x0) (fun (n : nat) => rec_rel n y) a1
|
||
end;
|
||
|
||
def R2_sub_R_case2 (x : nat) (y : A) : alt_cond2 x y → rec_rel x y :=
|
||
fun (case2 : alt_cond2 x y) =>
|
||
let (h1 := cond_x2 x y)
|
||
(h2 := cond_y2 x y)
|
||
in
|
||
exists_elim nat (rec_rel x y) h1 case2
|
||
(fun (x2 : nat) (hx2 : h1 x2) =>
|
||
let (hpred := and_elim_l (pred x x2) (exists A (h2 x2)) hx2)
|
||
(hex := and_elim_r (pred x x2) (exists A (h2 x2)) hx2)
|
||
in
|
||
exists_elim A (rec_rel x y) (h2 x2) hex
|
||
(fun (y2 : A) (hy2 : h2 x2 y2) =>
|
||
let (hpreim := and_elim_l (eq A y (fS x2 y2)) (rec_rel x2 y2) hy2)
|
||
(hR := and_elim_r (eq A y (fS x2 y2)) (rec_rel x2 y2) hy2)
|
||
(a1 := rec_rel_cond2 x2 y2 hR)
|
||
(a2 := (eq_sym A y (fS x2 y2) hpreim) (rec_rel (suc x2)) a1)
|
||
in
|
||
(eq_sym nat x (suc x2) hpred) (fun (n : nat) => rec_rel n y) a2
|
||
end)
|
||
end)
|
||
end;
|
||
|
||
def R2_sub_R (x : nat) (y : A) : rec_rel_alt x y → rec_rel x y :=
|
||
fun (h : rec_rel_alt x y) =>
|
||
or_elim (alt_cond1 x y) (alt_cond2 x y) (rec_rel x y) h
|
||
(R2_sub_R_case1 x y)
|
||
(R2_sub_R_case2 x y);
|
||
-- }}}
|
||
|
||
-- {{{ R ⊆ R2
|
||
def R2_cond1 : cond1 rec_rel_alt :=
|
||
or_intro_l (alt_cond1 zero z) (alt_cond2 zero z)
|
||
(and_intro (zero = zero) (eq A z z)
|
||
(eq_refl nat zero)
|
||
(eq_refl A z));
|
||
|
||
def R2_cond2 : cond2 rec_rel_alt :=
|
||
fun (x2 : nat) (y2 : A) (h : rec_rel_alt x2 y2) =>
|
||
let (x := suc x2)
|
||
(y := fS x2 y2)
|
||
(cx2 := cond_x2 x y)
|
||
(cy2 := cond_y2 x y x2)
|
||
in
|
||
or_intro_r (alt_cond1 x y) (alt_cond2 x y)
|
||
(exists_intro nat cx2 x2
|
||
(and_intro (pred x x2) (exists A cy2)
|
||
(eq_refl nat x)
|
||
(exists_intro A cy2 y2
|
||
(and_intro (eq A y y) (rec_rel x2 y2)
|
||
(eq_refl A y)
|
||
(R2_sub_R x2 y2 h)))))
|
||
end;
|
||
|
||
|
||
def R_sub_R2 (x : nat) (y : A) : rec_rel x y → rec_rel_alt x y :=
|
||
fun (h : rec_rel x y) => h rec_rel_alt R2_cond1 R2_cond2;
|
||
-- }}}
|
||
|
||
-- }}}
|
||
|
||
-- {{{ R2 (hence R) is functional
|
||
|
||
def fl_in (A B : ★) (R : A → B → ★) (x : A) := forall (y1 y2 : B),
|
||
R x y1 → R x y2 → eq B y1 y2;
|
||
|
||
def fl (A B : ★) (R : A → B → ★) := forall (x : A), fl_in A B R x;
|
||
|
||
def R2_zero (y : A) : rec_rel_alt zero y → eq A y z :=
|
||
let (cx2 := cond_x2 zero y)
|
||
(cy2 := cond_y2 zero y)
|
||
in fun (h : rec_rel_alt zero y) =>
|
||
or_elim (alt_cond1 zero y) (alt_cond2 zero y) (eq A y z) h
|
||
(fun (case1 : alt_cond1 zero y) => and_elim_r (zero = zero) (eq A y z) case1)
|
||
(fun (case2 : alt_cond2 zero y) =>
|
||
exists_elim nat (eq A y z) cx2 case2
|
||
(fun (x2 : nat) (h2 : cx2 x2) =>
|
||
suc_nonzero x2
|
||
(eq_sym nat zero (suc x2) (and_elim_l (pred zero x2) (exists A (cy2 x2)) h2))
|
||
(eq A y z)))
|
||
end;
|
||
|
||
def R2_suc (x2 : nat) (y : A) : rec_rel_alt (suc x2) y → exists A (cond_y2 (suc x2) y x2) :=
|
||
let (x := suc x2)
|
||
(cx2 := cond_x2 x y)
|
||
(cy2 := cond_y2 x y)
|
||
(goal := exists A (cy2 x2))
|
||
in
|
||
fun (h : rec_rel_alt x y) =>
|
||
or_elim (alt_cond1 x y) (alt_cond2 x y) goal h
|
||
(fun (case1 : alt_cond1 x y) => suc_nonzero x2 (and_elim_l (x = zero) (eq A y z) case1) goal)
|
||
(fun (case2 : alt_cond2 x y) =>
|
||
exists_elim nat goal cx2 case2
|
||
(fun (x22 : nat) (hx22 : cx2 x22) =>
|
||
let (hpred := and_elim_l (pred x x22) (exists A (cy2 x22)) hx22)
|
||
(hgoal := and_elim_r (pred x x22) (exists A (cy2 x22)) hx22)
|
||
(x2_x22 := suc_inj x2 x22 hpred)
|
||
in
|
||
(eq_sym nat x2 x22 x2_x22)
|
||
(fun (n : nat) => exists A (cy2 n))
|
||
hgoal
|
||
end))
|
||
end;
|
||
|
||
def R2_functional_base_case : fl_in nat A rec_rel_alt zero :=
|
||
fun (y1 y2 : A) (h1 : rec_rel_alt zero y1) (h2 : rec_rel_alt zero y2) =>
|
||
eq_trans A y1 z y2
|
||
(R2_zero y1 h1)
|
||
(eq_sym A y2 z (R2_zero y2 h2));
|
||
|
||
def R2_functional_inductive_step (x2 : nat) (IH : fl_in nat A rec_rel_alt x2) : fl_in nat A rec_rel_alt (suc x2) :=
|
||
fun (y1 y2 : A) (h1 : rec_rel_alt (suc x2) y1) (h2 : rec_rel_alt (suc x2) y2) =>
|
||
let (x := suc x2)
|
||
(cy1 := cond_y2 x y1 x2)
|
||
(cy2 := cond_y2 x y2 x2)
|
||
(goal := eq A y1 y2)
|
||
in
|
||
exists_elim A goal cy1 (R2_suc x2 y1 h1)
|
||
(fun (y12 : A) (h12 : cy1 y12) =>
|
||
exists_elim A goal cy2 (R2_suc x2 y2 h2)
|
||
(fun (y22 : A) (h22 : cy2 y22) =>
|
||
let (y1_preim := and_elim_l (eq A y1 (fS x2 y12)) (rec_rel x2 y12) h12)
|
||
(y2_preim := and_elim_l (eq A y2 (fS x2 y22)) (rec_rel x2 y22) h22)
|
||
(R_x2_y12 := and_elim_r (eq A y1 (fS x2 y12)) (rec_rel x2 y12) h12)
|
||
(R_x2_y22 := and_elim_r (eq A y2 (fS x2 y22)) (rec_rel x2 y22) h22)
|
||
(R2_x2_y12 := R_sub_R2 x2 y12 R_x2_y12)
|
||
(R2_x2_y22 := R_sub_R2 x2 y22 R_x2_y22)
|
||
(y12_y22 := IH y12 y22 R2_x2_y12 R2_x2_y22)
|
||
in
|
||
eq_trans A y1 (fS x2 y12) y2
|
||
y1_preim
|
||
(eq_trans A (fS x2 y12) (fS x2 y22) y2
|
||
(eq_cong A A y12 y22 (fun (y : A) => fS x2 y) y12_y22)
|
||
(eq_sym A y2 (fS x2 y22) y2_preim))
|
||
end))
|
||
end;
|
||
|
||
def R2_functional : fl nat A rec_rel_alt :=
|
||
nat_ind (fl_in nat A rec_rel_alt) R2_functional_base_case R2_functional_inductive_step;
|
||
|
||
def R_functional : fl nat A rec_rel :=
|
||
fun (n : nat) (y1 y2 : A) (h1 : rec_rel n y1) (h2 : rec_rel n y2) =>
|
||
R2_functional n y1 y2 (R_sub_R2 n y1 h1) (R_sub_R2 n y2 h2);
|
||
|
||
-- }}}
|
||
|
||
-- {{{ Actually defining the function
|
||
|
||
def rec_def (x : nat) : A :=
|
||
exists_elim A A (rec_rel x) (rec_rel_total x) (fun (y : A) (_ : rec_rel x y) => y);
|
||
|
||
-- }}}
|
||
|
||
-- {{{ It satisfies the properties we want it to
|
||
|
||
-- Kind of stupidly, we still need one more axiom. Due to how existentials are
|
||
-- defined, even though rec_def n is defined to be the y such that R n y, we
|
||
-- can't actually conclude that R n (rec_def n).
|
||
|
||
-- We need to assert that, even if you "forget" that a value came from an
|
||
-- existential, it still satisfies the property it definitionally is supposed
|
||
-- to satisfy. This annoying problem would be subverted with proper Σ-types,
|
||
-- provided they had η-equality.
|
||
axiom definite_description (A : ★) (P : A → ★) (h : exists A P) :
|
||
P (exists_elim A A P h (fun (x : A) (_ : P x) => x));
|
||
|
||
-- Now we can use this axiom to prove that R n (rec_def n).
|
||
def rec_def_sat (x : nat) : rec_rel x (rec_def x) :=
|
||
definite_description A (rec_rel x) (rec_rel_total x);
|
||
|
||
def eq1 (f : nat → A) := eq A (f zero) z;
|
||
|
||
def eq2 (f : nat → A) := forall (n : nat), eq A (f (suc n)) (fS n (f n));
|
||
|
||
-- f zero = z
|
||
def rec_def_sat_zero : eq1 rec_def := R_functional zero (rec_def zero) z (rec_def_sat zero) rec_rel_cond1;
|
||
|
||
-- f n = y → f (suc n) = fS n y
|
||
def rec_def_sat_suc : eq2 rec_def := fun (n : nat) =>
|
||
R_functional (suc n) (rec_def (suc n)) (fS n (rec_def n)) (rec_def_sat (suc n)) (rec_rel_cond2 n (rec_def n) (rec_def_sat n));
|
||
|
||
-- }}}
|
||
|
||
-- {{{ The function satisfying these equations is unique
|
||
|
||
def rec_def_unique (f g : nat → A) (h1f : eq1 f) (h2f : eq2 f) (h1g : eq1 g) (h2g : eq2 g)
|
||
: forall (n : nat), eq A (f n) (g n) :=
|
||
nat_ind (fun (n : nat) => eq A (f n) (g n))
|
||
-- base case: f 0 = g 0
|
||
(eq_trans A (f zero) z (g zero) h1f (eq_sym A (g zero) z h1g))
|
||
|
||
-- Inductive step
|
||
(fun (n : nat) (IH : eq A (f n) (g n)) =>
|
||
-- f (suc n) = fS n (f n)
|
||
-- = fS n (g n)
|
||
-- = g (suc n)
|
||
eq_trans A (f (suc n)) (fS n (f n)) (g (suc n))
|
||
-- f (suc n) = fS n (f n)
|
||
(h2f n)
|
||
-- fS n (f n) = g (suc n)
|
||
(eq_trans A (fS n (f n)) (fS n (g n)) (g (suc n))
|
||
-- fS n (f n) = fS n (g n)
|
||
(eq_cong A A (f n) (g n) (fS n) IH)
|
||
-- fS n (g n) = g (suc n)
|
||
(eq_sym A (g (suc n)) (fS n (g n)) (h2g n))));
|
||
|
||
-- }}}
|
||
|
||
end RecursiveDefs
|
||
|
||
-- }}}
|
||
|
||
-- Now we can safely define addition.
|
||
|
||
-- First, here's the RHS of equation 2 as a function, since it will show up
|
||
-- multiple times.
|
||
def psuc (_ r : nat) := suc r;
|
||
|
||
-- And here's plus!
|
||
def plus (n : nat) : nat → nat := rec_def nat n psuc;
|
||
|
||
-- And here's an infix version of it
|
||
def + (n m : nat) : nat := plus n m;
|
||
infixl 20 +;
|
||
|
||
-- The first equation manifests itself as the familiar
|
||
-- n + 0 = 0.
|
||
def plus_0_r (n : nat) : n + zero = n :=
|
||
rec_def_sat_zero nat n psuc;
|
||
|
||
-- The second equation, after a bit of massaging, manifests itself as the
|
||
-- likewise familiar
|
||
-- n + suc m = suc (n + m).
|
||
def plus_s_r (n m : nat) : n + suc m = suc (n + m) :=
|
||
rec_def_sat_suc nat n psuc m;
|
||
|
||
-- -- We can now prove 1 + 1 = 2!
|
||
def one_plus_one_two : one + one = two :=
|
||
-- 1 + (suc zero) = suc (1 + zero) = suc one
|
||
eq_trans nat (one + one) (suc (one + zero)) two
|
||
|
||
-- 1 + (suc zero) = suc (1 + zero)
|
||
(plus_s_r one zero)
|
||
|
||
-- suc (1 + zero) = suc one
|
||
(eq_cong nat nat (one + zero) one suc (plus_0_r one));
|
||
|
||
-- We have successfully defined addition! Note that evaluating 1 + 1 to 2
|
||
-- requires a proof, unfortunately, since this computation isn't visible to
|
||
-- perga.
|
||
--
|
||
-- We will now prove a couple standard properties of addition.
|
||
|
||
-- First, associativity, namely that n + (m + p) = (n + m) + p.
|
||
def plus_assoc : forall (n m p : nat), n + (m + p) = n + m + p
|
||
:= [n m : nat]
|
||
-- We prove this via induction on p for any fixed n and m.
|
||
nat_ind
|
||
(fun (p : nat) => n + (m + p) = n + m + p)
|
||
|
||
-- Base case: p = 0
|
||
-- WTS n + (m + 0) = (n + m) + 0
|
||
-- n + (m + 0) = n + m = (n + m) + 0
|
||
(eq_trans nat (n + (m + zero)) (n + m) (n + m + zero)
|
||
-- n + (m + 0) = n + m
|
||
(eq_cong nat nat (m + zero) m (fun (p : nat) => n + p) (plus_0_r m))
|
||
|
||
-- n + m = (n + m) + 0
|
||
(eq_sym nat (n + m + zero) (n + m) (plus_0_r (n + m))))
|
||
|
||
-- Inductive step: IH = n + (m + p) = (n + m) + p
|
||
(fun (p : nat) (IH : n + (m + p) = n + m + p) =>
|
||
-- WTS n + (m + suc p) = (n + m) + suc p
|
||
-- n + (m + suc p) = n + suc (m + p)
|
||
-- = suc (n + (m + p))
|
||
-- = suc ((n + m) + p)
|
||
-- = (n + m) + suc p
|
||
eq_trans nat (n + (m + suc p)) (n + (suc (m + p))) (n + m + suc p)
|
||
|
||
-- n + (m + suc p) = n + suc (m + p)
|
||
(eq_cong nat nat (m + suc p) (suc (m + p)) (fun (a : nat) => (n + a)) (plus_s_r m p))
|
||
|
||
-- n + suc (m + p) = (n + m) + suc p
|
||
(eq_trans nat (n + suc (m + p)) (suc (n + (m + p))) (n + m + suc p)
|
||
-- n + suc (m + p) = suc (n + (m + p))
|
||
(plus_s_r n (m + p))
|
||
|
||
-- suc (n + (m + p)) = (n + m) + suc p
|
||
(eq_trans nat (suc (n + (m + p))) (suc (n + m + p)) (n + m + suc p)
|
||
-- suc (n + (m + p)) = suc ((n + m) + p)
|
||
(eq_cong nat nat (n + (m + p)) (n + m + p) suc IH)
|
||
|
||
-- suc ((n + m) + p) = (n + m) + suc p
|
||
(eq_sym nat (n + m + suc p) (suc (n + m + p))
|
||
(plus_s_r (n + m) p)))));
|
||
|
||
-- Up next is commutativity, but we will need a couple lemmas first.
|
||
|
||
-- First, we will show that 0 + n = n.
|
||
def plus_0_l : forall (n : nat), zero + n = n :=
|
||
-- We prove this by induction on n.
|
||
nat_ind ([n : nat] zero + n = n)
|
||
-- base case: WTS 0 + 0 = 0
|
||
-- This is just plus_0_r 0
|
||
(plus_0_r zero)
|
||
|
||
-- inductive case
|
||
(fun (n : nat) (IH : zero + n = n) =>
|
||
-- WTS 0 + (suc n) = suc n
|
||
-- 0 + suc n = suc (0 + n) = suc n
|
||
eq_trans nat (zero + suc n) (suc (zero + n)) (suc n)
|
||
-- 0 + suc n = suc (0 + n)
|
||
(plus_s_r zero n)
|
||
|
||
-- suc (0 + n) = suc n
|
||
(eq_cong nat nat (zero + n) n suc IH));
|
||
|
||
-- Next, we will show that (suc n) + m = suc (n + m).
|
||
def plus_s_l (n : nat) : forall (m : nat), suc n + m = suc (n + m) :=
|
||
-- We proceed by induction on m.
|
||
nat_ind ([m : nat] suc n + m = suc (n + m))
|
||
-- base case: (suc n) + 0 = suc (n + 0)
|
||
-- suc n + 0 = suc n = suc (n + 0)
|
||
(eq_trans nat (suc n + zero) (suc n) (suc (n + zero))
|
||
-- suc n + 0 = suc n
|
||
(plus_0_r (suc n))
|
||
|
||
-- suc n = suc (n + 0)
|
||
(eq_cong nat nat n (n + zero) suc
|
||
-- n = n + 0
|
||
(eq_sym nat (n + zero) n (plus_0_r n))))
|
||
|
||
-- inductive case
|
||
-- IH = suc n + m = suc (n + m)
|
||
(fun (m : nat) (IH : suc n + m = suc (n + m)) =>
|
||
-- WTS suc n + suc m = suc (n + suc m)
|
||
-- suc n + suc m = suc (suc n + m)
|
||
-- = suc (suc (n + m))
|
||
-- = suc (n + suc m)
|
||
(eq_trans nat (suc n + suc m) (suc (suc n + m)) (suc (n + suc m))
|
||
-- suc n + suc m = suc (suc n + m)
|
||
(plus_s_r (suc n) m)
|
||
|
||
-- suc (suc n + m) = suc (n + suc m)
|
||
(eq_trans nat (suc (suc n + m)) (suc (suc (n + m))) (suc (n + suc m))
|
||
-- suc (suc n + m) = suc (suc (n + m))
|
||
(eq_cong nat nat (suc n + m) (suc (n + m)) suc IH)
|
||
|
||
-- suc (suc (n + m)) = suc (n + suc m)
|
||
(eq_cong nat nat (suc (n + m)) (n + suc m) suc
|
||
-- suc (n + m) = n + suc m
|
||
(eq_sym nat (n + suc m) (suc (n + m)) (plus_s_r n m))))));
|
||
|
||
-- Finally, we can prove commutativity.
|
||
def plus_comm (n : nat) : forall (m : nat), n + m = m + n :=
|
||
-- As usual, we proceed by induction.
|
||
nat_ind ([m : nat] n + m = m + n)
|
||
|
||
-- Base case: WTS n + 0 = 0 + n
|
||
-- n + 0 = n = 0 + n
|
||
(eq_trans nat (n + zero) n (zero + n)
|
||
-- n + 0 = n
|
||
(plus_0_r n)
|
||
|
||
-- n = 0 + n
|
||
(eq_sym nat (zero + n) n (plus_0_l n)))
|
||
|
||
-- Inductive step:
|
||
(fun (m : nat) (IH : n + m = m + n) =>
|
||
-- WTS n + suc m = suc m + n
|
||
-- n + suc m = suc (n + m)
|
||
-- = suc (m + n)
|
||
-- = suc m + n
|
||
(eq_trans nat (n + suc m) (suc (n + m)) (suc m + n)
|
||
-- n + suc m = suc (n + m)
|
||
(plus_s_r n m)
|
||
|
||
-- suc (n + m) = suc m + n
|
||
(eq_trans nat (suc (n + m)) (suc (m + n)) (suc m + n)
|
||
-- suc (n + m) = suc (m + n)
|
||
(eq_cong nat nat (n + m) (m + n) suc IH)
|
||
|
||
-- suc (m + n) = suc m + n
|
||
(eq_sym nat (suc m + n) (suc (m + n)) (plus_s_l m n)))));
|