Lecture 4: Tactics in UniMath

by Ralph Matthes, IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, France My employer is the CNRS, my lab is the IRIT, but the above affiliation is obligatory for any scientific production I release. This is the extended version of a presentation at the UniMath school 2022 in Cortona, meant for self-study and for exploring the UniMath library. The material is based on the extended version of the presentation at the UniMath schools 2017 and 2019 in Birmingham, but updated to fit with the changes in (the practice of) UniMath. Works with current UniMath (as of July 15, 2022, but also the Coq platform of April '22). Compiles with the command
coqc -type-in-type lecture_tactics_long_version.v

when Coq is set up according to the instructions for this school and the associated coqc executable has priority in the path. However, you do not need to compile this file. The option is crucial, and also your own developments will need the Coq options configured through the installation instructions, most notably the present one. Can be transformed into HTML documentation with the command
coqdoc -utf8 lecture_tactics_long_version.v

(If internal links in the generated lecture_tactics_long_version.html are desired, compilation with coqc is needed.) In Coq, one can define concepts by directly giving well-typed terms (see Part 2), but one can also be helped in the construction by the interactive mode.

define a concept interactively:

a separate definition - Init.Datatypes.bool is in the Coq library, not available for UniMath

only the identifier and its type given, not the definiens This opens the interactive mode. The UniMath style guide asks us to start what follows with Proof. in a separate line. In vanilla Coq, this would be optional (it is anyway a "nop").

Now we still have to give the term, but we are in interactive mode. If you want to see everything in the currently loaded part of the UniMath library that *involves* booleans, then do

If you only want to find library elements that *yield* booleans, then try

true does not take an argument, and it is already a term we can take as definiens.

exact is a tactic which takes the term as argument and informs Coq in the proof mode to finish the current goal with that term. We see in the response buffer: "No more subgoals." Hence, there is nothing more to do, except for leaving the proof mode properly.

Defined. instructs Coq to complete the whole interactive construction of a term, verify it and to associate it with the given identifer, here myfirsttruthvalue. This may go wrong for different reasons, including implementation errors of the Coq system - that will not affect trustworthiness of the library.

The new definition appears at the beginning of the list.

or just point to the identifier and hit the key combination mentioned in Part 2 myfirsttruthvalue relies on an unsafe universe hierarchy is output to indicate that we are using Coq with option -type-in-type.

a more compelling example

applies the function negb to obtain the required boolean, thus the system has to ask for its argument

mysecondtruthvalue = negb myfirsttruthvalue
     : bool

the definition is "as is", evaluation can be done subsequently:

     = false
     : bool

Again, not much has been gained by the interactive mode. Here, we see a copy of the definition from the Coq library:

only for illustration purposes - it would be better to define it according to UniMath style

apply andb. applies the function andb to obtain the required boolean, thus the system has to ask for its TWO arguments, one by one. This follows the proof pattern of "backward chaining" that tries to attack goals instead of building up evidence. In the course of action, more goals can be generated. The proof effort is over when no more goal remains. UniMath coding style asks you to use proof structuring syntax, while vanilla Coq would allow you to write formally verified "spaghetti code". We tell Coq that we start working on the first subgoal.

only the "focused" subgoal is now on display

this again spawns two subgoals we tell Coq that we start working on the first subgoal

normally, one would not leave the "bullet symbol" isolated in a line

The response buffer signals:
There are unfocused goals.

ProofGeneral would give more precise instructions as how to proceed. But we know what we are doing...

The usual "UniMath bullet order" is -, +, *, --, ++, **, ---, +++, ***, and so on (all the ones shown are being used). Coq does not impose any order, so one can start with, e.g., *****, if need be for the sake of experimenting with a proof. Reuse of bullets even on one branch is possible by enclosing subproofs in curly braces {}.

You only saw the tactics exact and apply at work, and there was no context.

doing Curry-Howard logic

Interactive mode is more wide-spread when it comes to carrying out proofs (the command Proof. is reminiscent of that). Disclaimer: this section has a logical flavour, but the "connectives" are not confined to the world of propositional or predicate logic. In particular, there is no reference to the sort Prop of Coq. Prop is not used at all in UniMath! On first reading, it is useful to focus on the logical meaning.

non-dependent product, can be seen as implication

an inductive type that has no constructor

we need to refer to the UniMath library more explicitly

Do not write the import statements in the middle of a vernacular file. Here, it is done to show the order of appearance, but this is only for reasons of pedagogy.

Negation is not a native concept; it is reduced to implication, as is usual in constructive logic.

non-dependent sum, can be seen as conjunction

how to infer an implication?

This is already a bit of "forward chaining" which is a fact-building process.

cbn simplifies a goal, and cbn in H does this for hypothesis H; note that simpl has the same high-level description but should better be avoided in new developments.

could be done with split. as well

instruct Coq to look into the current context this could be done with exact Hyp3. as well

deconstruct the hypothesis at the time of introduction; notice that × associates to the right; intros can also introduce multiple hypotheses, see below

the two definitions are even convertible:

In late 2017, combinatorS_intro_pattern would have contained match constructs, but now, the introduction patterns use less overhead when possible. The UniMath style guide still does not want them to be used with square brackets. another style to make life easier:

deconstruct the hypothesis when needed

deconstruct the hypothesis when needed

Again, the definition is definitionally equal to the first one:

In late 2017, combinatorS_destruct would also have contained match constructs, which is why destruct is forbidden in the UniMath style guide. Now, this is fine in our example. The (hitherto) preferred idiom:

the comfort for the user does not change the normal form of the constructed proof

use intro three times or rather intros once; reasonable coding style gives names to all hypotheses that are not already present in the goal formula, see also the next definition

set up abbreviations that can make use of the current context; will be considered as an extra element of the context:

We see that set gives rise to let-expressions that are known from functional programming languages, in other words: the use of set is not a "macro" facility to ease typing. let-bindings disappear when computing the normal form of a term:

set can only be used if the term of the desired type is provided, but we can also work interactively as follows:

we can momentarily forget about our goal and build up knowledge:

the current goal C becomes the second sub-goal, and the new current goal is B It is not wise to handle this situation by "bullets" since many assertions can appear in a linearly thought argument. It would pretend a tree structure although it would rather be a comb. The proof of the assertion should be packaged by enclosing it in curly braces like so:

Now, proofofB is in the context with type B.

the wildcard ? for intros

a question mark instructs Coq to use the corresponding identifier from the goal formula

the wildcard _ for intros forgets the respective hypothesis

this symbol is typed as \amalg when the recommended extension packages for VSCode are loaded

defined in UniMath preamble as inductive type, can be seen as disjunction

the identity type of UniMath

A word of warning for those who read "Coq in a Hurry": SearchRewrite does not find equations w.r.t. this notion, only w.r.t. Coq's built-in propositional equality.

Among the search results is pathsinv0r that has idpath in its conclusion.

No result!

How to decompose formulas

In "Coq in a Hurry", Yves Bertot gives recipes for decomposing the usual logical connectives. Crucially, one has to distinguish between decomposition of the goal or decomposition of a hypothesis in the context. Here, we do it alike.

Decomposition of goal formulas:

A1,...,An -> B: tactic intro or intros ¬ A: idem (negation is defined through implication) Π-type: idem (implication is a special case of product) ×: apply dirprodpair, less specifically apply tpair or split Σ-type: use tpair or ∃ or split with, see explanations below A ⨿ B: apply ii1 or apply ii2, but this constitutes a choice of which way to go A = B: apply idpath, however this only works when the expressions are convertible nat: exact 1000, for example (a logical reading is not useful for this type); beware that UniMath knows only 27 numerals, Goal nat. Fail exact 2022. leads to
The command has indeed failed with message: No interpretation for number "2022".

Decomposition of formula of hypothesis H:

∅: induction H This terminates a goal. (It corresponds to ex falso quodlibet.) There is naturally no recipe for getting rid of ∅ in the conclusion. But apply fromempty allows to replace any goal by ∅. A1,...,An -> B: apply H, but the formula has to fit with the goal ×: induction H as [H1 H2] As seen above, this introduces names of hypotheses for the two components. Σ-type: idem, but rather more asymmetric as induction H as [x H'] A ⨿ B: induction H as [H1 | H2] This introduces names for the hypotheses in the two branches. A = B: induction H The supposedly equal A and B become the same A in the goal. This is the least intuitive rule for the non-expert in type theory. nat: induction n as [ | n IH] Here, we assume that the hypothesis has the name n which is more idiomatic than H, and there is no extra name in the base case, while in the step case, the preceding number is now given the name n and the induction hypothesis is named IH.

Handling unfinished proofs

In the middle of a proof effort - not in the UniMath library - you can use admit to abandon the current goal.

seems difficult in the current context

we continue with decent proof work:

This is strictly forbidden to commit to UniMath! admit allows to pursue the other goals, while Admitted. makes the lemma available for further proofs. A warning is shown that badex1 has been assumed as axiom. An alternative to interrupt work on a proof:

badex2 is not in the symbol table. Abort. is a way of documenting a problem with proving a result. At least, Coq can check the partial proof up to the Abort. command.

Working with holes in proofs

Our previous proofs were particularly clear because the goal formulas and all hypotheses were fully given by the system.

This is the UniMath proof of transitivity of equality. The salient feature of transitivity is that the intermediate expression cannot be deduced from the equation to be proven.

Notice that the outermost parentheses are needed here.

The command has indeed failed with message:
Cannot infer the implicit parameter b of pathscomp0 whose type is
"Type" in environment:
A, B, C, D : UU

Fail announces failure and therefore allows to continue with the interpretation of the vernacular file. We need to help Coq with the argument b to pathscomp0.

is this not just associativity with third argument C × D?

Nothing for our equation - we can only hope for weak equivalence ≃.

eapply generates "existential variables" for the expressions it cannot infer from applying a lemma. The further proof will narrow on those variables and finally make them disappear - otherwise, the proof is not considered completed.

We recall that on this side, only associativity was missing.

The subgoal is now fully given. The missing link is associativity, but only on the right-hand side of the top × symbol.

Warning: tactic exact does not work if there are existential variables in the goal, but eexact can then be tried.

decompose the implication:

decompose the Σ-type:

decompose the pair:

decompose the pair in the goal

The command has indeed failed with message:
         Unable to find an instance for the variable pr1.

A simple way out, by providing the first component:

∃ x does the same

or use eapply and create an existential variable:

the assumption H2 does not agree with the goal

Notice that eapply tpair is not used in the UniMath library, since use tpair normally comes in handier, see below.

Warning on existential variables

It may happen that the process of instantiating existential variables is not completed when all goals have been treated. an example adapted from one by Arnaud Spiwack, ~2007

from the UniMath preamble

refine is like exact, but one can leave holes with the wildcard "_". This tactic should hardly be needed since most uses in UniMath can be replaced by a use of the "tactic" use, see further down on this tactic notation for an Ltac definition. Still, refine can come to rescue in difficult situations, in particular during proof development. Its simpler variant simple refine is captured by the use "tactic".

Now, Coq presents a subgoal that pops up from the "shelved goals". Still, no more "-" bullets can be used. [ - Error: Wrong bullet - : No more subgoals. ]

a natural number is still being asked for

Like this, we can focus on the remaining goal.

one can also name the existential variables in refine:

give a name to the existential variable

more symbols to type but better to grasp

a bit more on equational reasoning

A section allows to introduce local variables/parameters that will be bound outside of the section.

this is just pointwise equality

the identity function

exchanges the arguments of funcomp

plain function composition in diagrammatic order, i.e., first the first argument, then the second argument; the second argument may even have a dependent type

makes good sense in a section, can be put in curly braces to indicate they will be implicit arguments for every construction in the section

is a nop since the formula structure is not analyzed

unfold unfolds a definition

the extra element a triggers Coq to unfold the formula further; unfold interestingstatement was there only for illustration! we want to use transitivity that is expressed by pathscomp0 and instruct Coq to take a specific intermediate term

not telling because implicit arg. is not shown

apply symmetry of equality

all the unfold were only for illustration!

we use the equation in hyp from right to left, i.e., backwards:

remark: for a forward rewrite, use rewrite without directional argument beautify the current goal:

just for illustration of change that allows to replace the goal by a convertible expression; also works for hypotheses, e.g.:

since hyp was no longer necessary, we should rather have deleted it:

Opaque made the definition opaque in the sense that the identifier is still in the symbol table, together with its type, but that it does not evaluate to anything but itself. If inhabitants of a type are irrelevant (for example if it is known that there is at most one inhabitant, and if one therefore is not interested in computing with that inhabitant), then opaqueness is an asset to make the subsequent proof process lighter. Opaque can be undone with Transparent:

If one uses Compute in place of Eval compute in, then Opaque has no effect. Full and irreversible opaqueness is obtained for a construction in interactive mode by completing it with Qed. in place of Defined. Using Qed. is discouraged by the UniMath style guide. In Coq, most lemmas, theorems, etc. (nearly every assertion in Prop) are made opaque in this way. In UniMath, many lemmas enter subsequent computation, and one should have good reasons for not closing an interactive construction with Defined.. More than 5kloc of the UniMath library have Qed., so these good reasons do exist and are not rare.

The section parameters A and B are abstracted away after the end of the section - only the relevant ones. assert is a "chameleon" w.r.t. to opaqueness:

proofofB is just an identifier and not associated to the construction we gave. Hence, the proof is opaque for us.

We see that proofofB is there with its definition, so it is transparent. See much further below for transparent assert that is like assert, but consistently transparent.

composing tactics

Up to now, we "composed" tactics in two ways: we gave them sequentially, separated by periods, or we introduced a tree structure through the "bullet" notation. We did not think of these operations as composition of tactics, in particular since we had to trigger each of them separately in interactive mode. However, we can also explicitly compose them, like so:

The sequential composition is written by (infix) semicolon, and the two branches reated by split are treated in the |-separated list of arguments to the brackets. Why would we want to do such compositions? There are at least four good reasons: (1) We indicate that the intermediate results are irrelevant for someone who executes the script so as to understand how and why the construction / the proof works. (2) The same tactic (expression) can uniformly treat all sub-goals stemming from the preceding tactic application, as will be shown next.

This illustrates the grouping of tactic expressions by parentheses, the variant assert by of assert used when only one tactic expression forms the proof of the assertion, and also point (2): the last line is simpler than the expected line
[assumption | assumption].

Why would we want to do such compositions (cont'd)? (3) We want to capture recurring patterns of construction / proof by tactics into reusable Ltac definitions, see below. (4) We want to make use of the abstract facility, explained now.

Now imagine that the following proof was very complicated but had no computational relevance, i.e., could also be packed into a lemma whose proof would be finished by Qed. We can encapsulate it into abstract:

The term features an occurrence of combinatorS_induction_with_abstract_subproof that contains the abstracted part; using the latter name is forbidden by the UniMath style guide. Note that abstract is used hundreds of times in the UniMath library.

Ltac language for defining tactics

Disclaimer: Ltac can do more than that, in fact Ltac is the name of the whole tactic language of Coq. Ltac definitions can associate identifiers for tactics with tactic expressions. We have already used one such identifier: intermediate_path in the Foundations package of UniMath. In file PartA.v, we have the code
Ltac intermediate_path x := apply (pathscomp0 (b := x)).

does not show the formal argument x in the right-hand side. Remedy (in ProofGeneral but not in VSCode):

The problem with these Ltac definitions is that they are barely typed, they behave rather like LaTeX macros.

This definition confounds the type argument X and its element b. The soundness of Coq is not at stake here, but the errors only appear at runtime, as we will see below. Normal printing output hides the difference with the correct tactic definition:

The message does not point to the problem that argument x appears a second time in the Ltac definition with a different needed type.

See https://github.com/UniMath/UniMath/blob/master/UniMath/PAdics/frac.v#L23 for a huge Ltac definition in the UniMath library to appreciate the lack of type information. The UniMath library provides some Ltac definitions for general use:

no need to explain - rather an abbreviation

problem with VSCode analogous to intermediate_path

for the next tactic

output with ProofGeneral (output with VSCode falls again short of crucial information)
Ltac show_id_type :=
       match goal with
       | |- @paths ?ID _ _ ⇒ set (TYPE := ID); simpl in TYPE
       end

Hardly ever present in proofs in the library, but it can be an excellent tool while trying to prove an equation: it puts the index of the path space into the context. This index is invisible in the notation with an equals sign that one normally sees as the goal, and coercions can easily give a wrong impression about that index.

The most useful Ltac definition of UniMath

It applies the simple refine tactic with zero up to fifteen unknown arguments. This tactic must not be used in UniMath since a "tactic notation" is favoured: Foundations/Preamble.v contains the definition
Tactic Notation "use" uconstr(p) := simple_rapply p.

Use of use:

this is often necessary since use does as little as possible

to remind the version where the "witness" is given explicitly:

To conclude: use tpair is the right idiom for an interactive construction of inhabitants of Σ-types. Note that the second generated sub-goal may need cbn to make further tactics applicable. If the first component of the inhabitant is already at hand, then the "exists" tactic yields a leaner proof script. use is not confined to Σ-types. Whenever one would be inclined to start trying to apply a lemma H with a varying number of underscores, use H may be a better option. There is another recommendable tactic notation that is also by Jason Gross:
Tactic Notation "transparent" "assert"
                "(" ident(name) ":" constr(type) ")" :=
                simple refine (let name := (_ : type) in _).

There is no transparent assert by. Now, proofB is present with the constructed proof of B.

To conclude: transparent assert is a replacement for assert if the construction of the assertion is needed in the rest of the proof.

a final word, just on searching the library

SearchPattern searches for the given pattern in what the library gives as *conclusions* of definitions, lemmas, etc., and the current hypotheses. Search searches in the (full) types of all the library elements (and the current hypotheses). It may provide too many irrelevant result for your question. At least, it will also show all the relevant ones. Anyway, only the imported part of the library is searched. The quick way for importing the whole UniMath library is
Require Import UniMath.All.

You may test it with
SearchPattern (_ ≃ _).

with very numerous results.

List of tactics that were mentioned

exact
apply
intro
set
cbn / cbn in (old but sometimes useful form: simpl / simpl in)
assumption
intros (with pattern, with wild cards)
split / split with / ∃
destruct as --- not desirable in UniMath
induction / induction as
admit --- only during proof development
eapply
eexact
refine --- first consider "use" instead
instantiate
unfold / unfold in
intermediate_path (Ltac def.)
rewrite / rewrite <-
change / change in
clear
assert {} / assert by
abstract
etrans (Ltac def.)
intermediate_weq (Ltac def.)
show_id_type (Ltac def.)
simple_rapply (Ltac def., not to be used)
use (Ltac notation)
transparent assert (Ltac notation)