Some tips, tricks, and features in Coq that are hard to discover.
If you have a trick you've found useful feel free to submit an issue or pull request!
pattern
tacticlazymatch
for better error messagesdeex
tactic::=
to re-define Ltaclearn
approach - see Learn.v for a self-contained example or Clément's thesis for more detailsunshelve
tactical, especially useful with an eapply - good example use case is constructing an object by refinement where the obligations end up being your proofs with the values as evars, when you wanted to construct the values by proofunfold "+"
worksdestruct matches
tactic- using
instantiate
to modify evar environment (thanks to Jonathan Leivent on coq-club) eexists ?[x]
lets one name an existential variable to be able to refer to it later- strong induction is in the standard library:
Require Import Arith.
and useinduction n as [n IHn] using lt_wf_ind.
- induction on the length of a list:
Require Import Coq.Arith.Wf_nat.
andinduction xs as [xs IHxs] using (induction_ltof1 _ (@length _)); unfold ltof in IHxs.
debug auto
,debug eauto
, anddebug trivial
give traces, including failed invocations.info_auto
,info_eauto
, andinfo_trivial
are less verbose ways to debug which only report what the resulting proof includesconstructor
andeconstructor
backtrack over the constructors over an inductive, which lets you do fun things exploring the constructors of an inductive type. See Constructors.v for some demonstrations.- There's a way to destruct and maintain an equality:
destruct_with_eqn x
. You can also dodestruct x eqn:H
to explicitly name the equality hypothesis. This is similar tocase_eq x; intros
; I'm not sure what the practical differences are. rew H in t
notation to useeq_rect
for a (safe) "type cast". Need to importEqNotations
- see RewNotation.v for a working example.intro
-patterns can be combined in a non-trivial way:intros [=->%lemma]
-- see IntroPatterns.v.change
tactic supports patterns (?var
): e.g.repeat change (fun x => ?f x) with f
would eta-reduce all the functions (of arbitrary arity) in the goal.- One way to implement a tactic that sleeps for n seconds is in Sleep.v.
- Some tactics take an "occurrence clause" to select where they apply. The common ones are
in *
andin H
to apply everywhere and in a specific hypotheses, but there are actually a bunch of forms, for example:in H1, H2
(justH1
andH2
)in H1, H2 |- *
(H1
,H2
, and the goal)in * |-
(just hypotheses)in |-
(nowhere)in |- *
(just the goal, same as leaving the whole thing off)in * |- *
(everywhere, same asin *
) These forms would be especially useful if occurrence clauses were first-class objects; that is, if tactics could take and pass occurrence clauses. Currently user-defined tactics support occurrence clauses via a set of tactic notations.
- You can use notations to shorten repetitive Ltac patterns (much like Haskell's PatternSynonyms). Define a notation with holes (underscores) and use it in an Ltac match, eg
Notation anyplus := (_ + _).
and thenI would recommend usingmatch goal with | |- context[anyplus] => idtac end
Local Notation
so the notation isn't available outside the current file. - You can make all constructors of an inductive hints with
Hint Constructors
; you can also do this locally in a proof witheauto using t
wheret
is the name of the inductive. - The
intuition
tactic has some unexpected behaviors. It takes a tactic to run on each goal, which isauto with *
by default, using hints from all hint databases.intuition idtac
orintuition eauto
are both much safer. When using these, note thatintuition eauto; simpl
is parsed asintuition (eauto; simpl)
, which is unlikely to be what you want; you'll need to instead write(intuition eauto); simpl
. - The
Coq.Program.Tactics
library has a number of useful tactics and tactic helpers. Some gems that I like:add_hypothesis
is likepose proof
but fails if the fact is already in the context (a lightweight version of thelearn
approach);destruct_one_ex
implements the tricky code to eliminate anexists
while retaining names (it's a better version of ourdeex
);on_application
matches any application off
by simply handling a large number of arities. - You can structure your proofs using bullets. You should use them in the order
-
,+
,*
so that Proof General indents them correctly. If you need more bullets you can keep going with--
,++
,**
(although you should rarely need more then three levels of bullets in one proof). - You can use the
set
tactic to create shorthand names for expressions. These are speciallet
-bound variables and show up in the hypotheses asv := def
. To "unfold" these definitions you can dosubst v
(note the explicit name is required,subst
will not do this by default). This is a good way to make large goals readable, perhaps while figuring out what lemma to extract. It can also be useful if you need to refer these expressions. - When you write a function in proof mode (useful when dependent types are involved), you probably want to end the proof with
Defined
instead ofQed
. The difference is thatQed
makes the proof term opaque and prevents reduction, whileDefined
will simplify correctly. If you mix computational parts and proof parts (eg, functions which produce sigma types) then you may want to separate the proof into a lemma so that it doesn't get unfolded into a large proof term. - To make an evar an explicit goal, you can use this trick:
unshelve (instantiate (1:=_))
. The way this work is to instantiate the evar with a fresh evar (created due to the_
) and then unshelve that evar, making it an explicit goal. See UnshelveInstantiate.v for a working example. - The
enough
tactic behaves likeassert
but puts the goal for the stated fact after the current goal rather than before.
-
tactics in terms, eg
ltac:(eauto)
can provide a proof argument -
maximally inserted implicit arguments are implicit even when for identifier alone (eg,
nil
is defined to include the implicit list element type) -
maximally inserted arguments can be defined differently for different numbers of arguments - undocumented but
eq_refl
provides an example -
r.(Field)
syntax: same asField r
, but convenient whenField
is a projection function for the (record) type ofr
. If you use these, you might also wantSet Printing Projections
so Coq re-prints calls to projections with the same syntax. -
Function
vernacular provides a more advanced way to define recursive functions, which removes the restriction of having a structurally decreasing argument; you just need to specify a well-founded relation or a decreasing measure maps to a nat, then prove all necessary obligations to show this function can terminate. See manual and examples inFunction.v
for more details.Two alternatives are considerable as drop-in replacements for
Function
.Program Fixpoint
may be useful when defining a nested recursive function. See manual and this StackOverflow post.- CPDT's way of defining general recursive functions with
Fix
combinator.
-
One can pattern-match on tuples under lambdas:
Definition fst {A B} : (A * B) -> A := fun '(x,_) => x.
(works since Coq 8.6). -
Records fields can be defined with
:>
, which make that field accessor a coercion. There are three ways to use this (since there are three types of coercion classes). See Coercions.v for some concrete examples.- If the field is an ordinary type, the record can be used as that type (the field will implicitly be accessed). One good use case for this is whenever a record includes another record; this coercion will make the field accessors of the sub-record work for the outer record as well. (This is vaguely similar to Go embedded structs)
- If the field has a function type, the record can be called.
- If the field is a sort (eg,
Type
), then the record can be used as a type.
-
When a Class field (as opposed to a record) is defined with
:>
, it becomes a hint for typeclass resolution. This is useful when a class includes a "super-class" requirement as a field. For example,Equivalence
has fields for reflexivity, symmetry, and transitivity. The reflexivity field can be used to generically take anEquivalence
instance and get a reflexivity instance for free. -
The type classes in RelationClasses are useful but can be repetitive to prove. RelationInstances.v goes through a few ways of making these more convenient, and why you would want to do so (basically you can make
reflexivity
,transitivity
, andsymmetry
more powerful). -
The types of inductives can be definitions, as long as they expand to an "arity" (a function type ending in
Prop
,Set
, orType
). See ArityDefinition.v. -
Record fields that are functions can be written in definition-style syntax with the parameters bound after the record name, eg
{| func x y := x + y; |}
(see RecordFunction.v for a complete example). -
If you have a coercion
get_function : MyRecord >-> Funclass
you can useAdd Printing Coercion get_function
and then add a notation forget_function
so your coercion can be parsed as function application but printed using some other syntax (and maybe you want that syntax to beprinting only
). -
You can pass implicit arguments explicitly in a keyword-argument-like style, eg
nil (A:=nat)
. UseAbout
to figure out argument names. -
If you do nasty dependent pattern matches or use
inversion
on a goal and it produces equalities ofexistT
's, you may benefit from small inversions, described in this blog post. While the small inversion tactic is still not available anywhere I can find, some support is built in to Coq's match return type inference; see SmallInversions.v for examples of how to use that. -
You can use tactics-in-terms with notations to write function-like definitions that are written in Ltac. For example, you can use this facility to write macros that inspect and transform Gallina terms, producing theorem statements and optionally their proofs automatically. A simple example is given in DefEquality.v of writing a function that produces an equality for unfolding a definition.
-
Notations can be dangerous since they by default have global scope and are imported by
Import
, with no way to selectively import. A pattern I now use by default to make notations controllable is to define every notation in a module with a scope; see NotationModule.v.This pattern has several advantages:
- notations are only loaded as needed, preventing conflicts when not using the notations
- the notations can be brought into scope everywhere as needed with
Import
andLocal Open Scope
, restoring the convenience of a global notation - if notations conflict, some of them can always be scoped appropriately
Search
vernacular variants; see Search.v for examples.Search s -Learnt
for a search of local hypotheses excluding LearntLocate
can search for notation, including partial searches.Optimize Heap
(undocumented) runs GC (specificallyGc.compact
)Optimize Proof
(undocumented) runs several simplifications on the current proof term (seeProofview.compact
)Generalizable Variable A
enables implicit generalization;Definition id `(x:A) := x
will implicitly add a parameterA
beforex
.Generalizable All Variables
enables implicit generalization for any identifier. Note that this surprisingly allows generalization without a backtick in Instances; see InstanceGeneralization.v. Issue #6030 generously requests this behavior be documented, but it should probably require enabling some option.Check
supports partial terms, printing a type along with a context of evars. A cool example isCheck (id _ _)
, where the first underscore must be a function (along with other constraints on the types involved).Unset Intuition Negation Unfolding
will causeintuition
to stop unfoldingnot
.- Definitions can be normalized (simplified/computed) easily with
Definition bar := Eval compute in foo.
Set Uniform Inductive Parameters
(in Coq v8.9+beta onwards) allows you to omit the uniform parameters to an inductive in the constructors.Lemma
andTheorem
are synonymous, except thatcoqdoc
will not show lemmas. Also synonymous:Corollary
,Remark
, andFact
.Definition
is nearly synonymous, except thatTheorem x := def
is not supported (you need to useDefinition
).- Sections are a powerful way to write a collection of definitions and lemmas that all take the same generic arguments. Here are some tricks for working with sections, which are illustrated in Sections.v:
- Use
Context
, which is strictly more powerful thanVariable
- you can declare multiple dependent parameters and get type inference, and can write{A}
to make sure a parameter is implicit and maximally inserted. - Tactics and hints are cleared at the end of a section. This is often annoying but you can take advantage of it by writing one-off tactics like
t
that are specific to the automation of a file, and callers don't see it. Similarly with adding hints tocore
with abandon. - Use notations and implicit types. Say you have a section that defines lists, and you want another file with a bunch of list theorems. You can start with
Context (A:Type). Notation list := (List.list A). Implicit Types (l:list).
and then in the whole section you basically never need to write type annotations. The notation and implicit type disappears at the end of the section so no worries about leaking it. Furthermore, don't writeTheorem foo : forall l,
but instead writeTheorem foo l :
; you can often also avoid usingintros
with this trick (though be careful about doing induction and ending up with a weak induction hypothesis). - If you write a general-purpose tactic
t
that solves most goals in a section, it gets annoying to writeProof. t. Qed.
every time. Instead, defineNotation magic := ltac:(t) (only parsing).
and writeDefinition foo l : l = l ++ [] = magic.
. You do unfortunately have to writeDefinition
;Lemma
andTheorem
do not support:=
definitions. You don't have to call itmagic
but of course it's more fun that way. Note that this isn't the best plan because you end up with transparent proofs, which isn't great; ideally Coq would just supportTheorem foo :=
syntax for opaque proofs.
- Use
- Haskell has an operator
f $ x
, which is the same asf x
except that its parsed differently:f $ 1 + 1
meansf (1 + 1)
, avoiding parentheses. You can simulate this in Coq with a notation:Notation "f $ x" := (f x) (at level 60, right associativity, only parsing).
(from jwiegley/coq-haskell). - A useful convention for notations is to have them start with a word and an exclamation mark. This is borrowed from @andres-erbsen, who borrowed it from the Rust macro syntax. An example of using this convention is in Macros.v. There are three big advantages to this approach: first, using it consistently alerts readers that a macro is being used, and second, using names makes it much easier to create many macros compared to inventing ASCII syntax, and third, starting every macro with a keyword makes them much easier to get parsing correctly.
- To declare an axiomatic instance of a typeclass, use
Declare Instance foo : TypeClass
. This replaces the now-deprecated optionTypeclasses Axioms Are Instances
which allows one to useAxiom
(this was the default behavior in Coq 8.7), as well as the pattern ofAxiom
+Existing Instance
. - To make Ltac scripts more readable, you can use
Set Default Goal Selector "!".
, which will enforce that every Ltac command (sentence) be applied to exactly one focused goal. You achieve that by using a combination of bullets and braces. As a result, when reading a script you can always see the flow of where multiple goals are generated and solved.
- You can pass
-noinit
tocoqc
orcoqtop
to avoid loading the standard library.- Ltac is provided as a plugin loaded by the standard library; to load it you need
Declare ML Module "ltac_plugin".
(see NoInit.v). - Numeral notations are only provided by the prelude, even if you issue
Require Import Coq.Init.Datatypes
.
- Ltac is provided as a plugin loaded by the standard library; to load it you need