The intro tactic

The intro tactic formalizes the “let” / “assuming” idiom in an informal proof:

• For example, to prove that a statement “for all natural numbers x, P(x)” holds, an informal proof starts with “let x denote such a natural number; under this assumption, let us prove that P(x) holds”.
• For example, to prove that an implication “A -> B” holds, an informal proof starts with “assuming that A holds, let us prove that B holds.

Resources

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

A simple example

Concretely, consider the following simple lemma:

Lemma a_proposition_implies_itself :
  forall A : Prop,
    A -> A.

In words: any proposition implies itself.

Its proof illustrates both uses of the intro tactic, first to process the universally quantified statement forall A : Prop, A -> A, and second to process the implication A -> A:

1. Let us process the universally quantified statement:

   Proof.
     intro A.
   

   In words: let A denote such a proposition.

   The *goals* window then reads:

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

2. Let us process the implication:

   intro H_A.
   

   In words: let us assume that A holds, under the name H_A (aloud: “the hypothesis about A”).

   The *goals* window then reads:

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

What’s in a name?

The intro tactic is provided with a name, and we have entire latitude to choose this name, as long as it does not exist already among the current assumptions. For example, we could pick rose instead of A in the proof of a_proposition_implies_itself:

Restart.

intro rose.

The *goals* window then reads:

rose : Prop
============================
rose -> rose

Note how tCPA has automatically renamed A into rose.

Anton: Shake! Spear!

Alfrothul: Star! Dust!

Neil Gaiman: Hi. It kind of looks like you guys need a chairperson?

Mimer: Mr. Gaiman, thanks for stopping by!

In practice, names matter because of readability, and so we rarely pick another name than the one that is supplied in the forall-statement. If we do, then the more intuitive this name, the better.

Common naming conventions

• The name of propositions tend to be capitalized.
• The name of assumptions (well, hypotheses) are typically H_ followed by a meaningful name.
• The plural naming convention of Haskell (v is a value, vs is a list of values, vss is a list of list of values, etc.) is also very convenient here.

The intros tactic

For notational convenience, consecutive occurrences of the intro tactic can be compressed into one occurrence of the intros tactic.

So for example:

intro A.
intro H_A.

can be compressed into:

intros A H_A.

For extra clarity, one sometimes separates usages of the intros tactic to handle a forall-statement and to handle an implication, as illustrated in the following example:

Lemma the_following_example :
  forall A B C : Prop,
    A ->
    B ->
    C ->
    forall i j : nat,
      A /\ B /\ C /\ i = i /\ j = j.
Proof.
  intros A B C.
  intros H_A H_B H_C.
  intros i j.

Naming, e.g., conjunctions vs. naming components of conjunctions

Say that we want to prove an implication where the left-hand side is the conjunction of two propositions. For example:

Lemma a_pair_of_propositions_implies_the_left_one :
  forall A B : Prop,
    A /\ B -> A.

The standard way to go is to let A and B denote the two propositions, and then to assume that their conjunction holds, under some intuitive name:

Proof.
  intros A B.
  intro H_A_and_B.

But we do not need to name the pair: we need to name its components. That is a job for the destruct tactic, which destructures the denotation of H_A_and_B into two named assumptions:

destruct H_A_and_B.

The *goals* window then reads:

A, B : Prop
H : A
H0 : B
============================
A

Among the assumptions, we can see that tCPA has picked two identifiers for us to name A and B. Therein lies confusion of course because the rest of our proof needs to use these two identifiers, and readability will suffer. (Not just that: our proof now depends on the name-generating algorithm used in the current version of tCPA.)

The CPA designers therefore offer the same naming facility as in OCaml, using the as keyword, followed by a naming pattern:

Restart.

intros A B.
intro H_A_and_B.
destruct H_A_and_B as [H_A H_B].

The *goals* window then reads:

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

Its content is relatable because it only contains names of our own choosing.

The naming pattern is specified as follows:

<naming-pattern> ::= identifier
                   | [<naming-pattern> <naming-pattern>]
                   | [<naming-pattern> | <naming-pattern>]

The pattern [... ...] stands for conjunctions, and the pattern [... | ...] stands for disjunctions.

Furthermore the two lines:

intro H_A_and_B.
destruct H_A_and_B as [H_A H_B].

can be compressed into one:

intros [H_A H_B].

We will have much of use of this style of destructuring intro tactic.

Naming the components of nested conjunctions

The destructuring intro tactic scales to nested conjunctions. For example:

Lemma about_nested_conjunctions :
  forall A B C D : Prop,
    (A /\ B) /\ (C /\ D) -> (D /\ A) /\ (B /\ C).
Proof.
  intros A B C D.
  intros [[H_A H_B] [H_C H_D]].

The *goals* window then reads:

A, B, C, D : Prop
H_A : A
H_B : B
H_C : C
H_D : D
============================
(D /\ A) /\ B /\ C

Alfrothul: Only one pair of parentheses in the goal?

Anton (with dignity): Well, conjunctions associate to the right in tCPA.

Naming, e.g., disjunctions vs. naming components of disjunctions

Say that we want to prove an implication where the left-hand side is the disjunction of two propositions. For example:

Lemma disjunction_is_commutative :
  forall A B : Prop,
    A \/ B -> B \/ A.

Since there is no need to name the disjunction, let us use a destructuring intro tactic:

Proof.
  intros A B.
  intros [H_A | H_B].

We will revisit disjunctions soon.

Naming the components of nested conjunctions and disjunctions

The destructuring intro tactic scales to nested disjunctions as well as to nested conjunctions and disjunctions. For (a silly) example:

Lemma about_nested_conjunctions_and_disjunctions :
  forall A B C D E F : Prop,
    (A \/ B) /\ (C \/ (D /\ E)) -> F.
Proof.
  intros A B C D E F.
  intros [[H_A | H_B] [H_C | [H_D H_E]]].

Resources

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

Version

Created [25 Jan 2024]