Quick Review

We've now seen a bunch of Coq's fundamental tactics -- enough, in fact, to do pretty much everything we'll want for a while. We'll introduce one or two more as we go along through the next few lectures, and later in the course we'll introduce some more powerful automation tactics that make Coq do more of the low-level work in many cases, but basically this is the set we need.

• intros
  
  move hypotheses/variables from goal to context
  
  
• reflexivity
  
  finish the proof (when the goal looks like e = e)
  
  
• apply
  
  prove goal using a hypothesis, lemma, or constructor
  
  
• apply... in H
  
  apply a hypothesis, lemma, or constructor to a hypothesis in the context (forward reasoning)
  
  
• apply... with...
  
  explicitly specify values for variables that cannot be determined by pattern matching
  
  
• simpl
  
  simplify computations in the goal
  
  
• simpl in H
  
  ... or a hypothesis
  
  
• rewrite
  
  use an equality to rewrite the goal
  
  
• rewrite ... in H
  
  ... or a hypothesis
  
  
• unfold
  
  replace a defined constant by its RHS in the goal
  
  
• unfold... in H
  
  ... or a hypothesis
  
  
• destruct... as...
  
  case analysis on values of inductively defined types
  
  
• induction... with...
  
  induction on values of inductively defined types inversion reason by injectivity and distinctness of constructors
  
  
• remember (e) as x
  
  give a name (x) to an expression (e) so that we can destruct x without "losing" e
  
  
• assert (e) as H
  
  introduce a "local lemma" e and call it H

Programming with Propositions

A proposition is a statement expressing a factual claim. In Coq, propositions are written as expressions of type Prop. Although we haven't mentioned it explicitly, we have already seen numerous examples of such expressions.

Both provable and unprovable claims are perfectly good propositions. Simply being a proposition is one thing; being provable is something else!

Both plus 2 2 = 4 and plus 2 2 = 5 are valid expressions of type Prop.

We've seen one way that propositions can be used in Coq: in Theorem declarations.

But they can be used in many other ways. For example, we can give a name to a proposition using a Definition, just as we have given names to expressions of other sorts (numbers, functions, types, type functions, ...).

Now we can use this name in any situation where a proposition is expected -- for example, as the subject of a theorem.

So far, all the propositions we have seen are equality propositions. But we can build on equality propositions to make other sorts of claims. For example, what does it mean to claim that "a number n is even"? We have a function that (we believe) tests evenness, so one possible definition is "n is even iff evenb n = true."

This defines even as a parameterized proposition. Think of it as a function that, when applied to a number n, yields a proposition asserting that n is even.

The type of even, nat->Prop, can be pronounced in two ways: either simply "even is a function from numbers to propositions" or, perhaps more helpfully, "even is a family of propositions, indexed by a number n."

Functions returning propositions are 100-percent first-class citizens in Coq. We can use them in other definitions:

We can define them to take multiple arguments...

... and then partially apply them:

We can pass propositions -- and even parameterized propositions -- as arguments to functions:

Let's unravel what this last one means in concrete terms:

That is, nat_induction expresses exactly the principle of induction for natural numbers that we've been using for most of our proofs about numbers. Indeed, we can use the induction tactic to prove very straightforwardly that nat_induction P holds for all P.

Induction axioms

You may be puzzled by the last proof because it seems like we're using a built-in reasoning principle of induction over natural numbers to prove a theorem that basically just says the same thing. Indeed, this is exactly what we just did.

In general, every time we declare a new datatype with Inductive, Coq automatically generates an induction principle as an axiom (a theorem that we do not need to prove).

The induction principle for a type t is called t_ind. Here is the one for natural numbers:

The ":" here can be pronounced "...is a theorem proving the proposition..."

In general, every time we declare a new datatype t with Inductive, Coq automatically generates an axiom t_ind (i.e., a theorem whose truth is assumed rather than being proved from other axioms). This axiom expresses the induction principle for t. The induction tactic is a straightforward wrapper that, at its core, simply performs apply t_ind.

To see this more clearly, let's experiment a little with using apply nat_ind directly, instead of induction, to carry out some proofs.

First, here is a direct proof of the validity of our formulation of the induction principle. The proof amounts to observing that, after unfolding the names we defined, our principle coincides with the built-in one.

Indeed, we can apply nat_ind (instead of using induction) in any inductive proof.

For example, here's an alternate proof of a theorem that we saw in the Basics chapter:

