Prove binomial expansion

Binomial.v

@@ -0,0 +1,130 @@
+Require Import Pascal.
+
+Require Import Ring.
+Require Import ArithRing.
+Require Import Arith.
+
+Fixpoint poly_sum_loop (f: nat -> nat -> nat) (remaining j: nat): nat :=
+  match remaining with
+  | 0 => 0
+  | S i => f i j + poly_sum_loop f i (S j)
+  end.
+
+Definition poly_sum (f: nat -> nat -> nat) (n: nat): nat :=
+  poly_sum_loop f (S n) 0.
+
+Definition binomial_term (a b: nat): nat -> nat -> nat :=
+  fun i j => pascal i j * a^i * b^j.
+
+Definition binomial (a b: nat): nat -> nat :=
+  poly_sum (binomial_term a b).
+
+Lemma binomial_terms_add: forall a b i j: nat,
+  a * binomial_term a b i (S j) + b * binomial_term a b (S i) j = binomial_term a b (S i) (S j).
+Proof.
+  intros.
+  have (a * binomial_term a b i (S j) + b * binomial_term a b (S i) j).
+  thatis (a * (pascal i (S j) * a^i * b^(S j)) + b * (pascal (S i) j * a^(S i) * b^j)).
+  rearrange (pascal i (S j) * (a * a^i) * b^(S j) + pascal (S i) j * a^(S i) * (b * b^j)).
+  thatis (pascal i (S j) * a^(S i) * b^(S j) + pascal (S i) j * a^(S i) * b^(S j)).
+  rearrange ((pascal (S i) j + pascal i (S j)) * a^(S i) * b^(S j)).
+  thatis (pascal (S i) (S j) * a^(S i) * b^(S j)).
+  thatis (binomial_term a b (S i) (S j)).
+  done.
+Qed.
+
+(* We want to show that (a + b) * binomial a b n = binomial a b (S n)
+   but to build this up inductively, we need to look at the partial sum
+   poly_sum_from i j (binomial_term a b) instead. Let's look at i=1.
+
+       poly_sum_from 2 (1+j) (binomial_term a b)
+     = binomial_term a b 1 (1+j) + binomial_term a b 0 (2+j)
+     = pascal 1 (1+j)*a*b^(1+j) + pascal 0 (2+j)*b^(2+j)
+     = (pascal 0 (1+j) + pascal 1 j)*a*b^(1+j) + pascal 0 (1+j)*b^(2+j)
+     = a*(pascal 0 (1+j)*b^(1+j)) + b*(pascal 1 j*a*b^j + pascal 0 (1+j)*b^(1+j))
+     = a*(poly_sum_from 1 (1+j) (binomial_term a b)) + b*(poly_sum_from 2 j (binomial_term a b))
+
+   So this should be our inductive approach. *)
+
+Lemma partial_binomial_equal: forall a b i j: nat,
+  poly_sum_loop (binomial_term a b) (S i) (S j)
+  = a*(poly_sum_loop (binomial_term a b) i (S j))
+    + b*(poly_sum_loop (binomial_term a b) (S i) j).
+Proof.
+  intros a b i.
+  set (f := binomial_term a b).
+  set (loop := poly_sum_loop f).
+  induction i; intro j.
+  *both_sides_equal (b * b^j).
+   -have (loop 1 (S j)).
+    thatis (1*1*b^(S j) + 0).
+    rearrange (b^(S j)).
+    thatis (b * b^j).
+    done.
+   -have (a * loop 0 (S j) + b * loop 1 j).
+    thatis (a * 0 + b * (1*1*b^j + 0)).
+    rearrange (b * b^j).
+    done.
+  *have (loop (S (S i)) (S j)).
+   thatis (binomial_term a b (S i) (S j) + loop (S i) (S (S j))).
+   rewrite <- (binomial_terms_add a b i j).
+   have (a * binomial_term a b i (S j) + b * binomial_term a b (S i) j + loop (S i) (S (S j))).
+   thatis (a * f i (S j) + b * f (S i) j + loop (S i) (S (S j))).
+   weknow Ind: (forall j: nat, loop (S i) (S j) = a * loop i (S j) + b * loop (S i) j).
+   rewrite (Ind (S j)).
+   have (a * f i (S j) + b * f (S i) j + (a * loop i (S (S j)) + b * loop (S i) (S j))).
+   rearrange (a * (f i (S j) + loop i (S (S j))) + b * (f (S i) j + loop (S i) (S j))).
+   thatis (a * (loop (S i) (S j)) + b * (loop (S (S i)) j)).
+   done.
+Qed.
+
+Theorem binomial_step: forall a b n: nat,
+  binomial a b (S n) = (a + b) * binomial a b n.
+Proof.
+  intros.
+  unfold binomial.
+  unfold poly_sum.
+  set (loop := poly_sum_loop (binomial_term a b)).
+  havegoal (loop (S (S n)) 0 = (a + b) * (loop (S n) 0)).
+  (* The LHS naturally splits up into three terms, *)
+  both_sides_equal (a * a^n + a * loop n 1 + b * loop (S n) 0).
+  -have (loop (S (S n)) 0).
+   thatis (binomial_term a b (S n) 0 + loop (S n) 1).
+   thatis ((pascal (S n) 0 * (a * a^n) * 1) + loop (S n) 1).
+   rewrite (pascal_0 (S n)); have ((1 * (a*a^n) * 1) + loop (S n) 1).
+   rearrange (a * a^n + loop (S n) 1).
+   assert (Eq: loop (S n) 1 = a * loop n 1 + b * loop (S n) 0). 
+     { exact (partial_binomial_equal a b n 0). }
+   rewrite Eq; have (a * a^n + (a * loop n 1 + b * loop (S n) 0)).
+   rearrange (a * a^n + a * loop n 1 + b * loop (S n) 0).
+   done.
+  (* The RHS happens to also break down into these three terms. *)
+  -have ((a + b) * loop (S n) 0).
+   rearrange (a * loop (S n) 0 + b * loop (S n) 0).
+   thatis (a * (pascal n 0 * a^n * 1 + loop n 1) + b * loop (S n) 0).
+   rewrite (pascal_0 n); have (a * (1 * a^n * 1 + loop n 1) + b * loop (S n) 0).
+   rearrange (a * a^n + a * loop n 1 + b * loop (S n) 0).
+   done.
+Qed.
+
+Theorem binomial_expansion: forall a b n: nat,
+  (a + b)^n = binomial a b n.
+Proof.
+  intros.
+  induction n.
+  *both_sides_equal 1.
+   -have ((a + b)^0).
+    thatis 1.
+    done.
+   -have (binomial a b 0).
+    thatis (binomial_term a b 0 0 + 0).
+    thatis (1 + 0).
+    thatis 1.
+    done.
+  *have ((a + b)^(S n)).
+   thatis ((a + b) * (a + b)^n).
+   weknow Ind: ((a + b)^n = binomial a b n).
+   rewrite Ind.
+   havegoal ((a + b) * binomial a b n = binomial a b (S n)).
+   exact (eq_sym (binomial_step a b n)).
+Qed.

