Library Coq.Classes.Morphisms





Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.
Require Import Coq.Relations.Relation_Definitions.
Require Export Coq.Classes.RelationClasses.

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.

Class Morphism {A} (R : relation A) (m : A) : Prop :=
  respect : R m m.

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.

Definition respectful {A B : Type}
  (R : relation A) (R' : relation B) : relation (A -> B) :=
  Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R').

Notations reminiscent of the old syntax for declaring morphisms.

Delimit Scope signature_scope with signature.

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.


Open Local Scope signature_scope.

Dependent pointwise lifting of a relation on the range.

Definition forall_relation {A : Type} {B : A -> Type} (sig : Π a : A, relation (B a)) : relation (Π x : A, B x) :=
  λ f g, Π a : A, sig a (f a) (g a).


Non-dependent pointwise lifting

Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) :=
  Eval compute in forall_relation (B:=λ _, B) (λ _, R).

Lemma pointwise_pointwise A B (R : relation B) :
  relation_equivalence (pointwise_relation A R) (@eq A ==> R).

We can build a PER on the Coq function space if we have PERs on the domain and codomain.

Hint Unfold Reflexive : core.
Hint Unfold Symmetric : core.
Hint Unfold Transitive : core.

Typeclasses Opaque respectful pointwise_relation forall_relation.

Program Instance respectful_per `(PER A (R : relation A), PER B (R' : relation B)) :
  PER (R ==> R').

  Next Obligation.


Subrelations induce a morphism on the identity.

Instance subrelation_id_morphism `(subrelation A R₁ R₂) : Morphism (R₁ ==> R₂) id.

The subrelation property goes through products as usual.

Instance morphisms_subrelation_respectful `(subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂) :
  subrelation (R₁ ==> S₁) (R₂ ==> S₂).

And of course it is reflexive.

Instance morphisms_subrelation_refl : ! subrelation A R R | 10.

Morphism is itself a covariant morphism for subrelation.

Lemma subrelation_morphism `(mor : Morphism A R₁ m, unc : Unconvertible (relation A) R₁ R₂,
  sub : subrelation A R₁ R₂) : Morphism R₂ m.


Instance morphism_subrelation_morphism :
  Morphism (subrelation ++> @eq _ ==> impl) (@Morphism A).

We use an external tactic to manage the application of subrelation, which is otherwise always applicable. We allow its use only once per branch.

Inductive subrelation_done : Prop := did_subrelation : subrelation_done.

Inductive normalization_done : Prop := did_normalization.

Ltac subrelation_tac :=
  match goal with
    | [ _ : subrelation_done |- _ ] => fail 1
    | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
      set(H:=did_subrelation) ; eapply @subrelation_morphism
  end.

Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.

Essential subrelation instances for iff, impl and pointwise_relation.
The complement of a relation conserves its morphisms.

Program Instance complement_morphism
  `(mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R) :
  Morphism (RA ==> RA ==> iff) (complement R).

  Next Obligation.

The inverse too, actually the flip instance is a bit more general.

Program Instance flip_morphism
  `(mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f) :
  Morphism (RB ==> RA ==> RC) (flip f).

  Next Obligation.

Every Transitive relation gives rise to a binary morphism on impl, contravariant in the first argument, covariant in the second.

Program Instance trans_contra_co_morphism
  `(Transitive A R) : Morphism (R --> R ++> impl) R.

  Next Obligation.

Morphism declarations for partial applications.

Program Instance trans_contra_inv_impl_morphism
  `(Transitive A R) : Morphism (R --> inverse impl) (R x) | 3.

  Next Obligation.

Program Instance trans_co_impl_morphism
  `(Transitive A R) : Morphism (R ==> impl) (R x) | 3.

  Next Obligation.

Program Instance trans_sym_co_inv_impl_morphism
  `(PER A R) : Morphism (R ==> inverse impl) (R x) | 2.

  Next Obligation.


Program Instance trans_sym_contra_impl_morphism
  `(PER A R) : Morphism (R --> impl) (R x) | 2.

  Next Obligation.


Program Instance per_partial_app_morphism
  `(PER A R) : Morphism (R ==> iff) (R x) | 1.

  Next Obligation.


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.

Program Instance trans_co_eq_inv_impl_morphism
  `(Transitive A R) : Morphism (R ==> (@eq A) ==> inverse impl) R | 2.

  Next Obligation.

Every Symmetric and Transitive relation gives rise to an equivariant morphism.

Program Instance PER_morphism `(PER A R) : Morphism (R ==> R ==> iff) R | 1.

  Next Obligation.



