# MoreCoqMore About Coq

Require Export Poly.

Theorem silly1 : ∀(n m o p : nat),

n = m →

[n;o] = [n;p] →

[n;o] = [m;p].

Proof.

intros n m o p eq1 eq2.

rewrite ← eq1.

(* At this point, we could finish with

"rewrite → eq2. reflexivity." as we have

done several times above. But we can achieve the

same effect in a single step by using the

apply tactic instead: *)

apply eq2. Qed.

apply also works with

*conditional*hypotheses:Theorem silly2 : ∀(n m o p : nat),

n = m →

(∀(q r : nat), q = r → [q;o] = [r;p]) →

[n;o] = [m;p].

Proof.

intros n m o p eq1 eq2.

apply eq2. apply eq1. Qed.

Could we have completed this proof without apply?
(1 for yes, 2 for no)

Observe how Coq picks appropriate values for the universal
variables of the hypothesis here:

Theorem silly2a : ∀(n m : nat),

(n,n) = (m,m) →

(∀(q r : nat), (q,q) = (r,r) → [q] = [r]) →

[n] = [m].

Proof.

intros n m eq1 eq2.

apply eq2. apply eq1. Qed.

The goal must match the hypothesis

*exactly*for apply to work:Theorem silly3_firsttry : ∀(n : nat),

true = beq_nat n 5 →

beq_nat (S (S n)) 7 = true.

Proof.

intros n H.

simpl.

(* Here we cannot use apply directly *)

Abort.

In this case we can use the symmetry tactic, which switches the
left and right sides of an equality in the goal.

Theorem silly3 : ∀(n : nat),

true = beq_nat n 5 →

beq_nat (S (S n)) 7 = true.

Proof.

intros n H.

symmetry.

simpl. (* Actually, this simpl is unnecessary, since

apply will perform simplification first. *)

apply H. Qed.

# The apply ... with ... Tactic

Example trans_eq_example : ∀(a b c d e f : nat),

[a;b] = [c;d] →

[c;d] = [e;f] →

[a;b] = [e;f].

Proof.

intros a b c d e f eq1 eq2.

rewrite → eq1. rewrite → eq2. reflexivity. Qed.

Theorem trans_eq : ∀(X:Type) (n m o : X),

n = m → m = o → n = o.

Proof.

intros X n m o eq1 eq2. rewrite → eq1. rewrite → eq2.

reflexivity. Qed.

But applying this lemma requires a slight
variation on apply:

Example trans_eq_example' : ∀(a b c d e f : nat),

[a;b] = [c;d] →

[c;d] = [e;f] →

[a;b] = [e;f].

Proof.

intros a b c d e f eq1 eq2.

(* Doing apply trans_eq doesn't work! But... *)

apply trans_eq with (m:=[c;d]). apply eq1. apply eq2. Qed.

In practice, often Coq can figure out the correct variable
and we can omit the "m :=" part.

# The inversion tactic

*injective*and

*disjoint*.

- the only way we can have S n = S m is if n = m (that is, S
is
*injective*) - O is not equal to S n for any n (that is, O and S are
*disjoint*)

c a1 a2 ... an = d b1 b2 ... bm

for some constructors c and d and arguments a1 ... an and
b1 ... bm. Then inversion H instructs Coq to "invert" this
equality to extract the information it contains about these terms:
- If c and d are the same constructor, then we know, by the
injectivity of this constructor, that a1 = b1, a2 = b2,
etc.; inversion H adds these facts to the context, and tries
to use them to rewrite the goal.
- If c and d are different constructors, then the hypothesis H is contradictory. That is, a false assumption has crept into the context, and this means that any goal whatsoever is provable! In this case, inversion H marks the current goal as completed and pops it off the goal stack.

Theorem eq_add_S : ∀(n m : nat),

S n = S m →

n = m.

Proof.

intros n m eq. inversion eq. reflexivity. Qed.

Theorem silly4 : ∀(n m : nat),

[n] = [m] →

n = m.

Proof.

intros n o eq. inversion eq. reflexivity. Qed.

Theorem silly5 : ∀(n m o : nat),

[n;m] = [o;o] →

[n] = [m].

Proof.

intros n m o eq. inversion eq. reflexivity. Qed.

Theorem silly6 : ∀(n : nat),

S n = O →

2 + 2 = 5.

Proof.

intros n contra. inversion contra. Qed.

Theorem silly7 : ∀(n m : nat),

false = true →

[n] = [m].

Proof.

intros n m contra. inversion contra. Qed.

A useful theorem in the reverse direction:

Theorem f_equal : ∀(A B : Type) (f: A → B) (x y: A),

x = y → f x = f y.

Proof. intros A B f x y eq. rewrite eq. reflexivity. Qed.

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

A couple more nontrivial but not-too-complicated proofs to work together in class, or for you to work as exercises.Theorem beq_nat_0_l : ∀n,

beq_nat 0 n = true → n = 0.

Proof.

(* FILL IN HERE *) Admitted.

Theorem beq_nat_0_r : ∀n,

beq_nat n 0 = true → n = 0.

Proof.

(* FILL IN HERE *) Admitted.

☐

Suppose Coq's proof state looks like
(1) No change
(2) Substitute true with false in the conclusion, leaving
negb false = negb false
(3) "No more subgoals"

1 subgoals, subgoal 1

H : false = true

============================

negb true = negb false

and we apply the tactic inversion H. What will happen?
H : false = true

============================

negb true = negb false

Suppose Coq's proof state looks like
(1) No change
(2) "No more subgoals"

1 subgoals, subgoal 1

x : bool

y : bool

H : x = y

============================

y = x

and we apply the tactic inversion H. What will happen?
x : bool

y : bool

H : x = y

============================

y = x

Suppose Coq's proof state looks like
(1) No change
(2) "No more subgoals"

1 subgoals, subgoal 1

H : negb false = negb true

============================

true = false

and we apply the tactic inversion H. What will happen?
H : negb false = negb true

============================

true = false

# Using Tactics on Hypotheses

Theorem S_inj : ∀(n m : nat) (b : bool),

beq_nat (S n) (S m) = b →

beq_nat n m = b.

Proof.

intros n m b H. simpl in H. apply H. Qed.

The tactic apply is a form of "backward reasoning": it
says "We're trying to prove X and we know Y→X, so if we can
prove Y we'll be done." By contrast, the variant
apply... in... is "forward reasoning": it says "We know Y and
we know Y→X, so we can deduce X."

Theorem silly3' : ∀(n : nat),

(beq_nat n 5 = true → beq_nat (S (S n)) 7 = true) →

true = beq_nat n 5 →

true = beq_nat (S (S n)) 7.

Proof.

intros n eq H.

symmetry in H. apply eq in H. symmetry in H.

apply H. Qed.

Theorem plus_n_n_injective : ∀n m,

n + n = m + m →

n = m.

Proof.

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

(* Hint: use the plus_n_Sm lemma *)

(* FILL IN HERE *) Admitted.

☐

# Varying the Induction Hypothesis

Fixpoint double (n:nat) :=

match n with

| O ⇒ O

| S n' ⇒ S (S (double n'))

