From ffc78ca1ffc569ee1343db4bcdf3d810310957b1 Mon Sep 17 00:00:00 2001 From: William Ball Date: Wed, 20 Nov 2024 22:21:43 -0800 Subject: [PATCH] treesitter doesn't like block comments --- examples/peano.pg | 237 ++++++++++++++++++++++++++++------------------ 1 file changed, 147 insertions(+), 90 deletions(-) diff --git a/examples/peano.pg b/examples/peano.pg index bca84ee..ab728c6 100644 --- a/examples/peano.pg +++ b/examples/peano.pg @@ -1,7 +1,7 @@ -[* - * We need some basic logic, so I'm stealing this from . See that file - * for more details on how these work. - *] +-- +-- We need some basic logic, so I'm stealing this from . See that file +-- 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 . We get a - * couple Peano axioms for free as theorems. - *] +-- +-- Next we can define equality. This is the same as in . 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) +-- (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 - * 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 - *] +-- +-- 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 , 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). - *] +-- +-- 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 , 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. +-- 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 - * 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. - *] +-- +-- 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; @@ -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 - -- successor of `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. - *] +-- +-- 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; @@ -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` - * requires a proof, unfortunately, since this computation isn't visible to - * perga. - * - * We will now prove a couple standard properties of addition. - *] +-- +-- 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 := @@ -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))))));