Two more goodies to go

This chapter introduces the eqn keyword to name new assumptions and the remember tactic to add new assumptions.

The eqn keyword

The eqn keyword lets us add named Leibniz equalities among the current assumptions.

For example, consider the following lemma:

Lemma O_or_S :
  forall n : nat,
    n = 0 \/ exists n' : nat, n = S n'.

Assume we start the proof with:

Proof.
  intro n.

The *goals* window then reads:

n : nat
============================
n = 0 \/ (exists n' : nat, n = S n')

Let us then use the case tactic to distinguish whether n is constructed with 0 or with S, and let us name the corresponding equality:

case n as [ | n'] eqn:H_n.
-

The *goals* window then reads:

n : nat
H_n : n = 0
============================
0 = 0 \/ (exists n' : nat, 0 = S n')

We are in the O case, and the corresponding Leibniz equality lies among the assumptions.

Let us complete the proof of this subgoal and focus on the other subgoal:

  left.
  reflexivity.
-

The *goals* window then reads:

n, n' : nat
H_n : n = S n'
============================
S n' = 0 \/ (exists n'0 : nat, S n' = S n'0)

We are in the S case, and the corresponding Leibniz equality lies among the assumptions.

The remember tactic

The remember tactic lets us add Leibniz equalities among our assumptions. The new assumption can be named using the eqn keyword.

For example, consider the following lemma and the beginning of its proof:

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

The *goals window reads:

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

Let us name the expression n + 1 with a Leibniz equality and let us name this Leibniz equality among the assumptions:

remember (n + 1) as n_plus_1 eqn:H_n_plus_1.

The *goals window now reads:

n, n_plus_1 : nat
H_n_plus_1 : n_plus_1 = n + 1
============================
n_plus_1 = S n

• The assumptions now include a new name, n_plus_1, and a new assumption, n_plus_1 = n + 1, which is named H_n_plus_1.
• The goal now contains n_plus_1 in lieu of n + 1.

Likewise, let us name the expression S n with a Leibniz equality and let us name this Leibniz equality among the assumptions:

remember (S n) as Sn eqn:H_Sn.

The *goals window now reads:

n, n_plus_1 : nat
H_n_plus_1 : n_plus_1 = n + 1
Sn : nat
H_Sn : Sn = S n
============================
n_plus_1 = Sn

• The assumptions now include a new name, Sn, and a new assumption, Sn = S n, which is named H_Sn.
• The goal now contains Sn in lieu of S n.

We can also name Leibniz equalities:

remember (n_plus_1 = Sn) as prove_me eqn:goal.

The *goals window now reads:

n, n_plus_1 : nat
H_n_plus_1 : n_plus_1 = n + 1
Sn : nat
H_Sn : Sn = S n
prove_me : Prop
goal : prove_me = (n_plus_1 = Sn)
============================
prove_me

• The assumptions now include two new names, prove_me and goal, and a new assumption, prove_me = (n_plus_1 = Sn), which is named goal.
• The goal now contains prove_me in lieu of n_plus_1 = Sn.

Resources

• The .v file for naming Leibniz equalities and creating new assumptions (latest version: 16 Feb 2024).

Version

Extracted this chapter from Chapter Structuring programs, structuring proofs [21 Mar 2024]