# Chapter 25 User defined equalities and relations

- 25.1 Relations and morphisms
- 25.2 Adding new relations and morphisms
- 25.3 Rewriting and non reflexive relations
- 25.4 Rewriting and non symmetric relations
- 25.5 Rewriting in ambiguous setoid contexts
- 25.6 First class setoids and morphisms
- 25.7 Tactics enabled on user provided relations
- 25.8 Printing relations and morphisms
- 25.9 Deprecated syntax and backward incompatibilities
- 25.10 Rewriting under binders
- 25.11 Sub-relations
- 25.12 Constant unfolding

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).

This documentation is adapted from the previous setoid documentation by
Claudio Sacerdoti Coen (based on previous work by Clément Renard).
The new implementation is a drop-in replacement for the old one ^{1}, hence most of the documentation still applies.

The work is a complete rewrite of the previous implementation, based on the type class infrastructure. It also improves on and generalizes the previous implementation in several ways:

- User-extensible algorithm. The algorithm is separated in two parts: generations of the rewriting constraints (done in ML) and solving of these constraints using type class resolution. As type class resolution is extensible using tactics, this allows users to define general ways to solve morphism constraints.
- Sub-relations. An example extension to the base algorithm is the ability to define one relation as a subrelation of another so that morphism declarations on one relation can be used automatically for the other. This is done purely using tactics and type class search.
- Rewriting under binders. It is possible to rewrite under binders in the new implementation, if one provides the proper morphisms. Again, most of the work is handled in the tactics.
- First-class morphisms and signatures. Signatures and morphisms are ordinary Coq terms, hence they can be manipulated inside Coq, put inside structures and lemmas about them can be proved inside the system. Higher-order morphisms are also allowed.
- Performance. The implementation is based on a depth-first search for the first solution to a set of constraints which can be as fast as linear in the size of the term, and the size of the proof term is linear in the size of the original term. Besides, the extensibility allows the user to customize the proof-search if necessary.

## 25.1 Relations and morphisms

A parametric *relation* `R` is any term of type
`forall (`*x*_{1}`:`*T*_{1}`) …(`*x*_{n}`:`*T*_{n}`), relation `` A`. The
expression

*A*, which depends on

*x*

_{1}…

*x*

_{n}, is called the

*carrier*of the relation and

`R`is said to be a relation over

`A`; the list

*x*

_{1},…,

*x*

_{n}is the (possibly empty) list of parameters of the relation.

**Example 1**

**(Parametric relation)**

*It is possible to implement finite sets of elements of type*

`A`*as unordered list of elements of type*

`A`*. The function*

`set_eq: forall (A: Type), relation (list A)`*satisfied by two lists with the same elements is a parametric relation over*

`(list A)`*with one parameter*

`A`*. The type of*

`set_eq`*is convertible with*

`forall (A: Type), list A -> list A -> Prop`*.*

An *instance* of a parametric relation `R` with *n* parameters
is any term `(R `*t*_{1}` …`*t*_{n}`)`.

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 (`*x*_{1}`:`*T*_{1}`) …(`*x*_{n}`:`*T*_{n}`),
reflexive (R `*x*_{1}` …`*x*_{n}`)`. Similar definitions are given for
parametric proofs of symmetry and transitivity.

**Example 2**

**(Parametric relation (cont.))**

*The*

`set_eq`*relation of the previous example can be proved to be reflexive, symmetric and transitive.*

A parametric unary function *f* of type
`forall (`*x*_{1}`:`*T*_{1}`) …(`*x*_{n}`:`*T*_{n}`), `*A*_{1}` -> `*A*_{2}
covariantly respects two parametric relation instances *R*_{1} and *R*_{2} if,
whenever *x*, *y* satisfy *R*_{1} *x* *y*, their images (*f* *x*) and (*f* *y*)
satisfy *R*_{2} (*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 *R*_{1} and *R*_{2}.
The sequence *x*_{1},… *x*_{n} represents the parameters of the morphism.

Let *R*_{1} and *R*_{2} be two parametric relations.
The *signature* of a parametric morphism of type
`forall (`*x*_{1}`:`*T*_{1}`) …(`*x*_{n}`:`*T*_{n}`), `*A*_{1}` -> `*A*_{2} that
covariantly respects two instances *I*_{R1} and *I*_{R2} of *R*_{1} and *R*_{2} is written *I*_{R1} `++>` *I*_{R2}.
Notice that the special arrow `++>`, which reminds the reader
of covariance, is placed between the two relation instances, not
between the two carriers. The signature relation instances and morphism will
be typed in a context introducing variables for the parameters.

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} (`inverse R` in Coq) 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 `*t*_{1}` …`*t*_{n}.

