Bounded-Error Log

theoretical and applied randomness by betaveros

Coq Reference

(4335 words) filed under CS

It seems like a rite of passage to create one of these because there are so many Coq tactic cheat sheets out there and there’s just so much to learn. Here’s mine.

This is mostly about tactics but I realized not really.

Links:

Meta-notes: I cover a lot of weak tactics because I like knowing exactly what my tools are doing. I try to use the variants of tactics that explicitly name things produced when possible. I am sure there is nomenclature I don’t understand precisely and use sloppily in this list; I am also sloppy with metavariables. Even things that are correct might be horrible style. There are likely other errors and omissions. They might be fixed one day. I’m putting this up nevertheless because it’s personally useful.

Things I wish I knew but didn’t learn from Software Foundations or Coq tactic cheat sheets

  • The first two sections are not about tactics per se but how to find theorems to use and how to use them. Knowing how to use all of these query commands is super useful.
  • To clean up repeating subexpressions with “local variables”, I find remember expr as X eqn:Hname. easier to work with than set (X := expr).
  • pose proof expr as Hname. adds expr to the context, with name Hname. Modus ponens where you know H1 and H2, which is “H1 implies H3”, is just pose proof (H2 H1) as H3.
  • Software Foundations covers bullets and curly braces early, but I like subgoal specification with 1:, 2: etc., which can really help limit nesting depth. 2: (tactic that solves subgoal 2). If you want more bullets, there are infinitely many, not just three. After - + * you can use -- ++ ** --- etc.

How to fish

  • Use the queries. Search "foo". Check foo. About foo. Compute foo. Print foo. To look up notation (e.g. what does <> mean?) use Locate (e.g. Locate "<>").
  • To look up a simple abstract theorem about natural numbers or equality without knowing what it’s called, SearchPattern is useful. For example, I was looking to prove x <> y given y <> x. SearchPattern (_ <> _ -> _ <> _). found the theorem for me (it was called not_eq_sym). Similarly SearchRewrite on some expression pattern searches for theorems you could use to rewrite that expression.

How to use hypotheses

To use that example again: If you run Check not_eq_sym. you’ll get:

not_eq_sym
     : forall (A : Type) (x y : A), x <> y -> y <> x

Mathematically, not_eq_sym says: for any type A and any two things x and y of type A, if x <> y, then y <> x.

However the literalist programmer view is more like: not_eq_sym is a (fully curried) function that takes in a type A, two things x and y of type A, and finally a proof of the Prop x <> y, and outputs a proof of the Prop y <> x. So if you supplied these four arguments, just by writing not_eq_sym A x y H where H is a proof of x <> y, you’d get a proof of y <> x out.

Well, not quite; you’d actually write @not_eq_sym A x y H. Here @ makes all implicit arguments of not_eq_sym explicit. If you also run About not_eq_sym., you’ll see (among other text):

not_eq_sym : forall (A : Type) (x y : A), x <> y -> y <> x

Arguments A, x, y are implicit

Without the @ you only need to supply (and are only allowed to supply) the one non-implicit argument, H, to not_eq_sym. In practice arguments are usually implicit because they’re deducible from the others, so not_eq_sym H is pretty good.

Implicits can appear in other ways and cause weird issues, such as when you’re trying to rewrite or do something else to an expression that seems to exactly match one side of the rule you’re rewriting with, but Coq refuses to operate on that expression even though it’s in plain sight. The expressions might actually be different because they have implicit arguments that differ. You can see those implicits in the expressions by issusing Show Print Implicit., or fiddling with your CoqIDE settings.

Finishing a proof of something true

  • reflexivity. proves something is equal to itself. It can handle some simplification.

  • exact T. proves a Prop that’s exactly the same as theorem or hypothesis T. “Exactly the same” includes quantifiers! But you can apply arguments to T. For example if your theorem all_foo says forall x : foo x and you want to prove foo y for a specific known y, you could use exact (all_foo y).

    Side note: I is the name for the unique thing of type True, so if you end up with the goal True after simplification and want to prove it with the weakest possible tactic, I think exact I. fits the bill.
  • assumption. proves a Prop that is one of our hypotheses, i.e., is in our context. It’s exact T. without needing to specify T.
  • refine X. proves a Prop that’s exactly the same as X, just like exact X., except that X here can be an expression with holes, or _. It opens up one subgoal for each _.
  • apply H. proves a Prop that directly follows from a theorem or hypothesis H (or, if the theorem is “P implies our goal”, sets the goal to P instead; see below). So apply all_foo. would work instead of exact (all_foo y).
  • trivial. is a weak tactic that proves some very easy goals, including the power of reflexivity and assumption at least.
  • easy. is slightly more powerful. It does split too.

  • There are a lot of automated tactics that can handle proving generally true math facts. We are told to use lia in 6.826.