Several details in this proof are worth noting. First, in the induction step of the proof (the "S" case), we have to do a little bookkeeping manually (the intros) that induction does automatically.

Second, we do not introduce n into the context before applying nat_ind -- the conclusion of nat_ind is a quantified formula, and apply needs this conclusion to exactly match the shape of the goal state, including the quantifier. The induction tactic works either with a variable in the context or a quantified variable in the goal.

Third, the apply tactic automatically chooses variable names for us (in the second subgoal, here), whereas induction lets us specify (with the as... clause) what names should be used. The automatic choice is actually a little unfortunate, since it re-uses the name n for a variable that is different from the n in the original theorem. This is why the Case annotation is just S -- if we tried to write it out in the more explicit form that we've been using for most proofs, we'd have to write n = S n, which doesn't make a lot of sense! All of these conveniences make induction nicer to use in practice than applying induction principles like nat_ind directly. But it is important to realize that, modulo this little bit of bookkeeping, applying nat_ind is what we are really doing.

Exercise: 2 stars

Complete this proof without using the induction tactic.

☐

Exercise: 2 stars

Our formulation of induction (the nat_induction proposition and the theorem stating that it works) can also be used directly to carry out proofs by induction.

Prove the same theorem again without induction or apply nat_ind.

☐

Induction principles for other datatypes

We've looked in depth now at the induction principle for natural numbers. The induction principles that Coq generates for other datatypes defined with Inductive follow a very similar pattern. If we define a type t with constructors c1 ... cn, Coq generates an induction principle with this shape:

    t_ind :
       forall P : t -> Prop,
            ... case for c1 ...
         -> ... case for c2 ...
         -> ...
         -> ... case for cn ...
         -> forall n : t, P n

The specific shape of each case depends on the arguments to the corresponding constructor. Before trying to write down a general rule, let's look at some more examples.

Exercise: 1 star

Write out the induction principle that Coq will generate for the following datatype. Write down your answer on paper, and then compare it with what Coq prints.

☐

Exercise: 1 star

Suppose we had written the above definition a little differently:

Now what will the induction principle look like?

☐

From these examples, we can extract this general rule:

• each constructor c takes argument types a1...an
• each ai can be either t (the datatype we are defining) or some other type s
• the corresponding case of the induction principle says (in English):
  • "for all values x1...xn of types a1...an, if P holds for each of the xs of type t, then P holds for c x1 ... xn".

Exercise: 1 star (ExSet)

Here is an induction principle for an inductively defined set.

      ExSet_ind :
         forall P : ExSet -> Prop,
             (forall b : bool, P (con1 b))
          -> (forall (n : nat) (e : ExSet), P e -> P (con2 n e))
          -> forall e : ExSet, P e

Give an Inductive definition of ExSet:

☐

Now, what about polymorphic datatypes?

The inductive definition of polymorphic lists [ Inductive list (X:Type) : Type := | nil : list X | cons : X -> list X -> list X. ] is very similar. The main difference is that, here, the whole definition is paramterized on a set X -- i.e., we are defining a family of inductive types list X, one for each X. Note that, wherever list appears in the body of the declaration, it is always applied to the parameter X. The induction principle is likewise parameterized on X:

     list_ind :
       forall (X : Type) (P : list X -> Prop),
            P []
         -> (forall (x : X) (l : list X), P l -> P (x :: l))
         -> forall l : list X, P l

Note the wording here (and, accordingly, the form of list_ind): The whole induction principle is parameterized on X. That is, list_ind can be thought of as a polymorphic function that, when applied to a set X, gives us back an induction principle specialized to list X.

Exercise: 1 star

Write out the induction principle that Coq will generate for the following datatype. Compare your answer with what Coq prints.

☐

Exercise: 1 star (mytype)

Find an inductive definition that gives rise to the following induction principle:

      mytype_ind :
        forall (X : Type) (P : mytype X -> Prop),
            (forall x : X, P (constr1 X x))
         -> (forall n : nat, P (constr2 X n))
         -> (forall m : mytype X, P m -> forall n : nat, P (constr3 X m n))
         -> forall m : mytype X, P m

☐

Exercise: 1 star (foo)

