A sketch of Iris-internal setoid rewriting

iris_setoid_rewrite.v

(** Iris-internal setoid rewriting, theory. *)
Require Import iris.proofmode.proofmode.

(** * Notation for functions in the Iris scope. To upstream,
per https://gitlab.mpi-sws.org/iris/iris/-/issues/320. *)
Notation "'λI' x .. y , t" := (fun x => .. (fun y => t%I) ..)
  (at level 200, x binder, y binder, right associativity,
  only parsing) : function_scope.

Section with_prop.
  Context {PROP : bi}.
  Definition irelation (A : Type) := A -> A -> PROP.
  Definition iiff : irelation PROP := λI P Q, □ (P ∗-∗ Q).

  (* respectful *)
  Definition irespectful {A B : Type} (R : irelation A) (S : irelation B) (f g : A → B) : PROP :=
    ∀ x y : A, R x y -∗ S (f x) (g y).

  (* Proper *)
  Definition IProper {A : Type} (R : irelation A) (f : A) : Prop := ⊢ R f f.
End with_prop.

Locate "_ ==> _".
Print Notation "_ ==> _".
Reserved Notation "R '=I=>' S" (right associativity, at level 55, S at level 55).
Print Notation "_ '=I=>' _".
Notation "R '=I=>' S" := (irespectful R S).

Existing Class IProper.
Section with_prop.
  Context {PROP : bi}.

  #[global] Instance bi_sep_iproper : IProper (PROP := PROP) (iiff =I=> iiff =I=> iiff) bi_sep.
  Proof.
    rewrite /IProper /irespectful /iiff.
    iIntros "%A1 %A2 #HA %B1 %B2 #HB !>" .
    iSplit; iIntros "[P Q]";
      (iSplitL "HA P"; [ iApply ("HA" with "P") | iApply ("HB" with "Q") ]).
  Qed.


  #[global] Instance bi_wand_iproper : IProper (PROP := PROP) (iiff =I=> iiff =I=> iiff) bi_wand.
  Proof.
    rewrite /IProper /irespectful /iiff.
    iIntros "%A1 %A2 #HA %B1 %B2 #HB !>" .
    iSplit; iIntros "W A"; iApply ("HB" with "(W (HA A))").
  Qed.
End with_prop.