# IndPropositions and Evidence

(* $Date: 2011-04-02 12:47:04 -0400 (Sat, 02 Apr 2011) $ *)

"Algorithms are the computational content of proofs." (Robert
Harper)

# Generalizing Induction Hypotheses

*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...
Theorem double_injective_FAILED : ∀ n m,

double n = double m →

n = m.

Proof.

intros n m. induction n as [| n'].

Case "n = O". simpl. intros eq. destruct m as [| m'].

SCase "m = O". reflexivity.

SCase "m = S m'". inversion eq.

Case "n = S n'". intros eq. destruct m as [| m'].

SCase "m = O". inversion eq.

SCase "m = S m'".

assert (n' = m') as H.

SSCase "Proof of assertion".

(* Here we are stuck. We need the assertion in order to

rewrite the final goal (subgoal 2 at this point) to an

identity. But the induction hypothesis, IHn', does

not give us n' = m' -- there is an extra S in the

way -- so the assertion is not provable. *)

Admitted.

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
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
the proposition
holds for all n by showing
If we look closely at the second statement, it is saying something
rather strange: it says that, for a
then we can prove
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
then we can prove
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
The good proof of double_injective leaves m in the goal
statement at the point where the induction tactic is invoked on
n:

*this particular*n and m, then n = m.- P n = "if double n = double m, then n = m"

- P O
- P n → P (S n)

*particular*m, if we know- "if double n = double m then n = m"

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

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

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

*every*n but just a*single*m.Theorem double_injective' : ∀ n m,

double n = double m →

n = m.

Proof.

intros n. induction n as [| n'].

Case "n = O". simpl. intros m eq. destruct m as [| m'].

SCase "m = O". reflexivity.

SCase "m = S m'". inversion eq.

Case "n = S n'".

(* Notice that both the goal and the induction

hypothesis have changed: the goal asks us to prove

something more general (i.e., to prove the

statement for *every* m), but the IH is

correspondingly more flexible, allowing us to

choose any m we like when we apply the IH. *)

intros m eq.

(* Now we choose a particular m and introduce the

assumption that double n = double m. Since we

are doing a case analysis on n, we need a case

analysis on m to keep the two "in sync." *)

destruct m as [| m'].

SCase "m = O". inversion eq. (* The 0 case is trivial *)

SCase "m = S m'".

(* At this point, since we are in the second

branch of the destruct m, the m' mentioned

in the context at this point is actually the

predecessor of the one we started out talking

about. Since we are also in the S branch of

the induction, this is perfect: if we

instantiate the generic m in the IH with the

m' that we are talking about right now (this

instantiation is performed automatically by

apply), then IHn' gives us exactly what we

need to finish the proof. *)

assert (n' = m') as H.

SSCase "Proof of assertion". apply IHn'.

inversion eq. reflexivity.

rewrite → H. reflexivity. Qed.

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.

Theorem double_injective_take2_FAILED : ∀ n m,

double n = double m →

n = m.

Proof.

intros n m. induction m as [| m'].

Case "m = O". simpl. intros eq. destruct n as [| n'].

SCase "n = O". reflexivity.

SCase "n = S n'". inversion eq.

Case "m = S m'". intros eq. destruct n as [| n'].

SCase "n = O". inversion eq.

SCase "n = S n'".

assert (n' = m') as H.

SSCase "Proof of assertion".

(* Here we are stuck again, just like before. *)

Admitted.

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.Theorem double_injective_take2 : ∀ n m,

double n = double m →

n = m.

Proof.

intros n m.

(* n and m are both in the context *)

generalize dependent n.

(* Now n is back in the goal and we can do induction on

m and get a sufficiently general IH. *)

induction m as [| m'].

Case "m = O". simpl. intros n eq. destruct n as [| n'].

SCase "n = O". reflexivity.

SCase "n = S n'". inversion eq.

Case "m = S m'". intros n eq. destruct n as [| n'].

SCase "n = O". inversion eq.

SCase "n = S n'".

assert (n' = m') as H.

SSCase "Proof of assertion".

apply IHm'. inversion eq. reflexivity.

rewrite → H. reflexivity. Qed.

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 m be a nat. We prove by induction on m that, for any n, if double n = double m then n = m.- First, suppose m = 0, and suppose n is a number such
that double n = double m. We must show that n = 0.
- Otherwise, suppose m = S m' and that n is again a number such
that double n = double m. We must show that n = S m', with
the induction hypothesis that for every number s, if double s =
double m' then s = m'.

#### Exercise: 3 stars (gen_dep_practice)

Carry out this proof by induction on m.Theorem plus_n_n_injective_take2 : ∀ n m,

n + n = m + m →

n = m.

Proof.

(* FILL IN HERE *) Admitted.

Now prove this by induction on l.

Theorem index_after_last: ∀ (n : nat) (X : Type) (l : list X),

length l = n →

index (S n) l = None.

Proof.

(* FILL IN HERE *) Admitted.

☐

☐

#### Exercise: 3 stars, optional (index_after_last_informal)

Write an informal proof corresponding to your Coq proof of index_after_last:*Theorem*: For all sets X, lists l : list X, and numbers n, if length l = n then index (S n) l = None.*Proof*: (* FILL IN HERE *)☐

#### Exercise: 3 stars, optional (gen_dep_practice_opt)

Prove this by induction on l.Theorem length_snoc''' : ∀ (n : nat) (X : Type)

(v : X) (l : list X),

length l = n →

length (snoc l v) = S n.

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 3 stars, optional (app_length_cons)

Prove this by induction on l1, without using app_length.Theorem app_length_cons : ∀ (X : Type) (l1 l2 : list X)

(x : X) (n : nat),

length (l1 ++ (x :: l2)) = n →

S (length (l1 ++ l2)) = n.

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 4 stars, optional (app_length_twice)

Prove this by induction on l, without using app_length.Theorem app_length_twice : ∀ (X:Type) (n:nat) (l:list X),

length l = n →

length (l ++ l) = n + n.

Proof.

(* FILL IN HERE *) Admitted.

☐
We've now seen a bunch of Coq's fundamental tactics — enough 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
Here are the ones we've seen:
So far, the only statements we have been able to state and
prove have been in the form of
A

# Review

*automation*tactics that make Coq do more of the low-level work in many cases. But basically we've got what we need to get work done.- 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 hypothesis (or lemma) to rewrite the goal
- rewrite ... in H:
... or a hypothesis
- unfold:
replace a defined constant by its right-hand side in the goal
- unfold... in H:
... or a hypothesis
- destruct... as...:
case analysis on values of inductively defined types
- induction... as...:
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
- generalize dependent e: "re-quantify" e, moving it from the local context back into the goal

# Programming with Propositions

*Note to readers*: Some of the concepts in this chapter may seem quite abstract on a first encounter. We've included a*lot*of exercises, most of which should be quite approachable even if you're still working on understanding the details of the text. Try to work as many of them as you can, especially the one-starred exercises.*equalities*. However, the language of mathematical statements and proofs is much richer than this! In this chapter we will take a much closer and more fundamental look at the sorts of mathematical statements (*propositions*) we can make in Coq, and how we go about proving them by providing logical*evidence*.*proposition*is a statement expressing a factual claim, like "two plus two equals four." In Coq, propositions are written as expressions of type Prop. Although we haven't mentioned it explicitly, we have already seen numerous examples.Check (2 + 2 = 4).

(* ===> 2 + 2 = 4 : Prop *)

Check (ble_nat 3 2 = false).

(* ===> ble_nat 3 2 = false : Prop *)

Both provable and unprovable claims are perfectly good
propositions. Simply

*being*a proposition is one thing; being*provable*is something else!Check (2 + 2 = 5).

(* ===> 2 + 2 = 5 : Prop *)

Both 2 + 2 = 4 and 2 + 2 = 5 are legal expressions
of type Prop.
We've seen one way that propositions can be used in Coq: in
Theorem (and Lemma and Example) 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. We can also form new propositions out of old
ones. For example, given propositions P and Q, we can form
the proposition "P implies Q."

Also, given a proposition P with a free variable n, we can
form the proposition ∀ n, P.

Finally, we can define

*parameterized propositions*. For example, what does it mean to claim that "a number n is even"? We have written a function that tests evenness, so one possible definition of what it means to be even is "n is even iff evenb n = true."
This defines even as a

*function*that, when applied to a number n,*yields a proposition*asserting that n is even.Check even.

(* ===> even : nat -> Prop *)

Check (even 4).

(* ===> even 4 : Prop *)

Check (even 3).

(* ===> even 3 : Prop *)

The type of even, nat→Prop, can be pronounced in three
ways: (1) "even is a
Propositions — including parameterized propositions — are
first-class citizens in Coq. We can use them in other
definitions:

*function*from numbers to propositions," (2) "even is a*family*of propositions, indexed by a number n," or (3) "even is a*property*of numbers."
We can define them to take multiple arguments...

... and then partially apply them:

We can even pass propositions — including parameterized
propositions — as arguments to functions:

Definition true_for_zero (P:nat→Prop) : Prop :=

P 0.

Definition true_for_n__true_for_Sn (P:nat→Prop) (n:nat) : Prop :=

P n → P (S n).

(Names of the form x__y, with two underscores in a row, can be
read "x implies y.")
Here are two more examples of passing parameterized
propositions as arguments to a function. The first makes the
claim that a whenever a proposition P is true for some natural
number n', it is also true by the successor of n':

And this one simply claims that a proposition is true for
all natural numbers:

We can put these pieces together to manually restate the
principle of induction for natural numbers. Given a parameterized
proposition P, if P is true for 0, and P (S n') is true
whenever P n' is, then P is true for all natural numbers.

Definition our_nat_induction (P:nat→Prop) : Prop :=

(true_for_zero P) →

(preserved_by_S P) →

(true_for_all_numbers P).

# Evidence

## Inductively Defined Propositions

*atomic*propositions — ones that aren't built into the logic we're using, but are rather introduced to model useful concepts in a particular domain. For example, having defined a type day as we did in Basics.v, we might have some concept in our minds about certain days, say the fact that saturday and sunday are "good" ones. If we want to use Coq to state and prove theorems involving good days, we need to begin by telling it what we mean by "good" — that is, we need to specify what counts as as evidence that some day d is good (namely, that d is either saturday or sunday. The following declaration achieves this:

The Inductive keyword means exactly the same thing whether
we are using it to define sets of data values (in the Type
world) or sets of evidence (in the Prop world). Consider the
parts of the definition above:
That is, we're

- The first line declares that good_day is a proposition indexed
by a day.
- The second line declares that the constructor gd_sat can be
taken as evidence for the assertion good_day saturday.
- The third line declares that the constructor gd_sun can be taken as evidence for the assertion good_day sunday.

*defining*what we mean by days being good by saying "Saturday is good, sunday is good, and that's all." Then someone can*prove*that Sunday is good simply by observing that we said it was when we defined what good_day meant.
The constructor gd_sun is "primitive evidence" — an
Similarly, we can define a proposition day_before
parameterized by

*axiom*— justifying the claim that Sunday is good.*two*days, together with axioms stating that Monday comes before Tuesday, Tuesday before Wednesday, and so on.Inductive day_before : day → day → Prop :=

| db_tue : day_before tuesday monday

| db_wed : day_before wednesday tuesday

| db_thu : day_before thursday wednesday

| db_fri : day_before friday thursday

| db_sat : day_before saturday friday

| db_sun : day_before sunday saturday

| db_mon : day_before monday sunday.

The axioms that we introduce along with an inductively
defined proposition can also involve universal quantifiers. For
example, it is well known that

*every*day is a fine day for singing a song:
The line above declares that, if d is a day, then fdfs_any d
can be taken as evidence for fine_day_for_singing d. That is,
we can construct evidence that d is a fine_day_for_singing
by applying the constructor fdfs_any to d.
In particular, Wednesday is a fine day for singing.

As always, the first line here can be read "I'm about to
show you some evidence for the proposition fine_day_for_singing
wednesday, and I want to introduce the name fdfs_wed to refer
to that evidence later on." The second line then instructs Coq
how to assemble the evidence.
There's another — more primitive — way to accomplish the
same thing: we can use a Definition whose left-hand side is the
name we're introducing and whose right-hand side is the evidence

## Proof Objects

*itself*, rather than a script for how to build it.Definition fdfs_wed' : fine_day_for_singing wednesday :=

fdfs_any wednesday.

Check fdfs_wed.

Check fdfs_wed'.

The expression fdfs_any wednesday can be thought of as
instantiating the parameterized axiom fdfs_any with the specific
argument wednesday. Alternatively, we can think of fdfs_any
as a primitive "evidence constructor" that, when applied to a
particular day, stands as evidence that that day is a fine day for
singing; its type, ∀ d:day, fine_day_for_singing d,
expresses this functionality, in the same way that the polymorphic
type ∀ X, list X in the previous chapter expressed the fact
that the constructor nil can be thought of as a function from
types to empty lists with elements of that type.
Let's take a slightly more interesting example. Let's say
that a day of the week is "ok" if either (1) it is a good day or
else (2) it falls the day before an ok day.

Inductive ok_day : day → Prop :=

| okd_gd : ∀ d,

good_day d →

ok_day d

| okd_before : ∀ d1 d2,

ok_day d2 →

day_before d2 d1 →

ok_day d1.

The first constructor can be read "One way to show that d
is an ok day is to present evidence that d is good." The second
can be read, "Another way to show that a day d1 is ok is to
present evidence that it is the day before some other day d2
together with evidence that d2 is ok."
Now suppose that we want to prove that wednesday is ok.
There are two ways to do it. First, we have the primitive way,
where we simply write down an expression that has the right
type — a big nested application of constructors:

Definition okdw : ok_day wednesday :=

okd_before wednesday thursday

(okd_before thursday friday

(okd_before friday saturday

(okd_gd saturday gd_sat)

db_sat)

db_fri)

db_thu.

Second, we have the machine-assisted way, where we go into Proof
mode and Coq guides us through a series of goals and subgoals
until it is finally satisfied:

Theorem okdw' : ok_day wednesday.

Proof.

(* wednesday is OK because it's the day before an OK day *)

apply okd_before with (d2:=thursday).

(* "subgoal: show that thursday is ok". *)

(* thursday is OK because it's the day before an OK day *)

apply okd_before with (d2:=friday).

(* "subgoal: show that friday is ok". *)

(* friday is OK because it's the day before an OK day *)

apply okd_before with (d2:=saturday).

(* "subgoal: show that saturday is ok". *)

(* saturday is OK because it's good! *)

apply okd_gd. apply gd_sat.

(* "subgoal: show that the day before saturday is friday". *)

apply db_sat.

(* "subgoal: show that the day before friday is thursday". *)

apply db_fri.

(* "subgoal: show that the day before thursday is wednesday". *)

apply db_thu. Qed.

Fundamentally, though, these two ways of making proofs are the
same, in the sense that what Coq is actually doing when it's
following the commands in a Proof script is

*literally*attempting to construct an expression with the desired type.Print okdw'.

(* ===> okdw' = okd_before wednesday thursday

(okd_before thursday friday

(okd_before friday saturday

(okd_gd saturday gd_sat) db_sat)

db_fri)

db_thu

: ok_day wednesday *)

These expressions are often called
Proof objects are the bedrock of Coq. Tactic proofs are
essentially
The analogy
Just as a set can be empty, a singleton, finite, or infinite — it
can have zero, one, or many inhabitants — a proposition may be
inhabited by zero, one, many, or infinitely many proofs. 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.
We've seen that the → operator (implication) builds bigger
propositions from smaller ones. What constitutes evidence for
propositions built in this way? Consider this statement:

*proof objects*.*programs*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. Moreover, we'll see later on in the course that Coq has a number of automation tactics that can construct quite complex proof objects without our needing to specify every step.## The Curry-Howard Correspondence

propositions ~ sets / types proofs ~ data valuesis called the

*Curry-Howard correspondence*(or*Curry-Howard isomorphism*). Many wonderful things follow from it.## Implication

In English: if we have three days, d1 which is before d2
which is before d3, and if we know d3 is ok, then so is
d1.
It should be easy to see how we'd construct a tactic proof of
okd_before2...

#### Exercise: 1 star, optional (okd_before2_valid)

☐
But what should the corresponding proof object look like?
Answer: We've made a notational pun between → as implication
and → as the type of functions. If we take this pun seriously,
then what we're looking for is an expression with

*type*∀ d1 d2 d3, ok_day d3 → day_before d2 d1 → day_before d3 d2 → ok_day d1, and so what we want is a*function*that takes six arguments (three days and three pieces of evidence) and returns a piece of evidence! Here it is:Definition okd_before2_valid' : okd_before2 :=

fun (d1 d2 d3 : day) =>

fun (H : ok_day d3) =>

fun (H0 : day_before d2 d1) =>

fun (H1 : day_before d3 d2) =>

okd_before d1 d2 (okd_before d2 d3 H H1) H0.

#### Exercise: 1 star, optional (okd_before2_valid_defn)

Predict what Coq will print in response to this:Print okd_before2_valid.

## Induction Principles for Inductively Defined Types

*induction principle*for this type.

Check nat_ind.

(* ===> nat_ind : forall P : nat -> Prop,

P 0 ->

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

forall n : nat, P n *)

Note that this is exactly the our_nat_induction property from
above.
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 the induction tactic, to carry out some
proofs. Here, for example, is an alternate proof of a theorem
that we saw in the Basics chapter.

Theorem mult_0_r' : ∀ n:nat,

n * 0 = 0.

Proof.

apply nat_ind.

Case "O". reflexivity.

Case "S". simpl. intros n IHn. rewrite → IHn.

reflexivity. Qed.

This proof is basically the same as the earlier one, but a
few minor differences 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 (plus_one_r')

Complete this proof without using the induction tactic.
☐
The induction principles that Coq generates for other
datatypes defined with Inductive follow a similar pattern. If we
define a type t with constructors c1 ... cn, Coq generates a
theorem with this shape:

t_ind :

∀ P : t → Prop,

... case for c1 ... →

... case for c2 ... →

... →

... case for cn ... →

∀ 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. First, an example where
the constructors take no arguments:
∀ P : t → Prop,

... case for c1 ... →

... case for c2 ... →

... →

... case for cn ... →

∀ n : t, P n

Inductive yesno : Type :=

| yes : yesno

| no : yesno.

Check yesno_ind.

(* ===> yesno_ind : forall P : yesno -> Prop,

P yes ->

P no ->

forall y : yesno, P y *)

#### Exercise: 1 star (rgb)

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.
☐
Here's another example, this time with one of the constructors
taking some arguments.

Inductive natlist : Type :=

| nnil : natlist

| ncons : nat → natlist → natlist.

Check natlist_ind.

(* ===> (modulo a little tidying)

natlist_ind :

forall P : natlist -> Prop,

P nnil ->

(forall (n : nat) (l : natlist), P l -> P (ncons n l)) ->

forall n : natlist, P n *)

Now what will the induction principle look like? ☐
From these examples, we can extract this general rule:

- The type declaration gives several constructors; each corresponds to one clause of the induction principle.
- 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 :

∀ P : ExSet → Prop,

(∀ b : bool, P (con1 b)) →

(∀ (n : nat) (e : ExSet), P e → P (con2 n e)) →

∀ e : ExSet, P e

Give an Inductive definition of ExSet:
∀ P : ExSet → Prop,

(∀ b : bool, P (con1 b)) →

(∀ (n : nat) (e : ExSet), P e → P (con2 n e)) →

∀ e : ExSet, P e

☐
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 to that of natlist. The main difference is
that, here, the whole definition is | nil : list X

| cons : X → list X → list X.

*parameterized*on a set X: that is, 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 :

∀ (X : Type) (P : list X → Prop),

P [] →

(∀ (x : X) (l : list X), P l → P (x :: l)) →

∀ l : list X, P l

Note the wording here (and, accordingly, the form of list_ind):
The ∀ (X : Type) (P : list X → Prop),

P [] →

(∀ (x : X) (l : list X), P l → P (x :: l)) →

∀ l : list X, P l

*whole*induction principle is parameterized on X. That is, list_ind can be thought of as a polymorphic function that, when applied to a type X, gives us back an induction principle specialized to the type list X.#### Exercise: 1 star (tree)

Write out the induction principle that Coq will generate for the following datatype. Compare your answer with what Coq prints.Inductive tree (X:Type) : Type :=

| leaf : X → tree X

| node : tree X → tree X → tree X.

Check tree_ind.

☐

#### Exercise: 1 star (mytype)

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

∀ (X : Type) (P : mytype X → Prop),

(∀ x : X, P (constr1 X x)) →

(∀ n : nat, P (constr2 X n)) →

(∀ m : mytype X, P m →

∀ n : nat, P (constr3 X m n)) →

∀ m : mytype X, P m

☐
∀ (X : Type) (P : mytype X → Prop),

(∀ x : X, P (constr1 X x)) →

(∀ n : nat, P (constr2 X n)) →

(∀ m : mytype X, P m →

∀ n : nat, P (constr3 X m n)) →

∀ m : mytype X, P m

#### Exercise: 1 star, optional (foo)

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

∀ (X Y : Type) (P : foo X Y → Prop),

(∀ x : X, P (bar X Y x)) →

(∀ y : Y, P (baz X Y y)) →

(∀ f1 : nat → foo X Y,

(∀ n : nat, P (f1 n)) → P (quux X Y f1)) →

∀ f2 : foo X Y, P f2

☐
∀ (X Y : Type) (P : foo X Y → Prop),

(∀ x : X, P (bar X Y x)) →

(∀ y : Y, P (baz X Y y)) →

(∀ f1 : nat → foo X Y,

(∀ n : nat, P (f1 n)) → P (quux X Y f1)) →

∀ f2 : foo X Y, P f2

#### Exercise: 1 star, optional (foo')

Consider the following inductive definition:
What induction principle will Coq generate for foo'? Fill
in the blanks, then check your answer with Coq.)
☐
Where does the phrase "induction hypothesis" fit into this
picture?
The induction principle for numbers
We can make the proof more explicit by giving this expression a
name. For example, instead of stating the theorem mult_0_r as
"∀ n, n * 0 = 0," we can write it as "∀ n, P_m0r
n", where P_m0r is defined as...

foo'_ind :

∀ (X : Type) (P : foo' X → Prop),

(∀ (l : list X) (f : foo' X),

_______________________ →

_______________________ ) →

___________________________________________ →

∀ f : foo' X, ________________________

∀ (X : Type) (P : foo' X → Prop),

(∀ (l : list X) (f : foo' X),

_______________________ →

_______________________ ) →

___________________________________________ →

∀ f : foo' X, ________________________

## Induction Hypotheses

∀ P : nat → Prop,

P 0 →

(∀ n : nat, P n → P (S n)) →

∀ 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.
P 0 →

(∀ n : nat, P n → P (S n)) →

∀ n : nat, P n

... or equivalently...

Now when we do the proof it is easier to see where P_m0r
appears.

Theorem mult_0_r'' : ∀ n:nat,

P_m0r n.

Proof.

apply nat_ind.

Case "n = O". reflexivity.

Case "n = S n'".

(* Note the proof state at this point! *)

unfold P_m0r. simpl. intros n' IHn'.

apply IHn'. Qed.

This extra naming step isn't something that we'll do in
normal proofs, but it is useful to do it explicitly for an example
or two, because it allows us to see exactly what the induction
hypothesis is. If we prove ∀ 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 ∀ 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
Some of the examples in the opening discussion of
propositions involved the concept of
Another alternative is to define the concept of evenness directly.
Instead of going indirectly via the evenb function ("a number is
even if a certain computation yields true"), we can say directly
what the concept of evenness means in terms of evidence.

*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'.## Evenness Again

*evenness*. We began with a computation evenb n that*checks*evenness, yielding a boolean. From this, we built a proposition even n (defined in terms of evenb) that*asserts*that n is even. That is, we defined "n is even" to mean "evenb returns true when applied to n."
This definition says that there are two ways to give
evidence that a number m is even. First, 0 is even, and
ev_0 is evidence for this. Second, if m = S (S n) for some
n and we can give evidence e that n is even, then m is
also even, and ev_SS n e is the evidence.

#### Exercise: 1 star, optional (four_ev)

Give a tactic proof and a proof object showing that four is even.Theorem four_ev' :

ev 4.

Proof.

(* FILL IN HERE *) Admitted.

Definition four_ev : ev 4 :=

(* FILL IN HERE *) admit.

☐

#### Exercise: 2 stars (ev_plus4)

Give a tactic proof and a proof object showing that, if n is even, then so is 4+n.Definition ev_plus4 : ∀ n, ev n → ev (4 + n) :=

(* FILL IN HERE *) admit.

Theorem ev_plus4' : ∀ n,

ev n → ev (4 + n).

Proof.

(* FILL IN HERE *) Admitted.

☐
The highly "orthogonal" organization of Coq's design might
suggest that, since we use the keyword Induction to define
primitive propositions together with their evidence, there must be
some sort of induction principles associated with these
definitions. Indeed there are, and in this section we'll take a
look at how they can be used. To get warmed up, let's look at how
the simpler destruct tactic works with inductively defined
evidence.
Besides
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 the tactics that we have already seen
for inductively defined
For example, here we use a destruct on evidence that n is even
in order to show that ev n implies ev (n-2).

#### 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 look a bit cluttered.) ☐## Reasoning by Induction Over Evidence

*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_0 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.*data*to reason instead about inductively defined*evidence*.Theorem ev_minus2: ∀ n,

ev n → ev (pred (pred n)).

Proof.

intros n E.

destruct E as [| n' E'].

Case "E = ev_0". simpl. apply ev_0.

Case "E = ev_SS n' E'". simpl. apply E'. Qed.

#### Exercise: 1 star (ev_minus2_n)

What happens if we try to destruct on n instead of E? ☐*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.

Theorem ev_even : ∀ n,

ev n → even n.

Proof.

intros n E. induction E as [| n' E'].

Case "E = ev_0".

unfold even. reflexivity.

Case "E = ev_SS n' E'".

unfold even. apply IHE'. Qed.

(Of course, we'd expect that even n → ev n also holds. We'll
see how to prove it in the next chapter.)
The induction principle for inductively defined propositions does
not follow quite the same form as that of inductively defined
sets. For now, you can take the intuitive view that induction on
evidence ev n is similar to induction on n, but restricts our
attention to only those numbers for which evidence ev n could be
generated. We'll look at the induction principle of ev in more
depth below, to explain what's really going on.
(* FILL IN HERE *)

☐

#### Exercise: 1 star (ev_even_n)

Could this proof be carried out by induction on n instead of E? ☐#### Exercise: 1 star (l_fails)

The following proof attempt will not succeed.
Theorem l : ∀ n,

ev n.

Proof.

intros n. induction n.

Case "O". simpl. apply ev_0.

Case "S".

...

Briefly explain why.
ev n.

Proof.

intros n. induction n.

Case "O". simpl. apply ev_0.

Case "S".

...

☐

#### Exercise: 2 stars (ev_sum)

Here's another exercise requiring induction.
☐
Here's another situation where we want to analyze evidence for
evenness: proving that if n+2 is even, then n is. Our first
idea might be to use destruct for this kind of case analysis:

Theorem SSev_ev_firsttry : ∀ n,

ev (S (S n)) → ev n.

Proof.

intros n E.

destruct E as [| n' E'].

(* Stuck: destruct gives us un-provable subgoals! *)

Admitted.

But this doesn't work. For example, in the first sub-goal, we've
lost the information that n is 0. The right thing to use here
is actually inversion:

Theorem SSev_even : ∀ n,

ev (S (S n)) → ev n.

Proof.

intros n E. inversion E as [| n' E']. apply E'. Qed.

(* Print SSev_even. *)

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 here.)
We'll begin exploring this more general behavior of inversion in
what follows.

#### Exercise: 1 star (inversion_practice)

The inversion tactic can also be used to derive goals by showing
the 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
get some auxiliary equalities that are rewritten in the goal
but not in the other hypotheses.

Theorem ev_minus2': ∀ n,

ev n → ev (pred (pred n)).

Proof.

intros n E. inversion E as [| n' E'].

Case "E = ev_0". simpl. apply ev_0.

Case "E = ev_SS n' E'". simpl. apply E'. Qed.

#### Exercise: 3 stars (ev_ev_even)

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

#### Exercise: 3 stars, optional (ev_plus_plus)

Here's an exercise that just requires applying existing lemmas. No induction or even case analysis is needed, but some of the rewriting may be tedious. You'll want the replace tactic used for plus_swap' in Basics.v
☐
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. Which we choose is basically a question of taste.
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:
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 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:

## Why Define Propositions Inductively?

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

Inductive MyProp : nat → Prop :=

| MyProp1 : MyProp 4

| MyProp2 : ∀ n:nat, MyProp n → MyProp (4 + n)

| MyProp3 : ∀ n:nat, MyProp (2 + n) → MyProp n.

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.

Theorem MyProp_ten : MyProp 10.

Proof.

apply MyProp3. simpl.

assert (12 = 4 + 8) as H12.

Case "Proof of assertion". reflexivity.

rewrite → H12.

apply MyProp2.

assert (8 = 4 + 4) as H8.

Case "Proof of assertion". reflexivity.

rewrite → H8.

apply MyProp2.

apply MyProp1. Qed.

Theorem MyProp_0 : MyProp 0.

Proof.

(* FILL IN HERE *) Admitted.

Theorem MyProp_plustwo : ∀ n:nat, MyProp n → MyProp (S (S n)).

Proof.

(* FILL IN HERE *) Admitted.

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

Theorem MyProp_ev : ∀ n:nat,

ev n → MyProp n.

Proof.

intros n E.

induction E as [| n' E'].

Case "E = ev_0".

apply MyProp_0.

Case "E = ev_SS n' E'".

apply MyProp_plustwo. apply IHE'. Qed.

Here's an informal proof of this theorem:

*Theorem*: For any nat n, if ev n then MyProp n.*Proof*: Suppose n is a nat and E is a derivation of ev n. We must exhibit a derivation of MyProp n. The proof is by induction on E. There are two cases to consider:- If the last step in E is a use of ev_0, then n is 0.
Then we must show that MyProp 0 holds; this is true by
lemma MyProp_0.
- If the last step in E is a use of ev_SS, then n = S (S n') for some n', and there is a derivation of ev n'. We must show MyProp (S (S n')), with the induction hypothesis that MyProp n' holds. But by lemma MyProp_plustwo, it's enough to show MyProp n', which is exactly the induction hypothesis. ☐

#### Exercise: 3 stars (ev_MyProp)

☐
Theorem: For any nat n, if MyProp n then ev n.
Proof:
(* FILL IN HERE *)

☐
Now that we've touched on several of Coq's basic structures,
it may be useful to take a step back and talk a little about how
it all fits together.
Expressions in Coq live in two distinct universes:
The two universes have some deep similarities — in each, we can
talk about values, inductive definitions, quantification, etc. —
but they play quite different roles in defining and reasoning about
mathematical structures.
Both universes start with an infinite set of
The simplest values are expressions consisting entirely of
constructor applications. Examples include:
Such expressions can be thought of as trees. Their leaves are
nullary constructors (applied to no arguments), and their internal
nodes are applications of constructors to one or more values. In
the universe Type, we think of values as
Functions are also values — for example:
Functions that return values in the universe Type represent
Inductive declarations give names to subsets of the set of all
values. For example, the declaration of the inductive type nat
defines a
Inductively defined sets can themselves appear as arguments to
constructors in compound values. Examples:
Also, we can write functions that take sets as arguments and
return sets as results. For example, list is a function that
takes a set X as argument and returns as result the set list
X (whose members are lists with elements drawn from X).
Similarly, the declaration of the inductive type ev defines a
Informally, a
Type, Prop, and compound expressions built from them (like
Type→Type) play a similar classifying role "one level up" —
that is, they can be thought of as the
Propositions and booleans are superficially similar, but they are
really quite different things!
The types A→B and ∀ x:A, B both describe functions from
A to B. The only difference is that, in the second case, the
expression B — the type of the result — can mention the
argument x by name. For example:
In fact, the two ways of writing function types are really the
same: In Coq, A→B is actually just an abbreviation for ∀
x:A, B, where x is some variable name not occurring in B. For
example, the type of fun x:nat => x + x can be written, if we
like, as ∀ x:nat, nat.
In both Type and Prop, we can write functions that transform
values into other values. Also, functions themselves are values;
this means we can
A function of type P→Q in Prop is something that takes
evidence for P as an argument and yields evidence for Q as its
result. Such a function can be regarded as
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
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
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
Since we've spent much of this chapter looking "under the hood" at
formal proofs by induction, now is a good moment to talk a little
about
In the real world of mathematical communication, written proofs
range from extremely longwinded and pedantic to extremely brief
and telegraphic. The ideal is somewhere in between, of course,
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.
With this in mind, we offer two templates below — one for proofs
by induction over
Since inductively defined proof objects are often called
"derivation trees," this form of proof is also known as
This section offers some additional details on how induction works
in Coq. It can safely be skimmed on a first reading. (We
recommend skimming rather than skipping over it outright: it
answers some questions that occur to many Coq users at some point,
so it is useful to have a rough idea of what's here.)
The induction tactic actually does even more low-level
bookkeeping for us than we discussed above.
Recall the informal statement of the induction principle for
natural numbers:
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...

#### Exercise: 3 stars, optional (ev_MyProp_informal)

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

# The Big Picture: Coq's Two Universes

- Type is the universe of
*computations*and*data*. - Prop is the universe of
*logical assertions*and*evidence*.

## Values

*constructors*. Constructors have no internal structure: they are just atomic symbols. For example, true, false, O, S, nil, cons, ev_0, ev_SS, ...- true
- O
- S (S (S O))
- ev_0
- ev_SS (S (S O)) ev_0
- ev_SS (S (S (S (S O)))) (ev_SS (S (S O)) ev_0)

*data*. In Prop, we think of values as*evidence*. Values in Prop are sometimes called*derivation trees*.- fun x => true
- fun b => negb b
- fun n => S (S (S n))
- fun n => fun (P : ev n) => ev_SS (S (S n)) P

*computations*: they take some input values and return an output value computed from the inputs. Functions returning values in Prop are*universally quantified evidence*: that is, they use their inputs to build evidence for some proposition (whose statement may also involve these inputs).## Inductive Definitions

*set*whose*elements*are values representing natural numbers. That is, it picks out a subset nat of the set of all values that satisfies the following properties:- the value O is in this set;
- the set is
*closed*under applications of S (i.e., if a value n is in the set, then S n is too); - it is the smallest set satisfying these conditions (i.e., the
only values in nat are the ones that
*must*be, according to the previous two conditions; there is no other "junk").

- nat
- nil nat
- cons nat O (cons nat (S O) (nil nat))

*family of propositions*whose*elements*are values representing evidence that numbers are even. That is, for each n, the definition picks out a subset ev n of the set of all values, satisfying the following properties:- the value ev_0 is in the set ev O;
- the sets are
*closed*under well-typed applications of ev_SS — i.e., if e is in the set ev n, then ev_SS n e is in the set ev (S (S n)); - it is the smallest family of sets satisfying these
conditions (i.e., the only values in any set ev n are the
ones that
*must*be, according to the previous two conditions; there is no other junk).

## Types and Kinds

*type*in Coq is an expression that is used to classify other expressions. For example, bool, nat, list bool, list nat, nat→nat, and so on are all types. The type bool classifies true and false; the type nat classifies O, S O, S (S O), etc.; the type nat→nat classifies function values (like fun n => S n) that yield a number when given a number as input.*types of type (and proposition) expressions*. Technically, they are called*kinds*, to avoid too many uses of the word "type." For example, the expressions nat, nat→nat and list nat all have kind Type, while list itself has kind Type→Type and ev has kind nat→Prop.## Propositions vs. Booleans

- 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."

## Functions vs. Quantifiers

- The function fun x:nat => x + x has type nat→nat —
that is, it maps each number n to a number.
- The function fun X:Type => nil (list X) has type ∀ X:Type, list (list X) — that is, it maps each set X to a particular list of lists of Xs. (Of course, nil is usually written as [] instead of nil X.)

## Functions vs. Implications

- write higher-order functions that take functions as arguments or return functions as results, and
- apply constructors to functions to build complex values containing functions.

*evidence*that P implies Q, since, whenever we have evidence that P is true, we can apply the function and get back evidence that Q is true: evidence for an implication is a function on evidence. This is why we use the same notation for functions and logical implications in Coq: they are exactly the same thing!# Informal Proofs

*teach*the reader how to produce the former.*ability*to reproduce the formal one for themselves, but it doesn't*teach*them anything.*talking about the same world*and they must*play by the same rules*.## Informal Proofs by Induction

*informal*proofs by induction.*data*(i.e., where the thing we're doing induction on lives in Type) and one for proofs by induction over*evidence*(i.e., where the inductively defined thing lives in Prop). In the rest of this course, please follow one of the two for*all*of your inductive proofs.### Induction Over an Inductively Defined Set

*Template*:-
*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.- 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)>.
- <other cases similarly...> ☐

- 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)>.

*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.
- 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.
length l = length (x::l') = S (length l'),it suffices to show thatindex (S (length l')) l' = None.But this follows directly from the induction hypothesis, picking n' to be length l'. ☐

- Suppose l = []. We must show, for all numbers n,
that, if length [] = n, then index (S n) [] =
None.

### Induction Over an Inductively Defined Proposition

*induction on derivations*.*Template*:-
*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"...>- 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>.
- <other cases similarly...> ☐

- 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>.

*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'.

- Suppose the final rule used to show m <= o is
le_n. Then m = o and the result is immediate.

# Optional Material

## More on the induction Tactic

- 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.

*particular*n (by introducing it into the context) and then telling it to prove something about*all*numbers (by using induction).Theorem plus_assoc' : ∀ n m p : nat,

n + (m + p) = (n + m) + p.

Proof.

(* ...we first introduce all 3 variables into the context,

which amounts to saying "Consider an arbitrary n, m, and

p..." *)

intros n m p.

(* ...We now use the induction tactic to prove P n (that

is, n + (m + p) = (n + m) + p) for _all_ n,

and hence also for the particular n that is in the context

at the moment. *)

induction n as [| n'].

Case "n = O". reflexivity.

Case "n = S n'".

(* In the second subgoal generated by induction -- the

"inductive step" -- we must prove that P n' implies

P (S n') for all n'. The induction tactic

automatically introduces n' and P n' into the context

for us, leaving just P (S n') as the goal. *)

simpl. rewrite → IHn'. reflexivity. Qed.

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

Theorem plus_comm' : ∀ n m : nat,

n + m = m + n.

Proof.

induction n as [| n'].

Case "n = O". intros m. rewrite → plus_0_r. reflexivity.

Case "n = S n'". intros m. simpl. rewrite → IHn'.

rewrite ← plus_n_Sm. reflexivity. Qed.

Note that induction n leaves m still bound in the goal —
i.e., what we are proving inductively is a statement beginning
with ∀ m.
If we do induction on a variable that is quantified in the goal

*after*some other quantifiers, the induction tactic will automatically introduce the variables bound by these quantifiers into the context.Theorem plus_comm'' : ∀ n m : nat,

n + m = m + n.

Proof.

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

induction m as [| m'].

Case "m = O". simpl. rewrite → plus_0_r. reflexivity.

Case "m = S m'". simpl. rewrite ← IHm'.

rewrite ← plus_n_Sm. reflexivity. Qed.

#### Exercise: 1 star, optional (plus_explicit_prop)

Rewrite both plus_assoc' and plus_comm' and their proofs in the same style as mult_0_r'' above — that is, for each theorem, give an explicit Definition of the proposition being proved by induction, and state the theorem and proof in terms of this defined proposition.(* FILL IN HERE *)

☐
One more 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 (true_upto_n__true_everywhere)

Define a recursive function true_upto_n__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.

*)

☐
Earlier, we looked in detail at the induction principles that Coq
generates for inductively defined
For example, from what we've said so far, you might expect the
inductive definition of ev...
But this is a little more flexibility than we actually need or
want: it is giving us a way to prove logical assertions where the
assertion involves properties of some piece of

## Induction Principles in Prop

*sets*. The induction principles for inductively defined*propositions*like ev are a tiny bit more complicated. As with all induction principles, we want to use the induction principle on ev to prove things by inductively considering the possible shapes that something in ev can have — either it is evidence that 0 is even, or it is evidence that, for some n, S (S n) is even, and it includes evidence that n itself is. Intuitively speaking, however, what we want to prove are not statements about*evidence*but statements about*numbers*. So we want an induction principle that lets us prove properties of numbers by induction on evidence.
Inductive ev : nat → Prop :=

| ev_0 : ev O

| ev_SS : ∀ n:nat, ev n → ev (S (S n)).

...to give rise to an induction principle that looks like this...
| ev_0 : ev O

| ev_SS : ∀ n:nat, ev n → ev (S (S n)).

ev_ind_max :

∀ P : (∀ n : nat, ev n → Prop),

P O ev_0 →

(∀ (n : nat) (e : ev n),

P n e → P (S (S n)) (ev_SS n e)) →

∀ (n : nat) (e : ev n), P n e

... because:
∀ P : (∀ n : nat, ev n → Prop),

P O ev_0 →

(∀ (n : nat) (e : ev n),

P n e → P (S (S n)) (ev_SS n e)) →

∀ (n : nat) (e : ev n), P n e

- 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.

- We must prove that P holds for O and ev_0.
- 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.

*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:
∀ P : nat → Prop,

... →

∀ n : nat, ev n → P n

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

∀ n : nat, ev n → P n

Check ev_ind.

(* ===> ev_ind

: forall P : nat -> Prop,

P 0 ->

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

forall n : nat, ev n -> P n *)

In particular, Coq has dropped the evidence term e as a parameter
of the the proposition P, and consequently has rewritten the
assumption ∀ (n:nat) (e:ev n), ... to be ∀ (n:nat), ev
n → ...; i.e., we no longer require explicit evidence of the
provability of ev n.
In English, ev_ind says:
We can apply ev_ind directly instead of using induction,
following pretty much the same pattern as above.

- Suppose, P is a property of 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).

- P holds for 0

Theorem ev_even' : ∀ n,

ev n → even n.

Proof.

apply ev_ind.

Case "ev_0". unfold even. reflexivity.

Case "ev_SS". intros n' E' IHE'. unfold even. apply IHE'. Qed.

#### 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.
☐

#### Exercise: 3 stars, optional (ev_MyProp')

Prove ev_MyProp again, using apply MyProp_ind instead of the induction tactic.Theorem ev_MyProp' : ∀ n:nat,

MyProp n → ev n.

Proof.

apply MyProp_ind.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 4 stars, optional (MyProp_pfobj)

Prove MyProp_ev and ev_MyProp again by constructing explicit proof objects by hand (as you did above in ev_plus4, for example).(* FILL IN HERE *)

☐

Inductive p : (tree nat) → nat → Prop :=

| c1 : ∀ n, p (leaf _ n) 1

| c2 : ∀ t1 t2 n1 n2,

p t1 n1 → p t2 n2 → p (node _ t1 t2) (n1 + n2)

| c3 : ∀ t n, p t n → p t (S n).

Describe, in English, the conditions under which the
proposition p t n is provable.
(* FILL IN HERE *)

☐

☐

# Additional Exercises

#### Exercise: 4 stars (palindromes)

A palindrome is a sequence that reads the same backwards as forwards.- Define an inductive proposition pal on list X that
captures what it means to be a palindrome. (Hint: You'll need
three cases. Your definition should be based on the structure
of the list; just having a single constructor
c : ∀ l, l = rev l → pal lmay seem obvious, but will not work very well.)
- Prove that
∀ l, pal (l ++ rev l).
- Prove that
∀ l, pal l → l = rev l.

(* FILL IN HERE *)

☐

#### Exercise: 5 stars, optional (palindrome_converse)

Using your definition of pal from the previous exercise, prove that
∀ l, l = rev l → pal l.

(* FILL IN HERE *)

☐

#### Exercise: 4 stars (subsequence)

A list is a*subsequence*of another list if all of the elements in the first list occur in the same order in the second list, possibly with some extra elements in between. For example,
[1,2,3]

is a subsequence of each of the lists
[1,2,3]

[1,1,1,2,2,3]

[1,2,7,3]

[5,6,1,9,9,2,7,3,8]

but it is [1,1,1,2,2,3]

[1,2,7,3]

[5,6,1,9,9,2,7,3,8]

*not*a subsequence of any of the lists
[1,2]

[1,3]

[5,6,2,1,7,3,8]

[1,3]

[5,6,2,1,7,3,8]

- Define an inductive proposition subseq on list nat that
captures what it means to be a subsequence. (Hint: You'll need
three cases.)
- Prove that subsequence is reflexive, that is, any list is a
subsequence of itself.
- Prove that for any lists l1, l2, and l3, if l1 is a
subsequence of l2, then l1 is also a subsequence of l2 ++
l3.
- (Optional, harder) Prove that subsequence is transitive — that is, if l1 is a subsequence of l2 and l2 is a subsequence of l3, then l1 is a subsequence of l3. Hint: choose your induction carefully!

(* FILL IN HERE *)

☐
☐
☐
☐
☐

#### Exercise: 2 stars, optional (foo_ind_principle)

Suppose we make the following inductive definition:
Inductive foo (X : Set) (Y : Set) : Set :=

| foo1 : X → foo X Y

| foo2 : Y → foo X Y

| foo3 : foo X Y → foo X Y.

Fill in the blanks to complete the induction principle that will be
generated by Coq.
| foo1 : X → foo X Y

| foo2 : Y → foo X Y

| foo3 : foo X Y → foo X Y.

foo_ind

: ∀ (X Y : Set) (P : foo X Y → Prop),

(∀ x : X, __________________________________) →

(∀ y : Y, __________________________________) →

(________________________________________________) →

________________________________________________

: ∀ (X Y : Set) (P : foo X Y → Prop),

(∀ x : X, __________________________________) →

(∀ y : Y, __________________________________) →

(________________________________________________) →

________________________________________________

#### Exercise: 2 stars, optional (bar_ind_principle)

Consider the following induction principle:
bar_ind

: ∀ P : bar → Prop,

(∀ n : nat, P (bar1 n)) →

(∀ b : bar, P b → P (bar2 b)) →

(∀ (b : bool) (b0 : bar), P b0 → P (bar3 b b0)) →

∀ b : bar, P b

Write out the corresponding inductive set definition.
: ∀ P : bar → Prop,

(∀ n : nat, P (bar1 n)) →

(∀ b : bar, P b → P (bar2 b)) →

(∀ (b : bool) (b0 : bar), P b0 → P (bar3 b b0)) →

∀ b : bar, P b

Inductive bar : Set :=

| bar1 : ________________________________________

| bar2 : ________________________________________

| bar3 : ________________________________________.

| bar1 : ________________________________________

| bar2 : ________________________________________

| bar3 : ________________________________________.

#### Exercise: 2 stars, optional (no_longer_than_ind)

Given the following inductively defined proposition:
Inductive no_longer_than (X : Set) : (list X) → nat → Prop :=

| nlt_nil : ∀ n, no_longer_than X [] n

| nlt_cons : ∀ x l n, no_longer_than X l n →

no_longer_than X (x::l) (S n)

| nlt_succ : ∀ l n, no_longer_than X l n →

no_longer_than X l (S n).

write the induction principle generated by Coq.
| nlt_nil : ∀ n, no_longer_than X [] n

| nlt_cons : ∀ x l n, no_longer_than X l n →

no_longer_than X (x::l) (S n)

| nlt_succ : ∀ l n, no_longer_than X l n →

no_longer_than X l (S n).

no_longer_than_ind

: ∀ (X : Set) (P : list X → nat → Prop),

(∀ n : nat, ____________________) →

(∀ (x : X) (l : list X) (n : nat),

no_longer_than X l n → ____________________ →

_____________________________ →

(∀ (l : list X) (n : nat),

no_longer_than X l n → ____________________ →

_____________________________ →

∀ (l : list X) (n : nat), no_longer_than X l n →

____________________

: ∀ (X : Set) (P : list X → nat → Prop),

(∀ n : nat, ____________________) →

(∀ (x : X) (l : list X) (n : nat),

no_longer_than X l n → ____________________ →

_____________________________ →

(∀ (l : list X) (n : nat),

no_longer_than X l n → ____________________ →

_____________________________ →

∀ (l : list X) (n : nat), no_longer_than X l n →

____________________

#### Exercise: 2 stars, optional (R_provability)

Suppose we give Coq the following definition:
Inductive R : nat → list nat → Prop :=

| c1 : R 0 []

| c2 : ∀ n l, R n l → R (S n) (n :: l)

| c3 : ∀ n l, R (S n) l → R n l.

Which of the following propositions are provable?
| c1 : R 0 []

| c2 : ∀ n l, R n l → R (S n) (n :: l)

| c3 : ∀ n l, R (S n) l → R n l.

- R 2 [1,0]
- R 1 [1,2,1,0]
- R 6 [3,2,1,0]