More tactics

The goal of this chapter is to introduce the simpl tactic and the do tactic.

Resources

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

The simpl tactic

The simpl tactic allegedly simplifies the current goal – and it does, after a fashion, though in an unpredictable way. Example:

Lemma foo :
  forall n : nat,
    1 + n = n + 1.
Proof.
  intro n.

The *goals* window reads:

n : nat
============================
1 + n = n + 1

Let us use the simpl tactic:

simpl.

The *goals* window reads:

n : nat
============================
S n = n + 1

Somehow, it has simplified the left-hand side, but not the right-hand side, which is unintuitive... unless we realize that part of what simpl does is to unfold the calls to recursive functions whose inductive variable is known. With that in mind, it is simple (so to speak) to reproduce – and therefore understand – what simpl does. Here, it exploits the fact that Nat.add is defined recursively on its first argument:

Print Nat.add.

The *response* window then reads ({struct n} is an internal annotation to convey that add is defined recursively over n):

Nat.add = fix add (n m : nat) {struct n} : nat := match n with
                                                  | 0 => m
                                                  | S p => S (add p m)
                                                  end
     : nat -> nat -> nat

With that, let us reproduce what simpl just did:

Abort.

Definition fold_unfold_add_O := Nat.add_0_l.
Definition fold_unfold_add_S := plus_Sn_m.

Lemma foo :
  forall n : nat,
    1 + n = n + 1.
Proof.
  intro n.
  rewrite -> (fold_unfold_add_S 0 n).
  rewrite -> (fold_unfold_add_O n).

The *goals* window reads:

n : nat
============================
S n = n + 1

We can then complete the proof:

rewrite <- (plus_n_Sm n 0).
rewrite -> (Nat.add_0_r n).
reflexivity.

Also, most of the time, the simpl tactic is overzealous: if it finds something to simplify, it will simplify it, making the user sink in a sea of irrelevant details more often than not.

The sane way to use the simpl tactic is to give it an argument: the expression in the goal that we want to simplify. This way, we stay in control.

The do tactic

Given a natural number n and a tactic t, the do tactic repeats t n times.

Exercise 01

Prove that for any natural number n strictly greater than 3, 2^n < n!.

Solution for Exercise 01

See the accompanying resource file after the live-proving session. The solution uses both simpl and do. It also selectively uses lemmas without applying them to all their arguments, when there is no ambiguity.

Exercise 02

The Solution for Exercise 01 uses do, but in practice one would use le_plus_l : forall n m : nat, n <= n + m.

1. State and prove a lemma lt_plus_l that is to < what le_plus_l is to <=.
2. Revisit the Solution for Exercise 01 and use either le_plus_l or lt_plus_l in its base case and in its induction step.

Resources

• The .v file for the present lecture note (latest version: 15 Mar 2024).
• The .v file for the present lecture note after the live-proving session (latest version: 15 Mar 2024).

Version

Added Exercise 02 [21 Mar 2024]

Added the resource file after today’s live-proving session [15 Mar 2024]

Created [15 Mar 2024]