wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

very minor cleanups

Browse source
This commit is contained in:
William Ball 2024-11-20 13:22:06 -08:00
parent 47dc90d872
commit e05c8e8a92
1 changed files with 22 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
examples/peano.pg
View file

@ -137,11 +137,12 @@ nat_ind : forall (φ : nat -> *), φ zero -> (forall (n : nat), φ n -> φ (suc
* long and complicated really quickly.
*]
one : nat := suc zero;
two : nat := suc one;
-- 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;
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);
@ -150,7 +151,7 @@ pred (n m : nat) : * := eq nat n (suc m);
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);
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`.
@ -192,41 +193,50 @@ suc_or_zero : forall (n : nat), szc n :=
-- 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.
-- Equation 1.
-- 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;
-- Equation 2.
-- 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
-- satisfies the equations, it is really `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 ->
rec_cond_suc A fzero fsuc f ->
rec_cond_zero A fzero fsuc g ->
rec_cond_suc 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;
-- n + 0 = n
-- 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;
-- n + suc m = suc (n + m)
-- 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));