Finishing a proof of something false

  • discriminate H. proves anything, given an equality H that says something equals something structurally different (with different constructors). You don’t need to specify H.
  • contradiction. proves anything if a hypothesis is false. Note that it has to be a hypothesis and not a thing before ->; if you want to do that, intros it. It also searches for two contradictory hypotheses.
  • absurd P. proves anything by breaking into subgoals P and ~P.

Sidebar: congruence. generalizes discriminate and injection in some way.

Modifying the goal with existing facts

  • apply H. sets the goal to P if H is “P implies our goal” (or, directly proves a Prop that directly follows from a theorem; see above). H can also take more than one argument or premise, in which case apply H. opens up one subgoal per premise. (So in fact, finishing a goal via “apply H.” is just the special case where there are zero premises.)
    • eapply is similar to apply, but it uses existential variables when it can’t figure out some of the variables, and just expects you to fill those in later. This was really hard for me for me to understand, but here’s an artificial example: let’s say you want to prove an equality a = b by the transitive property. a = b matches the conclusion of the built-in theorem eq_trans, which is x = y -> y = z -> x = z. However, apply eq_trans. will fail, because Coq can’t figure out what you want y to be. You could solve this by explicitly specifying what y is by passing some arguments to eq_trans. Alternatively, you can eapply eq_trans. and Coq will create a new existential variable to pass as y. Later, if you implicitly use any tactic that implies something about that variable, Coq will collapse or elaborate that variable.
  • simpl. simplifies the expression. It’s often not necessary in a finished proof, but can help clarify what the goal looks like in the interactive process.
  • rewrite -> H. resp. rewrite <- H. If H is something that says “A = B”, replace A with B in the goal, resp., B with A. If H requires some hypotheses, it will open up those hypotheses as subgoals, coming last.
  • rewrite -> H by tactic. resp. rewrite <- H by tactic. As above but immediately solve the subgoals.
  • subst x. substitutes x everywhere it appears. If you defined x := expr or got an equation like x = expr then this will replace x with expr everywhere and then get rid of x. This is useful if you had two variables x and y introduced in different places in your proof, proved they were equal, and want to fully get rid of one from your context. You can write subst. without x and it will do it automatically.
  • unfold f. Unfold some function f in the goal; approximately, inline it. This may be required if f is a match expression; Coq won’t automatically “simplify” expressions with f since they might actually get more complicated.
  • replace term with term'. Replace term with term' in the goal, and adds a new goal to prove that term = term', putting it last.
  • replace term with term' by tactic. Same, but prove that new goal immediately with a tactic.
  • change term with term'. Roughly same as replace without opening subgoals, if the terms are “convertible”. I was told this means something like “you can prove they’re equal by reflexivity”.
  • symmetry. swaps the goal a = b with b = a.
  • exfalso. explicitly sets the goal to False; sometimes this makes applying theorems easier.

Adding intermediate goals

  • assert U as Name. adds hypothesis U with name Name to context; immediately opens subgoal U. Name can be a destruct pattern.
  • assert U as Name by tactic. Same, but immediately prove the subgoal with a tactic instead.
  • enough U as Name. is the same, but U is proved afterwards.
  • cut P. splits the goal into P -> goal and P.
  • transitivity X. lets you prove A = B through subgoals A = X and X = B.

(There’s also an assert (Name : U) syntax but I never remember the order.)