Find an inductive definition that gives rise to the following induction principle:

      foo_ind :
        forall (X Y : Type) (P : foo X Y -> Prop),
             (forall x : X, P (bar X Y x))
          -> (forall y : Y, P (baz X Y y))
          -> (forall f1 : nat -> foo X Y,
               (forall n : nat, P (f1 n)) -> P (quux X Y f1))
          -> forall f2 : foo X Y, P f2

☐

Exercise: 1 star

Consider the following inductive definition:

What induction principle will Coq generate for foo'? (fill in the blanks, then check your answer with Coq.)

     foo'_ind :
        forall (X : Type) (P : foo' X -> Prop),
              (forall (l : list X) (f : foo' X),
                    ______________________ -> _______________________)
          -> _________________________________________________
          -> forall f : foo' X, _______________________________

☐

Induction hypotheses

The induction principle for numbers

       forall P : nat -> Prop,
            P 0
         -> (forall n : nat, P n -> P (S n))
         -> forall n : nat, P n

is a generic statement that holds for all propositions P (strictly speaking, for all families of propositions P indexed by a number n). Each time we use this principle, we are choosing P to be a particular expression of type nat->Prop.

We can make the proof more explicit by giving this expression a name.

For example, instead of stating the theorem mult_0_r as "forall n, mult n 0 = 0," we can write it as "forall n, P_m0r n", where P_m0r is defined as...

... or equivalently...

This extra naming step isn't something that we'll do in normal proofs, but it is something that we should be able to do, because it allows us to see exactly what is the induction hypothesis. If we prove forall n, P_m0r n by induction on n (using either induction or apply nat_ind), we see that the first subgoal requires us to prove P_m0r 0 ("P holds for zero"), while the second subgoal requires us to prove forall n', P_m0r n' -> P_m0r n' (S n') (that is "P holds of S n' if it holds of n'" or, more elegantly, "P is preserved by S"). The induction hypothesis is the premise of this latter implication -- the assumption that P holds of n', which we are allowed to use in proving that P holds for S n'.

A closer look at the induction tactic

The induction tactic actually does quite a bit of low-level bookkeeping for us.

Recall the informal statement of the induction principle for natural numbers:

• If P n is some proposition involving a natural number n, and we want to show that P holds for all numbers n, we can reason like this:
  • show that P O holds
  • show that, if P n' holds, then so does P (S n')
  • conclude that P n holds for all n.

So, when we begin a proof with intros n and then induction n, we are first telling Coq to consider a particular n (by introducing it into the context) and then telling it to prove something about all numbers (by using induction).

What Coq actually does in this situation, internally, is to "re-generalize" the variable we perform induction on. For example, in the proof above that plus is associative...

It also works to apply induction to a variable that is quantified in the goal.

Note that induction n leaves m still bound in the goal -- i.e., what we are proving inductively is a statement beginning with forall m.

If we do induction on a variable that is quantified in the goal after some other quantifiers, the induction tactic will automatically introduce these quantifiers into the context.

Let's do induction on m this time, instead of n...

Exercise: 1 star (plus_comm)

Rewrite the previous two theorems and their proofs in the same style as mult_0_r'' above -- i.e., give, for each, an explicit Definition of the proposition being proved by induction and state the theorem and proof in terms of this defined proposition.

☐

A quick digression, for adventurous souls... If we can define parameterized propositions using Definition, then can we also define them using Fixpoint? Of course we can! However, this kind of "recursive parameterization" doesn't correspond to anything very familiar from everyday mathematics. The following exercise gives a slightly contrived example.

Exercise: 4 stars, optional

Define a recursive function true_upto_n_implies_true_everywhere that makes true_upto_n_example work.

Fixpoint true_upto_n__true_everywhere 
(* FILL IN HERE *)

Example true_upto_n_example :
    (true_upto_n__true_everywhere 3 (fun n => even n))
  = (even 3 -> even 2 -> even 1 -> forall m : nat, even m).
Proof. reflexivity.  Qed.

☐

Generalizing induction hypotheses

Last week's homework included a proof that the double function is injective. The way we START this proof is a little bit delicate: if we begin it with

      intros n. induction n.

all is well. But if we begin it with

      intros n m. induction n.

we get stuck in the middle of the inductive case...

What went wrong here?

The problem is that, at the point we invoke the induction hypothesis, we have already introduced m into the context -- intuitively, we have told Coq, "Let's consider some particular n and m..." and we now have to prove that, if double n = double m for this this particular n and m, then n = m.

The next tactic, induction n says to Coq: We are going to show the goal by induction on n. That is, we are going to prove that

