Library Coq.Classes.Morphisms
Morphisms.
We now turn to the definition of
Morphism and declare standard instances.
These will be used by the
setoid_rewrite tactic later.
A morphism on a relation R is an object respecting the relation (in its kernel).
The relation R will be instantiated by respectful and A by an arrow type
for usual morphisms.
Respectful morphisms.
The fully dependent version, not used yet.
Definition respectful_hetero
(
A B :
Type)
(
C :
A ->
Type) (
D :
B ->
Type)
(
R :
A ->
B ->
Prop)
(
R' :
forall (
x :
A) (
y :
B),
C x ->
D y ->
Prop) :
(
forall x :
A,
C x) -> (
forall x :
B,
D x) ->
Prop :=
fun f g =>
forall x y,
R x y ->
R' x y (
f x) (
g y).
The non-dependent version is an instance where we forget dependencies.
Notations reminiscent of the old syntax for declaring morphisms.
Delimit Scope signature_scope with signature.
Module MorphismNotations.
Notation " R ++> R' " := (@
respectful _ _ (
R%signature) (
R'%signature))
(
right associativity,
at level 55) :
signature_scope.
Notation " R ==> R' " := (@
respectful _ _ (
R%signature) (
R'%signature))
(
right associativity,
at level 55) :
signature_scope.
Notation " R --> R' " := (@
respectful _ _ (
inverse (
R%signature)) (
R'%signature))
(
right associativity,
at level 55) :
signature_scope.
End MorphismNotations.
Export MorphismNotations.
Open Local Scope signature_scope.
Dependent pointwise lifting of a relation on the range.
Non-dependent pointwise lifting
We can build a PER on the Coq function space if we have PERs on the domain and
codomain.
Subrelations induce a morphism on the identity.
The subrelation property goes through products as usual.
And of course it is reflexive.
Morphism is itself a covariant morphism for subrelation.
We use an external tactic to manage the application of subrelation, which is otherwise
always applicable. We allow its use only once per branch.
Essential subrelation instances for iff, impl and pointwise_relation.
The complement of a relation conserves its morphisms.
The inverse too, actually the flip instance is a bit more general.
Every Transitive relation gives rise to a binary morphism on impl,
contravariant in the first argument, covariant in the second.
Morphism declarations for partial applications.
Every Transitive relation induces a morphism by "pushing" an R x y on the left of an R x z proof
to get an R y z goal.
Every Symmetric and Transitive relation gives rise to an equivariant morphism.
Coq functions are morphisms for leibniz equality,
applied only if really needed.
respectful is a morphism for relation equivalence.
Every element in the carrier of a reflexive relation is a morphism for this relation.
We use a proxy class for this case which is used internally to discharge reflexivity constraints.
The Reflexive instance will almost always be used, but it won't apply in general to any kind of
Morphism (A -> B) _ _ goal, making proof-search much slower. A cleaner solution would be to be able
to set different priorities in different hint bases and select a particular hint database for
resolution of a type class constraint.
R is Reflexive, hence we can build the needed proof.
Special-purpose class to do normalization of signatures w.r.t. inverse.
Current strategy: add inverse everywhere and reduce using subrelation
afterwards.
Treating inverse: can't make them direct instances as we
need at least a flip present in the goal.
Once we have normalized, we will apply this instance to simplify the problem.
Bootstrap !!!
Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables.