# MoreCoqMore About Coq

Require Export Poly.

# The apply Tactic

We can use apply when some hypothesis or an earlier lemma matches the goal:

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

Examples like this one use two rewrites to exploit the transitivity of equality. We can abstract this into its own lemma.

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

In Coq, the constructors of inductive types are injective and disjoint.
E.g., for nat...
• 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)
Coq provides a tactic called inversion that allows us to exploit these principles in proofs.
The inversion tactic is used like this. Suppose H is a hypothesis in the context (or a previously proven lemma) of the form
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 subgoalssubgoal 1

H : false = true
============================
negb true = negb false
and we apply the tactic inversion H. What will happen?
(1) No change
(2) Substitute true with false in the conclusion, leaving negb false = negb false
(3) "No more subgoals"
Suppose Coq's proof state looks like
1 subgoalssubgoal 1

x : bool
y : bool
H : x = y
============================
y = x
and we apply the tactic inversion H. What will happen?
(1) No change
(2) "No more subgoals"
Suppose Coq's proof state looks like
1 subgoalssubgoal 1

H : negb false = negb true
============================
true = false
and we apply the tactic inversion H. What will happen?
(1) No change
(2) "No more subgoals"

# Using Tactics on Hypotheses

Tactics often come with "...in..." variants that can be used on hypotheses instead of goals.

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

#### Exercise: 3 stars (plus_n_n_injective)

Practice using "in" variants in this exercise.

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

Here's a function for doubling a natural number (from the Induction chapter):

Fixpoint double (n:nat) :=
match n with
| OO
| 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 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 : 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

The destruct tactic can be used on expressions as well as variables:

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.

We can use the eqn: qualifier to save that information.

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

We've now seen a bunch of Coq's fundamental tactics. We'll introduce a few more as we go along through the coming lectures, and later in the course we'll introduce some more powerful automation tactics that make Coq do more of the low-level work in many cases. But basically we've got what we need to get work done.
Here are the ones we've seen:
• 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

# Micro Sermon

Mindless proof-hacking is a terrible temptation...
Try to resist!