• P n = "if double n = double m, then n = m"

holds for all n by showing

• P O
  
  (i.e., "if double O = double m then O = m")
  
  
• P n -> P (S n)
  
  (i.e., "if double n = double m then n = m" implies "if double (S n) = double m then S n = m").

If we look closely at the second statement, it is saying something rather strange: it says that, for any particular m, if we know

• "if double n = double m then n = m"

then we can prove

• "if double (S n) = double m then S n = m".

To see why this is strange, let's think of a particular m -- say, 5. The statement is then saying that, if we can prove

• Q = "if double n = 10 then n = 5"

then we can prove

• R = "if double (S n) = 10 then S n = 5".

But knowing Q doesn't give us any help with proving R! (If we tried to prove R from Q, we would say something like "Suppose double (S n) = 10..." but then we'd be stuck: knowing that double (S n) is 10 tells us nothing about whether double n is 10, so Q is useless at this point.)

To summarize: Trying to carry out this proof by induction on n when m is already in the context doesn't work because we are trying to prove a relation involving every n but just a single m.

The good proof of double_injective leaves m in the goal statement at the point where the induction tactic is invoked on n:

So what we've learned is that we need to be careful about using induction to try to prove something too specific: If we're proving a property of n and m by induction on n, we may need to leave m generic.

However, this strategy doesn't always apply directly; sometimes a little rearrangement is needed. Suppose, for example, that we had decided we wanted to prove double_injective by induction on m instead of n.

Here we are stuck again, just like before.

The problem is that, to do induction on m, we must first introduce n. (If we simply say induction m without introducing anything first, Coq will automatically introduce n for us!) What can we do about this?

One possibility is to rewrite the statement of the lemma so that m is quantified before n. This will work, but it's not nice: We don't want to have to mangle the statements of lemmas to fit the needs of a particular strategy for proving them -- we want to state them in the most clear and natural way.

What we can do instead is to first introduce all the quantified variables and then re-generalize one or more of them, taking them out of the context and putting them back at the beginning of the goal. The generalize dependent tactic does this.

Let's look at an informal proof of this theorem. Note that the proposition we prove by induction leaves n quantified, corresponding to the use of generalize dependent in our formal proof.

Theorem: For any nats n and m, if double n = double m, then n = m.

Proof: Let a nat m be given. We prove that for any n, if double n = double m then n = m by induction on m.

