When should ==> be used over ++> for morphisms?

Using Rocq
1

I’m trying to understand why the notation R ==> S has the same definition as R ++> S.

I would naively expect it to have a definition like (fun x y => R x y \/ R y x) ++> S, since according to the documentation:

The special arrow ==> is used in signatures for morphisms that are both covariant and contravariant.

I understand that for symmetric relations the distinction doesn’t matter. But for relations that are not symmetric, I believe it does.

When/why would one use ==> over ++>?

Here’s a development to illustrate what my question:

From Stdlib Require Import Setoid Morphisms.

(* Simple pre-order (implication on truth values). *)
Inductive P : Set := F | T.
Inductive R : P -> P -> Prop :=
| RFF : R F F
| RFT : R F T
| RTT : R T T
.
Lemma R_refl : reflexive P R.
Proof. intros [|]; auto using R. Qed.
Lemma R_not_sym : ~ (symmetric P R).
Proof. intro H; specialize (H F T RFT); inversion H. Qed.
Lemma R_trans : transitive P R.
Proof. intros [|] [|] [|]; auto using R. Qed.

(* Register the relation. *)
Add Relation P R
  reflexivity proved by R_refl
  transitivity proved by R_trans
  as pr.

(* Simple co- and contra-variant morphism (constant function). *)
Definition f (_ : P) : P := F.

Section fails.

  (* Register the morphism as co- and contra-variant. *)
  Add Morphism f with signature R ==> R as fm.
  (* But somehow only prove the co-variant part. *)
  Proof. intros; exact RFF. Qed.

  (* Co-variance works as expected. *)
  Goal forall x y, R x y -> R (f x) (f y).
  Proof. intros x y H; rewrite H; reflexivity. Qed.

  (* Contra-variance does not work (as expected?). *)
  Goal forall x y, R y x -> R (f x) (f y).
  Proof.
    intros x y H.
    (* Not sure how to read the error (if it expects symmetry or a missing morphism). *)
    Fail rewrite H.
  Abort.

End fails.

Section works.

  (* Register the morphism as co- and then contra-variant. *)
  Add Morphism f with signature R ++> R as fmp.
  Proof. intros; exact RFF. Qed.
  Add Morphism f with signature R --> R as fmn.
  Proof. intros; exact RFF. Qed.

  (* Co-variance still works as expected. *)
  Goal forall x y, R x y -> R (f x) (f y).
  Proof. intros x y H; rewrite H; reflexivity. Qed.

  (* Contra-variance now also works as expected. *)
  Goal forall x y, R y x -> R (f x) (f y).
  Proof. intros x y H; rewrite H; reflexivity. Qed.

End works.

Section naive.

  (* Define ==> as being both co- and contra-variant. *)
  Definition or_flip {T} (R : relation T) : relation T := fun x y => R x y \/ R y x.
  Notation "R ==> S" := (respectful (or_flip R) S) : signature_scope.

  (* Prove the morphism is both co- and contra-variant. *)
  Lemma m : Proper (R ==> R) f.
  Proof. intros x y _; exact RFF. Qed.

  (* Co-variance works using the left side of [or_flip]. *)
  Goal forall x y, R x y -> R (f x) (f y).
  Proof. intros x y H; apply m; left; exact H. Qed.

  (* Contra-variance works using the right side of [or_flip]. *)
  Goal forall x y, R y x -> R (f x) (f y).
  Proof. intros x y H; apply m; right; exact H. Qed.

End naive.
2

Actually, it’s possible to register the morphism a single time and still achieve both co- and contra-variance (this solution thus scales with the number of parameters to the morphism), by registering R and flip R as sub-relations of or_flip R. This is however twice slower to rewrite as registering the morphism twice.

Section works2.

  (* Define ==> as being both co- and contra-variant. *)
  Definition or_flip {T} (R : relation T) : relation T := fun x y => R x y \/ R y x.
  Notation "R ==> S" := (respectful (or_flip R) S) : signature_scope.

  (* Register R and flip R as subrelations of (or_flip R). *)
  Instance sub_or_flip {A} (R : relation A) : subrelation R (or_flip R).
  Proof. intros x y H; left; exact H. Qed.
  Instance sub_flip_or_flip {A} (R : relation A) : subrelation (flip R) (or_flip R).
  Proof. intros x y H; right; exact H. Qed.

  (* Register the morphism as co- and contra-variant. *)
  Add Morphism f with signature R ==> R as fm.
  Proof. intros; exact RFF. Qed.

  (* Co-variance works. *)
  Goal forall x y, R x y -> R (f x) (f y).
  Proof. intros x y H; rewrite H; reflexivity. Qed.

  (* Contra-variance works. *)
  Goal forall x y, R y x -> R (f x) (f y).
  Proof. intros x y H; rewrite H; reflexivity. Qed.

Reset works2.

(Note that all sections were supposed to be closed by Reset instead of End in the initial post, but I can’t edit it. This doesn’t change the results.)