**Example 3**

**(Morphisms)**

*Continuing the previous example, let*

`union: forall (A: Type), list A -> list A -> list A`*perform the union of two sets by appending one list to the other.*

`union`*is a binary morphism parametric over*

`A`*that respects the relation instance*

`(set_eq A)`*. The latter condition is proved by showing*

`forall (A: Type) (S1 S1’ S2 S2’: list A), set_eq A S1 S1’ -> set_eq A S2 S2’ -> set_eq A (union A S1 S2) (union A S1’ S2’)`*.*

*The signature of the function *`union A`* is
*`set_eq A ==> set_eq A ==> set_eq A`* for all *`A`*.
*

**Example 4**

**(Contravariant morphism)**

*The division function*

`Rdiv: R -> R -> R`*is a morphism of signature*

`le ++> le --> le`*where*

`le`*is the usual order relation over real numbers. Notice that division is covariant in its first argument and contravariant in its second argument.*

Leibniz equality is a relation and 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. 25.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.

**Example 5**

**(Rewriting)**

*Continuing the previous examples, suppose that the user must prove*

`set_eq int (union int (union int S1 S2) S2) (f S1 S2)`*under the hypothesis*

`H: set_eq int S2 (nil int)`*. It is possible to use the*

`rewrite`*tactic to replace the first two occurrences of*

`S2`*with*

`nil int`*in the goal since the context*

`set_eq int (union int (union int S1 nil) nil) (f S1 S2)`*, being a composition of morphisms instances, is a morphism. However the tactic will fail replacing the third occurrence of*

`S2`*unless*

`f`*has also been declared as a morphism.*

## 25.2 Adding new relations and morphisms

A parametric relation
*Aeq*`: forall (`*y*_{1}` : β`_{!}` …`*y*_{m}` : β`_{m}`), relation (A `*t*_{1}` …`*t*_{n}`)` over
*(A : **α*_{i}* -> …**α*_{n}* -> *`Type`)
can be declared with the following command:

Add Parametric Relation(x_{1}:T_{1}) …(x_{n}:T_{k}) :(At_{1}…t_{n}) (Aeqt′_{1}…t′_{m})

[reflexivity proved byrefl]

[symmetry proved bysym]

[transitivity proved bytrans]

asid.

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 the carrier and relation parameters may refer to the context
of variables introduced at the beginning of the declaration, but the
instances need not be made only of variables.
Also notice that *A* is *not* required to be a term
having the same parameters as *Aeq*, although that is often the
case in practice (this departs from the previous implementation).

In case the carrier and relations are not parametric, one can use the
command `Add Relation` instead, whose syntax is the same except
there is no local context.

The proofs of reflexivity, symmetry and transitivity can be omitted if the
relation is not an equivalence relation. The proofs must be instances of the
corresponding relation definitions: e.g. the proof of reflexivity must
have a type convertible to `reflexive (A `*t*_{1}` …`*t*_{n}`) (Aeq `*t*′_{1}` …`*t*′_{n}`)`. Each proof may refer to the introduced variables as well.

**Example 6**

**(Parametric relation)**

*For Leibniz equality, we may declare:*

`Add Parametric Relation (A : Type) :`

`A (@eq A)`

*[*

`reflexivity proved by`

`@refl_equal A`

*]*

…

…

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 Parametric Morphism(x_{1}:T_{!}) …(x_{k}:T_{k})

(ft_{1}…t_{n})

with signaturesig

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 as the base name of the type class instance definition
and as the name of the lemma that proves the well-definedness of the morphism.
The parameters of the morphism as well as the signature may refer to the
context of variables.
The command asks the user to prove interactively that *f* respects
the relations identified from the signature.