• In the base case, we have m = 0. Let a nat n be given such that double n = double m. Since m = 0, we have double n = 0. If n = S n' for some n', then double n = S (S (double n')) by the definition of double. This would be a contradiction of the assumption that double n = 0, so n = 0, and thus n = m.
  
  
• In the inductive case, we have m = S m' for some nat m'. Let a nat n be given such that double n = double m. By the definition of double, we therefore have:
  
        double n = S (S (double m'))
  
  
  
  If n = 0, then double n = 0 (by the definition of double), which we have just seen is not the case. Thus, n = S n' for some n', and we have:
  
        S (S (double n')) = S (S (double m'))
  
  which implies that double n' = double m'.
  
  But observe that our inductive hypothesis here is: for any n, if double n = double m' then n = m'
  
  Applying this for n' then yields n' = m', and it follows directly that S n' = S m'. Since S n' = n and S m' = m, this is just what we wanted to show. ☐

Exercise: 3 stars (gen_dep_practice)

Carry out this proof by induction on m.

Prove this by induction on l

☐

Exercise: 3 stars (index_after_last_informal)

Write an informal proof corresponding to your coq proof of index_after_last:

Theorem: For any nat n and list l, if length l = n then index (S n) l = None.

Proof: (* FILL IN HERE *)
☐

Exercise: 3 stars (gen_dep_practice_opt)

Prove this by induction on l.

☐

Exercise: 3 stars, optional

Prove this by induction on m.

☐

Exercise: 3 stars, optional

Prove this by induction on l1, without using app_length.

☐

Exercise: 4 stars

Prove this by induction on l, without using app_length.

☐

Constructing Evidence

One of the first examples in the discussion of propositions involved the concept of evenness. It is important to notice that we have two rather different ways of talking about this concept:

• a computation evenb n that checks evenness, yielding a boolean
  
  
• a proposition even n (defined in terms of evenb) that asserts that n is even.

There is another way of defining what it means to say that a number is even. Instead of going "indirectly" via the evenb function, we can give a "direct" definition of evenness by saying, straight out, what we would be willing to accept as evidence that a given number is even.

Informally, this definition says that there are two ways to give evidence that a number m is even: observe that it is zero, or observe that n = S (S m) for some m, if we have evidence that m itself is even. The constructors ev_0 and ev_SS are names for these different ways of giving evidence for evenness.

The role of ":" here is interesting. Before, we've written "e : t" in situations where either e is an expression denoting a value and t is the type of this value or else where e is an expression describing some set and t is Type. In both cases, the ":" is pronounced "is a" or, more formally, "is classified by" or "has type." Here, the type is a proposition and the thing that has that type is evidence for the proposition.

In other words, we are thinking of a proposition as analogous to a set... a set of proofs (or evidence)! Saying "e has type P" (where P is a proposition) and saying "e is a proof of P" are exactly the same thing.

The analogy

                 propositions  ~  sets
                 proofs        ~  data values 

is called the Curry-Howard correspondence (or, sometimes, the Curry-Howard Isomorphism).

A great many things follow from it.

First, just as a set can be empty, a singleton, finite, or infinite, a proposition may be "inhabited" by zero, one, many, or infinitely many proofs. This makes sense: each inhabitant of a proposition P is a different way of giving evidence for P. If there are none, then P is not provable. If there are many, then P has many different proofs.

Second, the Inductive construction means exactly the same thing whether we are using it to define sets of data values (in the Type world) or sets of evidence. Let's look at the parts of the inductive definition of ev above:

• The first line declares that ev is a proposition indexed by a natural number
  
  
• The second line declares that the constructor ev_0 can be taken as evidence for the assertion ev O.
  
  
• The third line declares that, if n is a number and E is evidence for the assertion ev n), then ev_SS n E can be taken as evidence for ev (S (S n)). That is, we can construct evidence that S (S n) is even by applying the constructor ev_SS to evidence that n is even.

For example, here is a proof that 4 is even:

Exercise: 1 star

What are the 2 and 0 doing there?

☐

Hang on a minute! Until now, we've constructed proofs by giving sequences of tactics that eventually caused Coq to say "Proof completed." Is this something new?

No, it is not. Here's the real story. In Coq, a proof of a proposition P is a precisely term of type P. So the fact that the above Definition typechecks means that four_ev really is a proof of ev 4. The other way of giving proofs in Coq -- using Theorem... Proof... Qed. -- is just a different notation for doing exactly the same thing. To see this, let's write a proof that four is even in the more familiar way.

It's worth working through this proof slowly to make sure you understand what each apply is doing and why it makes sense to use apply with the constructors of ev instead of with hypotheses and theorems, as we've been doing.

Notice the similarity between the first two lines of this theorem and the previous Definition of four_ev: they can be read "four_ev' is evidence for the proposition ev 4." But there's more. The theorem actually builds a proof object that embodies the evidence that 4 is even. Let's look at it:

Proof objects are the "bedrock" of reasoning in Coq. Tactic proofs are convenient shorthands that instruct Coq how to construct proof objects for us instead of our writing them out explicitly. (Here, of course, the proof object is actually shorter than the tactic proof. But the proof objects for more interesting proofs can become quite large and complex -- building them by hand would be painful.)

Third, the correspondence between values and proofs induces a strong correpondence between functions and proofs of hypothetical propositions. For example, consider the proposition

       forall n, ev n -> ev (plus 4 n).

This can be read "assuming we have evidence that n is even, we can construct evidence that plus 4 n is even." Viewed differently, it is the type of a function taking a number n and evidence that n is even and yielding evidence that plus 4 n is even.

For comparison, here is a tactic proof of the same proposition.

Again, the proof object constructed by this tactic proof is identical to the one that we built by hand.

Fourth, just as hypothetical propositions have "arrow implication types", the use of a hypothetical proposition exactly corresponds to function application.

For example, consider this theorem:

Fifth, and finally, simplification of expressions denoting data values also has an analog in the world of propositions and proofs. Just as the computational expression plus 4 (plus 4 2) simplifies to 10...

..f. the proof term ev_ten, which contains two applications of the theorem ev_plus4 (which we defined above as a function), can be simplified to a direct proof of the same proposition:

(Note fthat we have to use the more aggressive Eval compute rather than just Eval simpl to get Coq to unfold the definitions here.)

To summarize: The Curry-Howard Correspondence is a powerful conceptual tool, establishing deep and fruitful links between programming languages and mathematical logic. Closer to home, it is the backbone for the organization of Coq.

PICTURE GOES HERE

Of course, this is just the backbone. There are lots of other types (and their inhabitants) that this picture doesn't show. For example, there is Type->Type, which is the type of things like list, there is (nat->Prop)->Prop, the type of things like nat_ind, and so on.

Exercise: 2 stars

Construct a tactic proof of the following proposition.

☐

Exercise: 4 stars, optional (double_even_pfobj)

Try to predict what proof object is constructed by the above tactic proof. (Before checking your answer, you'll want to strip out any uses of Case, as these will make the proof object a bit cluttered.)

☐

Manipulating Evidence

Besides constructing evidence of evenness, we can also reason about evidence of evenness. The fact that we introduced ev with an Inductive declaration tells us not only that the constructors ev_O and ev_SS are ways to build evidence of evenness, but also that these two constructors are the ONLY ways that evidence of evenness can be built.

In other words, if someone gives us evidence E justifying the assertion ev n, then we know that E can only have one of two forms: either E is ev_0 (and n is O), or E is ev_SS n' E' (and n is S (S n')) and E' is evidence that n' is even.

Thus, it makes sense to use all the tactics that we have already seen for inductively defined data to reason instead about inductively defined evidence.

For example, here we use a destruct on evidence that n is even in order to show that ev n implies evf (n-2). (Recall that pred 0 is 0.)

Exercise: 1 star (ev_minus2_n)

What happens if we try to destruct on n instead of E?

☐

We can also perform induction on evidence that n is even. Here we use it show that the old evenb function returns true on n when n is even according to ev.

Exercise: 1 star (ev_even_n)

Could this proof be carried out by induction on n instead of E?

☐

Exercise: 3 stars (l_fails)

The following proof attempt will not succeed.

     Theorem l : forall n,
       ev n.
     Proof.
       intros n. induction n.
         Case "O". simpl. apply ev_0.
         Case "S".
           ...

Briefly explain why.

(* FILL IN HERE *)

☐

Exercise: 2 stars

Here's another exercise requiring induction.

☐

Here's another situation where we want analyze evidence for evenness and build two sub-goals.

The right thing to use here is inversion (!)

This use of inversion may seem a bit mysterious at first. Until now, we've only used inversion on equality propositions, to utilize injectivity of constructors or to discriminate between different constructors. But we see here that inversion can also be applied to analyzing evidence for inductively defined propositions.

Here's how inversion works in general. Suppose the name I refers to an assumption P in the current context, where P has been defined by an Inductive declaration. Then, for each of the constructors of P, inversion I generates a subgoal in which I has been replaced by the exact, specific conditions under which this constructor could have been used to prove P. Some of these subgoals will be self-contradictory; inversion throws these away. The ones that are left represent the cases that must be proved to establish the original goal.

In this particular case, the inversion analyzed the construction ev (S (S n)), determined that this could only have been constructed using ev_SS, and generated a new subgoal with the arguments of that constructor as new hypotheses. (It also produced an auxiliary equality, which happens to be useless.) We'll begin exploring this more genefral behavior of inversion in what follows.

Exercise: 1 star (inversion_practice)

inversion can also be used to derive goals by showing absurdity of a hypothesis.

☐

We can generally use inversion instead of destruct on inductive propositions. This illustrates that in general, we get one case for each possible constructor. Again, we also getf some auxiliary equalities which are rewritten in the goal but not in the other hypotheses.

Exercise: 3 stars

Finding the appropriate thing to do induction on is a bit tricky here.

☐

More on inductively defined propositions

We have seen that the proposition "some number is even" can be phrased in two different ways -- indirectly, via a testing function evenb, or directly, by inductively describing what constitutes evidence for evenness. These two ways of defining evenness are about equally easy to state and work with.

However, for many other properties of interest, the direct inductive definition is preferable, since writing a testing function may be awkward or even impossible. For example, consider the property MyProp defined as follows:

• the number 4 has property MyProp
• if n has property MyProp, then so does 4+n
• if n+2 has property MyProp, then so does n
• no other numbers have property MyProp

This is a perfectly sensible definition of a set of numbers, but we cannot translate this definition directly as a Coq Fixpoint (or translate it directly into a recursive function in any other programming language). We might be able to find a clever way of testing this property using a Fixpoint (indeed, it is not even too hard to find one in this case), but in general this could require arbitrarily much thinking.

In fact, if the property we are interested in is uncomputable, then we cannot define it as a Fixpoint no matter how hard we try, because Coq requires that all Fixpoints correspond to terminating computations.

On the other hand, writing an inductive definition of what it means to give evidence for the property MyProp is straightforward:

The first three clauses in the informal definition of MyProp above are reflected in the first three clauses of the inductive definition. The fourth clause is the precise force of the keyword Inductive.

As we did with evenness, we can now construct evidence that certain numbers satisfy MyProp.

Exercise: 2 stars (MyProp)

Here are two useful facts about MyProp. (The proofs are left to you.)

☐

With these, we can show that MyProp holds of all even numbers, and vice versa.

Here's an informal proof of this theorem:

Theorem : For any nat n, if ev n then MyProp n.

Proof: Let a nat n and a derivation E of ev n be given. We go by induction on E. There are two case:

• If the last step in E is a use of ev_0, then n is 0. But we know by lemma MyProp_0 that MyProp 0, so the theorem is satisfied in this case.
  
  
• If the last step in E is by ev_SS, then n = S (S n') for some n' and there is a derivation of ev n'. By lemma MyProp_plustwo, it's enough to show MyProp n'. This follows directly from the inductive hypothesis for the derivation of ev n'. ☐

Exercise: 3 stars

☐

Exercise: 3 stars (ev_MyProp_informal)

Write an informal proof corresponding to your formal proof of ev_MyProp:

Theorem: For any nat n, if MyProp n then ev n.

Proof: (* FILL IN HERE *)
☐

Exercise: 4 stars, optional (MyProp_pfobj)

Prove MyProp_ev and ev_MyProp again by constructing explicit proof objects by hand (as we did above in ev_plus4, for example).

☐

Exercise: 3 stars

Complete this proof using apply MyProp_ind instead of the induction tactic.

☐

Induction principles in Prop

Last week, we looked in detail at the induction principles that Coq generates for inductively defined sets. Inductively defined propositions are handled slightly differently. For example, from what we've said so far, you might expect the inductive definition of ev

    Inductive ev : nat -> Prop :=
       | ev_0 : ev O
       | ev_SS : forall n:nat, ev n -> ev (S (S n)).

to give rise to an induction principle that looks like this...

    ev_ind_max :
       forall P : (forall n : nat, ev n -> Prop),
            P O ev_0
         -> (forall (n : nat) (e : ev n),
              P n e -> P (S (S n)) (ev_SS n e))
         -> forall (n : nat) (e : ev n), P n e

... because:

• Since ev is indexed by a number n (every ev object e is a piece of evidence that some particular number n is even), the proposition P is parameterized by both n and e -- that is, the induction principle can be used to prove assertions involving both an even number and the evidence that it is even.
  
  
• Since there are two ways of giving evidence of evenness (ev has two constructors), applying the induction principle generates two subgoals:
  
  
  • We must prove that P holds for O and ev_0.
    
    
  • We must prove that, whenever n is an even number and e is evidence of its evenness, if P holds of n and e, then it also holds of S (S n) and ev_SS n e.
    
    
• If these subgoals can be proved, then the induction principle tells us that P is true for all even numbers n and evidence e of their evenness.

But this is a little more flexibility than we actually need or want: it is giving us a way to prove logical assertions involving evidence of evenness, while all we really care about is proving properties of numbers that are even -- we are interested in assertions about numbers, not about evidence. It would therefore be more convenient to have an induction principle for proving propositions P that are parameterized just by n and whose conclusion establishes P for all even numbers n:

       forall P : nat -> Prop,
          ...
          -> forall n : nat, ev n -> P n

For this reason, Coq actually generates the following simplified induction principle for ev:

     ev_ind :
       forall P : nat -> Prop,
            P O
         -> (forall n : nat, ev n -> P n -> P (S (S n)))
         -> forall n : nat, ev n -> P n

Similarly, from the inductive definition of the proposition and A B

     Inductive and (A B : Prop) : Prop :=
       conj : A -> B -> (and A B).

we might expect Coq to generate this induction principle

     and_ind_max :
       forall (A B : Prop) (P : A /\ B -> Prop),
            (forall (a : A) (b : B), P (conj A B a b))
         -> forall a : A /\ B, P a

but actually it generates this simpler and more useful one:

     and_ind :
       forall A B P : Prop,
            (A -> B -> P)
         -> A /\ B -> P

In the same way, when given the inductive definition of or A B

     Inductive or (A B : Prop) : Prop :=
       | or_introl : A -> or A B
       | or_intror : B -> or A B.

instead of the "maximal induction principle"

     or_ind_max :
       forall (A B : Prop) (P : A \/ B -> Prop),
            (forall a : A, P (or_introl A B a))
         -> (forall b : B, P (or_intror A B b))
         -> forall o : A \/ B, P o

what Coq actually generates is this:

     or_ind :
       forall A B P : Prop,
            (A -> P)
         -> (B -> P)
         -> A \/ B -> P

Exercise: 3 stars (p_provability)

Consider the following inductively defined proposition:

Describe, in English, the conditions under which the proposition p t n is provable.

(* FILL IN HERE *)

☐

Informal proofs, again

Q: What is the relation between a formal proof of a proposition P and an informal proof of the same proposition P?

A: The latter should *teach* the reader how to produce the former.

Q: How much detail is needed?

A: There is no single right answer; rather, there is a range of choices.

At one end of the spectrum, we can essentially give the reader the whole formal proof (i.e., the informal proof amounts to just transcribing the formal one into words). This gives the reader the *ability* to reproduce the formal one for themselves, but it doesn't *teach* them anything.

At the other end of the spectrum, we can say "The theorem is true and you can figure out why for yourself if you think about it hard enough." This is also not a good teaching strategy, because usually writing the proof requires some deep insights into the thing we're proving, and most readers will give up before they rediscover all the same insights as we did.

In the middle is the golden mean -- a proof that includes all of the essential insights (saving the reader the hard part of work that we went through to find the proof in the first place) and clear high-level suggestions for the more routine parts to save the reader from spending too much time reconstructing these parts (e.g., what the IH says and what must be shown in each case of an inductive proof), but not so much detail that the main ideas are obscured.

---

Another key point: if we're talking about a formal proof of a proposition P and an informal proof of P, the proposition P doesn't change. That is, formal and informal proofs are talking about the same world and they must play by the same rules.

In particular, whether we are talking about formal or informal proofs, propositions and booleans are different things!

• Booleans are values in the computational world. Every expression of type bool (with no free variables) can be simplified to either true or false.
  
  
• Propositions are types in the logical world. They are either provable (i.e., there is some expression that has this type) or not (there is no such expression). It doesn't make sense to say that a proposition is "equivalent to true," and it is not necessarily the case that, if a proposition P is not provable, then ~P is provable.
  
  We do sometimes use the words "true" and "false" when referring to propositions. Strictly speaking, we should not: a proposition is either provable or it is not.

Induction principles for inductively defined Props

The induction principles for inductively defined propositions like ev are a tiny bit more complicated than the ones for inductively defined sets. Intuitively, this is because we want to use them to prove things by inductively considering the possible shapes that something in ev can have -- either it is evidence that 0 is even, or else it is evidence that, for some n, S (S n) is even, and it includes evidence that n itself is. But the things we want to prove are not statements about evidence, they are statements about numbers. So we want an induction principle that allows reasoning by induction on the former to prove properties of the latter.

In English, the induction principle for ev goes like this:

• Suppose, P is a predicate on natural numbers (that is, P n is a Prop for every n). To show that P n holds whenever n is even, it suffices to show:
  
  
  • P holds for 0
    
    
  • for any n, if n is even and P holds for n, then P holds for S (S n).

Formally:

We can apply ev_ind directly instead of using induction, following pretty much the same pattern as above.

Exercise: 3 stars, optional (prop_ind)

Write out the induction principles that Coq will generate for the inductive declarations list and MyProp. Compare your answers against the results Coq prints for the following queries.

☐

Additional Exercises

Exercise: 2 stars, optional

The following proof attempt is not going to succeed. Briefly explain why.

☐

Exercise: 4 stars

A palindrome is a sequence that reads the same backwards as forwards.

• Define an inductive proposition pal on list nat that captures what it means to be a palindrome. (Hint: You'll need three cases.)
  
  
• Prove that
  
         forall l, pal(l++(rev l))
  
  
• Prove that
  
         forall l, pal l => l = rev l.
  
  

Note: The converse thoerem

     forall l, l = rev l => pal l.

is much harder! We won't have the tools to attack this for some time...

☐