Require Import Ring.
Require Import ArithRing.

(* 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)).
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. Proofs are meant to
   convince the reader, and ideally to inform them as well. "Look! It type
   checks!" is convincing, but not informative.

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

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

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

(* 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. *)
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 prove our goal a little more explicitly. *)
  both_sides_equal 0.
  -have 0.
   done.
  -have (2 * 0).
   thatis 0.
   done.
Qed.

(* 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, 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.
  (* Now we actually have to prove that S n = 2 * k + 1, though. *)
  have (S n).
  rewrite Eq.
  have (S (2 * k)).
  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.

(* 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
  | |- ?Rel ?L ?R =>
    transitivity expr; [> ring | ]
  | |- ?Other =>
    fail "Goal is not a relation. Goal:" Other
  end.

(* 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 :=
  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).
  (* 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).
  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)).
   (* 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.

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

(* 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, it's useful to embrace these un-optimized definitions when trying to
   demonstrate Coq tactics. *)



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

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