**Example 7**

*We start the example by assuming a small theory over homogeneous sets and we declare set equality as a parametric equivalence relation and union of two sets as a parametric morphism.*

`Coq`

`<`

`Require Export Setoid.`

`Coq`

`<`

`Require Export Relation_Definitions.`

`Coq`

`<`

`Set Implicit Arguments.`

`Coq`

`<`

`Parameter set: Type -`

`>`

`Type.`

`Coq`

`<`

`Parameter empty: forall A, set A.`

`Coq`

`<`

`Parameter eq_set: forall A, set A -`

`>`

`set A -`

`>`

`Prop.`

`Coq`

`<`

`Parameter union: forall A, set A -`

`>`

`set A -`

`>`

`set A.`

`Coq`

`<`

`Axiom eq_set_refl: forall A, reflexive _ (eq_set (A:=A)).`

`Coq`

`<`

`Axiom eq_set_sym: forall A, symmetric _ (eq_set (A:=A)).`

`Coq`

`<`

`Axiom eq_set_trans: forall A, transitive _ (eq_set (A:=A)).`

`Coq`

`<`

`Axiom empty_neutral: forall A (S: set A), eq_set (union S (empty A)) S.`

`Coq`

`<`

`Axiom union_compat:`

`Coq`

`<`

`forall (A : Type),`

`Coq`

`<`

`forall x x’ : set A, eq_set x x’ -`

`>`

`Coq`

`<`

`forall y y’ : set A, eq_set y y’ -`

`>`

`Coq`

`<`

`eq_set (union x y) (union x’ y’).`

`Coq`

`<`

`Add Parametric Relation A : (set A) (@eq_set A)`

`Coq`

`<`

`reflexivity proved by (eq_set_refl (A:=A))`

`Coq`

`<`

`symmetry proved by (eq_set_sym (A:=A))`

`Coq`

`<`

`transitivity proved by (eq_set_trans (A:=A))`

`Coq`

`<`

`as eq_set_rel.`

`Coq`

`<`

`Add Parametric Morphism A : (@union A) with`

`Coq`

`<`

`signature (@eq_set A) ==`

`>`

`(@eq_set A) ==`

`>`

`(@eq_set A) as union_mor.`

`Coq`

`<`

`Proof. exact (@union_compat A). Qed.`

Is is possible to reduce the burden of specifying parameters using
(maximally inserted) implicit arguments. If `A` is always set as
maximally implicit in the previous example, one can write:

`Coq`

`<`

`Add Parametric Relation A : (set A) eq_set`

`Coq`

`<`

`reflexivity proved by eq_set_refl`

`Coq`

`<`

`symmetry proved by eq_set_sym`

`Coq`

`<`

`transitivity proved by eq_set_trans`

`Coq`

`<`

`as eq_set_rel.`

`Coq`

`<`

`Add Parametric Morphism A : (@union A) with`

`Coq`

`<`

`signature eq_set ==`

`>`

`eq_set ==`

`>`

`eq_set as union_mor.`

`Coq`

`<`