pascal.v

@@ -1,8 +1,25 @@
 Require Import Ring.
 Require Import ArithRing.
 
-(* Coq is a powerful language, that can search for proofs automatically, and
-   then verify them automatically. This results in proofs like *)
+(* Coq is like Lisp in that it is so powerful, that every user tends to invent
+   a whole new programming language using its features. This makes Lisp by
+   itself an easy tool to misuse, but constrained by an application like CAD or
+   Emacs, it becomes quite a powerful approach for implementing a small
+   language.
+
+   The goal of this file is to consciously and deliberately create a new
+   dialect of proof assistant, constrained by the goal that the proofs should
+   explain themselves as they go, without requiring an IDE, the same way that
+   real life math proofs explain themselves as you read them.
+
+   The two main things that stop an 'idiomatic' Coq proof from being readable
+   without an IDE, are heavy reliance on proof automation, and hidden state
+   that varies from line to line in other terse and clever ways. In general the
+   philosophy of many Coq proofs is, the computer has checked it, so who cares
+   why it is true? This is not going to be our philosophy.
+
+   For an example of both of these weaknesses at their maximum, consider the
+   following Coq proof: *)
 
 Theorem not_not_law_of_excluded_middle: forall A: Prop,
   not (not (A \/ not A)).
@@ -17,21 +34,19 @@ Qed.
    'intuition' tactic, which specializes in intuitionist logic tautologies.
 
    While it is useful to know that Coq *can* go that far with automation, it is
