Tutorial: Intro Patterns

Main contributors

• Thomas Lamiaux, Pierre Rousselin

Summary

In this tutorial, we discuss intro patterns that enable us to introduce hypotheses and transform them at the same time, e.g. by pattern-matching or rewriting them. This enables us to factorize and to write more direct code.

Table of content

• 1. Introducing Variables
• 2. Destructing Variables
• 3. Rewriting and Injection
• 4. Simplifying Equalities
• 5. Applying Lemmas
• 6. Intro patterns everywhere

Prerequisites

Needed:

• No Prerequisites

Not Needed:

• No Prerequisites

Installation:

• Available by default with Coq/Rocq

1. Introducing Variables

The basic tactic to introduce variables is intros. Its most basic form intros x y ... z will introduce as many variables and hypotheses as mentioned with the names specified x, y, ..., z, and fails if one of the names is already used, or if there are no more variables or hypotheses to introduce.

It can happen that we have a hypothesis to introduce that is not useful to our proof. In this case, rather than introducing it we would rather like to directly forget it. This is possible using the wildcard pattern _, that will introduce and forget a variable that does not appear in the conclusion.

In some cases, we do not wish to choose a name and would rather have Coq choose a name for us. This is possible with the ? pattern.

However, be careful that referring explicitly to auto-generated names in a proof is bad practice as subsequent modifications of the file could change the generated names, and hence break the proof. This can happen very fast. Auto-generated names should hence only be used in combination with tactics like assumption that do not rely on names. Similarly to ?, it happens that we want to introduce all the variables automatically and without naming them. This is possible by simply writing intros or as an alias intros **.

As a variant of intros, intros × will introduce all the hypothesis from the goal until it reaches one depending on the ones that it is has introduced, or that there is no more hypotheses to introduce. In this example, intros × will introduce n and m, then stops at n < m as it depends on n and m that it has just introduced.

This is particularly convenient to introduce type variables that other variables depend upon, but that we do not want to perform any specific action on but introduction.

An important difference between intros and intros x is that intros introduce as much variables as possible without simplifying the goal, whereas intros x will first compute the head normal form before trying to introduce a variable. This difference can be intuitively understood by considering that intros x means there is a variable to introduce, and requires to find it. For instance, consider the definition that a relation is reflexive.

If we try to prove that logical equivalence is reflexive by using intros then nothing will happen as Reflexive is a constant, and it needs to be unfolded for a variable to introduce to appear. However, as intros x simplifies the goal first, it will succeed and progress:

2. Destructing Variables

When proving properties, it is very common to introduce variables only to pattern-match on them just after, e.g. to prove properties about an inductive type or simplify an inductively defined function:

To shorten the code, it is possible to do both at the same time using the intro pattern [ x ... y | ... | z ... w ]. It enables to give a name to each argument of each constructor, separating them by |. If neither branches nor names are specified, Coq will just use auto-generated names.

As a side remark, the fact that intro patterns have the same syntax that what is after as in destruct ... as is no accident, since the as keyword in a tactic is followed by ... an intro pattern.

Note that destructing over False expects neither branches nor names as False has no constructors, and that it solves the goal automatically:

Using intro patterns is not at all restricted to logical formulas. Consider Peano's natural numbers (the type nat here).

It has two constructors, one called O : nat without argument for the number zero, and the successor function S : nat → nat, basically 1 + _. This says that any number of type nat is either 0 or the successor of another number of type nat. This can be used to reason by case analysis on (the nullity of) a natural number.

Again, we can intros and destruct our n variable in one step.

It is further possible to nest the intro-patterns when inductive types are nested into each other:

Actually, the latter pattern is common enough that there is a specific intro-pattern for it. When the goal is of the form X Op1 (Y ... Opk W) where all the binary operations have one constructor with two arguments like ∧, then it is possible to introduce the variables with intros (p & q & r & h) rather than by having to destruct recursively with intros [p [q [r h]]] .

