# Library Ind

(* Induction

Version of 4/28/2009

*)

Require Export Poly.

Version of 4/28/2009

*)

Require Export Poly.

Administrivia...

What we've seen so far:

- Midterm I is Wednesday Feb 18

- New convention for "exercise stars"...

- one star: very easy exercises that should be considered as REQUIRED (ideally they should be done while reading the lecture notes), but that are NOT TO BE HANDED IN (and will not be graded)

- two, three, or four stars: real homework problems that (unless explicitly marked "optional") should be done and handed in for grading

What we've seen so far:

- inductive definitions of datatypes
- Fixpoints over inductive datatypes
- higher-order functions (map, filter, etc.)
- polymorphism
- basic Coq
- inductive proofs
- several fundamental tactics

- more on induction: generalizing the IH, induction principles
- "programming with propositions"
- logical connectives as inductive propositions

A PROPOSITION is a factual claim. In Coq, propositions
are written as expressions of type Prop.

(* Check (plus 2 2 = 4). *)

(* Check (ble_nat 3 2 = false). *)

(* Check (ble_nat 3 2 = false). *)

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

(* Check (plus 2 2 = 4). *)

(* Check (plus 2 2 = 5). *)

(* Check (plus 2 2 = 5). *)

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

Theorem plus_2_2_is_4 :

plus 2 2 = 4.

Proof. reflexivity. Qed.

plus 2 2 = 4.

Proof. reflexivity. Qed.

Coq allows us to do many other things with
propositions. For example, we can give a name to a
proposition using a Definition.

Definition plus_fact : Prop := plus 2 2 = 4.

(* Check plus_fact. *)

Theorem plus_fact_is_true :

plus_fact.

Proof. unfold plus_fact. reflexivity. Qed.

(* Check plus_fact. *)

Theorem plus_fact_is_true :

plus_fact.

Proof. unfold plus_fact. reflexivity. Qed.

Note that we need an unfold in the proof because
plus_fact was introduced as a Definition.

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

Definition even (n:nat) :=

evenb n = true.

evenb n = true.

even is a PARAMETERIZED PROPOSITION. Think of it as a
FUNCTION that, when applied to a number n, yields a
proposition asserting that n is even.

(* Check even. *)

(* Check (even 4). *)

(* Check (even 4). *)

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:

Definition even_n__even_SSn (n:nat) :=

(even n) -> (even (S (S n))).

(even n) -> (even (S (S n))).

We can define them to take multiple arguments...

Definition between (n m o: nat) : Prop :=

andb (ble_nat n o) (ble_nat o m) = true.

andb (ble_nat n o) (ble_nat o m) = true.

... and then partially apply them:

Definition teen : nat->Prop := between 13 19.

We can pass propositions -- and even 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).

Definition preserved_by_S (P:nat->Prop) : Prop :=