end.

Suppose we want to show that double is injective — i.e.,
that it always maps different arguments to different results. The
way we

*start*this proof is a little bit delicate: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'". apply f_equal.

(* Here we are stuck. The induction hypothesis, IHn', does

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

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

Abort.

What went wrong?
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:

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

intros m eq.

destruct m as [| m'].

SCase "m = O".

inversion eq.

SCase "m = S m'".

apply f_equal.

apply IHn'. inversion eq. reflexivity. Qed.

What this teaches us 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.
The proof of this theorem has to be treated similarly:

Theorem beq_nat_true : ∀n m,

beq_nat n m = true → n = m.

Proof.

(* FILL IN HERE *) Admitted.

The strategy of doing fewer intros before an induction doesn't
always work directly; sometimes a little

*rearrangement*of quantified variables is needed. Suppose, for example, that 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'". apply f_equal.

(* Stuck again here, just like before. *)

Abort.

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

apply IHm'. inversion eq. reflexivity. Qed.

# Using destruct on Compound Expressions

Definition sillyfun (n : nat) : bool :=

if beq_nat n 3 then false

else if beq_nat n 5 then false

else false.

Theorem sillyfun_false : ∀(n : nat),

sillyfun n = false.

Proof.

intros n. unfold sillyfun.

destruct (beq_nat n 3).

Case "beq_nat n 3 = true". reflexivity.

Case "beq_nat n 3 = false". destruct (beq_nat n 5).

SCase "beq_nat n 5 = true". reflexivity.

SCase "beq_nat n 5 = false". reflexivity. Qed.

Sometimes, doing a destruct on a compound expression (a
non-variable) will erase information we need to complete a proof.

Definition sillyfun1 (n : nat) : bool :=

if beq_nat n 3 then true

else if beq_nat n 5 then true

else false.

Theorem sillyfun1_odd_FAILED : ∀(n : nat),

sillyfun1 n = true →

oddb n = true.

Proof.

intros n eq. unfold sillyfun1 in eq.

destruct (beq_nat n 3).

(* stuck... *)

Abort.

Theorem sillyfun1_odd : ∀(n : nat),

sillyfun1 n = true →

oddb n = true.

Proof.

intros n eq. unfold sillyfun1 in eq.

destruct (beq_nat n 3) eqn:Heqe3.

Case "e3 = true". apply beq_nat_true in Heqe3.

rewrite → Heqe3. reflexivity.

Case "e3 = false".

destruct (beq_nat n 5) eqn:Heqe5.

SCase "e5 = true".

apply beq_nat_true in Heqe5.

rewrite → Heqe5. reflexivity.

SCase "e5 = false". inversion eq. Qed.

# 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
- symmetry:
changes a goal of the form t=u into u=t
- symmetry in H:
changes a hypothesis of the form t=u into u=t
- 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
- destruct... eqn:...:
specify the name of an equation to be added to the context,
recording the result of the case analysis
- induction... as...:
induction on values of inductively defined types
- inversion:
reason by injectivity and distinctness of constructors
- assert (e) as H:
introduce a "local lemma" e and call it H
- generalize dependent x: move the variable x (and anything else that depends on it) from the context back to an explicit hypothesis in the goal formula