`Proof. exact (@union_compat A). 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.

`Coq`

`<`

`Goal forall (S: set nat),`

`Coq`

`<`

`eq_set (union (union S empty) S) (union S S).`

`Coq`

`<`

`Proof. intros. rewrite empty_neutral. reflexivity. Qed.`

The tables of relations and morphisms are managed by the type class
instance mechanism. The behavior on section close is to generalize
the instances by the variables of the section (and possibly hypotheses
used in the proofs of instance declarations) but not to export them in
the rest of the development for proof search. One can use the
`Existing Instance` command to do so outside the section,
using the name of the declared morphism suffixed by `_Morphism`,
or use the `Global` modifier for the corresponding class instance
declaration (see §25.6) at definition time.
When loading a compiled file or importing a module,
all the declarations of this module will be loaded.

## 25.3 Rewriting and non reflexive relations

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.

**Example 8**

*To replace*

`(union S empty)`*with*

`S`*in*

`(union (union S empty) S) (union S S)`*the rewrite tactic must exploit the monotony of*

`union`*(axiom*

`union_compat`*in the previous example). Applying*

`union_compat`*by hand we are left with the goal*

`eq_set (union S S) (union S S)`*.*

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.

**Example 9**

*Let*

`eqO`*be*

`fun x y => x = y`

`∧`

`x`

`≠`

`0`*(the smaller PER over non zero elements). Division can be declared as a morphism of signature*

`eq ==> eq0 ==> eq`*. Replace*

`x`*with*

`y`*in*

`div x n = div y n`*opens the additional goal*

`eq0 n n`*that is equivalent to*

`n=n`

`∧`

`n`

`≠`

`0`*.*

## 25.4 Rewriting and non symmetric relations

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.

**Example 10**

**(Covariance and contravariance)**

*Suppose that division over real numbers has been defined as a morphism of signature*

`Zdiv: Zlt ++> Zlt --> Zlt`*(i.e.*

`Zdiv`*is increasing in its first argument, but decreasing on the second one). Let*

`<`*denotes*

`Zlt`*. Under the hypothesis*

`H: x < y`*we have*

`k < x / y -> k < x / x`*, but not*

`k < y / x -> k < x / x`*. Dually, under the same hypothesis*

`k < x / y -> k < y / y`*holds, but*

`k < y / x -> k < y / y`*does not. Thus, if the current goal is*

`k < x / x`*, it is possible to replace only the second occurrence of*

`x`*(in contravariant position) with*

`y`*since the obtained goal must imply the current one. On the contrary, if*

`k < x / x`*is an hypothesis, it is possible to replace only the first occurrence of*

`x`*(in covariant position) with*

`y`*since the current hypothesis must imply the obtained one.*

Contrary to the previous implementation, no specific error message will
be raised when trying to replace a term that occurs in the wrong
position. It will only fail because the rewriting constraints are not
satisfiable. However it is possible to use the `at` modifier to
specify which occurrences should be rewritten.

As expected, composing morphisms together propagates the variance annotations by switching the variance every time a contravariant position is traversed.

**Example 11**

*Let us continue the previous example and let us consider the goal*

`x / (x / x) < k`*. The first and third occurrences of*

`x`*are in a contravariant position, while the second one is in covariant position. More in detail, the second occurrence of*

`x`*occurs covariantly in*

`(x / x)`*(since division is covariant in its first argument), and thus contravariantly in*

`x / (x / x)`*(since division is contravariant in its second argument), and finally covariantly in*

`x / (x / x) < k`*(since*

`<`*, as every transitive relation, is contravariant in its first argument with respect to the relation itself).*

## 25.5 Rewriting in ambiguous setoid contexts

One function can respect several different relations and thus it can be declared as a morphism having multiple signatures.

**Example 12**

*Union over homogeneous lists can be given all the following signatures:*

`eq ==> eq ==> eq`*(*

`eq`*being the equality over ordered lists)*

`set_eq ==> set_eq ==> set_eq`*(*

`set_eq`*being the equality over unordered lists up to duplicates),*

`multiset_eq ==> multiset_eq ==> multiset_eq`*(*

`multiset_eq`*being the equality over unordered lists).*

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. Contrary to the previous implementation, the
tactic will always choose the first possible solution to the set of
constraints generated by a rewrite and will not try to find *all*
possible solutions to warn the user about.

## 25.6 First class setoids and morphisms

The implementation is based on a first-class representation of properties of relations and morphisms as type classes. That is, the various combinations of properties on relations and morphisms are represented as records and instances of theses classes are put in a hint database. For example, the declaration:

Add Parametric Relation(x_{1}:T_{1}) …(x_{n}:T_{k}) :(At_{1}…t_{n}) (Aeqt′_{1}…t′_{m})

[reflexivity proved byrefl]

[symmetry proved bysym]

[transitivity proved bytrans]

asid.

is equivalent to an instance declaration:

Instance(x_{1}:T_{1}) …(x_{n}:T_{k})=>id:@Equivalence(At_{1}…t_{n}) (Aeqt′_{1}…t′_{m}):=

[Equivalence_Reflexive :=refl]

[Equivalence_Symmetric :=sym]

[Equivalence_Transitive :=trans].

The declaration itself amounts to the definition of an object of the
record type `Coq.Classes.RelationClasses.Equivalence` and a
hint added to the `typeclass_instances` hint database.
Morphism declarations are also instances of a type class defined in
`Classes.Morphisms`.
See the documentation on type classes 18 and
the theories files in `Classes` for further explanations.

One can inform the rewrite tactic about morphisms and relations just by
using the typeclass mechanism to declare them using `Instance`
and `Context` vernacular commands.
Any object of type `Proper` (the type of morphism declarations)
in the local context will also be automatically used by the rewriting
tactic to solve constraints.

Other representations of first class setoids and morphisms can also be handled by encoding them as records. In the following example, the projections of the setoid relation and of the morphism function can be registered as parametric relations and morphisms.

**Example 13**

**(First class setoids)**

`Coq`

`<`

`Require Import Relation_Definitions Setoid.`

`Coq`

`<`

`Record Setoid: Type :=`

`Coq`

`<`

`{ car:Type;`

`Coq`

`<`

`eq:car-`

`>`

`car-`

`>`

`Prop;`

`Coq`

`<`

`refl: reflexive _ eq;`

`Coq`

`<`

`sym: symmetric _ eq;`

`Coq`

`<`

`trans: transitive _ eq`

`Coq`

`<`

`}.`

`Coq`

`<`

`Add Parametric Relation (s : Setoid) : (@car s) (@eq s)`

`Coq`

`<`

`reflexivity proved by (refl s)`

`Coq`

`<`

`symmetry proved by (sym s)`

`Coq`

`<`

`transitivity proved by (trans s) as eq_rel.`

`Coq`

`<`

`Record Morphism (S1 S2:Setoid): Type :=`

`Coq`

`<`

`{ f:car S1 -`

`>`

`car S2;`

`Coq`

`<`

`compat: forall (x1 x2: car S1), eq S1 x1 x2 -`

`>`

`eq S2 (f x1) (f x2) }.`

`Coq`

`<`

`Add Parametric Morphism (S1 S2 : Setoid) (M : Morphism S1 S2) :`

`Coq`

`<`

`(@f S1 S2 M) with signature (@eq S1 ==`

`>`

`@eq S2) as apply_mor.`

`Coq`

`<`

`Proof. apply (compat S1 S2 M). Qed.`

`Coq`

`<`

`Lemma test: forall (S1 S2:Setoid) (m: Morphism S1 S2)`

`Coq`

`<`

`(x y: car S1), eq S1 x y -`

`>`

`eq S2 (f _ _ m x) (f _ _ m y).`

`Coq`

`<`

`Proof. intros. rewrite H. reflexivity. Qed.`

## 25.7 Tactics enabled on user provided relations

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
`using relation`.

`setoid_rewrite` *[**orientation**]* *term*
*[*`at` *occs**]* *[*`in` *ident**]*

`setoid_replace` *term* `with` *term*
*[*`in` *ident**]*
*[*`using relation` *term**]*
*[*`by` *tactic**]*

The `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 the `DefaultRelation` instance on the type of the objects.
By default, it means the most recent `Equivalence` instance in
the environment, but it can be customized by declaring new
`DefaultRelation` instances. As Leibniz equality is a declared
equivalence, it will fall back to it if no other relation is declared on
a given type.

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.

