Last active
May 18, 2023 19:18
-
-
Save Blaisorblade/429ecf0ebe814d3e17d2ed0e797a150a to your computer and use it in GitHub Desktop.
A sketch of Iris-internal setoid rewriting
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** 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