gave up on proving recursion, proved associativity of addition

examples/peano.pg

@@ -1,7 +1,7 @@
-(*
+[*
  * 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;
@@ -31,17 +31,18 @@ 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;
 
+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)
@@ -63,9 +64,12 @@ 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,
@@ -77,11 +81,11 @@ eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
  * 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;
@@ -101,7 +105,7 @@ nat : * := axiom;
  * 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;
@@ -122,7 +126,7 @@ nat_ind : forall (φ : nat -> *), φ zero -> (forall (n : nat), φ n -> φ (suc
 
 -- --------------------------------------------------------------------------------------------------------------
 
-(*
+[*
  * Now that we have stipulated these axioms, we are free to use them to make
  * definitions, prove theorems, etc.
  *
@@ -131,7 +135,13 @@ nat_ind : forall (φ : nat -> *), φ zero -> (forall (n : nat), φ n -> φ (suc
  *
  * First, we will make a bunch of abbreviations, since these terms get really
  * long and complicated really quickly.
- *)
+ *]
+
+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);
@@ -160,115 +170,126 @@ suc_or_zero : forall (n : nat), szc 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
+ * Before we continue one to defining addition, we need one more bunch of
- * addition, but first we need a mechanism for even defining addition in the
+ * axioms. Addition is normally defined recursively, which is difficult without
- * first place. The way we will go about this is proving that we can define
+ * inductive definitions. I'm pretty sure this axiom is derivable from the
- * functions recursively. In particular, we will prove that for any `A : *`, any
+ * others, but I've spent a very long time trying to derive it, and it has
- * `fzero : A`, and any `fsuc : nat -> A -> A`, there is a unique function
+ * proven extremely difficult. I'm still convinced it's possible, just
- * `f : nat -> A` satisfying the following equations:
+ * prohibitively difficult and tedious without further language features
- *   (1)    f zero    = fzero
+ * (implicit arguments and let bindings would help a ton).
- *   (2)    f (suc x) = fsuc x (f x)
+ *
- *)
+ * 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.
+ *]
 
--- Here is equation (1)
+-- For any such equations, there exists a function.
-rec_cond_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) :=
+rec_def (A : *) (fzero : A) (fsuc : nat -> A -> A) : nat -> A := axiom;
+
+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),
+  forall (n : nat) (y : A),
-    eq A (f x) y -> eq A (f (suc x)) (fsuc x y);
+    eq A (f n) y -> eq A (f (suc n)) (fsuc n y);
 
-(*
+-- Said function satisfies the equations.
- * Our proof strategy is to first define a relation `R` on `nat` such that
+-- Equation 1.
- * `R x y` only holds if `f x = y` for every function `f : nat -> A` satisfying
+rec_def_sat_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) :
- * equations (1) and (2). Then we will prove that `R` is actually total, and use
+  rec_cond_zero A fzero fsuc (rec_def A fzero fsuc) := axiom;
- * 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.
+-- Equation 2.
-rec_rel (A : *) (fzero : A) (fsuc : nat -> A -> A) (n : nat) (x : A) : * :=
+rec_def_sat_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) :
-  forall (f : nat -> A),
+  rec_cond_suc A fzero fsuc (rec_def A fzero fsuc) := axiom;
-    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`.
+-- And, finally, this function is unique in the sense that if any other function
-rec_rel_zero (A : *) (fzero : A) (fsuc : nat -> A -> A)
+-- satisfies the equations, it is really `rec_def`.
-  : rec_rel A fzero fsuc zero fzero :=
+rec_def_unique (A : *) (fzero : A) (fsuc : nat -> A -> A) (f g : nat -> A) :
-    fun (f : nat -> A)
+  rec_cond_zero A fzero fsuc f ->
-        (Hzero : rec_cond_zero A fzero fsuc f)
+  rec_cond_suc A fzero fsuc f ->
-        (Hsuc : rec_cond_suc A fzero fsuc f) =>
+  rec_cond_zero A fzero fsuc g ->
-      Hzero;
+  rec_cond_suc A fzero fsuc g ->
+  forall (x : nat), eq A (f x) (g x) := axiom;
 
--- Likewise, we show that if `R x y`, then `R (suc x) (fsuc x y)`.
+-- Now we can safely define addition.
-rec_rel_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) (x : nat) (y : A)
+psuc (_ r : nat) := suc r;
-  (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`.
+plus (n : nat) : nat -> nat := rec_def nat n psuc;
-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.
+-- n + 0 = n
-rec_rel_total (A : *) (fzero : A) (fsuc : nat -> A -> A)
+plus_0_r (n : nat) : eq nat (plus n zero) n :=
-  : forall (x : nat), rec_rel_def A fzero fsuc x :=
+  rec_def_sat_zero nat n psuc;
-    -- 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`.
+-- n + suc m = suc (n + m)
-    (exists_intro A (rec_rel A fzero fsuc zero) fzero (rec_rel_zero A fzero fsuc))
+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));
 
-    -- For the inductive case, let `x : nat` and suppose `R` is defined on `x`.
+-- We can now prove 1 + 1 = 2!
-    (fun (x : nat) (IH : rec_rel_def A fzero fsuc x) =>
+one_plus_one_two : eq nat (plus one one) two :=
-      -- Then let `y` be such that `R x y`.
+  -- 1 + (suc zero) = suc (1 + zero) = suc one
-      exists_elim A (exists A (rec_rel A fzero fsuc (suc x))) (rec_rel A fzero fsuc x) IH
+  eq_trans nat (plus one one) (suc (plus one zero)) two
-        (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`.
+  -- 1 + (suc zero) = suc (1 + zero)
-rec_def (A : *) (fzero : A) (fsuc : nat -> A -> A) (x : nat) : A :=
+  (plus_s_r one zero)
-  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
+  -- suc (1 + zero) = suc one
--- equations (1) and (2), we must have that `f x = g x` for all `x : nat`.
+  (eq_cong nat nat (plus one zero) one suc (plus_0_r one));
-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.
+ * 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)))));