Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • iris/iris
  • jeehoon.kang/iris-coq
  • amintimany/iris-coq
  • dfrumin/iris-coq
  • Villetaneuse/iris
  • gares/iris
  • shiatsumat/iris
  • Blaisorblade/iris
  • jihgfee/iris-coq
  • mrhaandi/iris
  • tlsomers/iris
  • Quarkbeast/iris-coq
  • janno/iris
  • amaurremi/iris-coq
  • proux/iris
  • tchajed/iris
  • herbelin/iris-coq
  • msammler/iris-coq
  • maximedenes/iris-coq
  • bpeters/iris
  • haidang/iris
  • lepigre/iris
  • lczch/iris
  • simonspies/iris
  • gpirlea/iris
  • dkhalanskiyjb/iris
  • gmalecha/iris
  • germanD/iris
  • aa755/iris
  • jules/iris
  • abeln/iris
  • simonfv/iris
  • atrieu/iris
  • arthuraa/iris
  • simonh/iris
  • jung/iris
  • mattam82/iris
  • Armael/iris
  • adamAndMath/iris
  • gmevel/iris
  • snyke7/iris
  • johannes/iris
  • NiklasM/iris
  • simonspies/iris-parametric-index
  • svancollem/iris
  • proux1/iris
  • wmansky/iris
  • LukeXuan/iris
  • ivanbakel/iris
  • SkySkimmer/iris
  • tjhance/iris
  • yiyunliu/iris
  • Lee-Janggun/iris
  • thomas-lamiaux/iris
  • dongjae/iris
  • dnezam/iris
  • Tragicus/iris
  • clef-men/iris
  • ffengyu/iris