Splitting into cases

  • constructor. splits the goal into cases if it’s some kind of product type. It’s actually basically just applying the constructor. When the goal is a sum type, constructor N. for some number N more precisely chooses to prove the Nth constructor.
  • f_equal., when the goal is to prove that two calls to the same function are equal, splits into proving that each of the corresponding arguments are equal. (Note that the original goal being true very much doesn’t imply these goals are all true, although it does if the function is a constructor.)
  • destruct expr as [pattern]. splits expr apart, possibly breaking into cases, depending on what constructor expr is. Here [pattern] should be an “intro pattern of disjunctions and conjunctions”. If expr is a product then [pattern] could be [H1 H2]; if expr is a sum then [pattern] could be [H1 | H2]; this could be nested, e.g. [H1 H2 | H3 H4 H5 | ] if it’s a sum of cases with 2, 3, and 0 fields, respectively (and this is what I mean elsewhere by [pattern]). You can even omit “as …” if there’s nothing to destruct to.
  • destruct expr eqn:Hname. does the same, but also giving you a hypothesis with name Hname that states that expr equals what the case is.
  • induction n as [pattern]. splits into base case and induction hypothesis based on what constructor n is. Every branch of the pattern comes with an induction hypothesis. Note: induction behind the scenes is just apply on the “inductive principle” Coq generated when it or you declared the type of n. It seems to have the name of the type of n concatenated with _ind.

Coq is constructive, so you can’t assume P \/ ~P (“P or not P”) in full generality. However you can do this for many common cases of P. Theorems that prove this often have dec in their name for “decidable”. Consider SearchPattern for not just _ \/ _, but also {_} + {_} (where either _ could be further refined depending on what you’re looking for).

The difference, based on my limited understanding and a Piazza answer: _ \/ _ is a Prop but {_} + {_} is a Type. Prop and Type belong to different “universes”, approximately proof stuff and computable stuff, and Coq enforces that information can’t flow from the proof universe to the computable universe. So a {_} + {_} is stronger than a _ \/ _ in that (after specifying any variables needed) you can explicitly compute which branch of the {_} + {_} you have evidence for, and use that information in a function that computes something.

In proofs, you use them in the same way, though: destruct into two cases to do case analysis. Example of theorems of two kinds:

Nat.eq_dec: forall n m : nat, {n = m} + {n <> m}
le_gt_dec: forall n m : nat, {n <= m} + {n > m}
le_dec: forall n m : nat, {n <= m} + {~ n <= m}
Nat.eq_0_gt_0_cases: forall n : nat, n = 0 \/ 0 < n
gt_0_eq: forall n : nat, n > 0 \/ 0 = n
Nat.lt_trichotomy: forall n m : nat, n < m \/ n = m \/ m < n

Note that you probably destruct these into patterns to name the proofs of things, and won’t want eqn:.

Modifying hypotheses

  • apply H in H2 as Hname. If H is “P implies Q” and H2 is “P”, conclude Q, with name Hname.
  • pose proof H as Hname. Add H to the context, with name Hname. Typically H will be an expression. Concrete applications: if H1 is a theorem “P implies Q” and H2 is a hypothesis in the context that “P”, pose proof (H1 H2) as Hname.
  • specialize (H1 H2). Kind of like pose proof specifically for plugging arguments into a local hypothesis H1. The name “specialize” makes the most sense if the arguments are universally quantified variables, e.g. the hypothesis H says forall x : T, foo x and you have a specific y for which you want to know foo y, so you specialize (H y). On the other hand this is more reliably useful when H2 is a premise of H1, since you get a strictly stronger result. Note that the result replaces H with the result of specialization, which makes more sense in the universally quantified variable interpretation but is more reliably useful in the premise interpretation. If you want to get a specialized version without losing the generalized version, use pose proof above.
  • rewrite -> H in H2. / rewrite <- H in H2. / replace term with term' in H2. / replace term with term' in H2 by tactic. / change term with term' in H2. / unfold X in H. / simpl in H. / symmetry in H. all do the same rewriting you’d expect in a hypothesis instead of the goal.
  • inversion H. analyzes H using constructor injectivity and disjointness. That is, it unwraps a constructor from both sides: e.g. if H is S x = S y, conclude x = y; or, if H claims the equality of different constructors, it explodes the case.
  • clear H. deletes something.
  • rename Hold into Hnew. renames a hypothesis in the context.
  • remember expr as X eqn:Hname. introduces a new variable X equal to the expression and an equation that the variable X equals the expression. (There’s also set (X := expr). but this gives you a definition instead of an equation, which seems a bit harder to work with; you can unfold the newly defined variable, but can’t directly refer to the definition by name to rewrite the expression into the variable if it comes up later.)

