275 lines
12 KiB
Text
275 lines
12 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;
|
||
|
|
exists_elim_val (A : *) (P : A -> *) (ex_a : exists A P) : A :=
|
||
|
|
exists_elim A A P ex_a (fun (a : A) (_ : P a) => a);
|
||
|
|
|
||
|
|
binop (A : *) := A -> A -> A;
|
||
|
|
|
||
|
|
-- --------------------------------------------------------------------------------------------------------------
|
||
|
|
|
||
|
|
(*
|
||
|
|
* 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;
|
||
|
|
|
||
|
|
-- --------------------------------------------------------------------------------------------------------------
|
||
|
|
|
||
|
|
(*
|
||
|
|
* 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.
|
||
|
|
*)
|
||
|
|
|
||
|
|
-- 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 (fun (m : nat) => pred n m);
|
||
|
|
|
||
|
|
-- 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))));
|
||
|
|
|
||
|
|
(*
|
||
|
|
* Now we would like to define addition and prove lots of lovely theorems about
|
||
|
|
* addition, but first we need a mechanism for even defining addition in the
|
||
|
|
* first place. The way we will go about this is proving that we can define
|
||
|
|
* functions recursively. In particular, we will prove that for any `A : *`, any
|
||
|
|
* `fzero : A`, and any `fsuc : nat -> A -> A`, there is a unique function
|
||
|
|
* `f : nat -> A` satisfying the following equations:
|
||
|
|
* (1) f zero = fzero
|
||
|
|
* (2) f (suc x) = fsuc x (f x)
|
||
|
|
*)
|
||
|
|
|
||
|
|
-- Here is equation (1)
|
||
|
|
rec_cond_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) :=
|
||
|
|
eq A (f zero) fzero;
|
||
|
|
|
||
|
|
-- And here's equation (2)
|
||
|
|
rec_cond_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) :=
|
||
|
|
forall (x : nat) (y : A),
|
||
|
|
eq A (f x) y -> eq A (f (suc x)) (fsuc x y);
|
||
|
|
|
||
|
|
(*
|
||
|
|
* Our proof strategy is to first define a relation `R` on `nat` such that
|
||
|
|
* `R x y` only holds if `f x = y` for every function `f : nat -> A` satisfying
|
||
|
|
* equations (1) and (2). Then we will prove that `R` is actually total, and use
|
||
|
|
* that to define our recursive function. Then we will show that all function
|
||
|
|
* satisfying equations (1) and (2) have the same outputs, and that this
|
||
|
|
* function actually satisfies the equations, meaning it is uniquely defined.
|
||
|
|
*)
|
||
|
|
|
||
|
|
-- Here's the relation.
|
||
|
|
rec_rel (A : *) (fzero : A) (fsuc : nat -> A -> A) (n : nat) (x : A) : * :=
|
||
|
|
forall (f : nat -> A),
|
||
|
|
rec_cond_zero A fzero fsuc f ->
|
||
|
|
rec_cond_suc A fzero fsuc f ->
|
||
|
|
eq A (f n) x;
|
||
|
|
|
||
|
|
-- Little lemma showing that `R zero fzero`.
|
||
|
|
rec_rel_zero (A : *) (fzero : A) (fsuc : nat -> A -> A)
|
||
|
|
: rec_rel A fzero fsuc zero fzero :=
|
||
|
|
fun (f : nat -> A)
|
||
|
|
(Hzero : rec_cond_zero A fzero fsuc f)
|
||
|
|
(Hsuc : rec_cond_suc A fzero fsuc f) =>
|
||
|
|
Hzero;
|
||
|
|
|
||
|
|
-- Likewise, we show that if `R x y`, then `R (suc x) (fsuc x y)`.
|
||
|
|
rec_rel_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) (x : nat) (y : A)
|
||
|
|
(H : rec_rel A fzero fsuc x y) : rec_rel A fzero fsuc (suc x) (fsuc x y) :=
|
||
|
|
fun (f : nat -> A)
|
||
|
|
(Hzero : rec_cond_zero A fzero fsuc f)
|
||
|
|
(Hsuc : rec_cond_suc A fzero fsuc f) =>
|
||
|
|
Hsuc x y (H f Hzero Hsuc);
|
||
|
|
|
||
|
|
-- This is an abbreviation for the statement that `R` is defined on `x`.
|
||
|
|
rec_rel_def (A : *) (fzero : A) (fsuc : nat -> A -> A) : nat -> * :=
|
||
|
|
fun (x : nat) => exists A (rec_rel A fzero fsuc x);
|
||
|
|
|
||
|
|
-- Finally, we prove that `R` is total.
|
||
|
|
rec_rel_total (A : *) (fzero : A) (fsuc : nat -> A -> A)
|
||
|
|
: forall (x : nat), rec_rel_def A fzero fsuc x :=
|
||
|
|
-- We prove this by induction.
|
||
|
|
nat_ind (rec_rel_def A fzero fsuc)
|
||
|
|
|
||
|
|
-- For our base case, since `R zero fzero` by the earlier lemma, `R` is defined on `zero`.
|
||
|
|
(exists_intro A (rec_rel A fzero fsuc zero) fzero (rec_rel_zero A fzero fsuc))
|
||
|
|
|
||
|
|
-- For the inductive case, let `x : nat` and suppose `R` is defined on `x`.
|
||
|
|
(fun (x : nat) (IH : rec_rel_def A fzero fsuc x) =>
|
||
|
|
-- Then let `y` be such that `R x y`.
|
||
|
|
exists_elim A (exists A (rec_rel A fzero fsuc (suc x))) (rec_rel A fzero fsuc x) IH
|
||
|
|
(fun (y : A) (H : rec_rel A fzero fsuc x y) =>
|
||
|
|
-- Then we claim `R (suc x) (fsuc x y)`.
|
||
|
|
exists_intro A (rec_rel A fzero fsuc (suc x)) (fsuc x y)
|
||
|
|
-- Indeed this follows by the earlier lemma.
|
||
|
|
(rec_rel_suc A fzero fsuc x y H)));
|
||
|
|
|
||
|
|
-- With this, we can define a function `nat -> A`.
|
||
|
|
rec_def (A : *) (fzero : A) (fsuc : nat -> A -> A) (x : nat) : A :=
|
||
|
|
exists_elim A A (rec_rel A fzero fsuc x)
|
||
|
|
(rec_rel_total A fzero fsuc x)
|
||
|
|
(fun (y : A) (_ : rec_rel A fzero fsuc x y) => y);
|
||
|
|
|
||
|
|
-- Now we can prove that for any two functions `f g : nat -> A` satisfying
|
||
|
|
-- equations (1) and (2), we must have that `f x = g x` for all `x : nat`.
|
||
|
|
rec_def_unique (A : *) (fzero : A) (fsuc : nat -> A -> A) (f g : nat -> A)
|
||
|
|
(Fzero : rec_cond_zero A fzero fsuc f)
|
||
|
|
(Fsuc : rec_cond_suc A fzero fsuc f)
|
||
|
|
(Gzero : rec_cond_zero A fzero fsuc g)
|
||
|
|
(Gsuc : rec_cond_suc A fzero fsuc g)
|
||
|
|
: forall (x : nat), eq A (f x) (g x) :=
|
||
|
|
-- We prove this by induction.
|
||
|
|
nat_ind (fun (x : nat) => eq A (f x) (g x))
|
||
|
|
-- For the base case, we have
|
||
|
|
-- f zero = fzero (by (1) for f)
|
||
|
|
-- = g zero (by (1) for g)
|
||
|
|
(eq_trans A (f zero) fzero (g zero)
|
||
|
|
Fzero
|
||
|
|
(eq_sym A (g zero) fzero Gzero))
|
||
|
|
-- Now suppose `f x = g x`. We want to show that `f (suc x) = g (suc x)`.
|
||
|
|
(fun (x : nat) (IH : eq A (f x) (g x)) =>
|
||
|
|
-- Well, we have
|
||
|
|
-- f (suc x) = fsuc x (f x) (by (2) for f)
|
||
|
|
-- = fsuc x (g x) (by the inductive hypothesis)
|
||
|
|
-- = g (suc x) (by (2) for g)
|
||
|
|
(eq_trans A (f (suc x)) (fsuc x (f x)) (g (suc x))
|
||
|
|
(Fsuc x (f x) (eq_refl A (f x)))
|
||
|
|
(eq_trans A (fsuc x (f x)) (fsuc x (g x)) (g (suc x))
|
||
|
|
(eq_cong A A (f x) (g x) (fun (y : A) => fsuc x y) IH)
|
||
|
|
(eq_sym A (g (suc x)) (fsuc x (g x))
|
||
|
|
(Gsuc x (g x) (eq_refl A (g x)))))));
|
||
|
|
|
||
|
|
-- Almost there! We just need to show that `rec_def` actually satisfies the
|
||
|
|
-- equations.
|