pascal-prh.v

@@ -0,0 +1,485 @@
+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 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 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
+   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 havelhs 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 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
+   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 havelhs 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 basic_lambda_calculus_tells_us_the_lhs_is 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 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. *)
+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 obvious :=
+  lazymatch goal with
+  | |- ?Rel ?L ?L =>
+    reflexivity
+  | |- ?Rel ?L ?R =>
+    fail "Chain derivation not obvious. 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.
+  -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
+   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 havelhs to prove that S n = 2 * k + 1, though. *)
+  havelhs (S n).
+  rewrite Eq.
+  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 _ _).
+  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 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 basic_algebra_tells_us_the_lhs_is 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 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 :=
+  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. *)
+  unfold Even.
+  exists (S k).
+  havegoal (S n = 2 * S k).
+  both_sides_equal (2 * k + 2).
+  -havelhs (S n).
+   (* Let's also annotate rewrites on the same line, if it will fit. *)
+   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. *)
+   basic_lambda_calculus_tells_us_the_lhs_is (1 + 2 * k + 1).
+   (* Now let's get Coq to prove our algebra for us! *)
+   basic_algebra_tells_us_the_lhs_is (2 * k + 2).
+   obvious.
+  -havelhs (2 * S k).
+   (* Again, get rid of the S. *)
+   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 havelhs 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 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).
+   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).
+    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)).
+    (* 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).
+    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).
+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 basic algebra, algebra which Coq
+   is prepared to do for us.
+
+   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
+   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 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. *)
+
+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.
+  *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).
+   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 havelhs 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.
+  *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')).
+   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).
+   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
+   this product function. *)
+Lemma factorial_up: forall n: nat,
+  prod_up n 1 = factorial n.
+Proof.
+  intro n.
+  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 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. *)
+
+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.
+  *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').
+   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
+   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.
+  *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.
+  **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 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)).
+    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. *)
+    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).
+    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. *)
+    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. *)
+    basic_lambda_calculus_tells_us_the_lhs_is ((1 + k) * prod_up k (2 + r) + prod_up k (2 + r) * (1 + r)).
+    (* And collect! *)
+    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.
+
+
+

pascal.v

@@ -28,9 +28,9 @@ Proof.
   assert (not A); auto.
 Qed.
 