A particularly useful case is to introduce existentially quantified hypotheses.

3. Rewriting Lemmas

It is also very common to introduce an equality that we only wish to use once as a rewrite rule on the goal:

It is possible to do both at the time using the intro patterns → and <- that will introduce H, rewrite it in the goal and context and then clear it. It has the advantage to be much more concise, and save us from introducing a name for n = 0 that we fundamentally do not really care about:

For a more concrete example, consider proving that if a list has one element and another one is empty, then the concatenation of the two lists has one element. The usual proof would require us to introduce the hypothesis and decompose it into pieces before being able to rewrite and simplify the goal:

Using intro patterns to do the pattern-matching and the rewriting, we can get a very intuitive and compact proof without having to introduce any fresh names:

4. Simplifying Equalities

Rewriting automatically equalities is practical but sometimes we first need to simplify them with injection before being able to rewrite with them. For instance in the example below, we have an equality S n = 1 but as it is n that appears in the conclusion, we first need to simplify the equation with injection to n = 0 before being able to rewrite it.

To do this automatically, there is a dedicated intro pattern [=] that will introduce the equalities obtained after simplification by injection.

It is then possible to combine this with the intro pattern for rewriting to directly simplify the goal, giving us a particularly simple proof.

Another particularly useful way of simplifying an equality is to deduce that the goal is true from an absurd equation like S n = 0. This is usually done by introducing variables then using discriminate, but can also be automatically done thanks to the intro pattern =:

5. Applying Lemmas

A situation that often arises when proving properties is having a hypothesis that we first need to transform before being able to use it. For instance, consider the following example where we know that length l1 = 0. To conclude that l1 ++ l2 = l2, we must first prove that l1 = [] by applying length_zero_iff_nil to length l1 = 0, and then rewrite it:

To help us do this, the % intro pattern H%impl introduces the hypothesis H and applies the implication impl in it. We can hence write intros H%length_zero_iff_nil rather than intros H. apply length_zero_iff_nil in H.

We can then further combine this with rewrite patterns to simplify the proof:

For a more involved example, consider the converse of the last example of section 3: if the concatenation of two lists has one element, then one list has one element and the other one is empty. After pattern matching on l1, we have an equality a1::l1++l2 = [a]. We must simplify it to a1 = a and l1 ++ l2 = [] with injection, then to l1 = [] and l2 = [] with app_eq_nil, before being able to rewrite. This creates a lot of overhead as introduction and operations like destruction, simplification and rewriting have to be done separately. Furthermore, at every step we have to introduce fresh names that do not really matter in the end.

Using intro patterns we can significantly shorten this proof and make it more intuitive, getting rid of tedious manipulations of hypotheses. We can use the intro pattern [=] to simplify the equality a1::l1++l2 = [a] to a1 = a and l1 ++ l2 = []. We can then rewrite the first equality with →, and simplify the second equality to l1 = [] ∧ l2 = [] thanks to %app_eq_nil. Finally, we can rewrite both equalities using →, giving us the intro pattern intros [= → [-> ->]%app_eq_nil]. This yields a much shorter proof without a bunch of fresh names.

6. Intro patterns everywhere

We mentioned before the fact that the tactic destruct ... as ... expects an intro pattern after as. In fact, many tactics can have an as ... part, with an intro pattern. Let's give examples. We concentrate on apply ... in .... In general, using this tactic can result in a weaker proof state, which may or may not be an issue.

In many cases, applying an implication in an hypothesis will give something which:

• can (and should) be destructed with [...] or
• is an equality to use with rewrite with → or <- or
• can be simplified (injection), or is directly contradictory discriminate (with [= ...]) or
• can be served as a condition to another implication with %

In that case, we're free to use everything we already learned after as.

We can go crazier:

Who needs apply?

Other useful and frequently used tactics which can be used with as intro_pattern include:

• destruct
• pose proof
• specialize
• assert and enough
• inversion (restricted to "and" and "or" intro patterns)
• injection