treesitter doesn't like block comments

examples/peano.pg

@@ -1,7 +1,7 @@
-[*
+-- 
- * We need some basic logic, so I'm stealing this from <logic.pg>. See that file
+-- We need some basic logic, so I'm stealing this from <logic.pg>. See that file
- * for more details on how these work.
+-- for more details on how these work.
- *]
+-- 
 
 false : * := forall (A : *), A;
 false_elim (A : *) (contra : false) : A := contra A;
@@ -39,13 +39,13 @@ comp (A B C : *) (g : B -> C) (f : A -> B) (x : A) : C :=
 
 -- --------------------------------------------------------------------------------------------------------------
 
-[*
+-- 
- * Next we can define equality. This is the same as in <logic.pg>. We get a
+-- Next we can define equality. This is the same as in <logic.pg>. We get a
- * couple Peano axioms for free as theorems.
+-- 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)
+-- (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)
@@ -59,7 +59,7 @@ eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P
 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`.
+-- 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;
@@ -69,51 +69,51 @@ assoc (A : *) (op : binop A) := forall (c a b : A),
 
 -- --------------------------------------------------------------------------------------------------------------
 
-[*
+-- 
- * Now we can define the Peano axioms. Unlike with equality, perga is not
+-- 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
+-- powerful enough to construct the natural numbers (or at least to prove the
- * Peano axioms as theorems from a definition constructible in perga). However,
+-- 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
+-- working with axioms is extremely common in math. As such, perga has a system
- * for doing just that, namely the *axiom* 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
+-- 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
+-- 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
+-- 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
+-- 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
+-- 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
+-- As you can imagine, this can be risky. For instance, there's nothing stopping
- * us from saying
+-- us from saying
- *     uh_oh : false := axiom;
+--     uh_oh : false := axiom;
- * or stipulating more subtly contradictory axioms. As such, as in mathematics,
+-- or stipulating more subtly contradictory axioms. As such, as in mathematics,
- * axioms should be used with care.
+-- axioms should be used with care.
- *
+-- 
- * There's another problem with axioms, namely that perga cannot do any
+-- There's another problem with axioms, namely that perga cannot do any
- * computations with axioms. The more you can define within perga natively, the
+-- computations with axioms. The more you can define within perga natively, the
- * better, as computations done without axioms can be utilized by perga. For
+-- better, as computations done without axioms can be utilized by perga. For
- * example, in <computation.pg>, we define the natural numbers as Church
+-- example, in <computation.pg>, we define the natural numbers as Church
- * numerals entirely within perga. There, the proof that `1 + 1 = 2` is just
+-- 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
+-- 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
+-- require a proof, since perga is unable to do computations with things defined
- * as axioms.
+-- as axioms.
- *
+-- 
- * With these warnings in place, the Peano axioms are proven to be consistent,
+-- 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
+-- so we should be fine. I'm formalizing the second order axioms given in the
- * wikipedia article on the Peano axioms
+-- wikipedia article on the Peano axioms
- * (https://en.wikipedia.org/wiki/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.
+-- 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`.
+-- 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.
@@ -126,16 +126,16 @@ 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
+-- Now that we have stipulated these axioms, we are free to use them to make
- * definitions, prove theorems, etc.
+-- definitions, prove theorems, etc.
- *
+-- 
- * Our first theorem, as a warm up, is to prove that every natural number is
+-- Our first theorem, as a warm up, is to prove that every natural number is
- * either 0 or the successor of another natural number.
+-- either 0 or the successor of another natural number.
- *
+-- 
- * First, we will make a bunch of abbreviations, since these terms get really
+-- First, we will make a bunch of abbreviations, since these terms get really
- * long and complicated really quickly.
+-- long and complicated really quickly.
- *]
+-- 
 
 -- Some abbreviations for common numbers.
 one   : nat := suc zero;
@@ -144,17 +144,17 @@ three : nat := suc two;
 four  : nat := suc three;
 five  : nat := suc four;
 
--- First, the predecessor of `n` is `m` if `n = suc m`.
+-- 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`.
+-- 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.
+-- 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`.
+-- holds for every n.
 szc (n : nat) := or (szc_l n) (szc_r n);
 
 -- And here's our proof!
@@ -164,31 +164,31 @@ suc_or_zero : forall (n : nat), szc n :=
         -- 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`.
+        -- 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
+            -- Then the right option holds for suc n, since suc n is the
-            -- successor of `n`
+            -- 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
+-- Before we continue one to defining addition, we need one more bunch of
- * axioms. Addition is normally defined recursively, which is difficult without
+-- axioms. Addition is normally defined recursively, which is difficult without
- * inductive definitions. I'm pretty sure this axiom is derivable from the
+-- 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
+-- 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
+-- proven extremely difficult. I'm still convinced it's possible, just
- * prohibitively difficult and tedious without further language features
+-- prohibitively difficult and tedious without further language features
- * (implicit arguments and let bindings would help a ton).
+-- (implicit arguments and let bindings would help a ton).
- *
+-- 
- * Normally, we define recursive functions `f : nat -> A` in the following format:
+-- Normally, we define recursive functions f : nat -> A in the following format:
- *            f 0 = fzero
+--            f 0 = fzero
- *      f (suc n) = fsuc n (f n)
+--      f (suc n) = fsuc n (f n)
- * More concretely, we have two equations, one for each possible case for `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
+-- 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
+-- 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
+-- assert that for any such pair of equations, there exists a unique function
- * satisfying said equations.
+-- satisfying said equations.
- *]
+-- 
 
 -- For any such equations, there exists a function.
 rec_def (A : *) (fzero : A) (fsuc : nat -> A -> A) : nat -> A := axiom;
@@ -212,7 +212,7 @@ 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`.
+-- 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 ->
@@ -226,7 +226,7 @@ rec_def_unique (A : *) (fzero : A) (fsuc : nat -> A -> A) (f g : nat -> A) :
 -- multiple times.
 psuc (_ r : nat) := suc r;
 
--- And here's `plus`!
+-- And here's plus!
 plus (n : nat) : nat -> nat := rec_def nat n psuc;
 
 -- The first equation manifests itself as the familiar
@@ -251,13 +251,13 @@ one_plus_one_two : eq nat (plus one one) two :=
   -- 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`
+-- We have successfully defined addition! Note that evaluating 1 + 1 to 2
- * requires a proof, unfortunately, since this computation isn't visible to
+-- requires a proof, unfortunately, since this computation isn't visible to
- * perga.
+-- perga.
- *
+-- 
- * We will now prove a couple standard properties of addition.
+-- 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 := 
@@ -303,3 +303,60 @@ plus_assoc : assoc nat plus :=
           -- 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))))));