-   important that we remain tasteful in how we apply it. If you are trying to
-   prove something formally, it is usually because you know that it works in
-   some cases, and what you really want to know is *why* those cases work.
+   important that we remain tasteful in how we apply it. Proofs are meant to
+   convince the reader, and ideally to inform them as well. "Look! It type
+   checks!" is convincing, but not informative.
 
-   In particular, in writing proofs about cryptography and number theory, we
-   will happily indulge in proof automation to expand brackets and collect like
-   terms, but the 'control flow' of our proof should be explicit. We want to
-   know what cases we are considering, and why, and what the key insights are
-   that make those mundane algebraic manipulations useful.
+   We will find that proof automation comes in very handy when doing routine
+   algebraic manipulations, but apart from that, the more explicit we can make
+   our control flow, the more informative (and thus useful) our proofs will be.
 
    As an example, let's look at a useful but surprisingly involved inductive
    proof, that all numbers are either even or odd. First let's define what we
-   mean by even and odd.
+   mean by even and odd. *)
 
-   A number is even if it is equal to some other number, doubled. *)
+(* A number is even if it is equal to some other number, doubled. *)
 
 Definition Even (n: nat): Prop :=
   exists k: nat, n = 2 * k.
@@ -71,18 +86,6 @@ Ltac have expr :=
     fail "Goal is not a relation. Goal:" Other
   end.
 
-(* Similarly, this tactic lets us declare what the RHS is, before we do
-   strong manipulations like ring. *)
-Ltac want expr :=
-  lazymatch goal with
-  | |- ?Rel ?L expr =>
-    idtac
-  | |- ?Rel ?L ?R =>
-    fail "Want annotation. Expected" expr "but got" R
-  | |- ?Other =>
-    fail "Goal is not a relation. Goal:" Other
-  end.
-
 (* 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 :=
@@ -94,6 +97,13 @@ 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
+   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. *)
+Ltac both_sides_equal expr :=
+  transitivity expr; [ | symmetry].
+
 (* 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. *)
@@ -113,45 +123,49 @@ Lemma zero_is_even_explicit: Even 0.
 Proof.
   (* We still need to pick a value for k. *)
   exists 0.
