Library Coq.Classes.Morphisms

Typeclass-based morphism definition and standard, minimal instances

Author: Matthieu Sozeau Institution: LRI, CNRS UMR 8623 - University Paris Sud

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

Local Obligation Tactic := simpl_relation.

Morphisms.

We now turn to the definition of Proper and declare standard instances. These will be used by the setoid_rewrite tactic later.

A morphism for a relation R is a proper element of the relation. The relation R will be instantiated by respectful and A by an arrow type for usual morphisms.

Class Proper {A} (R : relation A) (m : A) : Prop :=
proper_prf : 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.

Module ProperNotations.

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

Export ProperNotations.

Local Open Scope signature_scope.

solve_proper try to solve the goal Proper (?==> ... ==>?) f by repeated introductions and setoid rewrites. It should work fine when f is a combination of already known morphisms and quantifiers.

Ltac solve_respectful t :=
match goal with
   | |- respectful _ _ _ _ =>
     let H := fresh "H" in
     intros ? ? H; solve_respectful ltac:(setoid_rewrite H; t)
   | _ => t; reflexivity
end.

Ltac solve_proper := unfold Proper; solve_respectful ltac:(idtac).

f_equiv is a clone of f_equal that handles setoid equivalences. For example, if we know that f is a morphism for E1==>E2==>E, then the goal E (f x y) (f x´ y´) will be transformed by f_equiv into the subgoals E1 x x´ and E2 y y´.

Ltac f_equiv :=
match goal with
  | |- ?R (?f ?x) (?f´ _) =>
    let T := type of x in
    let Rx := fresh "R" in
    evar (Rx : relation T);
    let H := fresh in
    assert (H : (Rx==>R)%signature f f´);
    unfold Rx in *; clear Rx; [ f_equiv | apply H; clear H; try reflexivity ]
  | |- ?R ?f ?f´ =>
    try reflexivity;
    change (Proper R f); eauto with typeclass_instances; fail
  | _ => idtac
end.

forall_def reifies the dependent product as a definition.

Definition forall_def {A : Type} (B : A -> Type) : Type := forall x : A, B x.

Dependent pointwise lifting of a relation on the range.

Definition forall_relation {A : Type} {B : A -> Type}
(sig : forall a, relation (B a)) : relation (forall x, B x) :=
fun f g => forall 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:=fun _ => B) (fun _ => 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, PER B R´) : PER (R ==> R´).

Subrelations induce a morphism on the identity.

Instance subrelation_id_proper `(subrelation A R₁ R₂) : Proper (R₁ ==> R₂) id.

The subrelation property goes through products as usual.

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

And of course it is reflexive.

Lemma subrelation_refl A R : @subrelation A R R.

Ltac subrelation_tac T U :=
(is_ground T ; is_ground U ; class_apply @subrelation_refl) ||
class_apply @subrelation_respectful || class_apply @subrelation_refl.

Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances.

Proper is itself a covariant morphism for subrelation.

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

CoInductive apply_subrelation : Prop := do_subrelation.

Ltac proper_subrelation :=
  match goal with
    [ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper
  end.

Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.

Instance proper_subrelation_proper :
  Proper (subrelation ++> eq ==> impl) (@Proper A).

Essential subrelation instances for iff, impl and pointwise_relation.

Instance iff_impl_subrelation : subrelation iff impl | 2.

Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl) | 2.

Instance pointwise_subrelation {A} `(sub : subrelation B R R´) :
subrelation (pointwise_relation A R) (pointwise_relation A R´) | 4.

For dependent function types.

Lemma forall_subrelation A (B : A -> Type) (R S : forall x : A, relation (B x)) :
(forall a, subrelation (R a) (S a)) -> subrelation (forall_relation R) (forall_relation S).

We use an extern hint to help unification.

Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) =>
apply (@forall_subrelation A B R S) ; intro : typeclass_instances.

Any symmetric relation is equal to its inverse.

Lemma subrelation_symmetric A R `(Symmetric A R) : subrelation (inverse R) R.

Hint Extern 4 (subrelation (inverse _) _) =>
class_apply @subrelation_symmetric : typeclass_instances.

The complement of a relation conserves its proper elements.

Program Definition complement_proper
  `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
  Proper (RA ==> RA ==> iff) (complement R) := _.

Hint Extern 1 (Proper _ (complement _)) =>
  apply @complement_proper : typeclass_instances.

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

Program Definition flip_proper
  `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
  Proper (RB ==> RA ==> RC) (flip f) := _.

Hint Extern 1 (Proper _ (flip _)) =>
  apply @flip_proper : typeclass_instances.

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) : Proper (R --> R ++> impl) R.

Proper declarations for partial applications.

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

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

Program Instance trans_sym_co_inv_impl_morphism
  `(PER A R) : Proper (R ++> inverse impl) (R x) | 3.

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

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

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) : Proper (R ==> (@eq A) ==> inverse impl) R | 2.

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

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

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

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

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.

