Commit bc0d8a6e by Amin Timany

### Add monotone resource algebra to iris_staging

parent 5119ab8b
 ... ... @@ -172,6 +172,7 @@ iris_heap_lang/lib/array.v iris_staging/algebra/list.v iris_staging/base_logic/algebra.v iris_staging/heap_lang/interpreter.v iris_staging/algebra/monotone.v iris_deprecated/base_logic/auth.v iris_deprecated/base_logic/sts.v ... ...
 From iris.algebra Require Export cmra. From iris.algebra Require Import updates local_updates. From iris.prelude Require Import options. Local Arguments pcore _ _ !_ /. Local Arguments cmra_pcore _ !_ /. Local Arguments validN _ _ _ !_ /. Local Arguments valid _ _ !_ /. Local Arguments cmra_validN _ _ !_ /. Local Arguments cmra_valid _ !_ /. (* 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: R x y iff principal x ≼ principal y where ≼ is the extension order of mra R resource algebra. This is exactly what the lemma [principal_included] shows. This resource algebra is useful for reasoning about monotonicity. See the following paper for more details: Reasoning About Monotonicity in Separation Logic Amin Timany and Lars Birkedal in Certified Programs and Proofs (CPP) 2021 *) Definition mra {A : Type} (R : relation A) : Type := list A. Definition principal {A : Type} (R : relation A) (a : A) : mra R := [a]. (* OFE *) Section ofe. Context {A : Type} {R : relation A}. Implicit Types a b : A. Implicit Types x y : mra R. Local Definition below (a : A) (x : mra R) := ∃ b, b ∈ x ∧ R a b. Local Lemma below_app a x y : below a (x ++ y) ↔ below a x ∨ below a y. Proof. 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. Proof. split. - 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. Proof. 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). End ofe. Global Arguments mraO [_] _. (* CMRA *) Section cmra. Context {A : Type} {R : relation A}. Implicit Types a b : A. Implicit Types x y : mra R. Local Instance mra_valid : Valid (mra R) := λ 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 Instance mra_pcore : PCore (mra R) := Some. Lemma mra_cmra_mixin : CmraMixin (mra R). Proof. apply discrete_cmra_mixin; first apply _. apply ra_total_mixin. - eauto. - intros ??? Heq a; specialize (Heq a); rewrite !below_app; firstorder. - intros ?; done. - done. - intros ????; rewrite !below_app; firstorder. - intros ???; rewrite !below_app; firstorder. - rewrite /core /pcore /=; intros ??; rewrite below_app; firstorder. - done. - intros ? ? [? ?]; eexists _; done. - done. Qed. Canonical Structure mraR : cmra := Cmra (mra R) mra_cmra_mixin. Global Instance mra_cmra_total : CmraTotal mraR. Proof. rewrite /CmraTotal; eauto. Qed. Global Instance mra_core_id (x : mra R) : CoreId x. Proof. by constructor. Qed. Global Instance mra_cmra_discrete : CmraDiscrete mraR. Proof. split; last done. intros ? ?; done. Qed. Local Instance mra_unit : Unit (mra R) := @nil A. Lemma auth_ucmra_mixin : UcmraMixin (mra R). Proof. split; done. Qed. Canonical Structure mraUR := Ucmra (mra R) auth_ucmra_mixin. Lemma mra_idemp (x : mra R) : x ⋅ x ≡ x. Proof. intros a; rewrite below_app; naive_solver. Qed. Lemma mra_included (x y : mra R) : x ≼ y ↔ y ≡ x ⋅ y. Proof. split; [|by intros ?; exists y]. intros [z ->]; rewrite assoc mra_idemp; done. Qed. Lemma principal_R_opN_base `{!Transitive R} n x y : (∀ b, b ∈ y → ∃ c, c ∈ x ∧ R b c) → y ⋅ x ≡{n}≡ x. Proof. intros HR; split; rewrite /op /mra_op below_app; [|by firstorder]. 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 : principal R a ≼{n} principal R b ↔ R a b. Proof. split. - intros [z Hz]; eapply principal_op_RN; first done. by rewrite Hz. - intros ?; exists (principal R b); rewrite principal_R_opN; eauto. 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: R a b → (principal R a, x) ~l~> (principal R b, principal R b). Proof. intros Hana Hanb. apply local_update_unital_discrete. 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. Lemma mra_local_update_get_frag `{!PreOrder R} a b: R b a → (principal R a, ε) ~l~> (principal R a, principal R b). Proof. intros Hana. apply local_update_unital_discrete. intros z _; rewrite left_id; intros <-. split; first done. apply mra_included; by apply principal_included. Qed. End cmra. Global Arguments mraR {_} _. Global Arguments mraUR {_} _. (* Might be useful if the type of elements is an OFE. *) Section mra_over_ofe. Context {A : ofe} {R : relation A}. Implicit Types a b : A. Implicit Types x y : mra R. Global Instance principal_ne `{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} : NonExpansive (principal R). Proof. intros n a1 a2 Ha; split; rewrite !below_principal !Ha; done. Qed. Global Instance principal_proper `{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} : Proper ((≡) ==> (≡)) (principal R) := ne_proper _. Lemma principal_inj_related a b : principal R a ≡ principal R b → R a a → R a b. Proof. intros Hab ?. destruct (Hab a) as [[? [?%elem_of_list_singleton ?]] _]; last by subst; auto. exists a; rewrite /principal elem_of_list_singleton; done. Qed. Lemma principal_inj_general a b : principal R a ≡ principal R b → R a a → R b b → (R a b → R b a → a ≡ b) → a ≡ b. Proof. intros ??? Has; apply Has; apply principal_inj_related; auto. Qed. Global Instance principal_inj_instance `{!Reflexive R} `{!AntiSymm (≡) R} : Inj (≡) (≡) (principal R). Proof. intros ???; apply principal_inj_general; auto. Qed. Global Instance principal_injN `{!Reflexive R} {Has : AntiSymm (≡) R} n : Inj (dist n) (dist n) (principal R). Proof. intros x y Hxy%discrete_iff; last apply _. eapply equiv_dist; revert Hxy; apply inj; apply _. Qed. End mra_over_ofe.
 (* This is just an integration file for [iris_staging.algebra.list]; both should be stabilized together. *) From iris.algebra Require Import cmra. From iris.staging.algebra Require Import list. From iris.staging.algebra Require Import list monotone. From iris.base_logic Require Import bi derived. From iris.prelude Require Import options. ... ... @@ -19,4 +19,16 @@ Section list_cmra. Lemma list_validI l : ✓ l ⊣⊢ ∀ i, ✓ (l !! i). Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed. 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.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!