## 25.8 Printing relations and morphisms

The `Print Instances` command can be used to show the list of
currently registered `Reflexive` (using `Print Instances Reflexive`),
`Symmetric` or `Transitive` relations,
`Equivalence`s, `PreOrder`s, `PER`s, and
Morphisms (implemented as `Proper` instances). When
the rewriting tactics refuse to replace a term in a context
because the latter is not a composition of morphisms, the `Print Instances`
commands can be useful to understand what additional morphisms should be
registered.

## 25.9 Deprecated syntax and backward incompatibilities

Due to backward compatibility reasons, the following syntax for the declaration of setoids and morphisms is also accepted.

Add SetoidA Aeq STasident

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 Morphismf:ident.

Proof.

…

Qed.

The latter command also 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. As discussed in
the next section, the semantics of the new `setoid_rewrite`
command differs slightly from the old one and `rewrite`.

## 25.10 Rewriting under binders

**Warning**: Due to compatibility issues, this feature is enabled only when calling
the `setoid_rewrite` tactics directly and not `rewrite`.

To be able to rewrite under binding constructs, one must declare
morphisms with respect to pointwise (setoid) equivalence of functions.
Example of such morphisms are the standard `all` and `ex`
combinators for universal and existential quantification respectively.
They are declared as morphisms in the `Classes.Morphisms_Prop`
module. For example, to declare that universal quantification is a
morphism for logical equivalence:

