Index

The inner mechanism going on when using tactics like reflexivity, transitivity or symmetry is typeclasses. However coq allows a particular facility to declare new relation without digging into this. The syntax goes roughly as follows:

Add Parametric Relation (A: Type): A (@R A)
reflexivity proved by ...
symmetry proved by ...
transitivity proved by ...
as R_is_an_equivalence_relation.

Note that you naturally only want to take A as a parameter if your relation is indeed polymorphic. For instance, suppose you need to manipulate predicates over program states up to propositional extentional equivalence. This relation is an equivalence relation, so you might want to declare it as so.

Axiom state: Type.
Definition Pred: state -> Prop.
Definition PEq (P1 P2: Pred): Prop := forall x, P1 x <-> P2 x.
Lemma PEq_reflexive: forall P, P ≡ P.
Proof.
  intros P s; go.
Qed.

Lemma PEq_trans: forall P1 P2 P3 (H1: P1 ≡ P2) (H2: P2 ≡ P3),
    P1 ≡ P3.
  intros P1 P2 P3 H1 H2 s; split; intros H3; [apply H2, H1 | apply H1,H2]; assumption.
Qed.

Lemma PEq_symm: forall P1 P2 (H: P1 ≡ P2), P2 ≡ P1.
Proof.
  intros P1 P2 H s; split; intros H'; apply H; assumption.
Qed.

Add Parametric Relation: Pred PEq
    reflexivity proved by PEq_reflexive
    symmetry proved by PEq_symm
    transitivity proved by PEq_trans
      as PEq_equiv.

We now are able to prove goals such that (forall P: Pred, PEq P P) with a simpl (intros P; reflexivity). Same goes for transitivity and symmetry.

Note that we can also only declare some of those properties, declaring that a relation is a preorder for instance:

Definition PWeaker (P1 P2: Pred): Prop := forall s, P2 s -> P1 s.

Lemma PWeaker_reflexive: forall P, P ⊆ P.
Proof.
  go.
Qed.

Lemma PWeaker_trans: forall P1 P2 P3 (H1: P1 ⊆ P2) (H2: P2 ⊆ P3), P1 ⊆ P3.
Proof.
  intros P1 P2 P3 H1 H2 s H3; apply H1,H2,H3.
Qed.

Add Parametric Relation: Pred PWeaker
    reflexivity proved by PWeaker_reflexive
    transitivity proved by PWeaker_trans
      as PWeaker_preorder.

In this case naturally symmetry will not work. Note that you are not required to provide the appropriate proof term directly in the relation declaration, you may use wildcards for coq to require the proofs interactively.

Remark: As said earlier, what is really going on is the typeclass mechanism. So all this is simply sugar for an instance declaration to the appropriate type class, Equivalence for example in the first case. We could have written instead:

Require Import Classes.RelationClasses.

Instance PEq_equiv: @Equivalence Pred PEq :=
 Equivalence_Reflexive := PEq_reflexive
 Equivalence_Symmetric := PEq_symm
 Equivalence_Transitive := PEq_trans.

The other typical case in which you might want to extend built-in tactics is the one of morphisms for which we would like to be able to use rewrite. Once again, we have syntactic sugar to avoir bothering explicitely with typeclasses. In the case of a binary function, it would look like this:

Add Parametric Morphism : f with
   signature (rel ==> rel ==> rel) as foo.

This one might seem a bit more cryptic. What is going on is that given a context, we want to be able to substitute a subterm for an other one given they are related by the relation rel. Said differently, we want to prove that f is a morphism with respect to rel, or that rel is compatible with f.

It is clearer with an example. Say we define the union of two predicates, we can actually rewrite any equivalent predicates under it.

Require Import Setoid.
Definition PJoin P1 P2: Pred := λ s, P1 s \/ P2 s.

Add Parametric Morphism : PJoin with
   signature (PEq ==> PEq ==> PEq) as foo.
Proof.
  intros Q1 Q1' eq1 Q2 Q2' eq2 s; split; intros H;
    (destruct H; [left; apply eq1; assumption | right; apply eq2; assumption]).
Qed.

coq asked us to prove that if four predicates are pairwise PEquivalent, their respective unions are PEquivalent. We therefore now are able to use the tactic rewrite to rewrite PEquivalences under unions in goals.