forall n', P n' -> P (S n').

Definition true_for_all_numbers (P:nat->Prop) : Prop :=

forall n, P n.

Definition nat_induction (P:nat->Prop) : Prop :=

(true_for_zero P)

-> (preserved_by_S P)

-> (true_for_all_numbers P).

P 0.

Definition true_for_n__true_for_Sn (P:nat->Prop) (n:nat) : Prop :=

P n -> P (S n).

Definition preserved_by_S (P:nat->Prop) : Prop :=

forall n', P n' -> P (S n').

Definition true_for_all_numbers (P:nat->Prop) : Prop :=

forall n, P n.

Definition nat_induction (P:nat->Prop) : Prop :=

(true_for_zero P)

-> (preserved_by_S P)

-> (true_for_all_numbers P).

Let's unravel what this means in concrete terms:

Example nat_induction_example : forall (P:nat->Prop),

nat_induction P

= ( (P 0)

-> (forall n', P n' -> P (S n'))

-> (forall n, P n)).

Proof.

unfold nat_induction, true_for_zero, preserved_by_S, true_for_all_numbers.

reflexivity. Qed.

Theorem our_nat_induction_works : forall (P:nat->Prop),

nat_induction P.

Proof.

intros P.

unfold nat_induction.

intros TFZ PPS.

unfold true_for_all_numbers. intros n.

induction n as [| n'].

Case "n = O". apply TFZ.

Case "n = S n'". apply PPS. apply IHn'. Qed.

nat_induction P

= ( (P 0)

-> (forall n', P n' -> P (S n'))

-> (forall n, P n)).

Proof.

unfold nat_induction, true_for_zero, preserved_by_S, true_for_all_numbers.

reflexivity. Qed.

Theorem our_nat_induction_works : forall (P:nat->Prop),

nat_induction P.

Proof.

intros P.

unfold nat_induction.

intros TFZ PPS.

unfold true_for_all_numbers. intros n.

induction n as [| n'].

Case "n = O". apply TFZ.

Case "n = S n'". apply PPS. apply IHn'. Qed.

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:

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:

(* Check nat_ind. *)

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

Here's a more direct proof that our induction principle
is valid, using the nat_ind axiom directly (with apply
instead of induction).

Theorem our_nat_induction_works' :

forall P, nat_induction P.

Proof.

intros P.

unfold nat_induction, true_for_zero,

preserved_by_S, true_for_all_numbers.

apply nat_ind. Qed.

forall P, nat_induction P.

Proof.

intros P.

unfold nat_induction, true_for_zero,

preserved_by_S, true_for_all_numbers.

apply nat_ind. Qed.

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

Theorem mult_0_r' : forall n:nat,

mult n 0 = 0.

Proof.

apply nat_ind.

Case "O". reflexivity.

Case "S". simpl. intros n IHn. rewrite -> IHn.

simpl. reflexivity. Qed.

mult n 0 = 0.

Proof.

apply nat_ind.

Case "O". reflexivity.

Case "S". simpl. intros n IHn. rewrite -> IHn.

simpl. reflexivity. Qed.

Some things to note:

- In the induction step of the proof we have to do a little manual bookkeeping (the intros)

- We do not introduce n into the context before applying nat_ind

- The apply tactic automatically chooses variable names for us (in the second subgoal, here), whereas induction gives us a way to specify what names should be used. The automatic choice is suboptimal.

Theorem plus_one_r' : forall n:nat,

plus n 1 = S n.

Proof.

(* Complete this proof without using the induction tactic. *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

plus n 1 = S n.

Proof.

(* Complete this proof without using the induction tactic. *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

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.

Theorem plus_one_r'' : forall n:nat,

plus n 1 = S n.

Proof.

plus n 1 = S n.

Proof.

Prove the same theorem again without induction or
apply nat_ind.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

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

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

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

Inductive yesno : Set :=

| yes : yesno

| no : yesno.

(* Check yesno_ind. *)

Yields:
yesno_ind
: forall P : yesno -> Prop,
P yes

- > P no
- > forall y : yesno, P y

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.

Inductive rgb : Set :=

| red : rgb

| green : rgb

| blue : rgb.

(* Check rgb_ind. *)

Inductive natlist : Set :=

| nnil : natlist

| ncons : nat -> natlist -> natlist.

(* Check natlist_ind. *)

| red : rgb

| green : rgb

| blue : rgb.

(* Check rgb_ind. *)

Inductive natlist : Set :=

| nnil : natlist

| ncons : nat -> natlist -> natlist.

(* Check natlist_ind. *)

Yields (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

Suppose we had written the above definition a little
differently:

Inductive natlist1 : Set :=

| nnil1 : natlist1

| nsnoc1 : natlist1 -> nat -> natlist1.

| nnil1 : natlist1

| nsnoc1 : natlist1 -> nat -> natlist1.

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

Here is an induction principle for an inductively
defined set s.

ExSet_ind : forall P : ExSet -> Prop, (forall b : bool, P (con1 b))

Inductive ExSet : Set := (* FILL IN HERE

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

Inductive ExSet : Set := (* FILL IN HERE

*)

(** Now, what about polymorphic datatypes?

The inductive definition of polymorphic lists

Inductive list (X:Set) : Set :=

| 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 : Set) (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. *)

Inductive tree (X:Set) : Set :=

| leaf : X -> tree X

| node : tree X -> tree X -> tree X.

(* Check tree_ind. *)

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

mytype_ind : forall (X : Set) (P : mytype X -> Prop), (forall x : X, P (constr1 X x))

mytype_ind : forall (X : Set) (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

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

foo_ind : forall (X Y : Set) (P : foo X Y -> Prop), (forall x : X, P (bar X Y x))

foo_ind : forall (X Y : Set) (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

Consider the following inductive definition:

Inductive foo' (X:Set) : Set :=

| C1 : list X -> foo' X -> foo' X

| C2 : foo' X.

| C1 : list X -> foo' X -> foo' X

| C2 : foo' X.

What induction principle will Coq generate for foo'?
(FILL IN THE BLANKS, then check your answer with Coq.)

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

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

- > _________________________________________________
- > forall f : foo' X, _______________________________

The induction principle for numbers

forall P : nat -> Prop, P 0

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

forall P : nat -> Prop, P 0

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

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

Definition P_m0r (n:nat) : Prop :=

mult n 0 = 0.

... or equivalently...

Definition P_m0r' : nat->Prop :=

fun n => mult n 0 = 0.

Theorem mult_0_r'' : forall n:nat,

P_m0r n.

Proof.

apply nat_ind.

Case "n = O". unfold P_m0r. reflexivity.

Case "n = S n'".

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

unfold P_m0r. simpl. intros n IHn.

rewrite -> IHn. reflexivity. Qed.

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:

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

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.

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

Theorem plus_assoc' : forall n m p : nat,

plus n (plus m p) = plus (plus n m) p.

Proof.

plus n (plus m p) = plus (plus 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, plus n (plus m p) = plus (plus 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'".

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' : forall n m : nat,

plus n m = plus 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.

plus n m = plus 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 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.

Theorem plus_comm'' : forall n m : nat,

plus n m = plus m n.

Proof.

plus n m = plus 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.

Case "m = O". simpl. rewrite -> plus_0_r. reflexivity.

Case "m = S m'". simpl. rewrite <- IHm'.

rewrite <- plus_n_Sm. reflexivity. Qed.

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

(* Define a recursive function [true_upto_n_implies_true_everywhere] that makes [true_upto_n_example] work. *) Fixpoint true_upto_n__true_everywhere (* OPTEXERCISE...*) (n:nat) (P:nat->Prop) {struct n} : Prop := match n with | 0 => (forall m, P m) | S n' => (P (S n') -> true_upto_n__true_everywhere n' P) end. 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.

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

Theorem double_injective_FAILED : forall 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".

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

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

Theorem double_injective' : forall 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'".

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

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.

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.

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

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.

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 : forall n m,

double n = double m

-> n = m.

Proof.

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

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 a nat m be given. We prove:

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.

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

Proof: Let a nat m be given. We prove:

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.

Theorem plus_n_n_injective_take2 : forall n m,

plus n n = plus m m

-> n = m.

Proof.

plus n n = plus m m

-> n = m.

Proof.

Carry out this proof by induction on m.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem index_after_last : forall (n : nat) (X : Set)

(l : list X),

length l = n

-> index (S n) l = None.

Proof.

(* Prove this by induction on l *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem index_after_last : forall (n : nat) (X : Set)

(l : list X),

length l = n

-> index (S n) l = None.

Proof.

(* Prove this by induction on l *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

(* 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 *)

*)

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

*)

Theorem length_snoc''' : forall (n : nat) (X : Set)

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

length l = n

-> length (snoc l v) = S n.

Proof.

(* Prove this by induction on l. *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

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

length l = n

-> length (snoc l v) = S n.

Proof.

(* Prove this by induction on l. *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem eqnat_false_S : forall n m,

beq_nat n m = false -> beq_nat (S n) (S m) = false.

Proof.

(* Prove this by induction on m. *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

beq_nat n m = false -> beq_nat (S n) (S m) = false.

Proof.

(* Prove this by induction on m. *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem length_append_cons : forall (X : Set) (l1 l2 : list X)

(x : X) (n : nat),

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

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

Proof.

(* Prove this by induction on l1, without using app_length. *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

(x : X) (n : nat),

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

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

Proof.

(* Prove this by induction on l1, without using app_length. *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem length_appendtwice : forall (X:Set) (n:nat)

(l:list X),

length l = n

-> length (l ++ l) = plus n n.

Proof.

(* Prove this by induction on l, without using app_length. *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

(l:list X),

length l = n

-> length (l ++ l) = plus n n.

Proof.

(* Prove this by induction on l, without using app_length. *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

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.

Inductive ev : nat -> Prop :=

| ev_0 : ev O

| ev_SS : forall n:nat, ev n -> ev (S (S n)).

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 Set. 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 Set world) or sets of evidence. Let's look at the parts of the inductive definition of ev above:

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

Definition four_ev : ev 4 :=

ev_SS 2 (ev_SS 0 ev_0).

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.

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.

Theorem four_ev' :

ev 4.

Proof.

apply ev_SS. apply ev_SS. apply ev_0. Qed.

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:

(* Print four_ev'. *)

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.

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.

Definition ev_plus4 : forall n, ev n -> ev (plus 4 n) :=

fun (n : nat) =>

fun (E : ev n) =>

ev_SS (S (S n)) (ev_SS n E).

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

Theorem ev_plus4' : forall n,

ev n -> ev (plus 4 n).

Proof.

intros n E. simpl. apply ev_SS. apply ev_SS. apply E. Qed.

ev n -> ev (plus 4 n).

Proof.

intros n E. simpl. apply ev_SS. apply ev_SS. apply E. Qed.

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

(* Print ev_plus4'. *)

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:

For example, consider this theorem:

Definition ev_ten : ev 10 :=

ev_plus4 6 (ev_plus4 2 (ev_SS 0 ev_0)).

ev_plus4 6 (ev_plus4 2 (ev_SS 0 ev_0)).

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

(* Eval simpl in (plus 4 (plus 4 2)). *)

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

(* Eval compute in (ev_plus4 6 (ev_plus4 2 (ev_SS 0 ev_0))). *)

(Note that 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 Set->Set, which is the type of things like list, there is (nat->Prop)->Prop, the type of things like nat_ind, and so on.

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 Set->Set, which is the type of things like list, there is (nat->Prop)->Prop, the type of things like nat_ind, and so on.

Construct a tactic proof of the following
proposition.

Theorem double_even : forall n,

ev (double n).

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

ev (double n).

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

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

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 ev (n-2). (Recall that pred 0 is 0.)

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 ev (n-2). (Recall that pred 0 is 0.)

Theorem ev_minus2: forall 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.

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.

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.

Theorem ev_even : forall 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. simpl. unfold even in IHE'. apply IHE'. Qed.

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. simpl. unfold even in IHE'. apply IHE'. Qed.

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

(* 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 *)

*)

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

*)

Here's another exercise requiring induction.

Theorem ev_sum : forall n m,

ev n -> ev m -> ev (n+m).

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

ev n -> ev m -> ev (n+m).

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

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

Theorem SSev_ev_firsttry : forall n,

ev (S (S n)) -> ev n.

Proof.

intros n E.

destruct E as [| n' E'].

(* Oops. destruct destroyed far too much!

In the first sub-goal, we don't know that n is 0. *)

Admitted.

ev (S (S n)) -> ev n.

Proof.

intros n E.

destruct E as [| n' E'].

(* Oops. destruct destroyed far too much!

In the first sub-goal, we don't know that n is 0. *)

Admitted.

The right thing to use here is inversion (!)

Theorem SSev_even : forall n,

ev (S (S n)) -> ev n.

Proof.

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

(* Print SSev_even. *)

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

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 general behavior of inversion in what follows.

Theorem SSSSev_even : forall n,

ev (S (S (S (S n)))) -> ev n.

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

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

Theorem even5_nonsense :

ev 5 -> plus 2 2 = 9.

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

ev 5 -> plus 2 2 = 9.

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

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 which are
rewritten in the goal but not in the other hypotheses.

Theorem ev_minus2': forall 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.

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.

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

Theorem ev_ev_even : forall n m,

ev (n+m) -> ev n -> ev m.

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

ev (n+m) -> ev n -> ev m.

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

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:

1) the number 4 has property MyProp 2) if n has property MyProp, then so does 4+n 3) if n+2 has property MyProp, then so does n 4) 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:

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:

1) the number 4 has property MyProp 2) if n has property MyProp, then so does 4+n 3) if n+2 has property MyProp, then so does n 4) 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:

Inductive MyProp : nat -> Prop :=

| MyProp1 : MyProp 4

| MyProp2 : forall n:nat, MyProp n -> MyProp (plus 4 n)

| MyProp3 : forall n:nat, MyProp (plus 2 n) -> MyProp n.

| MyProp1 : MyProp 4

| MyProp2 : forall n:nat, MyProp n -> MyProp (plus 4 n)

| MyProp3 : forall n:nat, MyProp (plus 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 = plus 4 8) as H12.

Case "Proof of assertion". reflexivity.

rewrite -> H12.

apply MyProp2.

assert (8 = plus 4 4) as H8.

Case "Proof of assertion". reflexivity.

rewrite -> H8.

apply MyProp2.

apply MyProp1. Qed.

Proof.

apply MyProp3. simpl.

assert (12 = plus 4 8) as H12.

Case "Proof of assertion". reflexivity.

rewrite -> H12.

apply MyProp2.

assert (8 = plus 4 4) as H8.

Case "Proof of assertion". reflexivity.

rewrite -> H8.

apply MyProp2.

apply MyProp1. Qed.

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

Theorem MyProp_0 : MyProp 0.

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem MyProp_plustwo : forall n:nat, MyProp n -> MyProp (S (S n)).

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem MyProp_plustwo : forall n:nat, MyProp n -> MyProp (S (S n)).

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

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

Theorem MyProp_ev : forall 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.

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: Let a nat n and a derivation E of ev n be given. We go by induction on E. There are two case:

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

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

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:

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

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

Theorem ev_MyProp : forall n:nat,

MyProp n -> ev n.

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

(* EXERCISE: 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 *)

*)

MyProp n -> ev n.

Proof.

(* FILL IN HERE (and delete "Admitted") *) Admitted.

(* EXERCISE: 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 *)

*)

(* Prove MyProp_ev and ev_MyProp again by constructing

explicit proof objects by hand (as we did above in

ev_plus4, for example). *)

(* FILL IN HERE *)

explicit proof objects by hand (as we did above in

ev_plus4, for example). *)

(* FILL IN HERE *)

Theorem ev_MyProp' : forall n:nat,

MyProp n -> ev n.

Proof.

(* Complete this proof using apply MyProp_ind instead

of the induction tactic. *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

(* --------------------------------------------------- *)

(* Induction principles for inductively defined Props *)

MyProp n -> ev n.

Proof.

(* Complete this proof using apply MyProp_ind instead

of the induction tactic. *)

(* FILL IN HERE (and delete "Admitted") *) Admitted.

(* --------------------------------------------------- *)

(* 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:

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

(* Check ev_ind. *)

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

Theorem ev_even' : forall n,

ev n -> even n.

Proof.

apply ev_ind.

Case "ev_0". unfold even. reflexivity.

Case "ev_SS". intros n H IHE. unfold even. apply IHE. Qed.

ev n -> even n.

Proof.

apply ev_ind.

Case "ev_0". unfold even. reflexivity.

Case "ev_SS". intros n H IHE. unfold even. apply IHE. Qed.

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.

(* Check list_ind. *)

(* Check MyProp_ind. *)

(* Check MyProp_ind. *)

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

Lemma failed_proof : forall n,

ev n.

Proof.

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

Case "n = O". simpl. apply ev_0.

Case "n = S n'".

Admitted.

(*

(* FILL IN HERE *)

*)

ev n.

Proof.

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

Case "n = O". simpl. apply ev_0.

Case "n = S n'".

Admitted.

(*

(* FILL IN HERE *)

*)

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

(1) Define an inductive proposition pal on list nat that captures what it means to be a palindrome. (Hint: You'll need three cases.)

(2) Prove that

forall l, pal(l++(rev l))

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

(1) Define an inductive proposition pal on list nat that captures what it means to be a palindrome. (Hint: You'll need three cases.)

(2) Prove that

forall l, pal(l++(rev l))

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

(* FILL IN HERE *)