diff --git a/pascal.v b/pascal.v index 1cf0fcb..6f84a20 100644 --- a/pascal.v +++ b/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.