Templates for informal proofs by induction

In the real world of mathematical communication, written proofs range from extremely longwinded and pedantic to extremely brief and telegraphic. The ideal is probably somewhere in between, but while you are getting used to the style it is better to start out at the pedantic end. Also, during the learning phase, it is probably helpful to have a clear standard to compare against. So...

For the rest of the course, ALL your inductive proofs should match one of the two following templates.

1) TEMPLATE FOR INFORMAL PROOFS BY INDUCTION OVER AN INDUCTIVELY DEFINED SET:

THEOREM: <Universally quantified proposition of the form "For all n:S, P(n)," where S is some inductively defined set.>

PROOF: By induction on n.

<one case for each constructor c of S...>

• Suppose n = c a1 ... ak, where <...and here we state the IH for each of the a's that has type S, if any>. We must show <...and here we restate P(c a1 ... ak)>.
  
  <go on and prove P(n) to finish the case...>
  
  
• <other cases similarly...> ☐

EXAMPLE

THEOREM: For all sets X, lists l : list X, and numbers n, if length l = n then index (S n) l = None.

PROOF: By induction on l.

• Suppose l = []. We must show, for all numbers n, that, if length [] = n, then index (S n) [] = None.
  
  This follows immediately from the definition of index.
  
  
• Suppose l = x :: l' for some x and l', where length l' = n' implies index (S n') l' = None, for any number n'. We must show, for all n, that, if length (x::l') = n then index (S n) (x::l') = None.
  
  Let n be a number with length l = n. Since
  
            length l = length (x::l') = S (length l'),
  
  it suffices to show that
  
            index (S (length l')) l' = None.
  
  But this follows directly from the induction hypothesis, picking n' to be length l'. ☐

2) TEMPLATE FOR INFORMAL PROOFS BY INDUCTION OVER AN INDUCTIVELY DEFINED PROPOSITION (I.E., "INDUCTION ON DERIVATIONS"):

THEOREM: <Proposition of the form "Q -> P," where Q is some inductively defined proposition. (More generally, "For all x y z, Q x y z -> P x y z.">

PROOF: By induction on a derivation of Q. <Or, more generally, "Suppose we are given x, y, and z. We show that Q x y z implies P x y z, by induction on a derivation of Q x y z"...>

<one case for each constructor c of Q...>

• Suppose the final rule used to show Q is c. Then <...and here we state the types of all of the a's together with any equalities that follow from the definition of the constructor and the IH for each of the a's that has type Q, if there are any>. We must show <...and here we restate P>.
  
  <go on and prove P to finish the case...>
  
  
• <other cases similarly...> ☐

EXAMPLE

THEOREM: The <= relation is transitive -- i.e., for all numbers n, m, and o, if n <= m and m <= o, then n <= o.

PROOF: By induction on a derivation of m <= o.

• Suppose the final rule used to show m <= o is le_n. Then m = o and the result is immediate.
  
  
• Suppose the final rule used to show m <= o is le_S. Then o = S o' for some o' with m <= o'. By induction hypothesis, n <= o'.
  
  But then, by le_S, n <= o. ☐

Evaluating arithmetic expressions

Since we're going to be writing a lot of these arithmetic expressions, let's introduce some concrete syntax that's nicer to look at.

Correctness of a simple optimization

Tacticals

The repetition in this last proof is starting to be a little annoying. It's still bearable here, but clearly, if either the language of arithmetic expressions or the optimization being proved sound were significantly more complex, it would start to be a real problem.

So far, we've been doing all our proofs using just a small handful of Coq's tactics and completely ignoring its very powerful facilities for constructing proofs automatically. This section introduces some of these facilities, and we will see more over the next several chapters. Getting used to them will take some energy -- Coq's automation is a power tool -- but it will allow us to scale up our efforts to more complex definitions and more interesting properties without becoming overwhelmed by boring, repetitive, or low-level details.

"Tactical" is Coq's term for operations that manipulate tactics -- higher-order tactics, if you will.

The try tactical

One very simple tactical is try: If T is a tactic, then try T is a tactic that is just like T except that, if T fails, try T does nothing at all (instead of failing).

The ; tactical

Another very basic tactical is written ;. If T, T1, ..., Tn are tactics, then

      T; [T1 | T2 | ... | Tn]

is a tactic that first performs T and then performs T1 on the first subgoal generated by T, performs T2 on the second subgoal, etc.

In the special case where all of the Tis are the same tactic T', we can just write T;T' instead of:

      T; [T' | T' | ... | T']

That is, if T and T' are tactics, then T;T' is a tactic that first performs T and then performs T' on EACH SUBGOAL generated by T. This is the form of ; that is used most often in practice.

For example, consider the following trivial lemma

We can simplify the proof above using ;

For a more interesting example of ;, consider the following proof...

Using try and ; together, we can get rid of the repetition in the above proof.

In practice, Coq experts often use try with a tactic like induction to take care of many similar "straightforward" cases all at once. Naturally, this practice has an analog in informal proofs. Here is an informal proof of our example theorem that matches the structure of the formal one:

Theorem: For all arithmetic expressions e,

       aeval (optimize_0plus e) = aeval e.

Proof: By induction on e. The AMinus and AMult cases follow directly from the IH. The remaining cases are as follows:

• Suppose e = ANum n for some n. We must show
  
            aeval (optimize_0plus (ANum n)) = aeval (ANum n).
  
  This is immediate from the definition of optimize_0plus.
  
  
• Suppose e = APlus e1 e2 for some e1 and e2. We must show
  
            aeval (optimize_0plus (APlus e1 e2))
          = aeval (APlus e1 e2).
  
  Consider the possible forms of e1. For most of them, optimize_0plus simply calls itself recursively for the subexpressions and rebuilds a new expression of the same form as e1; in these cases, the result follows directly from the IH.
  
  The interesting case is when e1 = ANum n for some n. If n = ANum 0, then
  
            optimize_0plus (APlus e1 e2) = optimize_0plus e2
  
  and the IH for e2 is exactly what we need. On the other hand, if n = S n' for some n', then again optimize_0plus simply calls itself recursively, and the result follows from the IH. ☐

This proof can still be improved: the first case (for e = ANum n) is very trivial -- even more trivial than the cases that we said simply followed from the IH -- yet we have chosen to write it out in full. It would be better and clearer to drop it and just say, at the top, "Most cases are either immediate or direct from the IH. The only interesting case is the one for APlus..."

Of course, we'd like to do the same thing in our formal proof too! Here's how this looks:

Defining new tactic notations

Coq also provides some handy ways to define "shorthand tactics" that, when invoked, apply several tactics at the same time.

Here's a more interesting use of this feature...

Bulletproofing case analyses

Being able to deal with most of the cases of an induction or destruct all at the same time is very convenient, but it can also be a little confusing. One problem that often comes up is that maintaining proofs written in this style can be difficult. For example, suppose that, later, we extended the definition of aexp with another constructor that also required a special argument. The above proof might break because Coq generated the subgoals for this constructor before the one for APlus, so that, at the point when we start working on the APlus case, Coq is actually expecting the argument for a completely different constructor. What we'd like is to get a sensible error message saying "I was expecting the AFoo case at this point, but the proof script is talking about APlus." Here's a nice little trick that smoothly achieves this.

If e is a variable of type aexp, then doing

      aexp_cases (induction e) (Case)

will perform an induction on e (the same as if we had just typed induction e) and also add a Case tag to each subgoal labeling which constructor it comes from.

Exercise: 3 stars (optimize_0plus_b)

Since the optimize_0plus tranformation doesn't change the value of aexps, we should be able to apply it to all the aexps that appear in a bexp without changing the bexp's value. Write a function which performs that transformation on bexps, and prove it is sound. Use the tacticals we've just seen to make the proof as elegant as possible.

☐

Exercise: 4 stars (optimizer)

DESIGN EXERCISE: The optimization implemented by our optimize_0plus function is only one of many imaginable optimizations on arithmetic and boolean expressions. Write a more sophisticated optimizer and prove it correct.

(* FILL IN HERE *)

☐

A couple more handy tactics

• clear H
  
  remove hypothesis H from the context
  
  
• subst x
  
  find an assumption x = e or e = x in the context, replace x with e throughout the context and current goal, and clear the assumption
  
  
• subst
  
  substitute away all assumptions of the form x = e or e = x
  
  
• assumption
  
  tries to find a hypothesis H in the context that exactly matches the goal; if one is found, behaves just like apply H

We'll see many examples of these in the proofs below...

While programs

Mappings

In the rest of the course, we'll often need to talk about "identifiers," such as program variables. We could use strings for this, or (as in a real compiler) some kind of fancier structures like symbols from a symbol table. For simplicity, though, let's just use natural numbers as identifiers. We define a new inductive datatype so that we won't confuse identifiers and numbers.

Exercise: 1 star

☐

Exercise: 1 star

☐

Exercise: 1 star

☐

Operations on States

Next, we redefine basic operations on states to use the new definition of ids

Exercise: 2 stars

☐

Exercise: 2 stars, optional

Before starting to play with tactics, make sure you understand exactly what the theorem is saying!

☐

Exercise: 2 stars, optional

☐

Exercise: 2 stars, optional

☐

Exercise: 2 stars, optional

☐

Imp program syntax

We now define the Imp language, an imperative programming language with loops, conditionals, and arithmetic.

We add variables to the arithmetic expressions we had before:

Same notations as before...

...plus one more:

Shorthands for variables:

Note that the choice of variable names (X, Y, Z) clashes a bit with our earlier use of uppercase letters for Types. Since we're not using polymorphism heavily in this section, this overloading will hopefully not cause confusion.

Same bexps as before (using the new aexps)

Finally, we can define the set of commands

Some programs...

Note that the notations we introduced make it easy to write down commands that look close to how they would in a real imperative programming language; for example, here's what plus2 looks like fully expanded:

loops

an infinite loop

factorial

exponentiation

Note that pexp should be run in a state where Z is 1.

Exercise: 2 stars

Write a While program that sums the numbers from 1 to X (inclusive: 1 + 2 + ... + X) in the variable Y.

☐

Exercise: 2 stars

Write a While program that sets Z to 0 if X is even and sets Z to 1 otherwise.

☐

Evaluation

Now we will define what it means to evaluate an Imp program

We extend the arith evaluator to handle variables.

We update the boolean evaluator with the new aeval.

First try at an evaluator for commands, omitting CWhile.

Second try, using an extra "step index" to ensure that evaluation always terminates

NOTE: It is tempting to think that the index i here is counting the "number of steps of evaluation." But if you look closely you'll see that this is not the case: for example, in the CSeq rule, the same i is passed to both recursive calls. Understanding the exact way that i is treated will be important in the proof of ceval__ceval_step, which is given as an exercise below.

Third try, returning an option state instead of just a state so that we can distinguish between normal and abnormal termination.

A better way: define ceval as a relation, rather than a (total) function.

Exercise: 3 stars (aeval_beval_rel)

Write relations aeval_rel and beval_rel in the same style as ceval, and prove that they are equivalent to aeval and beval.

☐

And here's the similar output of ceval_step

Exercise: 2 stars

☐

Equivalence of step-indexed and relational evaluation

Exercise: 4 stars (ceval_step__ceval_inf)

Write an informal proof of ceval_step__ceval, following the template at the top of the file. (The template for case analysis on an inductively defined value should look the same as for induction, except that there are no induction hypothesis.) Make your proof communicate the main ideas to a human reader; do *not* simply transcribe the steps of the formal proof.

(* FILL IN HERE *)
☐

Exercise: 4 stars

Finish the following proof. You'll need ceval_step_more in a few places, as well as some basic facts about <= and plus.

☐

Reasoning about programs

Exercise: 3 stars (XtimesYinZ_spec)

State and prove a specification of the XtimesYinZ Imp program

☐

Exercise: 3 stars

☐

Exercise: 2 stars

The no_whiles predicate yields true on just those programs that have no while loops. Using Inductive, write a predicate no_Whiles that returns True instead of true. Then prove its equivalence with no_whiles. Hint: If some case of an inductive definitions is always False, you can simply leave it out.

☐

Exercise: 4 stars

On the other hand, Imp programs that don't involve while loops always terminate. State and prove a theorem that says this. Use either no_whiles or no_Whiles, as you prefer.

☐