59 results
Show changes
Commits on Source (23)
...@@ -47,6 +47,7 @@ Coq 8.13 is no longer supported. ...@@ -47,6 +47,7 @@ Coq 8.13 is no longer supported.
* Add hints for `a ≼ a ⋅ _` / `a ≼ _ ⋅ a` / `ε ≼ _` / `_ ≼ CsumBot` / * Add hints for `a ≼ a ⋅ _` / `a ≼ _ ⋅ a` / `ε ≼ _` / `_ ≼ CsumBot` /
`_ ≼ ExclBot` with cost 0, which means they are used by `done` to finish `_ ≼ ExclBot` with cost 0, which means they are used by `done` to finish
proofs. (by Ike Mulder) proofs. (by Ike Mulder)
* Rename `singleton_mono` to `singleton_included_mono`.
**Changes in `bi`:** **Changes in `bi`:**
...@@ -105,6 +106,10 @@ Coq 8.13 is no longer supported. ...@@ -105,6 +106,10 @@ Coq 8.13 is no longer supported.
* Add `∗-∗` as notation in `stdpp_scope` similar to `-∗`. This means `P ∗-∗ Q` * Add `∗-∗` as notation in `stdpp_scope` similar to `-∗`. This means `P ∗-∗ Q`
can be directly used as lemma statement, and is syntactic sugar for `⊢ P ∗-∗ Q`. can be directly used as lemma statement, and is syntactic sugar for `⊢ P ∗-∗ Q`.
* Add `≼` connective (`internal_included`) on the BI level. (by Ike Mulder) * Add `≼` connective (`internal_included`) on the BI level. (by Ike Mulder)
* Move laws of persistence modality out of `BiMixin` into `BiPersistentlyMixin`.
* Provide smart constructor `bi_persistently_mixin_discrete` for
`BiPersistentlyMixin`: Given a discrete BI that enjoys the existential
property, a trivial definition of the persistence modality can be given.
**Changes in `proofmode`:** **Changes in `proofmode`:**
......
...@@ -210,10 +210,6 @@ theories/base_logic/lib is for constructions in the base logic (using own) ...@@ -210,10 +210,6 @@ theories/base_logic/lib is for constructions in the base logic (using own)
* `list_lookup_insert` is named by context (the type involved), then the two functions outside-in on the left-hand-side, so it has the type `lookup (insert …) = …` where the `insert` is on a list. Notations mean it doesn’t actually look like this and the insert is textually first. * `list_lookup_insert` is named by context (the type involved), then the two functions outside-in on the left-hand-side, so it has the type `lookup (insert …) = …` where the `insert` is on a list. Notations mean it doesn’t actually look like this and the insert is textually first.
* Injectivity theorems are instances of `Inj` and then are used with `inj` * Injectivity theorems are instances of `Inj` and then are used with `inj`
* Suffixes `_l` and `_r` when we have binary `op x y` and a theorem related to the left or right. For example, `sep_mono_l` says bi_sep is monotonic in its left argument (holding the right constant). * Suffixes `_l` and `_r` when we have binary `op x y` and a theorem related to the left or right. For example, `sep_mono_l` says bi_sep is monotonic in its left argument (holding the right constant).
* Entailments at the top level are typically written `P -* Q`, which is notation
for `P ⊢ Q`. If you have a theorem which has no premises you have to write ⊢ P
explicitly (for example, it is common to have `⊢ |==> ∃ γ, …` for an allocation
theorem)
* Suffix `'` (prime) is used when `foo'` is a corollary of `foo`. Try to avoid * Suffix `'` (prime) is used when `foo'` is a corollary of `foo`. Try to avoid
these since the name doesn't convey how `foo'` is related to `foo`. these since the name doesn't convey how `foo'` is related to `foo`.
* Given a polymorphic function/relation `f` (e.g., `eq`, `equiv`, `subseteq`), the instance of type `A` is called `A_f_instance`, and we add a lemma `A_f` that characterizes the instance. In case of many instances, this lemma is proved by unfolding the definition of the instance, e.g., `frac_op`, `frac_valid`. However, in some cases, e.g., `list_eq`, `map_eq`, `set_eq` this lemma might require non-trivial proof work. * Given a polymorphic function/relation `f` (e.g., `eq`, `equiv`, `subseteq`), the instance of type `A` is called `A_f_instance`, and we add a lemma `A_f` that characterizes the instance. In case of many instances, this lemma is proved by unfolding the definition of the instance, e.g., `frac_op`, `frac_valid`. However, in some cases, e.g., `list_eq`, `map_eq`, `set_eq` this lemma might require non-trivial proof work.
...@@ -224,6 +220,7 @@ theories/base_logic/lib is for constructions in the base logic (using own) ...@@ -224,6 +220,7 @@ theories/base_logic/lib is for constructions in the base logic (using own)
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P) M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
``` ```
* Monotonicity lemmas where the relation can be ambiguous are called `<f>_<relation>_mono`, e.g. `Some_included_mono`.
### Naming algebra libraries ### Naming algebra libraries
......
...@@ -369,7 +369,7 @@ Qed. ...@@ -369,7 +369,7 @@ Qed.
Lemma singleton_included_total `{!CmraTotal A} i x y : Lemma singleton_included_total `{!CmraTotal A} i x y :
{[ i := x ]} ({[ i := y ]} : gmap K A) x y. {[ i := x ]} ({[ i := y ]} : gmap K A) x y.
Proof. rewrite singleton_included Some_included_total. done. Qed. Proof. rewrite singleton_included Some_included_total. done. Qed.
Lemma singleton_mono i x y : Lemma singleton_included_mono i x y :
x y {[ i := x ]} ({[ i := y ]} : gmap K A). x y {[ i := x ]} ({[ i := y ]} : gmap K A).
Proof. intros Hincl. apply singleton_included, Some_included_mono. done. Qed. Proof. intros Hincl. apply singleton_included, Some_included_mono. done. Qed.
......
...@@ -860,6 +860,10 @@ Section product. ...@@ -860,6 +860,10 @@ Section product.
Global Instance prod_ofe_discrete : Global Instance prod_ofe_discrete :
OfeDiscrete A OfeDiscrete B OfeDiscrete prodO. OfeDiscrete A OfeDiscrete B OfeDiscrete prodO.
Proof. intros ?? [??]; apply _. Qed. Proof. intros ?? [??]; apply _. Qed.
Lemma pair_dist n (a1 a2 : A) (b1 b2 : B) :
(a1, b1) {n} (a2, b2) a1 {n} a2 b1 {n} b2.
Proof. reflexivity. Qed.
End product. End product.
Global Arguments prodO : clear implicits. Global Arguments prodO : clear implicits.
......
...@@ -13,8 +13,7 @@ Local Existing Instance entails_po. ...@@ -13,8 +13,7 @@ Local Existing Instance entails_po.
Lemma uPred_bi_mixin (M : ucmra) : Lemma uPred_bi_mixin (M : ucmra) :
BiMixin BiMixin
uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
(@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand.
uPred_persistently.
Proof. Proof.
split. split.
- exact: entails_po. - exact: entails_po.
...@@ -27,7 +26,6 @@ Proof. ...@@ -27,7 +26,6 @@ Proof.
- exact: exist_ne. - exact: exist_ne.
- exact: sep_ne. - exact: sep_ne.
- exact: wand_ne. - exact: wand_ne.
- exact: persistently_ne.
- exact: pure_intro. - exact: pure_intro.
- exact: pure_elim'. - exact: pure_elim'.
- exact: and_elim_l. - exact: and_elim_l.
...@@ -49,6 +47,15 @@ Proof. ...@@ -49,6 +47,15 @@ Proof.
- exact: sep_assoc'. - exact: sep_assoc'.
- exact: wand_intro_r. - exact: wand_intro_r.
- exact: wand_elim_l'. - exact: wand_elim_l'.
Qed.
Lemma uPred_bi_persistently_mixin (M : ucmra) :
BiPersistentlyMixin
uPred_entails uPred_emp uPred_and
(@uPred_exist M) uPred_sep uPred_persistently.
Proof.
split.
- exact: persistently_ne.
- exact: persistently_mono. - exact: persistently_mono.
- exact: persistently_idemp_2. - exact: persistently_idemp_2.
- (* emp ⊢ <pers> emp (ADMISSIBLE) *) - (* emp ⊢ <pers> emp (ADMISSIBLE) *)
...@@ -96,7 +103,8 @@ Qed. ...@@ -96,7 +103,8 @@ Qed.
Canonical Structure uPredI (M : ucmra) : bi := Canonical Structure uPredI (M : ucmra) : bi :=
{| bi_ofe_mixin := ofe_mixin_of (uPred M); {| bi_ofe_mixin := ofe_mixin_of (uPred M);
bi_bi_mixin := uPred_bi_mixin M; bi_bi_mixin := uPred_bi_mixin M;
bi_bi_later_mixin := uPred_bi_later_mixin M |}. bi_bi_later_mixin := uPred_bi_later_mixin M;
bi_bi_persistently_mixin := uPred_bi_persistently_mixin M |}.
Lemma uPred_internal_eq_mixin M : BiInternalEqMixin (uPredI M) (@uPred_internal_eq M). Lemma uPred_internal_eq_mixin M : BiInternalEqMixin (uPredI M) (@uPred_internal_eq M).
Proof. Proof.
......
...@@ -132,20 +132,42 @@ Qed. ...@@ -132,20 +132,42 @@ Qed.
(** * [fupd] soundness lemmas *) (** * [fupd] soundness lemmas *)
(** "Unfolding" soundness stamement for no-LC fupd:
This exposes that when initializing the [invGS_gen], we can provide
a general lemma that lets one unfold a [|={E1, E2}=> P] into a basic update
while also carrying around some frame [ω E] that tracks the current mask.
We also provide a bunch of later credits for consistency,
but there is no way to use them since this is a [HasNoLc] lemma. *)
Lemma fupd_soundness_no_lc_unfold `{!invGpreS Σ} m E :
|==> `(Hws: invGS_gen HasNoLc Σ) (ω : coPset iProp Σ),
£ m ω E ( E1 E2 P, (|={E1, E2}=> P) -∗ ω E1 ==∗ (ω E2 P)).
Proof.
iMod wsat_alloc as (Hw) "[Hw HE]".
(* We don't actually want any credits, but we need the [lcGS]. *)
iMod (later_credits.le_upd.lc_alloc m) as (Hc) "[_ Hlc]".
set (Hi := InvG HasNoLc _ Hw Hc).
iExists Hi, (λ E, wsat ownE E)%I.
rewrite (union_difference_L E ); [|set_solver].
rewrite ownE_op; [|set_solver].
iDestruct "HE" as "[HE _]". iFrame.
iIntros "!>!>" (E1 E2 P) "HP HwE".
rewrite fancy_updates.uPred_fupd_unseal
/fancy_updates.uPred_fupd_def -assoc /=.
by iApply ("HP" with "HwE").
Qed.
(** Note: the [_no_lc] soundness lemmas also allow generating later credits, but (** Note: the [_no_lc] soundness lemmas also allow generating later credits, but
these cannot be used for anything. They are merely provided to enable making these cannot be used for anything. They are merely provided to enable making
the adequacy proof generic in whether later credits are used. *) the adequacy proof generic in whether later credits are used. *)
Lemma fupd_soundness_no_lc `{!invGpreS Σ} E1 E2 (P : iProp Σ) `{!Plain P} m : Lemma fupd_soundness_no_lc `{!invGpreS Σ} E1 E2 (P : iProp Σ) `{!Plain P} m :
( `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={E1,E2}=∗ P) P. ( `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={E1,E2}=∗ P) P.
Proof. Proof.
iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hw) "[Hw HE]". iIntros (Hfupd).
(* We don't actually want any credits, but we need the [lcGS]. *) apply later_soundness, bupd_soundness; [by apply later_plain|].
iMod (later_credits.le_upd.lc_alloc m) as (Hc) "[_ Hc]". iMod fupd_soundness_no_lc_unfold as (hws ω) "(Hlc & Hω & #H)".
set (Hi := InvG HasNoLc _ Hw Hc). iMod ("H" with "[Hlc] Hω") as "H'".
iAssert (|={,E2}=> P)%I with "[Hc]" as "H". { iMod (Hfupd with "Hlc") as "H'". iModIntro. iApply "H'". }
{ iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd; last done. } iDestruct "H'" as "[>H1 >H2]". by iFrame.
rewrite uPred_fupd_unseal /uPred_fupd_def.
iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
Qed. Qed.
Lemma fupd_soundness_lc `{!invGpreS Σ} n E1 E2 (P : iProp Σ) `{!Plain P} : Lemma fupd_soundness_lc `{!invGpreS Σ} n E1 E2 (P : iProp Σ) `{!Plain P} :
......
...@@ -19,7 +19,6 @@ Section bi_mixin. ...@@ -19,7 +19,6 @@ Section bi_mixin.
Context (bi_exist : A, (A PROP) PROP). Context (bi_exist : A, (A PROP) PROP).
Context (bi_sep : PROP PROP PROP). Context (bi_sep : PROP PROP PROP).
Context (bi_wand : PROP PROP PROP). Context (bi_wand : PROP PROP PROP).
Context (bi_persistently : PROP PROP).
Bind Scope bi_scope with PROP. Bind Scope bi_scope with PROP.
Local Infix "⊢" := bi_entails. Local Infix "⊢" := bi_entails.
...@@ -36,7 +35,6 @@ Section bi_mixin. ...@@ -36,7 +35,6 @@ Section bi_mixin.
(bi_exist _ (λ x, .. (bi_exist _ (λ y, P%I)) ..)) : bi_scope. (bi_exist _ (λ x, .. (bi_exist _ (λ y, P%I)) ..)) : bi_scope.
Local Infix "∗" := bi_sep : bi_scope. Local Infix "∗" := bi_sep : bi_scope.
Local Infix "-∗" := bi_wand : bi_scope. Local Infix "-∗" := bi_wand : bi_scope.
Local Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
(** * Axioms for a general BI (logic of bunched implications) *) (** * Axioms for a general BI (logic of bunched implications) *)
...@@ -64,7 +62,6 @@ Section bi_mixin. ...@@ -64,7 +62,6 @@ Section bi_mixin.
Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A); Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A);
bi_mixin_sep_ne : NonExpansive2 bi_sep; bi_mixin_sep_ne : NonExpansive2 bi_sep;
bi_mixin_wand_ne : NonExpansive2 bi_wand; bi_mixin_wand_ne : NonExpansive2 bi_wand;
bi_mixin_persistently_ne : NonExpansive bi_persistently;
(** Higher-order logic *) (** Higher-order logic *)
bi_mixin_pure_intro (φ : Prop) P : φ P φ ; bi_mixin_pure_intro (φ : Prop) P : φ P φ ;
...@@ -95,8 +92,40 @@ Section bi_mixin. ...@@ -95,8 +92,40 @@ Section bi_mixin.
bi_mixin_sep_assoc' P Q R : (P Q) R P (Q R); bi_mixin_sep_assoc' P Q R : (P Q) R P (Q R);
bi_mixin_wand_intro_r P Q R : (P Q R) P Q -∗ R; bi_mixin_wand_intro_r P Q R : (P Q R) P Q -∗ R;
bi_mixin_wand_elim_l' P Q R : (P Q -∗ R) P Q R; bi_mixin_wand_elim_l' P Q R : (P Q -∗ R) P Q R;
}.
(** We require any BI to have a persistence modality that carves out the
intuitionistic fragment of the separation logic. For logics such as Iris,
the persistence modality has a non-trivial definition (involving the [core] of
the camera). It is not clear whether a trivial definition exists: while
[<pers> P := False] comes close, it does not satisfy [later_persistently_1].
However, for some simpler discrete BIs the persistence modality
can be defined as:
<pers> P := ⌜ emp ⊢ P ⌝
That is, [P] holds persistently if it holds without resources.
The nesting of the entailment below the pure embedding ⌜ ⌝ only works for
discrete BIs: Non-expansiveness of [<pers>] relies on [dist] ignoring the
step-index.
To prove the rule [<pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> Ψ a] the BI furthermore
needs to satisfy the "existential property": [emp ⊢ ∃ x, Φ x] implies
[∃ x, emp ⊢ Φ x].
This construction is formalized by the smart constructor
[bi_persistently_mixin_discrete] for [BiPersistentlyMixin]. See
[tests/heapprop] and [tests/heapprop_affine] for examples of how to use this
smart constructor. *)
Context (bi_persistently : PROP PROP).
Local Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
Record BiPersistentlyMixin := {
bi_mixin_persistently_ne : NonExpansive bi_persistently;
(** Persistently *)
(* In the ordered RA model: Holds without further assumptions. *) (* In the ordered RA model: Holds without further assumptions. *)
bi_mixin_persistently_mono P Q : (P Q) <pers> P <pers> Q; bi_mixin_persistently_mono P Q : (P Q) <pers> P <pers> Q;
(* In the ordered RA model: `core` is idempotent *) (* In the ordered RA model: `core` is idempotent *)
...@@ -121,6 +150,50 @@ Section bi_mixin. ...@@ -121,6 +150,50 @@ Section bi_mixin.
bi_mixin_persistently_and_sep_elim P Q : <pers> P Q P Q; bi_mixin_persistently_and_sep_elim P Q : <pers> P Q P Q;
}. }.
Lemma bi_persistently_mixin_discrete :
( n (P Q : PROP), P {n} Q P Q)
( {A} (Φ : A PROP), (emp x, Φ x) x, emp Φ x)
( P : PROP, (<pers> P)%I = emp P ⌝%I)
BiMixin
BiPersistentlyMixin.
Proof.
intros Hdiscrete Hex Hpers Hbi. pose proof (bi_mixin_entails_po Hbi).
split.
- (* [NonExpansive bi_persistently] *)
intros n P Q [HPQ HQP]%Hdiscrete%(bi_mixin_equiv_entails Hbi).
rewrite !Hpers. apply (bi_mixin_pure_ne Hbi). split=> ?; by etrans.
- (*[(P ⊢ Q) → <pers> P ⊢ <pers> Q] *)
intros P Q HPQ. rewrite !Hpers. apply (bi_mixin_pure_elim' Hbi)=> ?.
apply (bi_mixin_pure_intro Hbi). by trans P.
- (* [<pers> P ⊢ <pers> <pers> P] *)
intros P. rewrite !Hpers. apply (bi_mixin_pure_elim' Hbi)=> ?.
by do 2 apply (bi_mixin_pure_intro Hbi).
- (* [emp ⊢ <pers> emp] *)
rewrite Hpers. by apply (bi_mixin_pure_intro Hbi).
- (* [<pers> P ∧ <pers> Q ⊢ <pers> (P ∧ Q)] *)
intros P Q. rewrite !Hpers.
apply (bi_mixin_impl_elim_l' Hbi). apply (bi_mixin_pure_elim' Hbi)=> ?.
apply (bi_mixin_impl_intro_r Hbi).
etrans; [apply (bi_mixin_and_elim_r Hbi)|].
apply (bi_mixin_pure_elim' Hbi)=> ?.
apply (bi_mixin_pure_intro Hbi). by apply (bi_mixin_and_intro Hbi).
- (* [<pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> Ψ a] *)
intros A Φ. rewrite !Hpers. apply (bi_mixin_pure_elim' Hbi)=> /Hex [x ?].
etrans; [|apply (bi_mixin_exist_intro Hbi x)]; simpl.
rewrite Hpers. by apply (bi_mixin_pure_intro Hbi).
- (* [<pers> P ∗ Q ⊢ <pers> P] *)
intros P Q. rewrite !Hpers.
apply (bi_mixin_wand_elim_l' Hbi). apply (bi_mixin_pure_elim' Hbi)=> ?.
apply (bi_mixin_wand_intro_r Hbi). by apply (bi_mixin_pure_intro Hbi).
- (* [<pers> P ∧ Q ⊢ P ∗ Q] *)
intros P Q. rewrite !Hpers.
apply (bi_mixin_impl_elim_l' Hbi). apply (bi_mixin_pure_elim' Hbi)=> ?.
apply (bi_mixin_impl_intro_r Hbi).
etrans; [apply (bi_mixin_and_elim_r Hbi)|].
etrans; [apply (bi_mixin_emp_sep_1 Hbi)|].
by apply (bi_mixin_sep_mono Hbi).
Qed.
(** We equip any BI with a later modality. This avoids an additional layer in (** We equip any BI with a later modality. This avoids an additional layer in
the BI hierachy and improves performance significantly (see Iris issue #303). the BI hierachy and improves performance significantly (see Iris issue #303).
...@@ -157,7 +230,7 @@ Section bi_mixin. ...@@ -157,7 +230,7 @@ Section bi_mixin.
BiMixin BiLaterMixin. BiMixin BiLaterMixin.
Proof. Proof.
intros Hlater Hbi. pose proof (bi_mixin_entails_po Hbi). intros Hlater Hbi. pose proof (bi_mixin_entails_po Hbi).
split; repeat intro; rewrite ?Hlater ?Hequiv //. split; repeat intro; rewrite ?Hlater //.
- apply (bi_mixin_forall_intro Hbi)=> a. - apply (bi_mixin_forall_intro Hbi)=> a.
etrans; [apply (bi_mixin_forall_elim Hbi a)|]. by rewrite Hlater. etrans; [apply (bi_mixin_forall_elim Hbi a)|]. by rewrite Hlater.
- etrans; [|apply (bi_mixin_or_intro_r Hbi)]. - etrans; [|apply (bi_mixin_or_intro_r Hbi)].
...@@ -194,7 +267,9 @@ Structure bi := Bi { ...@@ -194,7 +267,9 @@ Structure bi := Bi {
bi_ofe_mixin : OfeMixin bi_car; bi_ofe_mixin : OfeMixin bi_car;
bi_cofe_aux : Cofe (Ofe bi_car bi_ofe_mixin); bi_cofe_aux : Cofe (Ofe bi_car bi_ofe_mixin);
bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall
bi_exist bi_sep bi_wand bi_persistently; bi_exist bi_sep bi_wand;
bi_bi_persistently_mixin :
BiPersistentlyMixin bi_entails bi_emp bi_and bi_exist bi_sep bi_persistently;
bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
bi_forall bi_exist bi_sep bi_persistently bi_later; bi_forall bi_exist bi_sep bi_persistently bi_later;
}. }.
...@@ -326,7 +401,7 @@ Proof. eapply bi_mixin_sep_ne, bi_bi_mixin. Qed. ...@@ -326,7 +401,7 @@ Proof. eapply bi_mixin_sep_ne, bi_bi_mixin. Qed.
Global Instance wand_ne : NonExpansive2 (@bi_wand PROP). Global Instance wand_ne : NonExpansive2 (@bi_wand PROP).
Proof. eapply bi_mixin_wand_ne, bi_bi_mixin. Qed. Proof. eapply bi_mixin_wand_ne, bi_bi_mixin. Qed.
Global Instance persistently_ne : NonExpansive (@bi_persistently PROP). Global Instance persistently_ne : NonExpansive (@bi_persistently PROP).
Proof. eapply bi_mixin_persistently_ne, bi_bi_mixin. Qed. Proof. eapply bi_mixin_persistently_ne, bi_bi_persistently_mixin. Qed.
(* Higher-order logic *) (* Higher-order logic *)
Lemma pure_intro (φ : Prop) P : φ P φ ⌝. Lemma pure_intro (φ : Prop) P : φ P φ ⌝.
...@@ -381,24 +456,28 @@ Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed. ...@@ -381,24 +456,28 @@ Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.
(* Persistently *) (* Persistently *)
Lemma persistently_mono P Q : (P Q) <pers> P <pers> Q. Lemma persistently_mono P Q : (P Q) <pers> P <pers> Q.
Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed. Proof. eapply bi_mixin_persistently_mono, bi_bi_persistently_mixin. Qed.
Lemma persistently_idemp_2 P : <pers> P <pers> <pers> P. Lemma persistently_idemp_2 P : <pers> P <pers> <pers> P.
Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed. Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_persistently_mixin. Qed.
Lemma persistently_emp_2 : emp ⊢@{PROP} <pers> emp. Lemma persistently_emp_2 : emp ⊢@{PROP} <pers> emp.
Proof. eapply bi_mixin_persistently_emp_2, bi_bi_mixin. Qed. Proof. eapply bi_mixin_persistently_emp_2, bi_bi_persistently_mixin. Qed.
Lemma persistently_and_2 (P Q : PROP) : Lemma persistently_and_2 (P Q : PROP) :
((<pers> P) (<pers> Q)) <pers> (P Q). ((<pers> P) (<pers> Q)) <pers> (P Q).
Proof. eapply bi_mixin_persistently_and_2, bi_bi_mixin. Qed. Proof. eapply bi_mixin_persistently_and_2, bi_bi_persistently_mixin. Qed.
Lemma persistently_exist_1 {A} (Ψ : A PROP) : Lemma persistently_exist_1 {A} (Ψ : A PROP) :
<pers> ( a, Ψ a) a, <pers> (Ψ a). <pers> ( a, Ψ a) a, <pers> (Ψ a).
Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed. Proof. eapply bi_mixin_persistently_exist_1, bi_bi_persistently_mixin. Qed.
Lemma persistently_absorbing P Q : <pers> P Q <pers> P. Lemma persistently_absorbing P Q : <pers> P Q <pers> P.
Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed. Proof.
eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_persistently_mixin.
Qed.
Lemma persistently_and_sep_elim P Q : <pers> P Q P Q. Lemma persistently_and_sep_elim P Q : <pers> P Q P Q.
Proof. eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_mixin. Qed. Proof.
eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_persistently_mixin.
Qed.
(* Later *) (* Later *)
Global Instance later_ne : NonExpansive (@bi_later PROP). Global Instance later_ne : NonExpansive (@bi_later PROP).
......
...@@ -315,8 +315,7 @@ Section instances. ...@@ -315,8 +315,7 @@ Section instances.
Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP) Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP)
monPred_entails monPred_emp monPred_pure monPred_and monPred_or monPred_entails monPred_emp monPred_pure monPred_and monPred_or
monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand.
monPred_persistently.
Proof. Proof.
split; rewrite ?monPred_defs.monPred_unseal; split; rewrite ?monPred_defs.monPred_unseal;
try by (split=> ? /=; repeat f_equiv). try by (split=> ? /=; repeat f_equiv).
...@@ -354,6 +353,15 @@ Section instances. ...@@ -354,6 +353,15 @@ Section instances.
apply bi.wand_intro_r. by rewrite -HR /= !Hij. apply bi.wand_intro_r. by rewrite -HR /= !Hij.
- intros P Q R [HP]. split=> i. apply bi.wand_elim_l'. - intros P Q R [HP]. split=> i. apply bi.wand_elim_l'.
rewrite HP /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //. rewrite HP /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
Qed.
Lemma monPred_bi_persistently_mixin :
BiPersistentlyMixin (PROP:=monPred I PROP)
monPred_entails monPred_emp monPred_and
monPred_exist monPred_sep monPred_persistently.
Proof.
split; rewrite ?monPred_defs.monPred_unseal;
try by (split=> ? /=; repeat f_equiv).
- intros P Q [?]. split=> i /=. by f_equiv. - intros P Q [?]. split=> i /=. by f_equiv.
- intros P. split=> i. by apply bi.persistently_idemp_2. - intros P. split=> i. by apply bi.persistently_idemp_2.
- split=> i. by apply bi.persistently_emp_intro. - split=> i. by apply bi.persistently_emp_intro.
...@@ -386,7 +394,9 @@ Section instances. ...@@ -386,7 +394,9 @@ Section instances.
Qed. Qed.
Canonical Structure monPredI : bi := Canonical Structure monPredI : bi :=
{| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin; {| bi_ofe_mixin := monPred_ofe_mixin;
bi_bi_mixin := monPred_bi_mixin;
bi_bi_persistently_mixin := monPred_bi_persistently_mixin;
bi_bi_later_mixin := monPred_bi_later_mixin |}. bi_bi_later_mixin := monPred_bi_later_mixin |}.
(** We restate the unsealing lemmas so that they also unfold the BI layer. The (** We restate the unsealing lemmas so that they also unfold the BI layer. The
......
...@@ -20,8 +20,7 @@ Local Existing Instance entails_po. ...@@ -20,8 +20,7 @@ Local Existing Instance entails_po.
Lemma siProp_bi_mixin : Lemma siProp_bi_mixin :
BiMixin BiMixin
siProp_entails siProp_emp siProp_pure siProp_and siProp_or siProp_impl siProp_entails siProp_emp siProp_pure siProp_and siProp_or siProp_impl
(@siProp_forall) (@siProp_exist) siProp_sep siProp_wand (@siProp_forall) (@siProp_exist) siProp_sep siProp_wand.
siProp_persistently.
Proof. Proof.
split. split.
- exact: entails_po. - exact: entails_po.
...@@ -34,7 +33,6 @@ Proof. ...@@ -34,7 +33,6 @@ Proof.
- exact: exist_ne. - exact: exist_ne.
- exact: and_ne. - exact: and_ne.
- exact: impl_ne. - exact: impl_ne.
- solve_proper.
- exact: pure_intro. - exact: pure_intro.
- exact: pure_elim'. - exact: pure_elim'.
- exact: and_elim_l. - exact: and_elim_l.
...@@ -68,6 +66,15 @@ Proof. ...@@ -68,6 +66,15 @@ Proof.
apply impl_intro_r. apply impl_intro_r.
- (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *) - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
apply impl_elim_l'. apply impl_elim_l'.
Qed.
Lemma siProp_bi_persistently_mixin :
BiPersistentlyMixin
siProp_entails siProp_emp siProp_and
(@siProp_exist) siProp_sep siProp_persistently.
Proof.
split.
- solve_proper.
- (* (P ⊢ Q) → <pers> P ⊢ <pers> Q *) - (* (P ⊢ Q) → <pers> P ⊢ <pers> Q *)
done. done.
- (* <pers> P ⊢ <pers> <pers> P *) - (* <pers> P ⊢ <pers> <pers> P *)
...@@ -119,7 +126,9 @@ Qed. ...@@ -119,7 +126,9 @@ Qed.
Canonical Structure siPropI : bi := Canonical Structure siPropI : bi :=
{| bi_ofe_mixin := ofe_mixin_of siProp; {| bi_ofe_mixin := ofe_mixin_of siProp;
bi_bi_mixin := siProp_bi_mixin; bi_bi_later_mixin := siProp_bi_later_mixin |}. bi_bi_mixin := siProp_bi_mixin;
bi_bi_persistently_mixin := siProp_bi_persistently_mixin;
bi_bi_later_mixin := siProp_bi_later_mixin |}.
Global Instance siProp_pure_forall : BiPureForall siPropI. Global Instance siProp_pure_forall : BiPureForall siPropI.
Proof. exact: @pure_forall_2. Qed. Proof. exact: @pure_forall_2. Qed.
......
...@@ -6,241 +6,186 @@ From iris.algebra Require Export cmra. ...@@ -6,241 +6,186 @@ From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates. From iris.algebra Require Import updates local_updates.
From iris.prelude Require Import options. From iris.prelude Require Import options.
Local Arguments pcore _ _ !_ /. (** Given a preorder [R] on a type [A] we construct the "monotone" resource
Local Arguments cmra_pcore _ !_ /. algebra [mra R] and an injection [to_mra : A → mra R] such that:
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /. [R x y] iff [to_mra x ≼ to_mra y]
Local Arguments cmra_validN _ _ !_ /.
Local Arguments cmra_valid _ !_ /. Here, [≼] is the extension order of the [mra R] resource algebra. This is
exactly what the lemma [to_mra_included] shows.
(* Given a preorder relation R on a type A we construct a resource algebra mra R
and an injection principal : A -> mra R such that: This resource algebra is useful for reasoning about monotonicity. See the
[R x y] iff [principal x ≼ principal y] following paper for more details ([to_mra] is called "principal"):
where ≼ is the extension order of mra R resource algebra. This is exactly
what the lemma [principal_included] shows. Reasoning About Monotonicity in Separation Logic
Amin Timany and Lars Birkedal
This resource algebra is useful for reasoning about monotonicity. in Certified Programs and Proofs (CPP) 2021
See the following paper for more details:
Note that unlike most Iris algebra constructions [mra A] works on [A : Type],
Reasoning About Monotonicity in Separation Logic not on [A : ofe]. See the comment at [mraO] below for more information. If [A]
Amin Timany and Lars Birkedal has an [Equiv A] (i.e., is a setoid), there are some results at the bottom of
in Certified Programs and Proofs (CPP) 2021 this file. *)
*) Record mra {A} (R : relation A) := { mra_car : list A }.
Definition to_mra {A} {R : relation A} (a : A) : mra R :=
Definition mra {A : Type} (R : relation A) : Type := list A. {| mra_car := [a] |}.
Definition principal {A : Type} (R : relation A) (a : A) : mra R := [a]. Global Arguments mra_car {_ _} _.
(* OFE *) Section mra.
Section ofe. Context {A} {R : relation A}.
Context {A : Type} {R : relation A}.
Implicit Types a b : A. Implicit Types a b : A.
Implicit Types x y : mra R. Implicit Types x y : mra R.
Local Definition below (a : A) (x : mra R) := b, b x R a b. (** Pronounced [a] is below [x]. *)
Local Definition mra_below (a : A) (x : mra R) := b, b mra_car x R a b.
Local Lemma below_app a x y : below a (x ++ y) below a x below a y. Local Lemma mra_below_to_mra a b : mra_below a (to_mra b) R a b.
Proof. Proof. set_solver. Qed.
split.
- intros (b & [|]%elem_of_app & ?); [left|right]; exists b; eauto.
- intros [(b & ? & ?)|(b & ? & ?)]; exists b; rewrite elem_of_app; eauto.
Qed.
Local Lemma below_principal a b : below a (principal R b) R a b. (* OFE *)
Proof. Local Instance mra_equiv : Equiv (mra R) := λ x y,
split. a, mra_below a x mra_below a y.
- intros (c & ->%elem_of_list_singleton & ?); done.
- intros Hab; exists b; split; first apply elem_of_list_singleton; done.
Qed.
Local Instance mra_equiv : Equiv (mra R) :=
λ x y, a, below a x below a y.
Local Instance mra_equiv_equiv : Equivalence mra_equiv. Local Instance mra_equiv_equiv : Equivalence mra_equiv.
Proof. Proof. unfold mra_equiv; split; intros ?; naive_solver. Qed.
split; [by firstorder|by firstorder|].
intros ??? Heq1 Heq2 ?; split; intros ?;
[apply Heq2; apply Heq1|apply Heq1; apply Heq2]; done.
Qed.
Canonical Structure mraO := discreteO (mra R). (** Generalizing [mra A] to [A : ofe] and [R : A -n> A -n> siProp] is not
End ofe. obvious. It is not clear what axioms to impose on [R] for the "extension
axiom" to hold:
Global Arguments mraO [_] _. cmra_extend :
x ≡{n}≡ y1 ⋅ y2 →
∃ z1 z2, x ≡ z1 ⋅ z2 ∧ y1 ≡{n}≡ z1 ∧ y2 ≡{n}≡ z2
(* CMRA *) To prove this, assume ([⋅] is defined as [++], see [mra_op]):
Section cmra.
Context {A : Type} {R : relation A}. x ≡{n}≡ y1 ++ y2
Implicit Types a b : A.
Implicit Types x y : mra R. When defining [dist] as the step-indexed version of [mra_equiv], this means:
∀ n' a, n' ≤ n →
mra_below a x n' ↔ mra_below a y1 n' ∨ mra_below a y2 n'
From this assumption it is not clear how to obtain witnesses [z1] and [z2]. *)
Canonical Structure mraO := discreteO (mra R).
(* CMRA *)
Local Instance mra_valid : Valid (mra R) := λ x, True. Local Instance mra_valid : Valid (mra R) := λ x, True.
Local Instance mra_validN : ValidN (mra R) := λ n x, True. Local Instance mra_validN : ValidN (mra R) := λ n x, True.
Local Program Instance mra_op : Op (mra R) := λ x y, x ++ y. Local Program Instance mra_op : Op (mra R) := λ x y,
{| mra_car := mra_car x ++ mra_car y |}.
Local Instance mra_pcore : PCore (mra R) := Some. Local Instance mra_pcore : PCore (mra R) := Some.
Lemma mra_cmra_mixin : CmraMixin (mra R). Lemma mra_cmra_mixin : CmraMixin (mra R).
Proof. Proof.
apply discrete_cmra_mixin; first apply _. apply discrete_cmra_mixin; first apply _.
apply ra_total_mixin. apply ra_total_mixin; try done.
- eauto. - (* [Proper] of [op] *) intros x y z Hyz a. specialize (Hyz a). set_solver.
- intros ??? Heq a; specialize (Heq a); rewrite !below_app; firstorder. - (* [Proper] of [core] *) apply _.
- intros ?; done. - (* [Assoc] *) intros x y z a. set_solver.
- done. - (* [Comm] *) intros x y a. set_solver.
- intros ????; rewrite !below_app; firstorder. - (* [core x ⋅ x ≡ x] *) intros x a. set_solver.
- intros ???; rewrite !below_app; firstorder.
- rewrite /core /pcore /=; intros ??; rewrite below_app; firstorder.
- done.
- intros ? ? [? ?]; eexists _; done.
- done.
Qed. Qed.
Canonical Structure mraR : cmra := Cmra (mra R) mra_cmra_mixin. Canonical Structure mraR : cmra := Cmra (mra R) mra_cmra_mixin.
Global Instance mra_cmra_total : CmraTotal mraR. Global Instance mra_cmra_total : CmraTotal mraR.
Proof. rewrite /CmraTotal; eauto. Qed. Proof. rewrite /CmraTotal; eauto. Qed.
Global Instance mra_core_id (x : mra R) : CoreId x. Global Instance mra_core_id x : CoreId x.
Proof. by constructor. Qed. Proof. by constructor. Qed.
Global Instance mra_cmra_discrete : CmraDiscrete mraR. Global Instance mra_cmra_discrete : CmraDiscrete mraR.
Proof. split; last done. intros ? ?; done. Qed. Proof. split; last done. intros ? ?; done. Qed.
Local Instance mra_unit : Unit (mra R) := @nil A. Local Instance mra_unit : Unit (mra R) := {| mra_car := [] |}.
Lemma auth_ucmra_mixin : UcmraMixin (mra R). Lemma auth_ucmra_mixin : UcmraMixin (mra R).
Proof. split; done. Qed. Proof. split; done. Qed.
Canonical Structure mraUR := Ucmra (mra R) auth_ucmra_mixin. Canonical Structure mraUR := Ucmra (mra R) auth_ucmra_mixin.
Lemma mra_idemp (x : mra R) : x x x. (* Laws *)
Proof. intros a; rewrite below_app; naive_solver. Qed. Lemma mra_idemp x : x x x.
Proof. intros a. set_solver. Qed.
Lemma mra_included (x y : mra R) : x y y x y. Lemma mra_included x y : x y y x y.
Proof. Proof.
split; [|by intros ?; exists y]. split; [|by intros ?; exists y].
intros [z ->]; rewrite assoc mra_idemp; done. intros [z ->]; rewrite assoc mra_idemp; done.
Qed. Qed.
Lemma principal_R_opN_base `{!Transitive R} n x y : Lemma to_mra_R_op `{!Transitive R} a b :
( b, b y c, c x R b c) y x {n} x. R a b
Proof. to_mra a to_mra b to_mra b.
intros HR; split; rewrite /op /mra_op below_app; [|by firstorder]. Proof. intros Hab c. set_solver. Qed.
intros [(c & (d & Hd1 & Hd2)%HR & Hc2)|]; [|done].
exists d; split; [|transitivity c]; done.
Qed.
Lemma principal_R_opN `{!Transitive R} n a b :
R a b principal R a principal R b {n} principal R b.
Proof.
intros; apply principal_R_opN_base; intros c; rewrite /principal.
setoid_rewrite elem_of_list_singleton => ->; eauto.
Qed.
Lemma principal_R_op `{!Transitive R} a b :
R a b principal R a principal R b principal R b.
Proof. by intros ? ?; apply (principal_R_opN 0). Qed.
Lemma principal_op_RN n a b x :
R a a principal R a x {n} principal R b R a b.
Proof.
intros Ha HR.
destruct (HR a) as [[z [HR1%elem_of_list_singleton HR2]] _];
last by subst; eauto.
rewrite /op /mra_op /principal below_app below_principal; auto.
Qed.
Lemma principal_op_R' a b x :
R a a principal R a x principal R b R a b.
Proof. intros ? ?; eapply (principal_op_RN 0); eauto. Qed.
Lemma principal_op_R `{!Reflexive R} a b x :
principal R a x principal R b R a b.
Proof. intros; eapply principal_op_R'; eauto. Qed.
Lemma principal_includedN `{!PreOrder R} n a b : Lemma to_mra_included `{!PreOrder R} a b :
principal R a {n} principal R b R a b. to_mra a to_mra b R a b.
Proof. Proof.
split. split.
- intros [z Hz]; eapply principal_op_RN; first done. by rewrite Hz. - move=> [z Hz]. specialize (Hz a). set_solver.
- intros ?; exists (principal R b); rewrite principal_R_opN; eauto. - intros ?; exists (to_mra b). by rewrite to_mra_R_op.
Qed. Qed.
Lemma principal_included `{!PreOrder R} a b :
principal R a principal R b R a b.
Proof. apply (principal_includedN 0). Qed.
Lemma mra_local_update_grow `{!Transitive R} a x b: Lemma mra_local_update_grow `{!Transitive R} a x b:
R a b R a b
(principal R a, x) ~l~> (principal R b, principal R b). (to_mra a, x) ~l~> (to_mra b, to_mra b).
Proof. Proof.
intros Hana Hanb. intros Hana. apply local_update_unital_discrete=> z _ Habz.
apply local_update_unital_discrete. split; first done. intros c. specialize (Habz c). set_solver.
intros z _ Habz.
split; first done.
intros w; split.
- intros (y & ->%elem_of_list_singleton & Hy2).
exists b; split; first constructor; done.
- intros (y & [->|Hy1]%elem_of_cons & Hy2).
+ exists b; split; first constructor; done.
+ exists b; split; first constructor.
specialize (Habz w) as [_ [c [->%elem_of_list_singleton Hc2]]].
{ exists y; split; first (by apply elem_of_app; right); eauto. }
etrans; eauto.
Qed. Qed.
Lemma mra_local_update_get_frag `{!PreOrder R} a b: Lemma mra_local_update_get_frag `{!PreOrder R} a b:
R b a R b a
(principal R a, ε) ~l~> (principal R a, principal R b). (to_mra a, ε) ~l~> (to_mra a, to_mra b).
Proof. Proof.
intros Hana. intros Hana. apply local_update_unital_discrete=> z _.
apply local_update_unital_discrete. rewrite left_id. intros <-. split; first done.
intros z _; rewrite left_id; intros <-. apply mra_included; by apply to_mra_included.
split; first done.
apply mra_included; by apply principal_included.
Qed. Qed.
End mra.
End cmra. Global Arguments mraO {_} _.
Global Arguments mraR {_} _. Global Arguments mraR {_} _.
Global Arguments mraUR {_} _. Global Arguments mraUR {_} _.
(** If [R] is a partial order, relative to a reflexive relation [S] on the
(* Might be useful if the type of elements is an OFE. *) carrier [A], then [to_mra] is proper and injective. The theory for
Section mra_over_ofe. arbitrary relations [S] is overly general, so we do not declare the results
Context {A : ofe} {R : relation A}. as instances. Below we provide instances for [S] being [=] and [≡]. *)
Section mra_over_rel.
Context {A} {R : relation A} (S : relation A).
Implicit Types a b : A. Implicit Types a b : A.
Implicit Types x y : mra R. Implicit Types x y : mra R.
Global Instance principal_ne Lemma to_mra_rel_proper :
`{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} : Reflexive S
NonExpansive (principal R). Proper (S ==> S ==> iff) R
Proof. intros n a1 a2 Ha; split; rewrite !below_principal !Ha; done. Qed. Proper (S ==> (≡@{mra R})) (to_mra).
Proof. intros ? HR a1 a2 Ha b. rewrite !mra_below_to_mra. by apply HR. Qed.
Global Instance principal_proper
`{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
Proper (() ==> ()) (principal R) := ne_proper _.
Lemma principal_inj_related a b : Lemma to_mra_rel_inj :
principal R a principal R b R a a R a b. Reflexive R
AntiSymm S R
Inj S (≡@{mra R}) (to_mra).
Proof. Proof.
intros Hab ?. intros ?? a b Hab. move: (Hab a) (Hab b). rewrite !mra_below_to_mra.
destruct (Hab a) as [[? [?%elem_of_list_singleton ?]] _]; intros. apply (anti_symm R); naive_solver.
last by subst; auto.
exists a; rewrite /principal elem_of_list_singleton; done.
Qed. Qed.
End mra_over_rel.
Lemma principal_inj_general a b :
principal R a principal R b Global Instance to_mra_inj {A} {R : relation A} :
R a a R b b (R a b R b a a b) a b. Reflexive R
Proof. intros ??? Has; apply Has; apply principal_inj_related; auto. Qed. AntiSymm (=) R
Inj (=) (≡@{mra R}) (to_mra) | 0. (* Lower cost than [to_mra_equiv_inj] *)
Global Instance principal_inj_instance `{!Reflexive R} `{!AntiSymm () R} : Proof. intros. by apply (to_mra_rel_inj (=)). Qed.
Inj () () (principal R).
Proof. intros ???; apply principal_inj_general; auto. Qed. Global Instance to_mra_proper `{Equiv A} {R : relation A} :
Reflexive (≡@{A})
Global Instance principal_injN `{!Reflexive R} {Has : AntiSymm () R} n : Proper (() ==> () ==> iff) R
Inj (dist n) (dist n) (principal R). Proper (() ==> (≡@{mra R})) (to_mra).
Proof. Proof. intros. by apply (to_mra_rel_proper ()). Qed.
intros x y Hxy%discrete_iff; last apply _.
eapply equiv_dist; revert Hxy; apply inj; apply _. Global Instance to_mra_equiv_inj `{Equiv A} {R : relation A} :
Qed. Reflexive R
AntiSymm () R
End mra_over_ofe. Inj () (≡@{mra R}) (to_mra) | 1.
Proof. intros. by apply (to_mra_rel_inj ()). Qed.
(** This is just an integration file for [iris_staging.algebra.list]; (** This is just an integration file for [iris_staging.algebra.list];
both should be stabilized together. *) both should be stabilized together. *)
From iris.algebra Require Import cmra. From iris.algebra Require Import cmra.
From iris.unstable.algebra Require Import list monotone. From iris.unstable.algebra Require Import list.
From iris.base_logic Require Import bi derived. From iris.base_logic Require Import bi derived.
From iris.prelude Require Import options. From iris.prelude Require Import options.
...@@ -19,16 +19,4 @@ Section list_cmra. ...@@ -19,16 +19,4 @@ Section list_cmra.
Lemma list_validI l : l ⊣⊢ i, (l !! i). Lemma list_validI l : l ⊣⊢ i, (l !! i).
Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed. Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
End list_cmra. End list_cmra.
Section monotone.
Lemma monotone_equivI {A : ofe} (R : relation A)
`{!( n : nat, Proper (dist n ==> dist n ==> iff) R)}
`{!Reflexive R} `{!AntiSymm () R} a b :
principal R a principal R b ⊣⊢ (a b).
Proof.
uPred.unseal. do 2 split; intros ?.
- exact: principal_injN.
- exact: principal_ne.
Qed.
End monotone.
End upred. End upred.
...@@ -94,7 +94,7 @@ Local Definition heapProp_wand_unseal: ...@@ -94,7 +94,7 @@ Local Definition heapProp_wand_unseal:
@heapProp_wand = @heapProp_wand_def := seal_eq heapProp_wand_aux. @heapProp_wand = @heapProp_wand_def := seal_eq heapProp_wand_aux.
Local Definition heapProp_persistently_def (P : heapProp) : heapProp := Local Definition heapProp_persistently_def (P : heapProp) : heapProp :=
{| heapProp_holds σ := P |}. heapProp_pure (heapProp_entails heapProp_emp P).
Local Definition heapProp_persistently_aux : seal (@heapProp_persistently_def). Local Definition heapProp_persistently_aux : seal (@heapProp_persistently_def).
Proof. by eexists. Qed. Proof. by eexists. Qed.
Definition heapProp_persistently := unseal heapProp_persistently_aux. Definition heapProp_persistently := unseal heapProp_persistently_aux.
...@@ -120,7 +120,7 @@ Section mixins. ...@@ -120,7 +120,7 @@ Section mixins.
BiMixin BiMixin
heapProp_entails heapProp_emp heapProp_pure heapProp_and heapProp_or heapProp_entails heapProp_emp heapProp_pure heapProp_and heapProp_or
heapProp_impl (@heapProp_forall) (@heapProp_exist) heapProp_impl (@heapProp_forall) (@heapProp_exist)
heapProp_sep heapProp_wand heapProp_persistently. heapProp_sep heapProp_wand.
Proof. Proof.
split. split.
- (* [PreOrder heapProp_entails] *) - (* [PreOrder heapProp_entails] *)
...@@ -145,8 +145,6 @@ Section mixins. ...@@ -145,8 +145,6 @@ Section mixins.
unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver. unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
- (* [NonExpansive2 bi_wand] *) - (* [NonExpansive2 bi_wand] *)
unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver. unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
- (* [NonExpansive2 bi_persistently] *)
unseal=> n P1 P2 [HP]; split; naive_solver.
- (* [φ → P ⊢ ⌜ φ ⌝] *) - (* [φ → P ⊢ ⌜ φ ⌝] *)
unseal=> φ P ?; by split. unseal=> φ P ?; by split.
- (* [(φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P] *) - (* [(φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P] *)
...@@ -193,21 +191,18 @@ Section mixins. ...@@ -193,21 +191,18 @@ Section mixins.
unseal=> P Q R [HPQR]; split=> σ1 ? σ2 ??. apply HPQR. by exists σ1, σ2. unseal=> P Q R [HPQR]; split=> σ1 ? σ2 ??. apply HPQR. by exists σ1, σ2.
- (* [(P ⊢ Q -∗ R) → P ∗ Q ⊢ R] *) - (* [(P ⊢ Q -∗ R) → P ∗ Q ⊢ R] *)
unseal=> P Q R [HPQR]; split; intros ? (σ1&σ2&->&?&?&?). by apply HPQR. unseal=> P Q R [HPQR]; split; intros ? (σ1&σ2&->&?&?&?). by apply HPQR.
- (* [(P ⊢ Q) → <pers> P ⊢ <pers> Q] *) Qed.
unseal=> P Q [HPQ]; split=> σ. apply HPQ.
- (* [<pers> P ⊢ <pers> <pers> P] *) Lemma heapProp_bi_persistently_mixin :
unseal=> P; split=> σ; done. BiPersistentlyMixin
- (* [emp ⊢ <pers> emp] *) heapProp_entails heapProp_emp heapProp_and
unseal; split=> σ; done. (@heapProp_exist) heapProp_sep heapProp_persistently.
- (* [(∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a)] *) Proof.
unseal=> A Ψ; split=> σ; done. eapply bi_persistently_mixin_discrete, heapProp_bi_mixin; [done|..].
- (* [<pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a)] *) - (* [(emp ⊢ ∃ x, Φ x) → ∃ x, emp ⊢ Φ x] *)
unseal=> A Ψ; split=> σ; done. unseal. intros A Φ [H]. destruct (H ) as [x ?]; [done|].
- (* [<pers> P ∗ Q ⊢ <pers> P] *) exists x. by split=> σ ->.
unseal=> P Q; split; intros ? (σ1&σ2&->&?&?&?); done. - by rewrite heapProp_persistently_unseal.
- (* [<pers> P ∧ Q ⊢ P ∗ Q] *)
unseal=> P Q; split=> σ [??]. eexists , σ. rewrite left_id_L.
split_and!; done || apply map_disjoint_empty_l.
Qed. Qed.
Lemma heapProp_bi_later_mixin : Lemma heapProp_bi_later_mixin :
...@@ -220,7 +215,9 @@ End mixins. ...@@ -220,7 +215,9 @@ End mixins.
Canonical Structure heapPropI : bi := Canonical Structure heapPropI : bi :=
{| bi_ofe_mixin := ofe_mixin_of heapProp; {| bi_ofe_mixin := ofe_mixin_of heapProp;
bi_bi_mixin := heapProp_bi_mixin; bi_bi_later_mixin := heapProp_bi_later_mixin |}. bi_bi_mixin := heapProp_bi_mixin;
bi_bi_persistently_mixin := heapProp_bi_persistently_mixin;
bi_bi_later_mixin := heapProp_bi_later_mixin |}.
Global Instance heapProp_pure_forall : BiPureForall heapPropI. Global Instance heapProp_pure_forall : BiPureForall heapPropI.
Proof. intros A φ. rewrite /bi_forall /bi_pure /=. unseal. by split. Qed. Proof. intros A φ. rewrite /bi_forall /bi_pure /=. unseal. by split. Qed.
......
From stdpp Require Import gmap.
From iris.bi Require Import interface.
From iris.proofmode Require Import tactics.
From iris.prelude Require Import options.
(** This file constructs a simple non step-indexed affine separation logic as
predicates over heaps (modeled as maps from integer locations to integer values).
It shows that Iris's [bi] canonical structure can be inhabited, and the Iris
proof mode can be used to prove lemmas in this separation logic. *)
Definition loc := Z.
Definition val := Z.
Record heapProp := HeapProp {
heapProp_holds :> gmap loc val Prop;
heapProp_closed σ1 σ2 : heapProp_holds σ1 σ1 σ2 heapProp_holds σ2;
}.
Global Arguments heapProp_holds : simpl never.
Add Printing Constructor heapProp.
Section ofe.
Inductive heapProp_equiv' (P Q : heapProp) : Prop :=
{ heapProp_in_equiv : σ, P σ Q σ }.
Local Instance heapProp_equiv : Equiv heapProp := heapProp_equiv'.
Local Instance heapProp_equivalence : Equivalence (≡@{heapProp}).
Proof. split; repeat destruct 1; constructor; naive_solver. Qed.
Canonical Structure heapPropO := discreteO heapProp.
End ofe.
(** logical entailement *)
Inductive heapProp_entails (P Q : heapProp) : Prop :=
{ heapProp_in_entails : σ, P σ Q σ }.
(** logical connectives *)
Local Program Definition heapProp_pure_def (φ : Prop) : heapProp :=
{| heapProp_holds _ := φ |}.
Solve Obligations with done.
Local Definition heapProp_pure_aux : seal (@heapProp_pure_def). Proof. by eexists. Qed.
Definition heapProp_pure := unseal heapProp_pure_aux.
Local Definition heapProp_pure_unseal :
@heapProp_pure = @heapProp_pure_def := seal_eq heapProp_pure_aux.
Definition heapProp_emp : heapProp := heapProp_pure True.
Local Program Definition heapProp_and_def (P Q : heapProp) : heapProp :=
{| heapProp_holds σ := P σ Q σ |}.
Solve Obligations with naive_solver eauto using heapProp_closed.
Local Definition heapProp_and_aux : seal (@heapProp_and_def). Proof. by eexists. Qed.
Definition heapProp_and := unseal heapProp_and_aux.
Local Definition heapProp_and_unseal:
@heapProp_and = @heapProp_and_def := seal_eq heapProp_and_aux.
Local Program Definition heapProp_or_def (P Q : heapProp) : heapProp :=
{| heapProp_holds σ := P σ Q σ |}.
Solve Obligations with naive_solver eauto using heapProp_closed.
Local Definition heapProp_or_aux : seal (@heapProp_or_def). Proof. by eexists. Qed.
Definition heapProp_or := unseal heapProp_or_aux.
Local Definition heapProp_or_unseal:
@heapProp_or = @heapProp_or_def := seal_eq heapProp_or_aux.
Local Program Definition heapProp_impl_def (P Q : heapProp) : heapProp :=
{| heapProp_holds σ := σ', σ σ' P σ' Q σ' |}.
Next Obligation. intros P Q σ1 σ2 HPQ ? σ' ?; simpl in *. apply HPQ. by etrans. Qed.
Local Definition heapProp_impl_aux : seal (@heapProp_impl_def). Proof. by eexists. Qed.
Definition heapProp_impl := unseal heapProp_impl_aux.
Local Definition heapProp_impl_unseal :
@heapProp_impl = @heapProp_impl_def := seal_eq heapProp_impl_aux.
Local Program Definition heapProp_forall_def {A} (Ψ : A heapProp) : heapProp :=
{| heapProp_holds σ := a, Ψ a σ |}.
Solve Obligations with naive_solver eauto using heapProp_closed.
Local Definition heapProp_forall_aux : seal (@heapProp_forall_def). Proof. by eexists. Qed.
Definition heapProp_forall {A} := unseal heapProp_forall_aux A.
Local Definition heapProp_forall_unseal :
@heapProp_forall = @heapProp_forall_def := seal_eq heapProp_forall_aux.
Local Program Definition heapProp_exist_def {A} (Ψ : A heapProp) : heapProp :=
{| heapProp_holds σ := a, Ψ a σ |}.
Solve Obligations with naive_solver eauto using heapProp_closed.
Local Definition heapProp_exist_aux : seal (@heapProp_exist_def). Proof. by eexists. Qed.
Definition heapProp_exist {A} := unseal heapProp_exist_aux A.
Local Definition heapProp_exist_unseal :
@heapProp_exist = @heapProp_exist_def := seal_eq heapProp_exist_aux.
Local Program Definition heapProp_sep_def (P Q : heapProp) : heapProp :=
{| heapProp_holds σ := σ1 σ2, σ = σ1 σ2 σ1 ## σ2 P σ1 Q σ2 |}.
Next Obligation.
intros P Q σ1 σ2 (σ11 & σ12 & -> & ? & ? & ?) ?.
assert (σ11 σ2) by (by etrans; [apply map_union_subseteq_l|]).
exists σ11, (σ2 σ11). split_and!; [| |done|].
- by rewrite map_difference_union.
- by apply map_disjoint_difference_r.
- eapply heapProp_closed; [done|].
apply map_union_reflecting_l with σ11; [done|..].
+ by apply map_disjoint_difference_r.
+ by rewrite map_difference_union.
Qed.
Local Definition heapProp_sep_aux : seal (@heapProp_sep_def). Proof. by eexists. Qed.
Definition heapProp_sep := unseal heapProp_sep_aux.
Local Definition heapProp_sep_unseal:
@heapProp_sep = @heapProp_sep_def := seal_eq heapProp_sep_aux.
Local Program Definition heapProp_wand_def (P Q : heapProp) : heapProp :=
{| heapProp_holds σ := σ', σ ## σ' P σ' Q (σ σ') |}.
Next Obligation.
intros P Q σ1 σ2 HPQ ? σ' ??; simpl in *.
apply heapProp_closed with (σ1 σ'); [by eauto using map_disjoint_weaken_l|].
by apply map_union_mono_r.
Qed.
Local Definition heapProp_wand_aux : seal (@heapProp_wand_def). Proof. by eexists. Qed.
Definition heapProp_wand := unseal heapProp_wand_aux.
Local Definition heapProp_wand_unseal:
@heapProp_wand = @heapProp_wand_def := seal_eq heapProp_wand_aux.
Local Definition heapProp_persistently_def (P : heapProp) : heapProp :=
heapProp_pure (heapProp_entails heapProp_emp P).
Local Definition heapProp_persistently_aux : seal (@heapProp_persistently_def).
Proof. by eexists. Qed.
Definition heapProp_persistently := unseal heapProp_persistently_aux.
Local Definition heapProp_persistently_unseal:
@heapProp_persistently = @heapProp_persistently_def := seal_eq heapProp_persistently_aux.
(** Iris's [bi] class requires the presence of a later modality, but for non
step-indexed logics, it can be defined as the identity. *)
Definition heapProp_later (P : heapProp) : heapProp := P.
Local Definition heapProp_unseal :=
(heapProp_pure_unseal, heapProp_and_unseal,
heapProp_or_unseal, heapProp_impl_unseal, heapProp_forall_unseal,
heapProp_exist_unseal, heapProp_sep_unseal, heapProp_wand_unseal,
heapProp_persistently_unseal).
Ltac unseal := rewrite !heapProp_unseal /=.
Section mixins.
(** Enable [simpl] locally, which is useful for proofs in the model. *)
Local Arguments heapProp_holds !_ _ /.
Lemma heapProp_bi_mixin :
BiMixin
heapProp_entails heapProp_emp heapProp_pure heapProp_and heapProp_or
heapProp_impl (@heapProp_forall) (@heapProp_exist)
heapProp_sep heapProp_wand.
Proof.
split.
- (* [PreOrder heapProp_entails] *)
split; repeat destruct 1; constructor; naive_solver.
- (* [P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P)] *)
intros P Q; split.
+ intros [HPQ]; split; split; naive_solver.
+ intros [[HPQ] [HQP]]; split; naive_solver.
- (* [Proper (iff ==> dist n) bi_pure] *)
unseal=> n φ1 φ2 ; split; naive_solver.
- (* [NonExpansive2 bi_and] *)
unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
- (* [NonExpansive2 bi_or] *)
unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
- (* [NonExpansive2 bi_impl] *)
unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
- (* [Proper (pointwise_relation _ (dist n) ==> dist n) (bi_forall A)] *)
unseal=> A n Φ1 Φ2 ; split=> σ /=; split=> ? x; by apply .
- (* [Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A)] *)
unseal=> A n Φ1 Φ2 ; split=> σ /=; split=> -[x ?]; exists x; by apply .
- (* [NonExpansive2 bi_sep] *)
unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
- (* [NonExpansive2 bi_wand] *)
unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
- (* [φ → P ⊢ ⌜ φ ⌝] *)
unseal=> φ P ?; by split.
- (* [(φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P] *)
unseal=> φ P HP; split=> σ ?. by apply HP.
- (* [P ∧ Q ⊢ P] *)
unseal=> P Q; split=> σ [??]; done.
- (* [P ∧ Q ⊢ Q] *)
unseal=> P Q; split=> σ [??]; done.
- (* [(P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R] *)
unseal=> P Q R [HPQ] [HPR]; split=> σ; split; auto.
- (* [P ⊢ P ∨ Q] *)
unseal=> P Q; split=> σ; by left.
- (* [Q ⊢ P ∨ Q] *)
unseal=> P Q; split=> σ; by right.
- (* [(P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R] *)
unseal=> P Q R [HPQ] [HQR]; split=> σ [?|?]; auto.
- (* [(P ∧ Q ⊢ R) → P ⊢ Q → R] *)
unseal=> P Q R HPQR; split=> σ ? σ' ??. apply HPQR.
split; eauto using heapProp_closed.
- (* [(P ⊢ Q → R) → P ∧ Q ⊢ R] *)
unseal=> P Q R HPQR; split=> σ [??]. by eapply HPQR.
- (* [(∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a] *)
unseal=> A P Ψ HPΨ; split=> σ ? a. by apply HPΨ.
- (* [(∀ a, Ψ a) ⊢ Ψ a] *)
unseal=> A Ψ a; split=> σ ?; done.
- (* [Ψ a ⊢ ∃ a, Ψ a] *)
unseal=> A Ψ a; split=> σ ?. by exists a.
- (* [(∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q] *)
unseal=> A Φ Q HΦQ; split=> σ [a ?]. by apply (HΦQ a).
- (* [(P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'] *)
unseal=> P P' Q Q' [HPQ] [HP'Q']; split; naive_solver.
- (* [P ⊢ emp ∗ P] *)
unfold heapProp_emp; unseal=> P; split=> σ ? /=.
eexists , σ. rewrite left_id_L.
split_and!; done || apply map_disjoint_empty_l.
- (* [emp ∗ P ⊢ P] *)
unfold heapProp_emp; unseal=> P; split; intros ? (?&σ&->&?&_&?).
eapply heapProp_closed; [done|]. by apply map_union_subseteq_r.
- (* [P ∗ Q ⊢ Q ∗ P] *)
unseal=> P Q; split; intros ? (σ1&σ2&->&?&?&?).
exists σ2, σ1. by rewrite map_union_comm.
- (* [(P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R)] *)
unseal=> P Q R; split; intros ? (?&σ3&->&?&(σ1&σ2&->&?&?&?)&?).
exists σ1, (σ2 σ3). split_and!; [by rewrite assoc_L|solve_map_disjoint|done|].
exists σ2, σ3; split_and!; [done|solve_map_disjoint|done..].
- (* [(P ∗ Q ⊢ R) → P ⊢ Q -∗ R] *)
unseal=> P Q R [HPQR]; split=> σ1 ? σ2 ??. apply HPQR. by exists σ1, σ2.
- (* [(P ⊢ Q -∗ R) → P ∗ Q ⊢ R] *)
unseal=> P Q R [HPQR]; split; intros ? (σ1&σ2&->&?&?&?). by apply HPQR.
Qed.
Lemma heapProp_bi_persistently_mixin :
BiPersistentlyMixin
heapProp_entails heapProp_emp heapProp_and
(@heapProp_exist) heapProp_sep heapProp_persistently.
Proof.
eapply bi_persistently_mixin_discrete, heapProp_bi_mixin; [done|..].
- (* The "existential property" [(emp ⊢ ∃ x, Φ x) → ∃ x, emp ⊢ Φ x]. For an
affine BI the proof relies on there being a smallest resource/the unit
(here the empty heap [∅]). *)
unfold heapProp_emp. unseal. intros A Φ [H].
destruct (H ) as [x ?]; [done|]. exists x. split=> σ _.
eapply heapProp_closed; [done|]. by apply map_empty_subseteq.
- by rewrite heapProp_persistently_unseal.
Qed.
Lemma heapProp_bi_later_mixin :
BiLaterMixin
heapProp_entails heapProp_pure heapProp_or heapProp_impl
(@heapProp_forall) (@heapProp_exist)
heapProp_sep heapProp_persistently heapProp_later.
Proof. eapply bi_later_mixin_id; [done|apply heapProp_bi_mixin]. Qed.
End mixins.
Canonical Structure heapPropI : bi :=
{| bi_ofe_mixin := ofe_mixin_of heapProp;
bi_bi_mixin := heapProp_bi_mixin;
bi_bi_persistently_mixin := heapProp_bi_persistently_mixin;
bi_bi_later_mixin := heapProp_bi_later_mixin |}.
Global Instance heapProp_pure_forall : BiPureForall heapPropI.
Proof. intros A φ. rewrite /bi_forall /bi_pure /=. unseal. by split. Qed.
Global Instance heapProp_affine : BiAffine heapPropI.
Proof. exact: bi.True_intro. Qed.
Lemma heapProp_proofmode_test {A} (P Q Q' R : heapProp) (Φ Ψ : A heapProp) :
P Q Q' -∗ (* [Q'] is not used, to demonstrate affinity *)
R -∗
(R -∗ x, Φ x) -∗
x, Φ x Φ x P Q.
Proof.
iIntros "(HP & HQ & HQ') #HR #HRΦ".
iDestruct ("HRΦ" with "HR") as (x) "#HΦ".
iExists x. iFrame. by iSplitL.
Qed.
"mra_test_eq"
: string
1 goal
X, Y : gset nat
H : X = Y
============================
X = Y
From stdpp Require Import propset gmap strings.
From iris.unstable.algebra Require Import monotone.
Unset Mangle Names.
Notation gset_mra K:= (mra (⊆@{gset K})).
(* Check if we indeed get [=], i.e., the right [Inj] instance is used. *)
Check "mra_test_eq".
Lemma mra_test_eq X Y : to_mra X ≡@{gset_mra nat} to_mra Y X = Y.
Proof. intros ?%(inj _). Show. done. Qed.
Notation propset_mra K := (mra (⊆@{propset K})).
Lemma mra_test_equiv X Y : to_mra X ≡@{propset_mra nat} to_mra Y X Y.
Proof. intros ?%(inj _). done. Qed.