Introducing universally quantified variables or LHS’s of implications

  • intros n. introduce universally quantified variables or LHS’s of implications into the context.

    • intros [pattern]. combines it with a destruct.
  • revert m. basically undoes an intros when it’s simple.
  • generalize m. undoes an intro in more cases, replacing m with a universally quantified variable. But m can be an expression.

  • generalize dependent m. undoes an intro in even more cases. It clears hypotheses depending on m.

Working with Ands and Ors

  • split. when trying to prove A /\ B, split into subgoals A and B. (This actually works for any goal with one constructor, and is basically just constructor 1.)
  • left. when trying to prove A \/ B, specifically prove A. (This actually works for any goal with two constructors, and is basically just constructor 1.)
  • right. when trying to prove A \/ B, specifically prove B. (This actually works for any goal with two constructors, and is basically just constructor 2.)
  • destruct Hand as [Hleft Hright]. turns a hypothesis A /\ B into hypotheses A and B.
  • destruct Hor as [Hleft | Hright]. uses a hypothesis A \/ B by splitting into cases where either A (named Hleft) or B (named Hright) is true.

The underlying proof objects, for the curious:

conj : forall A B : Prop, A -> B -> A /\ B
or_introl : forall A B : Prop, A -> A \/ B
or_intror : forall A B : Prop, B -> A \/ B

Projecting clauses from a conjunction:

proj1: forall A B : Prop, A /\ B -> A
proj2: forall A B : Prop, A /\ B -> B

Working with Existence

  • exists x. is how you prove an exists a, (something about a), by explicitly exhibiting an x satisfying that something.
  • destruct Hexists as [x H]. turns an existence result into the explicit example (“witness”) satisfying that result and the hypothesis stating that the result does hold for the witness.
ex_intro : forall (A : Type) (P : A -> Prop) (x : A), P x -> exists y, P y

What is this exists y, P y business anyway? It’s special notation for ex:

"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope (default interpretation)
"'exists' ! x .. y , p" := ex (unique (fun x => .. (ex (unique (fun y => p))) ..)) : type_scope (default interpretation)
ex : forall A : Type, (A -> Prop) -> Prop

Argument A is implicit

And ex_intro above is the one constructor of this type.

Equality and negation, while we’re at it

eq_refl : forall (A : Type) (x : A), x = x

"x = y" := eq x y : type_scope (default interpretation)
"x <> y" := not (eq x y) : type_scope (default interpretation)

Working with subgoals

These are the things that come out of case-splitting tactics.

  • Bullets. Basically when you’ve spilt your goal into N subgoals, you make a list with N items, one per subgoal, each with the same bullet. It’s checked that you’ve totally finished a subgoal before you go to the next bullet on the same level. Nested levels must have different bullet types.

    (* some tactic that splits into three cases *)
- (* handle case 1 *)
  + (* handle case 1.1 *)
  + (* handle case 1.2 *)