-(* How does this proof work? Who knows! You'll havelhs to run `debug auto`
+(* 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 havelhs been replaced with a single
+   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
@@ -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 havelhs a base
+(* 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.
@@ -68,7 +68,7 @@ Proof.
   reflexivity.
 Qed.
 
-(* It is annoying that we havelhs to write all of these comments to explain what
+(* 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
@@ -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 havelhs expr :=
+Ltac have expr :=
   lazymatch goal with
   | |- ?Rel expr ?R =>
     idtac
@@ -88,7 +88,7 @@ Ltac havelhs 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 basic_lambda_calculus_tells_us_the_lhs_is expr :=
+Ltac thatis expr :=
   lazymatch goal with
   | |- ?Rel ?L ?R =>
     unify L expr;
@@ -97,7 +97,7 @@ Ltac basic_lambda_calculus_tells_us_the_lhs_is expr :=
     fail "Goal is not a relation. Goal:" Other
   end.
 
-(* Using basic_lambda_calculus_tells_us_the_lhs_is makes it easy to annotate how an expression simplifies as it is
+(* 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. *)
@@ -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 obvious :=
+Ltac done :=
   lazymatch goal with
   | |- ?Rel ?L ?L =>
     reflexivity
   | |- ?Rel ?L ?R =>
-    fail "Chain derivation not obvious. Left:" L "Right:" R
+    fail "Chain derivation not done. 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.
-  -havelhs 0.
+  -have 0.
-   obvious.
+   done.
-  -havelhs (2 * 0).
+  -have (2 * 0).
-   basic_lambda_calculus_tells_us_the_lhs_is 0.
+   thatis 0.
-   obvious.
+   done.
 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 havelhs to prove that S n = 2 * k + 1, though. *)
+  (* Now we actually have to prove that S n = 2 * k + 1, though. *)
-  havelhs (S n).
+  have (S n).
   rewrite Eq.
-  havelhs(S (2 * k)).
+  have (S (2 * k)).
-  basic_lambda_calculus_tells_us_the_lhs_is (1 + 2 * k).
+  thatis (1 + 2 * k).
   (* This is almost what we want. Let's do a commutativity rewrite. *)
   rewrite (PeanoNat.Nat.add_comm _ _).
-  havelhs(2 * k + 1).
+  have (2 * k + 1).
-  obvious.
+  done.
 Qed.
 
 (* Having these tactics definitely makes the control flow easier to follow, but
-   it would be nice if we didn't havelhs to appeal to the laws of associativity
+   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 basic_algebra_tells_us_the_lhs_is expr :=
+Ltac rearrange expr :=
   lazymatch goal with
   | |- ?Rel ?L ?R =>
     transitivity expr; [> ring | ]
@@ -177,7 +177,7 @@ Ltac basic_algebra_tells_us_the_lhs_is 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 havelhs to prove, as each of these things change from line to line. *)
+   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 :=
@@ -214,29 +214,27 @@ 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. *)
-  unfold Even.
+  exists (S k); havegoal (S n = 2 * S k).
-  exists (S k).
-  havegoal (S n = 2 * S k).
   both_sides_equal (2 * k + 2).
-  -havelhs (S n).
+  -have (S n).
    (* Let's also annotate rewrites on the same line, if it will fit. *)
-   rewrite OddEq; havelhs (S (2 * k + 1)).
+   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. *)
-   basic_lambda_calculus_tells_us_the_lhs_is (1 + 2 * k + 1).
+   thatis (1 + 2 * k + 1).
    (* Now let's get Coq to prove our algebra for us! *)
-   basic_algebra_tells_us_the_lhs_is (2 * k + 2).
+   rearrange (2 * k + 2).
-   obvious.
+   done.
-  -havelhs (2 * S k).
+  -have (2 * S k).
    (* Again, get rid of the S. *)
-   basic_lambda_calculus_tells_us_the_lhs_is (2 * (1 + k)).
+   thatis (2 * (1 + k)).
-   (* And basic_algebra_tells_us_the_lhs_is. *)
+   (* And rearrange. *)
-   basic_algebra_tells_us_the_lhs_is (2 * k + 2).
+   rearrange (2 * k + 2).
-   obvious.
+   done.
 Qed.
 
-(* You might see where this is going now. We havelhs all the pieces to build an
+(* 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,
@@ -244,7 +242,7 @@ Theorem even_or_odd: forall n: nat,
 Proof.
   intro n.
   induction n.
-  (* To prove something inductively, we havelhs to prove it is true for 0, and
+  (* 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).
@@ -255,7 +253,6 @@ 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)).
@@ -263,7 +260,6 @@ 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).
@@ -272,10 +268,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 basic algebra, algebra which Coq
+   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 havelhs been
+   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
@@ -297,7 +293,7 @@ Qed.
      pascal 3 k = k*(k+1)*(k+2)/6
    etc.
 
-   To do this without getting horny over nested cases, let's get horny over
+   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. *)
@@ -328,12 +324,12 @@ Lemma pascal_0: forall r: nat,
 Proof.
   intro r.
   induction r.
-  *havelhs (pascal 0 0).
+  *have (pascal 0 0).
-   basic_lambda_calculus_tells_us_the_lhs_is 1.
+   thatis 1.
-   obvious.
+   done.
-  *havelhs (pascal (S r) 0).
+  *have (pascal (S r) 0).
-   basic_lambda_calculus_tells_us_the_lhs_is (series (pascal r) 0).
+   thatis (series (pascal r) 0).
-   basic_lambda_calculus_tells_us_the_lhs_is (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).
@@ -356,7 +352,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 havelhs division in peano arithmetic, so let's show this relation
+   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,
@@ -364,28 +360,21 @@ Lemma prod_up_ratio: forall k r: nat,
 Proof.
   intros k.
   induction k; intro r.
-  *both_sides_equal (factorial r).
+  *cbn.
-   -basic_lambda_calculus_tells_us_the_lhs_is (1 * factorial r).
+   havegoal (factorial r + 0 = factorial r).
-    basic_algebra_tells_us_the_lhs_is (factorial r).
+   ring.
-    obvious.
+  *have (prod_up (S k) (1 + r) * factorial r).
-   -havelhs (factorial (0 + r)).
+   thatis (prod_up k (2 + r) * (1 + r) * factorial 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')).
-   basic_algebra_tells_us_the_lhs_is (prod_up k (2 + r) * ((1 + r) * factorial r)).
+   rearrange (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)).
+   thatis (prod_up k (1 + (1 + r)) * factorial (1 + r)).
-   pose (NigFace := Ind (1 + r)).
+   rewrite (Ind (1 + r)); have (factorial (k + (1 + r))).
-   rewrite NigFace.
+   thatis (factorial (k + S r)).
-   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).
+   rewrite <- (plus_n_Sm k r); have (factorial (S (k + r))).
-   havelhs (factorial (S (k + r))).
+   thatis (factorial (S k + r)).
-   basic_lambda_calculus_tells_us_the_lhs_is (factorial (S k + r)).
+   done.
-   obvious.
 Qed.
 
 (* If we let r = 0 then we even show that the factorial is a special case of
@@ -394,16 +383,15 @@ Lemma factorial_up: forall n: nat,
   prod_up n 1 = factorial n.
 Proof.
   intro n.
-  havelhs (prod_up n 1).
+  have (prod_up n 1).
-  basic_algebra_tells_us_the_lhs_is (prod_up n 1 * 1).
+  rearrange (prod_up n 1 * 1).
-  basic_lambda_calculus_tells_us_the_lhs_is (prod_up n (1 + 0) * factorial 0).
+  thatis (prod_up n (1 + 0) * factorial 0).
-  pose (Foo := prod_up_ratio n 0).
+  rewrite (prod_up_ratio n 0); have (factorial (n + 0)).
-  rewrite Foo; havelhs (factorial (n + 0)).
+  rewrite <- (plus_n_O); have (factorial n).
-  rewrite <- (plus_n_O); havelhs (factorial n).
+  done.
-  obvious.
 Qed.
 
-(* Another trick that is implicit in pen-and-paper notation, that we havelhs to be
+(* 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. *)
 
@@ -412,24 +400,17 @@ Lemma prod_up_down: forall k r: nat,
 Proof.
   intro k.
   induction k; intro r.
-  *both_sides_equal r.
+  *cbn.
-   -basic_lambda_calculus_tells_us_the_lhs_is (prod_up 1 r).
+   havegoal (r + 0 = r * 1).
-    basic_lambda_calculus_tells_us_the_lhs_is (r + 0).
+   ring.
-    basic_algebra_tells_us_the_lhs_is r.
+  *have (prod_up (1 + S k) r).
-    obvious.
+   thatis (prod_up (1 + k) (1 + r) * r).
-   -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').
-   pose (Foo := Ind (1 + r)).
+   rewrite (Ind (1 + r)).
-   rewrite Foo.
+   have ((k + (1 + r)) * prod_up k (1 + r) * r).
-   havelhs ((k + (1 + r)) * prod_up k (1 + r) * r).
+   rearrange ((S k + r) * (prod_up k (1 + r) * r)).
-   basic_algebra_tells_us_the_lhs_is ((S k + r) * (prod_up k (1 + r) * r)).
+   thatis ((S k + r) * prod_up (S k) r).
-   basic_lambda_calculus_tells_us_the_lhs_is ((S k + r) * prod_up (S k) r).
+   done.
-   obvious.
 Qed.
 
 (* Now let's get to the theorem! I haven't broken this one up at all. Turn your
@@ -440,45 +421,39 @@ Theorem pascal_choose: forall r k: nat,
 Proof.
   intro r.
   induction r; intro k.
-  *basic_lambda_calculus_tells_us_the_lhs_is (1 * factorial k).
+  *cbn.
-   basic_algebra_tells_us_the_lhs_is (factorial k).
+   ring_simplify.
-   pose (Foo := factorial_up k).
+   exact (eq_sym (factorial_up k)). 
-   symmetry.
-   exact Foo. 
   *induction k.
-  **basic_lambda_calculus_tells_us_the_lhs_is (pascal (S r) 0 * 1).
+  **cbn.
-    basic_algebra_tells_us_the_lhs_is (pascal (S r) 0).
+    ring_simplify.
-    pose (Foo := pascal_0 (S r)).
+    exact (pascal_0 r).
-    both_sides_equal 1.
+  **have (pascal (S r) (S k) * factorial (S k)).
-    -exact Foo.
+    thatis ((pascal (S r) k + pascal r (S k)) * factorial (S k)).
-    -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 havelhs a pascal r (S k) and a factorial (S k), let's get them together. *)
+    (* We have 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)).
+    rearrange (pascal (S r) k * factorial (S k) + pascal r (S k) * factorial (S k)).
     rewrite (IndR (S k)).
-    havelhs (pascal (S r) k * factorial (S k) + prod_up (S k) (S r)).
+    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. *)
-    basic_lambda_calculus_tells_us_the_lhs_is (pascal (S r) k * (S k * factorial k) + prod_up (S k) (S r)).
+    thatis (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)).
+    rearrange (S k * (pascal (S r) k * factorial k) + prod_up (S k) (S r)).
     rewrite (IndK).
-    havelhs (S k * prod_up k (S (S r)) + prod_up (S k) (S r)).
+    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. *)
-    basic_lambda_calculus_tells_us_the_lhs_is (S k * prod_up k (S (S r)) + prod_up k (S (S r)) * S r).
+    thatis (S k * prod_up k (S (S r)) + prod_up k (S (S r)) * S r).
     (* Let's rewrite these S's. *)
-    basic_lambda_calculus_tells_us_the_lhs_is ((1 + k) * prod_up k (2 + r) + prod_up k (2 + r) * (1 + r)).
+    thatis ((1 + k) * prod_up k (2 + r) + prod_up k (2 + r) * (1 + r)).
     (* And collect! *)
-    basic_algebra_tells_us_the_lhs_is ((k + (2 + r)) * prod_up k (2 + r)).
+    rearrange ((k + (2 + r)) * prod_up k (2 + r)).
-    symmetry.
+    (* And look at that, the coefficients add up to the next factor. *)
-    basic_lambda_calculus_tells_us_the_lhs_is (prod_up (S k) (2 + r)).
+    rewrite <- (prod_up_down k (2 + r)).
-    pose (Foo := prod_up_down k (2 + r)).
+    have (prod_up (1 + k) (2 + r)).
-    basic_lambda_calculus_tells_us_the_lhs_is (prod_up (1 + k) (2 + r)).
+    thatis (prod_up (S k) (S (S r))).
-    exact Foo.
+    done.
 Qed.