The clear tactic

Occasionally, in the *goals* window, there is a large number of assumptions over the horizontal bar. Some of them are unnecessary to prove the current goal, and we can use the clear tactic to remove them.

For example, consider the following lemma:

Lemma for_example :
  forall A B : Prop,
    A -> B -> A.
Proof.
  intros A B H_A H_B.

At that point, the *goals* window reads:

A, B : Prop
H_A : A
H_B : B
============================
A

Among these assumptions, H_B is unnecessary to prove A. We can clear it away from the assumptions using the clear tactic:

clear H_B.

The *goals* window then reads:

A, B : Prop
H_A : A
============================
A

(As can be observed, H_B no longer occurs among the assumptions.)

We can then conclude the proof:

  exact H_A.
Qed.

A worked-out example

Let us revisit the food for thought from Week 01:

Definition specification_of_foo_in_Week_01 (foo : nat -> nat) :=
  (foo O = 0)
  /\
  (forall n' : nat,
    foo (S n') = S (S (foo n'))).

Lemma twice_S :
  forall n : nat,
    2 * S n = S (S (2 * n)).
Proof.
Admitted.

Theorem about_foo :
  forall foo : nat -> nat,
    specification_of_foo_in_Week_01 foo ->
    forall a b : nat,
      foo a = b ->
      b = 2 * a.

The .v file for the present lecture note contain six attempts at proving Theorem about_foo, one of which is unsuccessful:

1. The first proof uses the Light of Inductil and then eq_S to simplify S (S (foo a')) = S (S (2 * a')) in the goal.

2. The second proof uses the Light of Inductil and eq_refl.

3. The third proof uses the Light of Inductil and eq_refl, and it uses the premiss foo a = b before starting the induction proof instead of both in the base case and in the induction step.

4. The fourth proof simplifies before starting the induction proof, and does not use the Light of Inductil. However, on the ground that the assumption H_b : foo a = b uses a over which we want do induct, the induction tactic silently inserts revert H_b for us and we get stuck.

5. On the ground that we don’t want the induction tactic to silently do anything for us, the fifth proof uses nat_ind and goes through, thank you very much.

6. The sixth proof uses the assumption H_b : foo a = b upfront and then, on the ground that H_b is no longer necessary, it clears it away from the assumptions. This clearing away makes b become unnecessary too, so the proof clears it away too. And then the proof goes through. Ha.

Halcyon (thoughtfully): To light is to delight.

Pablito (wondering): The Delight of Inductil?

Bong-sun (facepalming): ...

Resources

• The .v file for the present lecture note (latest version: 16 Feb 2025).

Version

Completed [16 Feb 2025]

Created [14 Feb 2025]