pharpend/number-theory
1
0
Fork 0
forked from spivee/number-theory
Code Pull Requests Activity

improve nomenclature in pascal.v

Browse Source
This commit is contained in:
Peter Harpending 2025-12-02 22:20:23 -08:00
parent 3bf3e02ceb
commit 7a9373654f
1 changed files with 122 additions and 97 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

219
pascal.v
View File

@ -28,9 +28,9 @@ Proof.
assert (not A); auto.
Qed.
(* How does this proof work? Who knows! You'll have to run `debug auto`
(* How does this proof work? Who knows! You'll havelhs to run `debug auto`
yourself and see. Lots of effort has been put into this sort of automation,
in fact, the entire proof above could have been replaced with a single
in fact, the entire proof above could havelhs been replaced with a single
'intuition' tactic, which specializes in intuitionist logic tautologies.
While it is useful to know that Coq *can* go that far with automation, it is
@ -56,7 +56,7 @@ Definition Even (n: nat): Prop :=
Definition Odd (n: nat): Prop :=
exists k: nat, n = 2 * k + 1.
(* Let's try proving a number is even. We'll do zero, since then we have a base
(* Let's try proving a number is even. We'll do zero, since then we havelhs a base
case for induction later. *)
Lemma zero_is_even: Even 0.
@ -68,7 +68,7 @@ Proof.
reflexivity.
Qed.
(* It is annoying that we have to write all of these comments to explain what
(* It is annoying that we havelhs to write all of these comments to explain what
the state of the proof assistant is *going* to be. Plus, these comments can
get out of sync with the program, which seems absurd in a language
specifically designed to check such things. Let's make some new tactics to
@ -76,7 +76,7 @@ Qed.
(* This first tactic lets us start such a string of manipulations, by declaring
what the LHS of our goal is, effectively just a comment, but checked. *)
Ltac have expr :=
Ltac havelhs expr :=
lazymatch goal with
| |- ?Rel expr ?R =>
idtac
@ -88,7 +88,7 @@ Ltac have expr :=
(* Next, all manipulations are ultimately built out of beta/eta equivalence,
so let's make a tactic to check these equivalences for us. *)
Ltac thatis expr :=
Ltac basic_lambda_calculus_tells_us_the_lhs_is expr :=
lazymatch goal with
| |- ?Rel ?L ?R =>
unify L expr;
@ -97,7 +97,7 @@ Ltac thatis expr :=
fail "Goal is not a relation. Goal:" Other
end.
(* Using thatis makes it easy to annotate how an expression simplifies as it is
(* Using basic_lambda_calculus_tells_us_the_lhs_is makes it easy to annotate how an expression simplifies as it is
reduced, but sometimes we need to show how the RHS simplifies as well, so
let's make a tactic to break up an equation into two parts, showing how each
side equals some simpler intermediate value. *)
@ -107,12 +107,12 @@ Ltac both_sides_equal expr :=
(* Finally, if we want to be sure that our above annotations are correct, this
tactic will check that the LHS and RHS are not just equivalent, but already
identical. *)
Ltac done :=
Ltac obvious :=
lazymatch goal with
| |- ?Rel ?L ?L =>
reflexivity
| |- ?Rel ?L ?R =>
fail "Chain derivation not done. Left:" L "Right:" R
fail "Chain derivation not obvious. Left:" L "Right:" R
| |- ?Other =>
fail "Goal is not a relation. Goal:" Other
end.
@ -125,11 +125,11 @@ Proof.
exists 0.
(* Now let's prove our goal a little more explicitly. *)
both_sides_equal 0.
-have 0.
done.
-have (2 * 0).
thatis 0.
done.
-havelhs 0.
obvious.
-havelhs (2 * 0).
basic_lambda_calculus_tells_us_the_lhs_is 0.
obvious.
Qed.
(* This case might be sort of overkill... As one gains/regains familiarity with
@ -150,24 +150,24 @@ Proof.
n+1 is odd. 'exists' is a tactic that says a term should be taken as the
term we are trying to prove exists. *)
exists k.
(* Now we actually have to prove that S n = 2 * k + 1, though. *)
have (S n).
(* Now we actually havelhs to prove that S n = 2 * k + 1, though. *)
havelhs (S n).
rewrite Eq.
have (S (2 * k)).
thatis (1 + 2 * k).
havelhs(S (2 * k)).
basic_lambda_calculus_tells_us_the_lhs_is (1 + 2 * k).
(* This is almost what we want. Let's do a commutativity rewrite. *)
rewrite (PeanoNat.Nat.add_comm _ _).
have (2 * k + 1).
done.
havelhs(2 * k + 1).
obvious.
Qed.
(* Having these tactics definitely makes the control flow easier to follow, but
it would be nice if we didn't have to appeal to the laws of associativity
it would be nice if we didn't havelhs to appeal to the laws of associativity
and commutativity every time our goal was expressed slightly differently to
what we expected. Let's take some of those powerful proof automation tools,
and use them for this very narrow task of algebraic manipulation. *)
Ltac rearrange expr :=
Ltac basic_algebra_tells_us_the_lhs_is expr :=
lazymatch goal with
| |- ?Rel ?L ?R =>
transitivity expr; [> ring | ]
@ -177,7 +177,7 @@ Ltac rearrange expr :=
(* Further, manipulating existence proofs using exists and destruct is a bit
hard to follow. Let's make some tactics for declaring what we know, and what
we have to prove, as each of these things change from line to line. *)
we havelhs to prove, as each of these things change from line to line. *)
(* If our goal isn't a relation yet, we might still want to declare it. *)
Ltac havegoal expr :=
@ -214,27 +214,29 @@ Proof.
weknow OddEq: (n = 2 * k + 1).
(* When we do goal manipulations like 'exists', let's annotate the new goal
on the same line using the semicolon separator. *)
exists (S k); havegoal (S n = 2 * S k).
unfold Even.
exists (S k).
havegoal (S n = 2 * S k).
both_sides_equal (2 * k + 2).
-have (S n).
-havelhs (S n).
(* Let's also annotate rewrites on the same line, if it will fit. *)
rewrite OddEq; have (S (2 * k + 1)).
rewrite OddEq; havelhs (S (2 * k + 1)).
(* We should get used to S as a first-class operation, since this is Peano
arithmetic, at the end of the day. But for now we will get rid of the S
and apply algebraic manipulations to more traditional expressions. *)
thatis (1 + 2 * k + 1).
basic_lambda_calculus_tells_us_the_lhs_is (1 + 2 * k + 1).
(* Now let's get Coq to prove our algebra for us! *)
rearrange (2 * k + 2).
done.
-have (2 * S k).
basic_algebra_tells_us_the_lhs_is (2 * k + 2).
obvious.
-havelhs (2 * S k).
(* Again, get rid of the S. *)
thatis (2 * (1 + k)).
(* And rearrange. *)
rearrange (2 * k + 2).
done.
basic_lambda_calculus_tells_us_the_lhs_is (2 * (1 + k)).
(* And basic_algebra_tells_us_the_lhs_is. *)
basic_algebra_tells_us_the_lhs_is (2 * k + 2).
obvious.
Qed.
(* You might see where this is going now. We have all the pieces to build an
(* You might see where this is going now. We havelhs all the pieces to build an
inductive proof! *)
Theorem even_or_odd: forall n: nat,
@ -242,7 +244,7 @@ Theorem even_or_odd: forall n: nat,
Proof.
intro n.
induction n.
(* To prove something inductively, we have to prove it is true for 0, and
(* To prove something inductively, we havelhs to prove it is true for 0, and
then that it is true for any number of the form S n. *)
*havegoal (Even 0 \/ Odd 0).
left; havegoal (Even 0).
@ -253,6 +255,7 @@ Proof.
when it comes to n being even or odd. *)
destruct Ind.
+weknow IsEven: (Even n).
havegoal (Even (S n) \/ Odd (S n)).
(* We can use the 'left' and 'right' tactics to choose how we are going to
prove a dysjunction. *)
right; havegoal (Odd (S n)).
@ -260,6 +263,7 @@ Proof.
that lemma, and apply it to produce the 'exact' proof we need. *)
exact (even_implies_odd n IsEven).
+weknow IsOdd: (Odd n).
havegoal (Even (S n) \/ Odd (S n)).
(* Very similar logic on the other side. *)
left; havegoal (Even (S n)).
exact (odd_implies_even n IsOdd).
@ -268,10 +272,10 @@ Qed.
(* Wasn't that a fun and pleasant adventure?
So we see that more explicit control flow sets us up for quite nice proofs,
where we can see that the goal follows by simple algebra, algebra which Coq
where we can see that the goal follows by basic algebra, algebra which Coq
is prepared to do for us.
Agda and Idris programmers will recognize that Even and Odd could have been
Agda and Idris programmers will recognize that Even and Odd could havelhs been
jerry-rigged so that the `ring` tactics weren't required at all, and while
we will be exploiting that sort of trick to simplify things when they get
hard, it's useful to embrace these un-optimized definitions when trying to
@ -293,7 +297,7 @@ Qed.
pascal 3 k = k*(k+1)*(k+2)/6
etc.
To do this without getting dizzy over nested cases, let's get dizzy over
To do this without getting horny over nested cases, let's get horny over
higher order functions instead. Let's define a function that takes a
sequence, and returns a sequence representing the partial sums of that
sequence. *)
@ -324,12 +328,12 @@ Lemma pascal_0: forall r: nat,
Proof.
intro r.
induction r.
*have (pascal 0 0).
thatis 1.
done.
*have (pascal (S r) 0).
thatis (series (pascal r) 0).
thatis (pascal r 0).
*havelhs (pascal 0 0).
basic_lambda_calculus_tells_us_the_lhs_is 1.
obvious.
*havelhs (pascal (S r) 0).
basic_lambda_calculus_tells_us_the_lhs_is (series (pascal r) 0).
basic_lambda_calculus_tells_us_the_lhs_is (pascal r 0).
(* Let's stop this chain reasoning here, and look at what our goal is now. *)
havegoal (pascal r 0 = 1).
weknow Ind: (pascal r 0 = 1).
@ -352,7 +356,7 @@ Fixpoint prod_up (k r: nat): nat :=
end.
(* Often this permutation prod_up is notated as factorial (k + r) / factorial k,
but we don't have division in peano arithmetic, so let's show this relation
but we don't havelhs division in peano arithmetic, so let's show this relation
through multiplication instead. *)
Lemma prod_up_ratio: forall k r: nat,
@ -360,21 +364,28 @@ Lemma prod_up_ratio: forall k r: nat,
Proof.
intros k.
induction k; intro r.
*cbn.
havegoal (factorial r + 0 = factorial r).
ring.
*have (prod_up (S k) (1 + r) * factorial r).
thatis (prod_up k (2 + r) * (1 + r) * factorial r).
*both_sides_equal (factorial r).
-basic_lambda_calculus_tells_us_the_lhs_is (1 * factorial r).
basic_algebra_tells_us_the_lhs_is (factorial r).
obvious.
-havelhs (factorial (0 + r)).
basic_lambda_calculus_tells_us_the_lhs_is (factorial r).
obvious.
*havelhs (prod_up (S k) (1 + r) * factorial r).
basic_lambda_calculus_tells_us_the_lhs_is (prod_up k (2 + r) * (1 + r) * factorial r).
weknow Ind: (forall r': nat, prod_up k (1 + r') * factorial r' = factorial (k + r')).
rearrange (prod_up k (2 + r) * ((1 + r) * factorial r)).
thatis (prod_up k (1 + (1 + r)) * factorial (1 + r)).
rewrite (Ind (1 + r)); have (factorial (k + (1 + r))).
thatis (factorial (k + S r)).
basic_algebra_tells_us_the_lhs_is (prod_up k (2 + r) * ((1 + r) * factorial r)).
basic_lambda_calculus_tells_us_the_lhs_is (prod_up k (1 + (1 + r)) * factorial (1 + r)).
pose (NigFace := Ind (1 + r)).
rewrite NigFace.
havelhs (factorial (k + (1 + r))).
basic_lambda_calculus_tells_us_the_lhs_is (factorial (k + S r)).
(* Use one of those manual manipulations, since the term we are manipulating
is inside of a function call, so ring will get confused. *)
rewrite <- (plus_n_Sm k r); have (factorial (S (k + r))).
thatis (factorial (S k + r)).
done.
rewrite <- (plus_n_Sm k r).
havelhs (factorial (S (k + r))).
basic_lambda_calculus_tells_us_the_lhs_is (factorial (S k + r)).
obvious.
Qed.
(* If we let r = 0 then we even show that the factorial is a special case of
@ -383,15 +394,16 @@ Lemma factorial_up: forall n: nat,
prod_up n 1 = factorial n.
Proof.
intro n.
have (prod_up n 1).
rearrange (prod_up n 1 * 1).
thatis (prod_up n (1 + 0) * factorial 0).
rewrite (prod_up_ratio n 0); have (factorial (n + 0)).
rewrite <- (plus_n_O); have (factorial n).
done.
havelhs (prod_up n 1).
basic_algebra_tells_us_the_lhs_is (prod_up n 1 * 1).
basic_lambda_calculus_tells_us_the_lhs_is (prod_up n (1 + 0) * factorial 0).
pose (Foo := prod_up_ratio n 0).
rewrite Foo; havelhs (factorial (n + 0)).
rewrite <- (plus_n_O); havelhs (factorial n).
obvious.
Qed.
(* Another trick that is implicit in pen-and-paper notation, that we have to be
(* Another trick that is implicit in pen-and-paper notation, that we havelhs to be
explicit about in code, is the fact that we can pull terms off of either
side of this product, to do algebraic manipulations with. *)
@ -400,17 +412,24 @@ Lemma prod_up_down: forall k r: nat,
Proof.
intro k.
induction k; intro r.
*cbn.
havegoal (r + 0 = r * 1).
ring.
*have (prod_up (1 + S k) r).
thatis (prod_up (1 + k) (1 + r) * r).
*both_sides_equal r.
-basic_lambda_calculus_tells_us_the_lhs_is (prod_up 1 r).
basic_lambda_calculus_tells_us_the_lhs_is (r + 0).
basic_algebra_tells_us_the_lhs_is r.
obvious.
-basic_lambda_calculus_tells_us_the_lhs_is (r * prod_up 0 r).
basic_lambda_calculus_tells_us_the_lhs_is (r * 1).
basic_algebra_tells_us_the_lhs_is r.
obvious.
*havelhs (prod_up (1 + S k) r).
basic_lambda_calculus_tells_us_the_lhs_is (prod_up (1 + k) (1 + r) * r).
weknow Ind: (forall r': nat, prod_up (1 + k) r' = (k + r') * prod_up k r').
rewrite (Ind (1 + r)).
have ((k + (1 + r)) * prod_up k (1 + r) * r).
rearrange ((S k + r) * (prod_up k (1 + r) * r)).
thatis ((S k + r) * prod_up (S k) r).
done.
pose (Foo := Ind (1 + r)).
rewrite Foo.
havelhs ((k + (1 + r)) * prod_up k (1 + r) * r).
basic_algebra_tells_us_the_lhs_is ((S k + r) * (prod_up k (1 + r) * r)).
basic_lambda_calculus_tells_us_the_lhs_is ((S k + r) * prod_up (S k) r).
obvious.
Qed.
(* Now let's get to the theorem! I haven't broken this one up at all. Turn your
@ -421,39 +440,45 @@ Theorem pascal_choose: forall r k: nat,
Proof.
intro r.
induction r; intro k.
*cbn.
ring_simplify.
exact (eq_sym (factorial_up k)).
*basic_lambda_calculus_tells_us_the_lhs_is (1 * factorial k).
basic_algebra_tells_us_the_lhs_is (factorial k).
pose (Foo := factorial_up k).
symmetry.
exact Foo.
*induction k.
**cbn.
ring_simplify.
exact (pascal_0 r).
**have (pascal (S r) (S k) * factorial (S k)).
thatis ((pascal (S r) k + pascal r (S k)) * factorial (S k)).
**basic_lambda_calculus_tells_us_the_lhs_is (pascal (S r) 0 * 1).
basic_algebra_tells_us_the_lhs_is (pascal (S r) 0).
pose (Foo := pascal_0 (S r)).
both_sides_equal 1.
-exact Foo.
-basic_lambda_calculus_tells_us_the_lhs_is 1.
obvious.
**havelhs (pascal (S r) (S k) * factorial (S k)).
basic_lambda_calculus_tells_us_the_lhs_is ((pascal (S r) k + pascal r (S k)) * factorial (S k)).
weknow IndR: (forall k': nat, pascal r k' * factorial k' = prod_up k' (S r)).
(* We have a pascal r (S k) and a factorial (S k), let's get them together. *)
rearrange (pascal (S r) k * factorial (S k) + pascal r (S k) * factorial (S k)).
(* We havelhs a pascal r (S k) and a factorial (S k), let's get them together. *)
basic_algebra_tells_us_the_lhs_is (pascal (S r) k * factorial (S k) + pascal r (S k) * factorial (S k)).
rewrite (IndR (S k)).
have (pascal (S r) k * factorial (S k) + prod_up (S k) (S r)).
havelhs (pascal (S r) k * factorial (S k) + prod_up (S k) (S r)).
(* Good. Now, look for similar to apply to pascal (S r) k *)
weknow IndK: (pascal (S r) k * factorial k = prod_up k (S (S r))).
(* So we need factorial k. That can be arranged. *)
thatis (pascal (S r) k * (S k * factorial k) + prod_up (S k) (S r)).
rearrange (S k * (pascal (S r) k * factorial k) + prod_up (S k) (S r)).
basic_lambda_calculus_tells_us_the_lhs_is (pascal (S r) k * (S k * factorial k) + prod_up (S k) (S r)).
basic_algebra_tells_us_the_lhs_is (S k * (pascal (S r) k * factorial k) + prod_up (S k) (S r)).
rewrite (IndK).
have (S k * prod_up k (S (S r)) + prod_up (S k) (S r)).
havelhs (S k * prod_up k (S (S r)) + prod_up (S k) (S r)).
(* This is good. All the factorial pascal stuff is gone. Now we just need
to factorise these big products. They are pretty close already. *)
thatis (S k * prod_up k (S (S r)) + prod_up k (S (S r)) * S r).
basic_lambda_calculus_tells_us_the_lhs_is (S k * prod_up k (S (S r)) + prod_up k (S (S r)) * S r).
(* Let's rewrite these S's. *)
thatis ((1 + k) * prod_up k (2 + r) + prod_up k (2 + r) * (1 + r)).
basic_lambda_calculus_tells_us_the_lhs_is ((1 + k) * prod_up k (2 + r) + prod_up k (2 + r) * (1 + r)).
(* And collect! *)
rearrange ((k + (2 + r)) * prod_up k (2 + r)).
(* And look at that, the coefficients add up to the next factor. *)
rewrite <- (prod_up_down k (2 + r)).
have (prod_up (1 + k) (2 + r)).
thatis (prod_up (S k) (S (S r))).
done.
basic_algebra_tells_us_the_lhs_is ((k + (2 + r)) * prod_up k (2 + r)).
symmetry.
basic_lambda_calculus_tells_us_the_lhs_is (prod_up (S k) (2 + r)).
pose (Foo := prod_up_down k (2 + r)).
basic_lambda_calculus_tells_us_the_lhs_is (prod_up (1 + k) (2 + r)).
exact Foo.
Qed.