- (* handle case 2 *)
- (* handle case 3 *)

    Software Foundations introduces you to the three bullets -, +, and *, but you can get more by repeating any of these: --, ++, **, ---, etc. Whether you’d want to is another matter.

  • { } serve a similar goal. { narrows down to a single subgoal; } forces you to have finished it. They can be arbitrarily nested, and reset the bullet context so you can reuse the same bullets inside and outside {}s. Also note that finishing one subgoal with } doesn’t require you to start the next one with {. Sometimes something like this will make sense, especially if the tactic splits into two cases with really different “weight” (e.g. asserting a relatively easy lemma before continuing).

    (* some tactic that splits into two cases *)
{ (* handle case 1 *) }
(* handle case 2 *)
  • 1:, 2:, etc. solves a specifically numbered subgoal with a tactic or bracketed logic. I like to use this when my goal splits into two or more cases where a particular case is very easy and I don’t want to spend a layer of bullets on this split. I have no idea whether this is good style. For example, if my goal splits into two cases and the second case can be proven with reflexivity but the first case is very complex, I might do split. 2: reflexivity. and then continue with the proof of case 1. Comma-separated numbers and ranges denoted with hyphens both work. Cases are 1-indexed.
  • ; (semicolon) solves all subgoals with the same tactic. For example, you could use split; reflexivity. to prove something like a = a /\ b = b.
  • repeat some tacic e.g. repeat rewrite -> H. repeats a tactic until it fails.

  • all: applies a tactic to all subgoals. This is like ; but you get to pause beforehand, and also is how you use goal-reordering tactics.

You can try tactics but not fail if they don’t apply. This is likely only useful acting on multiple subgoals at once, so most likely after ; or all:. I think they should probably be used sparingly. Or maybe in custom tactics.

  • try tries a tactic but doesn’t fail if it fails.
  • || combines two tactics, trying the left tactic before trying the right tactic.

“Cheating”

  • admit. lets you pretend a subgoal is proved and move on. The proof will need to end with Admitted. instead of Qed.

Custom tactics and hint databases

Let’s say you’re building a hint database called foo. If you got a theorem bar that you want to rewrite rightwards automatically, you can add it like:

Hint Rewrite bar : foo.

Probably only do this if bar doesn’t take any premises. If you want to autorewrite using a theorem bar with premises that might not always be true, and you only want to autorewrite when the premises can be automatically proven, you can say that the premises must be solved with auto to use the hint:

Hint Rewrite bar2 using (solve [ auto ]) : foo.

After all that you can use autorewrite with foo.

The simplest way to build a custom tactic just looks like:

Ltac my_tactic := tactic1; tactic2; tactic3.

More interesting tactics will pattern match on the goal or on hypotheses. Use the syntax match goal with .... The pattern has |- to separate hypotheses from the goal.

You can name hypotheses. To name variables or expressions that might appear in the hypotheses or goal but might vary and that you want to use in the tactic, use a question mark in front of a name in the pattern. Don’t use that question mark in the body of the tactic. Example:

Ltac subst_Some_eq :=
  match goal with
  | H : Some ?a = Some ?b |- _ =>
        inversion H; subst b
  end.

If you want to pattern-match on any expression anywhere, use context[ ].

Ltac destruct_if :=
  match goal with
  | |- context[if ?a then _ else _] => destruct a
  end.

If you only want to do something if some variable ?x is a variable, you can use is_var x before the tactic. match backtracks and tries matching its pattern to more hypotheses; it also tries the next branch if the branch pattern doesn’t match or if the tactics fail. Alternate: lazymatch doesn’t backtrack from tactic failures.

progress on some tactic only works if the tactic makes progress.

idtac is a tactic that does nothing, plus you can pass arguments to debug.

The fail tactic takes a number, the number of levels to propagate the failure up, and then extra debugging stuff.

first [ t1 | t2 | ... ] takes some tactics and does the first one that succeeds.

type of X gives the, well, type of X

Ltac is also a functional programming language! Use constr:(...) to break back into Gallina. Note that match patterns are implicitly Gallina.

(* can't infer T sad *)
Ltac map T f l :=
  let rec map_impl l :=
    match l with
    | nil => constr:(@nil T)
    | ?h :: ?t => let h' := f h in let t' := map_impl t in constr:(h' :: t')
  end in map_impl.

Goal False.
let ls := map (nat * nat)%type ltac:(fun x -> constr:((x, x))) (1 :: 2 :: 3 :: nil) in pose ls.

You can’t do ; in functional programming Ltac, it turns into a procedure thing.

Brackets are super precise. This applies these three tactics respectively to the three focused goals. There must be exactly three. You can omit tactics to do idtac, the identity tactic.

[> tactic1 | tactic2 | tactic3 ]

Note that in a proof script you have to apply to all focused goals so it would look like all: [> tactic1 | tactic2 | tactic3 ] although this is a silly way to do it. If you’re putting this after a semicolon, you can drop the >. I’m not sure how this works.

FRAP tactics

  • simplify. improves on simpl.
  • cases expr. improves on destruct expr. (No patterns though.)
  • invert x. improves on inversion x.
  • linear_arithmetic. improves on lia.
  • propositional. handles and simplifies things based on propositional logic: conjunctions, disjunctions, implications…
  • first_order. handles and simplifies things based on first order logic. It’s more powerful, but riskier; it might run forever.

(note: the commenting setup here is experimental and I may not check my comments often; if you want to tell me something instead of the world, email me!)