`Coq`

`<`

`Instance all_iff_morphism (A : Type) :`

`Coq`

`<`

`Proper (pointwise_relation A iff ==`

`>`

`iff) (@all A).`

*1 subgoal*

*A : Type*

*============================*

*Proper (pointwise_relation A iff ==*

*>*

*iff) all*`Coq`

`<`

`Proof. simpl_relation.`

*1 subgoal*

*A : Type*

*x : A -*

*>*

*Prop*

*y : A -*

*>*

*Prop*

*H : pointwise_relation A iff x y*

*============================*

*all x*

*<*

*-*

*>*

*all y*One then has to show that if two predicates are equivalent at every
point, their universal quantifications are equivalent. Once we have
declared such a morphism, it will be used by the setoid rewriting tactic
each time we try to rewrite under an `all` application (products
in Prop are implicitly translated to such applications).

Indeed, when rewriting under a lambda, binding variable *x*, say from
*P* *x* to *Q* *x* using the relation `iff`, the tactic will generate
a proof of `pointwise_relation A iff (fun x => P x) (fun x => Q
x)` from the proof of `iff (P x) (Q x)` and a constraint of the
form `Proper (pointwise_relation A iff ==> ?) m` will be
generated for the surrounding morphism `m`.

Hence, one can add higher-order combinators as morphisms by providing
signatures using pointwise extension for the relations on the functional
arguments (or whatever subrelation of the pointwise extension).
For example, one could declare the `map` combinator on lists as
a morphism:

`Coq`

`<`

`Instance map_morphism ‘{Equivalence A eqA, Equivalence B eqB} :`

`Coq`

`<`

`Proper ((eqA ==`

`>`

`eqB) ==`

`>`

`list_equiv eqA ==`

`>`

`list_equiv eqB)`

`Coq`

`<`

`(@map A B).`

where `list_equiv` implements an equivalence on lists
parameterized by an equivalence on the elements.

Note that when one does rewriting with a lemma under a binder
using `setoid_rewrite`, the application of the lemma may capture
the bound variable, as the semantics are different from rewrite where
the lemma is first matched on the whole term. With the new
`setoid_rewrite`, matching is done on each subterm separately
and in its local environment, and all matches are rewritten
*simultaneously* by default. The semantics of the previous
`setoid_rewrite` implementation can almost be recovered using
the `at 1` modifier.

## 25.11 Sub-relations

Sub-relations can be used to specify that one relation is included in
another, so that morphisms signatures for one can be used for the other.
If a signature mentions a relation *R* on the left of an arrow
`==>`, then the signature also applies for any relation *S* that
is smaller than *R*, and the inverse applies on the right of an arrow.
One can then declare only a few morphisms instances that generate the complete set
of signatures for a particular constant. By default, the only declared
subrelation is `iff`, which is a subrelation of `impl`
and `inverse impl` (the dual of implication). That’s why we can
declare only two morphisms for conjunction:
`Proper (impl ==> impl ==> impl) and` and
`Proper (iff ==> iff ==> iff) and`. This is sufficient to satisfy
any rewriting constraints arising from a rewrite using `iff`,
`impl` or `inverse impl` through `and`.

Sub-relations are implemented in `Classes.Morphisms` and are a
prime example of a mostly user-space extension of the algorithm.

## 25.12 Constant unfolding

The resolution tactic is based on type classes and hence regards user-defined
constants as transparent by default. This may slow down the resolution
due to a lot of unifications (all the declared `Proper`
instances are tried at each node of the search tree).
To speed it up, declare your constant as rigid for proof search
using the command `Typeclasses Opaque` (see §18.6.5).

- 1
- Nicolas Tabareau helped with the gluing