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 (2)
...@@ -6,223 +6,164 @@ From iris.algebra Require Export cmra. ...@@ -6,223 +6,164 @@ 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 [principal : A → mra R] such that:
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] [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. Here, [≼] is the extension order of the [mra R] resource algebra. This is
See the following paper for more details: 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 Reasoning About Monotonicity in Separation Logic
Amin Timany and Lars Birkedal Amin Timany and Lars Birkedal
in Certified Programs and Proofs (CPP) 2021 in Certified Programs and Proofs (CPP) 2021
*) *)
Definition mra {A : Type} (R : relation A) : Type := list A. Record mra {A} (R : relation A) := { mra_car : list A }.
Definition principal {A : Type} (R : relation A) (a : A) : mra R := [a]. Definition principal {A} {R : relation A} (a : A) : mra R :=
{| mra_car := [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. Local Definition 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.
Proof. set_solver. Qed.
Local Lemma below_principal a b : below a (principal R b) R a b. Local Lemma below_principal a b : below a (principal b) R a b.
Proof. set_solver. Qed. Proof. set_solver. Qed.
Local Instance mra_equiv : Equiv (mra R) := (* OFE *)
λ x y, a, below a x below a y. 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. unfold mra_equiv; split; intros ?; naive_solver. Qed. Proof. unfold mra_equiv; split; intros ?; naive_solver. Qed.
Canonical Structure mraO := discreteO (mra R). 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.
(* 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; by rewrite !below_app (Heq a). - (* [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; by intuition. - (* [core x ⋅ x ≡ x] *) intros x a. set_solver.
- intros ???; rewrite !below_app; by intuition.
- rewrite /core /pcore /=; intros ??; rewrite below_app; by intuition.
- 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_op_base `{!Transitive R} x y :
( b, b y c, c x R b c) y x x.
Proof.
intros HR. split; rewrite /op /mra_op below_app; [|by intuition].
intros [(c & (d & Hd1 & Hd2)%HR & Hc2)|]; [|done].
exists d; split; [|transitivity c]; done.
Qed.
Lemma principal_R_op `{!Transitive R} a b : Lemma principal_R_op `{!Transitive R} a b :
R a b principal R a principal R b principal R b. R a b
Proof. principal a principal b principal b.
intros; apply principal_R_op_base; intros c; rewrite /principal. Proof. intros Hab c. set_solver. Qed.
set_solver.
Qed.
Lemma principal_op_R' a b x :
R a a principal R a x principal R b R a b.
Proof. move=> Ha /(_ a) HR. set_solver. Qed.
Lemma principal_op_R `{!Reflexive R} a b x :
principal R a x principal R b R a b.
Proof. by apply principal_op_R'. Qed.
Lemma principal_included `{!PreOrder R} a b : Lemma principal_included `{!PreOrder R} a b :
principal R a principal R b R a b. principal a principal b R a b.
Proof. Proof.
split. split.
- move=> [z Hz]. by eapply principal_op_R. - move=> [z Hz]. specialize (Hz a). set_solver.
- intros ?; exists (principal R b). by rewrite principal_R_op. - intros ?; exists (principal b). by rewrite principal_R_op.
Qed. Qed.
(* Useful? *)
Lemma principal_includedN `{!PreOrder R} n a b :
principal R a {n} principal R b R a b.
Proof. by rewrite -principal_included -cmra_discrete_included_iff. 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). (principal a, x) ~l~> (principal b, principal 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. specialize (Habz w).
set_solver.
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). (principal a, ε) ~l~> (principal a, principal 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 <-.
split; first done.
apply mra_included; by apply principal_included. 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
If [R] is a partial order, relative to a setoid [S] on the carrier [A], carrier [A], then [principal] is proper and injective. The theory for
then [principal R] is proper and injective. arbitrary relations [S] is overly general, so we do not declare the results
as instances. Below we provide instances for [S] being [=] and [≡]. *)
The following theory generalizes over an arbitrary setoid [S] and necessary properties,
but is overly general, so we encapsulate the instances in an opt-in module.
*)
Module mra_over_rel.
Section mra_over_rel. Section mra_over_rel.
Context {A : Type} {R : relation A}. 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.
Implicit Type (S : relation A).
#[export] Instance principal_rel_proper S Lemma principal_rel_proper :
`{!Proper (S ==> S ==> iff) R} `{!Reflexive S} : Reflexive S
Proper (S ==> ()) (principal R). Proper (S ==> S ==> iff) R
Proof. intros a1 a2 Ha; split; rewrite ->!below_principal, !Ha; done. Qed. Proper (S ==> (≡@{mra R})) (principal).
Proof. intros ? HR a1 a2 Ha b. rewrite !below_principal. by apply HR. Qed.
Lemma principal_inj_related a b : Lemma principal_rel_inj :
principal R a principal R b R a a R a b. Reflexive R
Proof. move=> /(_ a). set_solver. Qed. AntiSymm S R
Inj S (≡@{mra R}) (principal).
Lemma principal_inj_general S a b : Proof.
principal R a principal R b intros ?? a b Hab. move: (Hab a) (Hab b). rewrite !below_principal.
R a a R b b (R a b R b a S a b) S a b. intros. apply (anti_symm R); naive_solver.
Proof. intros ??? Has; apply Has; apply principal_inj_related; auto. Qed. Qed.
#[export] Instance principal_inj {S} `{!Reflexive R} `{!AntiSymm S R} :
Inj S () (principal R).
Proof. intros ???. apply principal_inj_general => //. apply: anti_symm. Qed.
End mra_over_rel.
End mra_over_rel. End mra_over_rel.
(* Specialize [mra_over_rel] to equality. Only [principal_inj] seems generally useful. *) Global Instance principal_inj {A} {R : relation A} :
Global Instance principal_inj `{R : relation A} `{!Reflexive R} `{!AntiSymm (=) R} : Reflexive R
Inj (=) () (principal R) := mra_over_rel.principal_inj. AntiSymm (=) R
Inj (=) (≡@{mra R}) (principal) | 0. (* Lower cost than [principal_inj] *)
(* Might be useful if the type of elements is an OFE. *) Proof. intros. by apply (principal_rel_inj (=)). Qed.
Section mra_over_ofe.
Context {A : ofe} {R : relation A}. Global Instance principal_proper `{Equiv A} {R : relation A} :
Implicit Types a b : A. Reflexive (≡@{A})
Implicit Types x y : mra R. Proper (() ==> () ==> iff) R
Proper (() ==> (≡@{mra R})) (principal).
Import mra_over_rel. Proof. intros. by apply (principal_rel_proper ()). Qed.
Global Instance principal_proper Global Instance principal_equiv_inj `{Equiv A} {R : relation A} :
`{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} : Reflexive R
Proper (() ==> ()) (principal R) := ne_proper _. AntiSymm () R
Inj () (≡@{mra R}) (principal) | 1.
(* TODO: Useful? Clients should rather call equiv_dist. *) Proof. intros. by apply (principal_rel_inj ()). Qed.
Lemma principal_injN `{!Reflexive R} {Has : AntiSymm () R} n :
Inj (dist n) () (principal R).
Proof. intros x y Hxy%(inj _). by apply equiv_dist. Qed.
End mra_over_ofe.
(** 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 Hp.
- exact: principal_injN.
- apply: mra_over_rel.principal_rel_proper Hp.
Qed.
End monotone.
End upred. End upred.
"mra_test_eq"
: string
1 goal
X, Y : gset nat
H : X = Y
============================
X = Y
Require Import iris.unstable.algebra.monotone. From stdpp Require Import propset gmap strings.
From iris.unstable.algebra Require Import monotone.
Section test_mra_over_eq. Unset Mangle Names.
Context {A : Type} {R : relation A}.
Context `{!Reflexive R} {Has : AntiSymm (=) R}.
Implicit Types a b : A. Notation gset_mra K:= (mra (⊆@{gset K})).
Implicit Types x y : mra R.
Lemma test1 a b : principal R a principal R b a = b. (* Check if we indeed get [=], i.e., the right [Inj] instance is used. *)
Proof. Check "mra_test_eq".
by intros ?%(inj _). Lemma mra_test_eq X Y : principal X ≡@{gset_mra nat} principal Y X = Y.
Qed. Proof. intros ?%(inj _). Show. done. Qed.
End test_mra_over_eq. Notation propset_mra K := (mra (⊆@{propset K})).
Section test_mra_over_ofe. Lemma mra_test_equiv X Y : principal X ≡@{propset_mra nat} principal Y X Y.
Context {A : ofe} {R : relation A}. Proof. intros ?%(inj _). done. Qed.
Implicit Types a b : A.
Implicit Types x y : mra R.
Import mra_over_rel.
Context `{!Reflexive R} {Has : AntiSymm () R}.
Lemma test a b : principal R a principal R b a b.
Proof.
by intros ?%(inj _).
Qed.
Lemma principal_ne
`{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
NonExpansive (principal R).
Proof. apply _. Abort.
Lemma principal_inj_instance :
Inj () () (principal R).
Proof. apply _. Abort.
(* Also questionable. *)
Instance principal_injN' n :
Inj (dist n) (dist n) (principal R).
Proof. apply principal_injN. Abort.
End test_mra_over_ofe.