-  (* Now let's fill our goal a little more explicitly. *)
-  want (2 * 0).
-  have 0.
-  (* So that is our RHS and LHS... How are we ever going to connect them?
-     Well let's compute our LHS a little! *)
-  thatis (2 * 0).
-  (* And that matches our goal! Look! *)
+  (* Now let's prove our goal a little more explicitly. *)
+  both_sides_equal 0.
+  -have 0.
+   done.
+  -have (2 * 0).
+   thatis 0.
    done.
 Qed.
 
-(* Probably overkill for that case, and frankly unintuitive when all the
-   computation happens on the RHS. Oh well, let's try something more involved. *)
+(* This case might be sort of overkill... As one gains/regains familiarity with
+   DTT, statements like "eq_refl is a proof that 0 = 2 * 0" becomes totally
+   intuitive, but still, these tactics hopefully explain why.
+
+   Now let's do something where this is a little less overkill, showing that if
+   a number is even, then the next number is odd.
+
+   S is the successor, in Peano arithmetic, and inductive proofs. *)
 
 Lemma even_implies_odd: forall n: nat,
   Even n -> Odd (S n).
 Proof.
   intros n IsEven.
   destruct IsEven as [k Eq].
-  (* n is 2 * k, and we need to show that n+1 = 2*k' + 1, I wonder what k' can
-     be? *)
+  (* n is 2 * k, so n+1 is 2 * k + 1, so k is the value we need to prove that
+     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.
-  want (2 * k + 1).
+  (* Now we actually have to prove that S n = 2 * k + 1, though. *)
   have (S n).
-  (* Now let's do some real tactical proving! The equation that proves n is
-     even can now be used to manipulate our term. *)
   rewrite Eq.
-  (* Now let's see what that did to our LHS. *)
   have (S (2 * k)).
-  (* This isn't quite our LHS. Let's dig into some natural number identities. *)
-  rewrite (plus_n_O (2 * k)) at 1.
-  have (S (2 * k + 0)).
-  rewrite (plus_n_Sm (2 * k) 0).
+  thatis (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.
 Qed.
 
-(* Rewriting n into 2 * k with these tactics was nice, but the identities at
-   the end sucked. Let's bring back a little more automation; just enough to do
-   algebra, but without hiding any important control flow. *)
+(* 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
+   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 :=
   lazymatch goal with
@@ -161,8 +175,9 @@ Ltac rearrange expr :=
     fail "Goal is not a relation. Goal:" Other
   end.
 
-(* Before we try using this one, let's also define some things that will help
-   us annotate these Even/Odd/exists manipulations. *)
+(* 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. *)
 
 (* If our goal isn't a relation yet, we might still want to declare it. *)
 Ltac havegoal expr :=
@@ -197,14 +212,25 @@ Proof.
   destruct IsOdd as [k].
   havegoal (Even (S n)).
   weknow OddEq: (n = 2 * k + 1).
-  (* From now on let's do the goal manipulation, and then justify it afterwards
-     by annotating what our goal is now. *)
+  (* 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).
-  have (S n).
-  (* Let's also combine rewrites with the new expression, if they'll fit on one line. *)
+  both_sides_equal (2 * k + 2).
+  -have (S n).
+   (* Let's also annotate rewrites on the same line, if it will fit. *)
    rewrite OddEq; have (S (2 * k + 1)).
-  (* Now let's write the algebra we would write on paper, and let Coq justify it. *)
-  rearrange (2 * S k).
+   (* 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).
+   (* Now let's get Coq to prove our algebra for us! *)
+   rearrange (2 * k + 2).
+   done.
+  -have (2 * S k).
+   (* Again, get rid of the S. *)
+   thatis (2 * (1 + k)).
+   (* And rearrange. *)
+   rearrange (2 * k + 2).
    done.
 Qed.
 
@@ -216,16 +242,25 @@ 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
+     then that it is true for any number of the form S n. *)
   *havegoal (Even 0 \/ Odd 0).
    left; havegoal (Even 0).
    exact zero_is_even.
   *havegoal (Even (S n) \/ Odd (S n)).
    weknow Ind: (Even n \/ Odd n).
+   (* To prove that S n is even or odd, we need to know which case we are in
+      when it comes to n being even or odd. *)
    destruct Ind.
    +weknow IsEven: (Even n).
+    (* We can use the 'left' and 'right' tactics to choose how we are going to
+       prove a dysjunction. *)
     right; havegoal (Odd (S n)).
+    (* We are appealing to a lemma, so get the Curry-Howard proof object for
+       that lemma, and apply it to produce the 'exact' proof we need. *)
     exact (even_implies_odd n IsEven).
    +weknow IsOdd: (Odd n).
+    (* Very similar logic on the other side. *)
     left; havegoal (Even (S n)).
     exact (odd_implies_even n IsOdd).
 Qed.
@@ -239,8 +274,8 @@ Qed.
    Agda and Idris programmers will recognize that Even and Odd could have 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, but for this simple example, having suboptimal definitions was useful
-   as it motivated us to learn how to make Coq do the boring parts for us. *)
+   hard, it's useful to embrace these un-optimized definitions when trying to
+   demonstrate Coq tactics. *)
 
 
 
@@ -295,7 +330,8 @@ Proof.
   *have (pascal (S r) 0).
    thatis (series (pascal r) 0).
    thatis (pascal r 0).
-   want 1.
+   (* 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).
    exact Ind.
 Qed.
@@ -334,6 +370,8 @@ Proof.
    thatis (prod_up k (1 + (1 + r)) * factorial (1 + r)).
    rewrite (Ind (1 + r)); have (factorial (k + (1 + r))).
    thatis (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.