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 do a simpl step first. *)
apply H. Qed.
Inversion
- 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.
Lemma eq_remove_S : ∀n m,
n = m → S n = S m.
Proof. intros n m 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. They may involve applying lemmas from earlier lectures or homeworks.Theorem beq_nat_0_l : ∀n,
true = beq_nat 0 n → 0 = n.
Proof.
(* FILL IN HERE *) Admitted.
Theorem beq_nat_0_r : ∀n,
true = beq_nat n 0 → 0 = n.
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'".
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. *)
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'".
assert (n' = m') as H.
SSCase "Proof of assertion". apply IHn'.
inversion eq. reflexivity.
rewrite → H. 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_eq : ∀n m,
true = beq_nat n m → n = m.
Proof.
(* FILL IN HERE *) Admitted.
true = beq_nat n m → 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'".
assert (n' = m') as H.
SSCase "Proof of assertion".
(* 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'".
assert (n' = m') as H.
SSCase "Proof of assertion".
apply IHm'. inversion eq. reflexivity.
rewrite → H. 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.
The remember Tactic
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.
remember (beq_nat n 3) as e3.
destruct e3.
Case "e3 = true". apply beq_nat_eq in Heqe3.
rewrite → Heqe3. reflexivity.
Case "e3 = false".
remember (beq_nat n 5) as e5. destruct e5.
SCase "e5 = true".
apply beq_nat_eq in Heqe5.
rewrite → Heqe5. reflexivity.
SCase "e5 = false". inversion eq. 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.
Review
- 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
- 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 x: move the variable x (and anything else that depends on it) from the context back to an explicit hypothesis in the goal formula