Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade
Last active May 18, 2023 19:18
Show Gist options
  • Save Blaisorblade/429ecf0ebe814d3e17d2ed0e797a150a to your computer and use it in GitHub Desktop.
Save Blaisorblade/429ecf0ebe814d3e17d2ed0e797a150a to your computer and use it in GitHub Desktop.
A sketch of Iris-internal setoid rewriting
(** 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment