394 lines
15 KiB
Text
394 lines
15 KiB
Text
--
|
|
-- We need some basic logic, so I'm stealing this from <logic.pg>. See that file
|
|
-- for more details on how these work.
|
|
--
|
|
|
|
false : * := forall (A : *), A;
|
|
false_elim (A : *) (contra : false) : A := contra A;
|
|
|
|
not (A : *) : * := A -> false;
|
|
not_intro (A : *) (h : A -> false) : not A := h;
|
|
not_elim (A B : *) (a : A) (na : not A) : B := na a B;
|
|
|
|
and (A B : *) : * := forall (C : *), (A -> B -> C) -> C;
|
|
and_intro (A B : *) (a : A) (b : B) : and A B :=
|
|
fun (C : *) (H : A -> B -> C) => H a b;
|
|
and_elim_l (A B : *) (ab : and A B) : A :=
|
|
ab A (fun (a : A) (b : B) => a);
|
|
and_elim_r (A B : *) (ab : and A B) : B :=
|
|
ab B (fun (a : A) (b : B) => b);
|
|
|
|
or (A B : *) : * := forall (C : *), (A -> C) -> (B -> C) -> C;
|
|
or_intro_l (A B : *) (a : A) : or A B :=
|
|
fun (C : *) (ha : A -> C) (hb : B -> C) => ha a;
|
|
or_intro_r (A B : *) (b : B) : or A B :=
|
|
fun (C : *) (ha : A -> C) (hb : B -> C) => hb b;
|
|
or_elim (A B C : *) (ab : or A B) (ha : A -> C) (hb : B -> C) : C :=
|
|
ab C ha hb;
|
|
|
|
exists (A : *) (P : A -> *) : * := forall (C : *), (forall (x : A), P x -> C) -> C;
|
|
exists_intro (A : *) (P : A -> *) (a : A) (h : P a) : exists A P :=
|
|
fun (C : *) (g : forall (x : A), P x -> C) => g a h;
|
|
exists_elim (A B : *) (P : A -> *) (ex_a : exists A P) (h : forall (a : A), P a -> B) : B :=
|
|
ex_a B h;
|
|
|
|
binop (A : *) := A -> A -> A;
|
|
|
|
comp (A B C : *) (g : B -> C) (f : A -> B) (x : A) : C :=
|
|
g (f x);
|
|
|
|
-- --------------------------------------------------------------------------------------------------------------
|
|
|
|
--
|
|
-- Next we can define equality. This is the same as in <logic.pg>. We get a
|
|
-- couple Peano axioms for free as theorems.
|
|
--
|
|
|
|
-- implies axiom 5
|
|
-- (if x : nat, then y : nat, since we can only compare objects of the same type)
|
|
eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
|
|
|
|
-- axiom 2 (but as a theorem)
|
|
eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
|
|
|
|
-- axiom 3 (but as a theorem)
|
|
eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) =>
|
|
Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy;
|
|
|
|
-- axiom 4 (but as a theorem)
|
|
eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) =>
|
|
Hyz P (Hxy P Hx);
|
|
|
|
-- This isn't an axiom, but is handy. If x = y, then f x = f y.
|
|
eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
|
|
fun (P : B -> *) (Hfx : P (f x)) =>
|
|
H (fun (a : A) => P (f a)) Hfx;
|
|
|
|
assoc (A : *) (op : binop A) := forall (c a b : A),
|
|
eq A (op a (op b c)) (op (op a b) c);
|
|
|
|
-- --------------------------------------------------------------------------------------------------------------
|
|
|
|
--
|
|
-- 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
|
|
--
|
|
|
|
nat : * := axiom;
|
|
|
|
--
|
|
-- 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
|
|
zero : nat := axiom;
|
|
|
|
-- axiom 6: For every n, S n is a natural number.
|
|
suc (n : nat) : nat := axiom;
|
|
|
|
-- axiom 7: If S n = S m, then n = m.
|
|
suc_inj : forall (n m : nat), eq nat (suc n) (suc m) -> eq nat n m := axiom;
|
|
|
|
-- axiom 8: No successor of any natural number is zero.
|
|
suc_nonzero : forall (n : nat), not (eq nat (suc n) zero) := axiom;
|
|
|
|
-- axiom 9: Induction! For any proposition φ on natural numbers, if φ(0) holds,
|
|
-- and if for every natural number n, φ(n) ⇒ φ(S n), then φ holds for all n.
|
|
nat_ind : forall (φ : nat -> *), φ zero -> (forall (n : nat), φ n -> φ (suc n))
|
|
-> forall (n : nat), φ n := axiom;
|
|
|
|
-- --------------------------------------------------------------------------------------------------------------
|
|
|
|
--
|
|
-- 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.
|
|
one : nat := suc zero;
|
|
two : nat := suc one;
|
|
three : nat := suc two;
|
|
four : nat := suc three;
|
|
five : nat := suc four;
|
|
|
|
-- First, the predecessor of n is m if n = suc m.
|
|
pred (n m : nat) : * := eq nat n (suc m);
|
|
|
|
-- Our claim is a disjunction, whose first option is that n = 0.
|
|
szc_l (n : nat) := eq nat n zero;
|
|
|
|
-- The second option is that n has a predecessor.
|
|
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.
|
|
szc (n : nat) := or (szc_l n) (szc_r n);
|
|
|
|
-- And here's our proof!
|
|
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))));
|
|
|
|
--
|
|
-- Before we continue one to defining addition, we need one more bunch of
|
|
-- axioms. Addition is normally defined recursively, which is difficult without
|
|
-- inductive definitions. I'm pretty sure this axiom is derivable from the
|
|
-- others, but I've spent a very long time trying to derive it, and it has
|
|
-- proven extremely difficult. I'm still convinced it's possible, just
|
|
-- prohibitively difficult and tedious without further language features
|
|
-- (implicit arguments and let bindings would help a ton).
|
|
--
|
|
-- Normally, we define recursive functions f : nat -> A in the following format:
|
|
-- f 0 = fzero
|
|
-- f (suc n) = fsuc n (f n)
|
|
-- More concretely, we have two equations, one for each possible case for n,
|
|
-- i.e. either zero or a successor. In the successor case, the value of
|
|
-- f (suc n) can depend on the value of f n. The recursion axioms below
|
|
-- assert that for any such pair of equations, there exists a unique function
|
|
-- satisfying said equations.
|
|
--
|
|
|
|
-- For any such equations, there exists a function.
|
|
rec_def (A : *) (fzero : A) (fsuc : nat -> A -> A) : nat -> A := axiom;
|
|
|
|
-- Here's equation one.
|
|
rec_cond_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) :=
|
|
eq A (f zero) fzero;
|
|
|
|
-- And equation two.
|
|
rec_cond_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) :=
|
|
forall (n : nat) (y : A),
|
|
eq A (f n) y -> eq A (f (suc n)) (fsuc n y);
|
|
|
|
-- Said function satisfies the equations.
|
|
-- It satisfies equation one.
|
|
rec_def_sat_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) :
|
|
rec_cond_zero A fzero fsuc (rec_def A fzero fsuc) := axiom;
|
|
|
|
-- And two.
|
|
rec_def_sat_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) :
|
|
rec_cond_suc A fzero fsuc (rec_def A fzero fsuc) := axiom;
|
|
|
|
-- And, finally, this function is unique in the sense that if any other function
|
|
-- also satisfies the equations, it takes the same values as rec_def.
|
|
rec_def_unique (A : *) (fzero : A) (fsuc : nat -> A -> A) (f g : nat -> A) :
|
|
rec_cond_zero A fzero fsuc f ->
|
|
rec_cond_suc A fzero fsuc f ->
|
|
rec_cond_zero A fzero fsuc g ->
|
|
rec_cond_suc A fzero fsuc g ->
|
|
forall (x : nat), eq A (f x) (g x) := axiom;
|
|
|
|
-- Now we can safely define addition.
|
|
|
|
-- First, here's the RHS of equation 2 as a function, since it will show up
|
|
-- multiple times.
|
|
psuc (_ r : nat) := suc r;
|
|
|
|
-- And here's plus!
|
|
plus (n : nat) : nat -> nat := rec_def nat n psuc;
|
|
|
|
-- The first equation manifests itself as the familiar
|
|
-- n + 0 = 0.
|
|
plus_0_r (n : nat) : eq nat (plus 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).
|
|
plus_s_r (n m : nat) : eq nat (plus n (suc m)) (suc (plus n m)) :=
|
|
rec_def_sat_suc nat n psuc m (plus n m) (eq_refl nat (plus n m));
|
|
|
|
-- We can now prove 1 + 1 = 2!
|
|
one_plus_one_two : eq nat (plus one one) two :=
|
|
-- 1 + (suc zero) = suc (1 + zero) = suc one
|
|
eq_trans nat (plus one one) (suc (plus one zero)) two
|
|
|
|
-- 1 + (suc zero) = suc (1 + zero)
|
|
(plus_s_r one zero)
|
|
|
|
-- suc (1 + zero) = suc one
|
|
(eq_cong nat nat (plus 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.
|
|
plus_assoc : assoc nat plus :=
|
|
-- We prove this via induction on p.
|
|
nat_ind
|
|
(fun (p : nat) =>
|
|
forall (n m : nat),
|
|
eq nat (plus n (plus m p)) (plus (plus n m) p))
|
|
|
|
-- Base case: p = 0
|
|
-- WTS n + (m + 0) = (n + m) + 0
|
|
(fun (n m : nat) =>
|
|
-- n + (m + 0) = n + m = (n + m) + 0
|
|
(eq_trans nat (plus n (plus m zero)) (plus n m) (plus (plus n m) zero)
|
|
-- n + (m + 0) = n + m
|
|
(eq_cong nat nat (plus m zero) m (fun (p : nat) => plus n p) (plus_0_r m))
|
|
|
|
-- n + m = (n + m) + 0
|
|
(eq_sym nat (plus (plus n m) zero) (plus n m) (plus_0_r (plus n m)))))
|
|
|
|
-- Inductive step: IH = n + (m + p) = (n + m) + p
|
|
(fun (p : nat) (IH : forall (n m : nat), eq nat (plus n (plus m p)) (plus (plus n m) p)) (n m : nat) =>
|
|
-- 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 (plus n (plus m (suc p))) (plus n (suc (plus m p))) (plus (plus n m) (suc p))
|
|
|
|
-- n + (m + suc p) = n + suc (m + p)
|
|
(eq_cong nat nat (plus m (suc p)) (suc (plus m p)) (fun (a : nat) => (plus n a)) (plus_s_r m p))
|
|
|
|
-- n + suc (m + p) = (n + m) + suc p
|
|
(eq_trans nat (plus n (suc (plus m p))) (suc (plus n (plus m p))) (plus (plus n m) (suc p))
|
|
-- n + suc (m + p) = suc (n + (m + p))
|
|
(plus_s_r n (plus m p))
|
|
|
|
-- suc (n + (m + p)) = (n + m) + suc p
|
|
(eq_trans nat (suc (plus n (plus m p))) (suc (plus (plus n m) p)) (plus (plus n m) (suc p))
|
|
-- suc (n + (m + p)) = suc ((n + m) + p)
|
|
(eq_cong nat nat (plus n (plus m p)) (plus (plus n m) p) suc (IH n m))
|
|
|
|
-- suc ((n + m) + p) = (n + m) + suc p
|
|
(eq_sym nat (plus (plus n m) (suc p)) (suc (plus (plus n m) p))
|
|
(plus_s_r (plus n m) p)))));
|
|
|
|
-- Up next is commutativity, but we will need a couple lemmas first.
|
|
|
|
-- First, we will show that 0 + n = n.
|
|
plus_0_l : forall (n : nat), eq nat (plus zero n) n :=
|
|
-- We prove this by induction on n.
|
|
nat_ind (fun (n : nat) => eq nat (plus 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 : eq nat (plus zero n) n) =>
|
|
-- WTS 0 + (suc n) = suc n
|
|
-- 0 + (suc n) = suc (0 + n) = suc n
|
|
eq_trans nat (plus zero (suc n)) (suc (plus zero n)) (suc n)
|
|
-- 0 + (suc n) = suc (0 + n)
|
|
(plus_s_r zero n)
|
|
|
|
-- suc (0 + n) = suc n
|
|
(eq_cong nat nat (plus zero n) n suc IH));
|
|
|
|
-- Next, we will show that (suc n) + m = suc (n + m).
|
|
plus_s_l (n : nat) : forall (m : nat), eq nat (plus (suc n) m) (suc (plus n m)) :=
|
|
-- We proceed by induction on m.
|
|
nat_ind (fun (m : nat) => eq nat (plus (suc n) m) (suc (plus n m)))
|
|
-- base case: (suc n) + 0 = suc (n + 0)
|
|
-- (suc n) + 0 = suc n = suc (n + 0)
|
|
(eq_trans nat (plus (suc n) zero) (suc n) (suc (plus n zero))
|
|
-- (suc n) + 0 = suc n
|
|
(plus_0_r (suc n))
|
|
|
|
-- suc n = suc (n + 0)
|
|
(eq_cong nat nat n (plus n zero) suc
|
|
-- n = n + 0
|
|
(eq_sym nat (plus n zero) n (plus_0_r n))))
|
|
|
|
-- inductive case
|
|
-- IH = suc n + m = suc (n + m)
|
|
(fun (m : nat) (IH : eq nat (plus (suc n) m) (suc (plus 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 (plus (suc n) (suc m)) (suc (plus (suc n) m)) (suc (plus 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 (plus (suc n) m)) (suc (suc (plus n m))) (suc (plus n (suc m)))
|
|
-- suc (suc n + m) = suc (suc (n + m))
|
|
(eq_cong nat nat (plus (suc n) m) (suc (plus n m)) suc IH)
|
|
|
|
-- suc (suc (n + m)) = suc (n + suc m)
|
|
(eq_cong nat nat (suc (plus n m)) (plus n (suc m)) suc
|
|
-- suc (n + m) = n + suc m
|
|
(eq_sym nat (plus n (suc m)) (suc (plus n m)) (plus_s_r n m))))));
|
|
|
|
-- Finally, we can prove commutativity.
|
|
plus_comm (n : nat) : forall (m : nat), eq nat (plus n m) (plus m n) :=
|
|
-- As usual, we proceed by induction.
|
|
nat_ind (fun (m : nat) => eq nat (plus n m) (plus m n))
|
|
|
|
-- Base case: WTS n + 0 = 0 + n
|
|
-- n + 0 = n = 0 + n
|
|
(eq_trans nat (plus n zero) n (plus zero n)
|
|
-- n + 0 = n
|
|
(plus_0_r n)
|
|
|
|
-- n = 0 + n
|
|
(eq_sym nat (plus zero n) n (plus_0_l n)))
|
|
|
|
-- Inductive step:
|
|
(fun (m : nat) (IH : eq nat (plus n m) (plus m n)) =>
|
|
-- WTS n + suc m = suc m + n
|
|
-- n + suc m = suc (n + m)
|
|
-- = suc (m + n)
|
|
-- = suc m + n
|
|
(eq_trans nat (plus n (suc m)) (suc (plus n m)) (plus (suc m) n)
|
|
-- n + suc m = suc (n + m)
|
|
(plus_s_r n m)
|
|
|
|
-- suc (n + m) = suc m + n
|
|
(eq_trans nat (suc (plus n m)) (suc (plus m n)) (plus (suc m) n)
|
|
-- suc (n + m) = suc (m + n)
|
|
(eq_cong nat nat (plus n m) (plus m n) suc IH)
|
|
|
|
-- suc (m + n) = suc m + n
|
|
(eq_sym nat (plus (suc m) n) (suc (plus m n)) (plus_s_l m n)))));
|