Lemma symmetric_equiv_inverse `(Symmetric A R) : relation_equivalence R (flip R).

Program Instance compose_morphism A B C R₀ R₁ R₂ :
  Morphism ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C).

  Next Obligation.


Coq functions are morphisms for leibniz equality, applied only if really needed.

Instance reflexive_eq_dom_reflexive (A : Type) `(Reflexive B R') :
  Reflexive (@Logic.eq A ==> R').

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.

Class MorphismProxy {A} (R : relation A) (m : A) : Prop :=
  respect_proxy : R m m.

Instance reflexive_morphism_proxy
  `(Reflexive A R) (x : A) : MorphismProxy R x | 1.

Instance morphism_morphism_proxy
  `(Morphism A R x) : MorphismProxy R x | 2.

R is Reflexive, hence we can build the needed proof.

Lemma Reflexive_partial_app_morphism `(Morphism (A -> B) (R ==> R') m, MorphismProxy A R x) :
   Morphism R' (m x).

Class Params {A : Type} (of : A) (arity : nat).

Class PartialApplication.

Ltac partial_application_tactic :=
  let rec do_partial_apps H m :=
    match m with
      | ?m' ?x => eapply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H]
      | _ => idtac
    end
  in
  let rec do_partial H ar m :=
    match ar with
      | 0 => do_partial_apps H m
      | S ?n' =>
        match m with
          ?m' ?x => do_partial H n' m'
        end
    end
  in
  let on_morphism m :=
    let m' := fresh in head_of_constr m' m ;
    let n := fresh in evar (n:nat) ;
    let v := eval compute in n in clear n ;
    let H := fresh in
      assert(H:Params m' v) by typeclasses eauto ;
      let v' := eval compute in v in
      do_partial H v' m
 in
  match goal with
    | [ _ : subrelation_done |- _ ] => fail 1
    | [ _ : normalization_done |- _ ] => fail 1
    | [ _ : @Params _ _ _ |- _ ] => fail 1
    | [ |- @Morphism ?T _ (?m ?x) ] =>
      match goal with
        | [ _ : PartialApplication |- _ ] =>
          eapply @Reflexive_partial_app_morphism
        | _ =>
          on_morphism (m x) ||
            (eapply @Reflexive_partial_app_morphism ;
              [ pose Build_PartialApplication | idtac ])
      end
  end.

Section PartialAppTest.
  Instance and_ar : Params and 0.

  Goal Morphism (iff) (and True True).

  Goal Morphism (iff) (or True True).

  Goal Morphism (iff ==> iff) (iff True).

End PartialAppTest.

Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.

Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
  relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R').

Special-purpose class to do normalization of signatures w.r.t. inverse.

Class Normalizes (A : Type) (m : relation A) (m' : relation A) : Prop :=
  normalizes : relation_equivalence m m'.

Current strategy: add inverse everywhere and reduce using subrelation afterwards.

Lemma inverse_atom A R : Normalizes A R (inverse (inverse R)).

Lemma inverse_arrow `(NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R'')) :
  Normalizes (A -> B) (R ==> R') (inverse (R''' ==> R'')%signature).



Ltac inverse :=
  match goal with
    | [ |- Normalizes _ (respectful _ _) _ ] => eapply @inverse_arrow
    | _ => eapply @inverse_atom
  end.

Hint Extern 1 (Normalizes _ _ _) => inverse : typeclass_instances.

Treating inverse: can't make them direct instances as we need at least a flip present in the goal.

Lemma inverse1 `(subrelation A R' R) : subrelation (inverse (inverse R')) R.

Lemma inverse2 `(subrelation A R R') : subrelation R (inverse (inverse R')).

Hint Extern 1 (subrelation (flip _) _) => eapply @inverse1 : typeclass_instances.
Hint Extern 1 (subrelation _ (flip _)) => eapply @inverse2 : typeclass_instances.

Once we have normalized, we will apply this instance to simplify the problem.

Definition morphism_inverse_morphism `(mor : Morphism A R m) : Morphism (inverse R) m := mor.

Hint Extern 2 (@Morphism _ (flip _) _) => eapply @morphism_inverse_morphism : typeclass_instances.

Bootstrap !!!

Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A).

Lemma morphism_releq_morphism `(Normalizes A R R', Morphism _ R' m) : Morphism R m.

Ltac morphism_normalization :=
  match goal with
    | [ _ : subrelation_done |- _ ] => fail 1
    | [ _ : normalization_done |- _ ] => fail 1
    | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
      set(H:=did_normalization) ; eapply @morphism_releq_morphism
  end.

Hint Extern 6 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.

Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables.

Lemma reflexive_morphism `{Reflexive A R} (x : A)
   : Morphism R x.

Ltac morphism_reflexive :=
  match goal with
    | [ _ : normalization_done |- _ ] => fail 1
    | [ _ : subrelation_done |- _ ] => fail 1
    | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism
  end.

Hint Extern 7 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.