Claudio Sacerdoti Coen1
This chapter presents the extension of several equality related tactics to work over user-defined structures (called setoids) that are equipped with ad-hoc equivalence relations meant to behave as equalities. Actually, the tactics have also been generalized to relations weaker then equivalences (e.g. rewriting systems).
The work generalizes, and is partially based on, a previous implementation of the setoid_replace tactic by Clément Renard.
A parametric relation R is any term of type forall (x1:T1) …(xn:Tn), relation A. The expression A, which depends on x1 …xn, is called the carrier of the relation and R is said to be a relation over A; the list x1,…,xn is the (possibly empty) list of parameters of the relation.
An instance of a parametric relation R with n parameters is any term (R t1 …tn).
Let R be a relation over A with n parameters. A term is a parametric proof of reflexivity for R if it has type forall (x1:T1) …(xn:Tn), reflexive (R x1 …xn). Similar definitions are given for parametric proofs of symmetry and transitivity.
A parametric unary function f of type forall (x1:T1) …(xn:Tn), A1 -> A2 covariantly respects two parametric relation instances R1 and R2 if, whenever x, y satisfy R1 x y, their images (f x) and (f y) satisfy R2 (f x) (f y) . An f that respects its input and output relations will be called a unary covariant morphism. We can also say that f is a monotone function with respect to R1 and R2. The sequence x1,… xn represents the parameters of the morphism.
Let R1 and R2 be two parametric relations. The signature of a parametric morphism of type forall (x1:T1) …(xn:Tn), A1 -> A2 that covariantly respects two parametric relations that are instances of R1 and R2 is written R1 ++> R2. Notice that the special arrow ++>, which reminds the reader of covariance, is placed between the two parametric relations, not between the two carriers or the two relation instances.
The previous definitions are extended straightforwardly to n-ary morphisms, that are required to be simultaneously monotone on every argument.
Morphisms can also be contravariant in one or more of their arguments. A morphism is contravariant on an argument associated to the relation instance R if it is covariant on the same argument when the inverse relation R−1 is considered. The special arrow --> is used in signatures for contravariant morphisms.
Functions having arguments related by symmetric relations instances are both covariant and contravariant in those arguments. The special arrow ==> is used in signatures for morphisms that are both covariant and contravariant.
An instance of a parametric morphism f with n parameters is any term f t1 …tn.
The signature of the function union is set_eq ==> set_eq ==> set_eq.
Notice that Leibniz equality is a relation and that every function is a morphism that respects Leibniz equality. Unfortunately, Leibniz equality is not always the intended equality for a given structure.
In the next section we will describe the commands to register terms as parametric relations and morphisms. Several tactics that deal with equality in Coq can also work with the registered relations. The exact list of tactic will be given in Sect. 21.7. For instance, the tactic reflexivity can be used to close a goal R n n whenever R is an instance of a registered reflexive relation. However, the tactics that replace in a context C[] one term with another one related by R must verify that C[] is a morphism that respects the intended relation. Currently the verification consists in checking whether C[] is a syntactic composition of morphism instances that respects some obvious compatibility constraints.
A parametric relation Aeq: forall (x1:T1) …(xn:Tn), relation (A x1 …xn) over (A x1 …xn) can be declared with the following command
Add Relation A Aeq
[reflexivity proved by refl]
[symmetry proved by sym]
[transitivity proved by trans]
as id.
after having required the Setoid module with the Require Setoid command.
The identifier id gives a unique name to the morphism and it is used by the command to generate fresh names for automatically provided lemmas used internally.
Notice that A is required to be a term having the same parameters of Aeq. This is a limitation of the tactic that is often unproblematic in practice.
The proofs of reflexivity, symmetry and transitivity can be omitted if the relation is not an equivalence relation.
If Aeq is a transitive relation, then the command also generates a lemma of type:
forall (x1:T1)…(xn:Tn) (x y x’ y’: (A x1 …xn))
Aeq x1 …xn x’ x -> Aeq x1 …xn y y’ ->
(Aeq x1 …xn x y -> Aeq x1 …xn x’ y’)
that is used to declare Aeq as a parametric morphism of signature Aeq --> Aeq ++> impl where impl is logical implication seen as a parametric relation over Aeq.
Some tactics (reflexivity, symmetry, transitivity) work only on relations that respect the expected properties. The remaining tactics (replace, rewrite and derived tactics such as autorewrite) do not require any properties over the relation. However, they are able to replace terms with related ones only in contexts that are syntactic compositions of parametric morphism instances declared with the following command.
Add Morphism f
with signature sig
as id.
Proof
…
Qed
The command declares f as a parametric morphism of signature sig. The identifier id gives a unique name to the morphism and it is used by the command to generate fresh names for automatically provided lemmas used internally. The number of parameters for f is inferred by comparing its type with the provided signature. The command asks the user to prove interactively that f respects the relations identified from the signature.
Require Export Relation_Definitions. Require Export Setoid. Set Implicit Arguments. Set Contextual Implicit. Parameter set: Type -> Type. Parameter empty: forall A, set A. Parameter eq_set: forall A, set A -> set A -> Prop. Parameter union: forall A, set A -> set A -> set A. Axiom eq_set_refl: forall A, reflexive _ (eq_set (A:=A)). Axiom eq_set_sym: forall A, symmetric _ (eq_set (A:=A)). Axiom eq_set_trans: forall A, transitive _ (eq_set (A:=A)). Axiom empty_neutral: forall A (S: set A), eq_set (union S empty) S. Axiom union_compat: forall (A : Type), forall x x' : set A, eq_set x x' -> forall y y' : set A, eq_set y y' -> eq_set (union x y) (union x' y'). Add Relation set eq_set reflexivity proved by (@eq_set_refl) symmetry proved by (@eq_set_sym) transitivity proved by (@eq_set_trans) as eq_set_rel. Add Morphism union with signature eq_set ==> eq_set ==> eq_set as union_mor. Proof. exact union_compat. Qed.
We proceed now by proving a simple lemma performing a rewrite step and then applying reflexivity, as we would do working with Leibniz equality. Both tactic applications are accepted since the required properties over eq_set and union can be established from the two declarations above.
Goal forall (S: set nat), eq_set (union (union S empty) S) (union S S). Proof. intros. rewrite (@empty_neutral). reflexivity. Qed.
The tables of relations and morphisms are compatible with the Coq sectioning mechanism. If you declare a relation or a morphism inside a section, the declaration will be thrown away when closing the section. And when you load a compiled file, all the declarations of this file that were not inside a section will be loaded.
To replace only one argument of an n-ary morphism it is necessary to prove that all the other arguments are related to themselves by the respective relation instances.
When the relations associated to some arguments are not reflexive, the tactic cannot automatically prove the reflexivity goals, that are left to the user.
Setoids whose relation are partial equivalence relations (PER) are useful to deal with partial functions. Let R be a PER. We say that an element x is defined if R x x. A partial function whose domain comprises all the defined elements only is declared as a morphism that respects R. Every time a rewriting step is performed the user must prove that the argument of the morphism is defined.
When the user works up to relations that are not symmetric, it is no longer the case that any covariant morphism argument is also contravariant. As a result it is no longer possible to replace a term with a related one in every context, since the obtained goal implies the previous one if and only if the replacement has been performed in a contravariant position. In a similar way, replacement in an hypothesis can be performed only if the replaced term occurs in a covariant position.
An error message will be raised by the rewrite and replace tactics when the user is trying to replace a term that occurs in the wrong position.
As expected, composing morphisms together propagates the variance annotations by switching the variance every time a contravariant position is traversed.
One function can respect several different relations and thus it can be declared as a morphism having multiple signatures.
To declare multiple signatures for a morphism, repeat the Add Morphism command.
When morphisms have multiple signatures it can be the case that a rewrite request is ambiguous, since it is unclear what relations should be used to perform the rewriting. When non reflexive relations are involved, different choices lead to different sets of new goals to prove. In this case the tactic automatically picks one choice, but raises a warning describing the set of alternative new goals. To force one particular choice, the user can switch to the following alternative syntax for rewriting:
setoid_rewrite [orientation] term [in ident]
generate side conditions term1 …termn
Up to the generate side conditions part, the syntax is equivalent to the one of the rewrite tactic. Additionally, the user can specify a list of new goals that the tactic must generate. The tactic will prune out from the alternative choices those choices that do not open at least the user proposed goals. Thus, providing enough side conditions, the user can restrict the tactic to at most one choice.
To pick the second set of goals it is sufficient to use setoid_rewrite H generate side conditions (m [=]- m) since the side condition m [=]- m is contained only in the second set of goals.
First class setoids and morphisms can also be handled by encoding them as records. The projections of the setoid relation and of the morphism function can be registered as parametric relations and morphisms, as illustrated by the following example.
Require Export Relation_Definitions.
Require Setoid.
Record Setoid: Type :=
{ car:Type;
eq:car->car->Prop;
refl: reflexive _ eq;
sym: symmetric _ eq;
trans: transitive _ eq
}.
Add Relation car eq
reflexivity proved by refl
symmetry proved by symm
transitivity proved by trans
as eq_rel.
Record Morphism (S1 S2:Setoid): Type :=
{ f:car S1 ->car S2;
compat: forall (x1 x2: car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2)
}.
Add Morphism f with signature eq ==> eq as apply_mor.
Proof.
intros S1 S2 m.
apply (compat S1 S2 m).
Qed.
Lemma test: forall (S1 S2:Setoid) (m: Morphism S1 S2)
(x y: car S1), eq S1 x y -> eq S2 (f _ _ m x) (f _ _ m y).
Proof.
intros.
rewrite H.
reflexivity.
Qed.
The following tactics, all prefixed by setoid_, deal with arbitrary registered relations and morphisms. Moreover, all the corresponding unprefixed tactics (i.e. reflexivity, symmetry, transitivity, replace, rewrite) have been extended to fall back to their prefixed counterparts when the relation involved is not Leibniz equality. Notice, however, that using the prefixed tactics it is possible to pass additional arguments such as generate side conditions or using relation.
setoid_reflexivity
setoid_symmetry [in ident]
setoid_transitivity
setoid_rewrite [orientation] term
[in ident]
[generate side conditions term1 …termn]
The generate side conditions argument cannot be passed to the unprefixed form.
setoid_replace term with term [in ident]
[using relation term]
[generate side conditions term1 …termn]
[by tactic]
The generate side conditions and using relation arguments cannot be passed to the unprefixed form. The latter argument tells the tactic what parametric relation should be used to replace the first tactic argument with the second one. If omitted, it defaults to Leibniz equality.
Every derived tactic that is based on the unprefixed forms of the tactics considered above will also work up to user defined relations. For instance, it is possible to register hints for autorewrite that are not proof of Leibniz equalities. In particular it is possible to exploit autorewrite to simulate normalization in a term rewriting system up to user defined equalities.
The Print Setoids command shows the list of currently registered parametric relations and morphisms. For each morphism its signature is also given. When the rewriting tactics refuse to replace a term in a context because the latter is not a composition of morphisms, the Print Setoids command is useful to understand what additional morphisms should be registered.
Due to backward compatibility reasons, the following syntax for the declaration of setoids and morphisms is also accepted.
Add Setoid A Aeq ST as ident
where Aeq is a congruence relation without parameters,
A is its carrier and ST is an object of type
(Setoid_Theory A Aeq) (i.e. a record packing together the reflexivity,
symmetry and transitivity lemmas). Notice that the syntax is not completely
backward compatible since the identifier was not required.
Add Morphism f : ident.
Proof.
…
Qed.
The latter command is restricted to the declaration of morphisms without parameters. It is not fully backward compatible since the property the user is asked to prove is slightly different: for n-ary morphisms the hypotheses of the property are permuted; moreover, when the morphism returns a proposition, the property is now stated using a bi-implication in place of a simple implication. In practice, porting an old development to the new semantics is usually quite simple.
Notice that several limitations of the old implementation have been lifted. In particular, it is now possible to declare several relations with the same carrier and several signatures for the same morphism. Moreover, it is now also possible to declare several morphisms having the same signature. Finally, the replace and rewrite tactics can be used to replace terms in contexts that were refused by the old implementation.