Rejig to use 'both_sides_equal' tactic

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! *)
-  done.
+  (* 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).
+  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.
 
-(* 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,15 +212,26 @@ 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. *)
-  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.
+  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
@@ -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.