README.md

Tricks in Coq

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!

Ltac

• pattern tactic
• lazymatch for better error messages
• deex tactic
• ::= to re-define Ltac
• learn approach - see Clément's thesis
• unshelve 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 proof
• unfold "+" works
• destruct 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 use induction n as [n IHn] using lt_wf_ind.
• induction on the length of a list: Require Import Coq.Arith.Wf_nat. and induction xs as [xs IHxs] using (induction_ltof1 _ (@length _)); unfold ltof in IHxs.
• debug auto, debug eauto, and debug trivial give traces, including failed invocations. info_auto, info_eauto, and info_trivial are less verbose ways to debug which only report what the resulting proof includes
• constructor and econstructor 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 do destruct x eqn:H to explicitly name the equality hypothesis. This is similar to case_eq x; intros; I'm not sure what the practical differences are.
• rew H in t notation to use eq_rect for a (safe) "type cast". Need to import EqNotations - 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 * and in H to apply everywhere and in a specific hypotheses, but there are actually a bunch of forms. The syntax is really silly so I'm just going to give examples and hope they help.
  • in H1, H2 (just H1 and H2)
  • 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 as in *) Why have all these forms, particularly the last two? They're useless, but if Coq ever supported first-class occurrence sets (that is, you could write tactics that takes occurrence sets and operate on them) they might be handy. Except in |-, which is probably useless and just an artifact of the grammar.
• 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 then

  match goal with
  | |- context[anyplus] => idtac
  end
  

  I would recommend using 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 with eauto using t where t is the name of the inductive.
• The intuition tactic has some unexpected behaviors. It takes a tactic to run on each goal, which is auto with * by default, using hints from all hint databases. intuition idtac or intuition eauto are both much safer. When using these, note that intuition eauto; simpl is parsed as intuition (eauto; simpl), which is unlikely to be what you want; you'll need to instead write (intuition eauto); simpl.

Gallina

• 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 as Field r, but convenient when Field is a projection function for the (record) type of r. If you use these, you might also want Set 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 in Function.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)
  • 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

• 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, and symmetry more powerful).

• The types of inductives can be definitions, as long as they expand to an "arity" (a function type ending in Prop, Set, or Type). See ArityDefinition.v.

Other Coq commands

• Search vernacular variants; see Search.v for examples.
• Search s -Learnt for a search of local hypotheses excluding Learnt
• Locate can search for notation, including partial searches.
• Optimize Heap (undocumented) runs GC (specifically Gc.compact)
• Optimize Proof (undocumented) runs several simplifications on the current proof term (see Proofview.compact)
• Generalizable Variable A enables implicit generalization; Definition id(x:A) := xwill implicitly add a parameterAbeforex.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 is Check (id _ _), where the first underscore must be a function (along with other constraints on the types involved).

Using Coq

• You can pass -noinit to coqc or coqtop 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).