number-theory/pascal.v

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 *)

Theorem not_not_law_of_excluded_middle: forall A: Prop,
  not (not (A \/ not A)).
Proof.
  intros A H.
  assert (not A); auto.
Qed.

(* How does this proof work? Who knows! You'll have 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
   '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.

   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.

   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.

   A number is even if it is equal to some other number, doubled. *)

Definition Even (n: nat): Prop :=
  exists k: nat, n = 2 * k.

(* And a number is odd if it is one more than that. *)

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
   case for induction later. *)

Lemma zero_is_even: Even 0.
Proof.
  (* We need to find a k so that 2 * k = 0. Let's try.... 0 *)
  exists 0.
  (* Now to show that 2 * 0 = 0, we let Coq beta/eta reduce it to 0 = 0, and
     then fall back to 'reflexivity', the defining property of Leibniz equality. *)
  reflexivity.
Qed.

(* It is annoying that we have 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
   let us represent this information better. *)

(* 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 :=
  lazymatch goal with
  | |- ?Rel expr ?R =>
    idtac
  | |- ?Rel ?L ?R =>
    fail "Have annotation. Expected" expr "but got" L
  | |- ?Other =>
    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 :=
  lazymatch goal with
  | |- ?Rel ?L ?R =>
    unify L expr;
    change_no_check (Rel expr R)
  | |- ?Other =>
    fail "Goal is not a relation. Goal:" Other
  end.

(* 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 :=
  lazymatch goal with
  | |- ?Rel ?L ?L =>
    reflexivity
  | |- ?Rel ?L ?R =>
    fail "Chain derivation not done. Left:" L "Right:" R
  | |- ?Other =>
    fail "Goal is not a relation. Goal:" Other
  end.

(* Let's try again at that simple zero example, but with annotations. *)

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! *)
  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. *)

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? *)
  exists k.
  want (2 * k + 1).
  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).
  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. *)

Ltac rearrange expr :=
  lazymatch goal with
  | |- ?Rel ?L ?R =>
    transitivity expr; [> ring | ]
  | |- ?Other =>
    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. *)

(* If our goal isn't a relation yet, we might still want to declare it. *)
Ltac havegoal expr :=
  lazymatch goal with
  | |- expr =>
    idtac
  | |- ?Other =>
    fail "Expected goal to be" expr "but it was" Other
  end.

(* The place where we learn new equations is often quite far from where we
   use them. This tactic lets us state in-context what hypothesis we are
   using, and defer choosing a name for it until then as well. *)
Ltac weknow newid P :=
  lazymatch goal with
  | proof: P |- ?Goal =>
    rename proof into newid
  | |- ?Goal =>
    fail "Knowledge assertion. Cannot find proof of" P
  end.

Tactic Notation "weknow" ident(newid) ":" constr(P) :=
  weknow newid P.

(* We're going to need these for odd_implies_even, as that case is harder! *)

Lemma odd_implies_even: forall n: nat,
  Odd n -> Even (S n).
Proof.
  intros.
  weknow IsOdd: (Odd n).
  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. *)
  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. *)
  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).
  done.
Qed.

(* You might see where this is going now. We have all the pieces to build an
   inductive proof! *)

Theorem even_or_odd: forall n: nat,
  Even n \/ Odd n.
Proof.
  intro n.
  induction 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).
   destruct Ind.
   +weknow IsEven: (Even n).
    right; havegoal (Odd (S n)).
    exact (even_implies_odd n IsEven).
   +weknow IsOdd: (Odd n).
    left; havegoal (Even (S n)).
    exact (odd_implies_even n IsOdd).
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
   is prepared to do for us.

   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. *)



(* Now, finally, let's get on with some number theory! First let's look at
   Pascal's triangle, since understanding that turns out to be essential to
   understanding how to find points on elliptic curves.

   Our way of indexing Pascal's triangle is going to be a little weird, though;
   in order to avoid having to make special cases for all the zeros to the left
   and right of the triangle, we will index the triangle in diagonal strips, so
   e.g. 
     pascal 0 _ = 1
     pascal 1 k = k
     pascal 2 k = k*(k+1)/2
     pascal 3 k = k*(k+1)*(k+2)/6
   etc.

   To do this without getting dizzy over nested cases, let's get dizzy 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. *)

Fixpoint partial_sum (seq: nat -> nat) (count: nat): nat :=
  match count with
  | O => 0
  | S count' => partial_sum seq count' + seq count'
  end.

(* But Triangular numbers aren't the sum of 0 or more numbers, they are the sum
   of one or more numbers! So let's also define a 'series' variation. *)

Definition series (seq: nat -> nat) (index: nat): nat :=
  partial_sum seq (1 + index).

Fixpoint pascal (r: nat): nat -> nat :=
  match r with
  | 0 => fun _ => 1
  | S r' => series (pascal r')
  end.

(* Now the first 'row' of our function is all 1 by definition, but it is useful
   to show that the first 'column' is all 1 as well. *)

Lemma pascal_0: forall r: nat,
  pascal r 0 = 1.
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).
   want 1.
   weknow Ind: (pascal r 0 = 1).
   exact Ind.
Qed.

(* Next let's define some combinatoric functions, and see if we can't prove how
   they relate to the recursive formula above. *)

Fixpoint factorial (n : nat): nat :=
  match n with
  | S n' => n * factorial n'
  | O => 1
  end.

Fixpoint prod_up (k r: nat): nat :=
  match k with
  | 0 => 1
  | S k' => prod_up k' (1 + r) * r
  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
   through multiplication instead. *)

Lemma prod_up_ratio: forall k r: nat,
  prod_up k (1 + r) * factorial r = factorial (k + r).
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).
   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)).
   rewrite <- (plus_n_Sm k r); have (factorial (S (k + r))).
   thatis (factorial (S k + r)).
   done.
Qed.

(* If we let r = 0 then we even show that the factorial is a special case of
   this product function. *)
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.
Qed.

(* Another trick that is implicit in pen-and-paper notation, that we have 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. *)

Lemma prod_up_down: forall k r: nat,
  prod_up (1 + k) r = (k + r) * prod_up k r.
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).
   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.
Qed.

(* Now let's get to the theorem! I haven't broken this one up at all. Turn your
   font up or something. *)

Theorem pascal_choose: forall r k: nat,
  pascal r k * factorial k = prod_up k (S r).
Proof.
  intro r.
  induction r; intro k.
  *cbn.
   ring_simplify.
   exact (eq_sym (factorial_up k)). 
  *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)).
    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)).
    rewrite (IndR (S k)).
    have (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)).
    rewrite (IndK).
    have (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).
    (* Let's rewrite these S's. *)
    thatis ((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.
Qed.