Note: beware, we only proved the compatibility of PEq with respect to the union! coq will complain if we try to rewrite PEquivalence under any other construction. The (Leibniz) equality has the peculiar property to be compatible with any context by definition.

Note bis: we have a very symmetric statement in the exemple using PEq everywhere, but that is not necessary. We could for instance assert compatibility only on the left by replacing the second PEq by an eq. An other reason of uniformity in the example is that the codomain of the function PJoin is the same as its arguments, but once again it could be otherwise. It notably is common to end up in Prop and therefore be interested in a result where the last PEq is replaced by iff: the proposition obtained after rewriting is guaranteed to be equivalent.

Finally, as was the case with relations, we can instead explicitely declare the adequate instance. The Typeclass at use here is Proper:

Instance foo: Proper (PEq ==> PEq ==> PEq) PJoin.
Proof.
  intros Q1 Q1' eq1 Q2 Q2' eq2 s; split; intros H;
    (destruct H; [left; apply eq1; assumption | right; apply eq2; assumption]).
Qed.

The auto (or its existential variant) tactics tries by default to solve a goal by exploring proofs trees, up to a fixed depth, that could be built using a fixed set of rules. These rules are defined in a so-called database, named core, essentially trying to unfold a few arithmetic and boolean functions from the standard library, and trying to apply a few lemmas and constructor over the elementary logical connectives. Its detail can be printed through the command:

Print HintDb core.

However, the auto tactics can be prompted to use another hint database. Are predefined the following, whose detail can be printed as seen previously: arith, zarith, bool, datatypes, sets and typeclass_instances. Note that the last one is automatically enriched when registering new instances for a typeclass, and used during resolution. The syntax to use a specific database is the following:

auto with db1 ... db2.

One can also define its own databases, for instance to reduce a user defined expression to its normal-form via rewriting lemmas. Its creation is done through the Create HintDb command:

Create HintDb my_lovely_db.

The user can then enrich the database by adding hints to it. A hint is a lemma (actually more generally a term) and a way to use it:

• by applying it (adds "simple apply term" to the db): keyword Resolve
• by succeeding applying it (adds "simple apply term; trivial" to the db): keyword Immediate
• by adding constructors of a type as Resolve hints: keyword Constructors
• by allowing auto to unfold a definition: keyword Unfold
• by applying any tactic: keyword Extern.

For instance:

Hint Resolve lemma1 lemma2: my_lovely_db.

For more details: https://coq.inria.fr/refman/Reference-Manual010.html#sec395

Reflexivity does more than simpl, it notably tries to unfold definitions.

Looking for an hypothesis of the form P x y, for any x and y.

match goal with
  H : P ?x ?y |- _ => destruct H; auto
end.

This will fail if no such hypothesis exists. You can add try in front of it.

To match all such hypotheses, add repeat.

The following example shows how to use hypotheses matching to remove duplicates in hypotheses.

Goal P x y -> P x y -> P x z -> P x z -> P x z -> P y z.
Proof.
  intros.

  repeat match goal with
    H1 : P ?x ?y,
        H2: P ?x ?y |- _ => clear H1
  end.
Qed.

We try to match two hypotheses of the form P ?x ?y. The pattern matching is strong enough to express that H1 and H2 must refer to the same x and y. H1 and H2 are guaranteed to be different though.

It is also possible to match part of an hypothesis. Using context:

match goal with
  H : context [P ?x ?y] |- _ => (* do stuff *)
end.

The matching can also be made on the conlusion of the goal (after |-):

match goal with
  |- context [P ?x ?y] => (* do stuff *)
end.

Of course, multiple patterns can be matched.

repeat match goal with
  H : context [P ?x ?y] |- _ => (* do stuff *)
| |- context [P ?x ?y] => (* do stuff *)
end.

This will loop as long as either the hypotheses or the conclusion contain a term matching P ?x ?y. Be sure to remove the matching hypotheses to enforce termination.

In Coq 8.5, the all: selector applies a given tactic to all goals. This seems very handy in cases where a eapply has generated lots of existentials, most of which would be solved in a particular subgoal. The strategy I would use here is to apply some tactic to the most discriminant subgoal and then call auto or eauto on the rest of the subgoals.

n: tac.
all: auto.