The revert tactic

The revert tactic is a left inverse of the intro tactic. It is given the name of one of the current assumptions, and restores it in the goal, provided no other assumptions depend on the one we want to revert.

Resources

• The .v file for the present lecture note (latest version: 28 Jan 2024).

The simple example, revisited

Let us revisit the simple lemma and its proof:

Lemma a_proposition_implies_itself :
  forall A : Prop,
    A -> A.
Proof.
  intro A.
  intro H_A.
  exact H_A.
Qed.

In words:

1. let A be a proposition;
2. let us assume that such a proposition hold (H_A denotes this hypothesis); and
3. what we need to prove lies among the hypotheses.

After the second proof step, the *goals* window reads as follows:

A : Prop
H_A : A
============================
A

As a third proof step, we could restore the implication with the revert tactic:

revert H_A.

The *goals* window then reads:

A : Prop
============================
A -> A

As the next proof step, we could restore the quantifier, again with the revert tactic:

revert A.

The *goals* window then reads:

============================
forall A : Prop, A -> A

Practical use of the revert tactic

Say that we want to prove the following lemma:

Lemma swapping_the_order_of_quantifiers :
  forall A B : Prop,
    (A -> B -> A /\ B) -> B -> A -> A /\ B.
Proof.
  intros A B H_implication H_B H_A.

The *goals* window reads:

A, B : Prop
H_implication : A -> B -> A /\ B
H_B : B
H_A : A
============================
A /\ B

Rather than directly proving the goal by applying H_implication to H_A and H_B, which does the job, we can first use the revert tactic on H_B:

revert H_B.

The *goals* window then reads:

A, B : Prop
H_implication : A -> B -> A /\ B
H_A : A
============================
B -> A /\ B

We can then use the revert tactic on H_A:

revert H_A.

The *goals* window then reads:

A, B : Prop
H_implication : A -> B -> A /\ B
============================
A -> B -> A /\ B

And now the goal lies among the assumptions.

Interlude

Anton: I think the proof could be more elegant.

Mimer (keeping a straight face): How so?

Anton: Well, we could use the revert tactic once more:

revert H_implication.

Pablito: OK?

Anton: Well, yes. Look at the *goals* windows:

A, B : Prop
============================
(A -> B -> A /\ B) -> A -> B -> A /\ B

Pablito: OK?

Anton: Well, the goal is an instance of a_proposition_implies_itself:

exact (a_proposition_implies_itself (A -> B -> A /\ B)).

Mimer: Well spotted, Anton.

Using the revert tactic with several arguments

Incidentally, rather than using the revert tactic two times in a row:

revert H_B.
revert H_A.

one can use it once with two arguments:

revert H_A H_B.

And likewise, rather than using the revert tactic three times in a row:

revert H_B.
revert H_A.
revert H_implication.

one can use it once with three arguments:

revert H_implication H_A H_B.

(N.B.: Compared with using the intros tactic once instead using the intro tactic several times in a row, the order of arguments is reversed here.)

Resources

• The .v file for the present lecture note (latest version: 28 Jan 2024).

Version

Added Section Using the revert tactic with several arguments [28 Jan 2024]

Created [25 Jan 2024]