Instance respectful_morphism :
Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B).

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 Proper (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 ProperProxy {A} (R : relation A) (m : A) : Prop :=
proper_proxy : R m m.

Lemma eq_proper_proxy A (x : A) : ProperProxy (@eq A) x.

Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x.

Lemma proper_proper_proxy `(Proper A R x) : ProperProxy R x.

Hint Extern 1 (ProperProxy _ _) =>
class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances.

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

Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R´) m, ProperProxy A R x) :
   Proper R´ (m x).

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

Class PartialApplication.

CoInductive normalization_done : Prop := did_normalization.

Ltac partial_application_tactic :=
  let rec do_partial_apps H m cont :=
    match m with
      | ?m´ ?x => class_apply @Reflexive_partial_app_morphism ;
        [(do_partial_apps H m´ ltac:idtac)|clear H]
      | _ => cont
    end
  in
  let rec do_partial H ar m :=
    match ar with
      | 0%nat => do_partial_apps H m ltac:(fail 1)
      | S ?n´ =>
        match m with
          ?m´ ?x => do_partial H n´ m´
        end
    end
  in
  let params m sk fk :=
    (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 subst m´;
            (sk H v´ || fail 1))
    || fk
  in
  let on_morphism m cont :=
    params m ltac:(fun H n => do_partial H n m)
      ltac:(cont)
  in
  match goal with
    | [ _ : normalization_done |- _ ] => fail 1
    | [ _ : @Params _ _ _ |- _ ] => fail 1
    | [ |- @Proper ?T _ (?m ?x) ] =>
      match goal with
        | [ H : PartialApplication |- _ ] =>
          class_apply @Reflexive_partial_app_morphism; [|clear H]
        | _ => on_morphism (m x)
          ltac:(class_apply @Reflexive_partial_app_morphism)
      end
  end.

Hint Extern 4 (@Proper _ _ _) => 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 _ _) _ ] => class_apply @inverse_arrow
    | _ => class_apply @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 _) _) => class_apply @inverse1 : typeclass_instances.
Hint Extern 1 (subrelation _ (flip _)) => class_apply @inverse2 : typeclass_instances.

That's if and only if

Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R.

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

Definition proper_inverse_proper `(mor : Proper A R m) : Proper (inverse R) m := mor.

Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_inverse_proper : typeclass_instances.

Bootstrap !!!

Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).

Lemma proper_normalizes_proper `(Normalizes A R0 R1, Proper A R1 m) : Proper R0 m.

Ltac proper_normalization :=
  match goal with
    | [ _ : normalization_done |- _ ] => fail 1
    | [ _ : apply_subrelation |- @Proper _ ?R _ ] => let H := fresh "H" in
      set(H:=did_normalization) ; class_apply @proper_normalizes_proper
  end.

Hint Extern 6 (@Proper _ _ _) => proper_normalization : typeclass_instances.

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

Lemma reflexive_proper `{Reflexive A R} (x : A)
   : Proper R x.

Lemma proper_eq A (x : A) : Proper (@eq A) x.

Ltac proper_reflexive :=
  match goal with
    | [ _ : normalization_done |- _ ] => fail 1
    | _ => class_apply proper_eq || class_apply @reflexive_proper
  end.

Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances.

When the relation on the domain is symmetric, we can inverse the relation on the codomain. Same for binary functions.

Lemma proper_sym_flip :
forall `(Symmetric A R1)`(Proper (A->B) (R1 ==>R2) f),
Proper (R1 ==>inverse R2) f.

Lemma proper_sym_flip_2 :
forall `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1 ==>R2 ==>R3) f),
Proper (R1 ==>R2 ==>inverse R3) f.

When the relation on the domain is symmetric, a predicate is compatible with iff as soon as it is compatible with impl. Same with a binary relation.

Lemma proper_sym_impl_iff : forall `(Symmetric A R)`(Proper _ (R ==>impl) f),
Proper (R ==>iff) f.

Lemma proper_sym_impl_iff_2 :
forall `(Symmetric A R)`(Symmetric B R´)`(Proper _ (R ==>R´==>impl) f),
Proper (R ==>R´==>iff) f.

A PartialOrder is compatible with its underlying equivalence.

Instance PartialOrder_proper `(PartialOrder A eqA R) :
Proper (eqA ==>eqA ==>iff) R.

From a PartialOrder to the corresponding StrictOrder: lt = le /\ ~eq. If the order is total, we could also say gt = ~le.

Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) :
StrictOrder (relation_conjunction R (complement eqA)).

Hint Extern 4 (StrictOrder (relation_conjunction _ _)) =>
class_apply PartialOrder_StrictOrder : typeclass_instances.

From a StrictOrder to the corresponding PartialOrder: le = lt \/ eq. If the order is total, we could also say ge = ~lt.

Lemma StrictOrder_PreOrder
`(Equivalence A eqA, StrictOrder A R, Proper _ (eqA ==>eqA ==>iff) R) :
PreOrder (relation_disjunction R eqA).

Hint Extern 4 (PreOrder (relation_disjunction _ _)) =>
  class_apply StrictOrder_PreOrder : typeclass_instances.

Lemma StrictOrder_PartialOrder
  `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA ==>eqA ==>iff) R) :
  PartialOrder eqA (relation_disjunction R eqA).

Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) =>
  class_apply StrictOrder_PartialOrder : typeclass_instances.