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 subgoals, subgoal 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 subgoals, subgoal 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 subgoals, subgoal 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 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.

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