Commit 7e480ad4 authored by Robbert Krebbers's avatar Robbert Krebbers

Move local updates to separate file.

parent a314151d
Pipeline #2374 failed with stage
......@@ -59,6 +59,7 @@ algebra/frac.v
algebra/csum.v
algebra/list.v
algebra/updates.v
algebra/local_updates.v
algebra/gset.v
algebra/coPset.v
program_logic/model.v
......
From iris.algebra Require Export excl updates.
From iris.algebra Require Import upred.
From iris.algebra Require Export excl local_updates.
From iris.algebra Require Import upred updates.
Local Arguments valid _ _ !_ /.
Local Arguments validN _ _ _ !_ /.
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates.
From iris.algebra Require Import updates local_updates.
From iris.prelude Require Export collections coPset.
(** This is pretty much the same as algebra/gset, but I was not able to
......
From iris.algebra Require Export cmra updates.
From iris.algebra Require Import upred.
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred updates local_updates.
Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_ /.
Local Arguments validN _ _ _ !_ /.
......
From iris.algebra Require Export cmra updates.
From iris.algebra Require Export cmra.
From iris.prelude Require Export gmap.
From iris.algebra Require Import upred.
From iris.algebra Require Import upred updates local_updates.
Section cofe.
Context `{Countable K} {A : cofeT}.
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates.
From iris.algebra Require Import updates local_updates.
From iris.prelude Require Export collections gmap.
Inductive gset_disj K `{Countable K} :=
......
From iris.algebra Require Export cmra updates.
From iris.algebra Require Export cmra.
From iris.prelude Require Export list.
From iris.algebra Require Import upred.
From iris.algebra Require Import upred updates local_updates.
Section cofe.
Context {A : cofeT}.
......
From iris.algebra Require Export cmra.
(** * Local updates *)
Record local_update {A : cmraT} (mz : option A) (x y : A) := {
local_update_valid n : {n} (x ? mz) {n} (y ? mz);
local_update_go n mz' :
{n} (x ? mz) x ? mz {n} x ? mz' y ? mz {n} y ? mz'
}.
Notation "x ~l~> y @ mz" := (local_update mz x y) (at level 70).
Instance: Params (@local_update) 1.
Section updates.
Context {A : cmraT}.
Implicit Types x y : A.
Global Instance local_update_proper :
Proper (() ==> () ==> () ==> iff) (@local_update A).
Proof.
cut (Proper (() ==> () ==> () ==> impl) (@local_update A)).
{ intros Hproper; split; by apply Hproper. }
intros mz mz' Hmz x x' Hx y y' Hy [Hv Hup]; constructor; setoid_subst; auto.
Qed.
Global Instance local_update_preorder mz : PreOrder (@local_update A mz).
Proof.
split.
- intros x; by split.
- intros x1 x2 x3 [??] [??]; split; eauto.
Qed.
Lemma exclusive_local_update `{!Exclusive x} y mz : y x ~l~> y @ mz.
Proof.
split; intros n.
- move=> /exclusiveN_opM ->. by apply cmra_valid_validN.
- intros mz' ? Hmz.
by rewrite (exclusiveN_opM n x mz) // (exclusiveN_opM n x mz') -?Hmz.
Qed.
Lemma op_local_update x1 x2 y mz :
x1 ~l~> x2 @ Some (y ? mz) x1 y ~l~> x2 y @ mz.
Proof.
intros [Hv1 H1]; split.
- intros n. rewrite !cmra_opM_assoc. move=> /Hv1 /=; auto.
- intros n mz'. rewrite !cmra_opM_assoc. move=> Hv /(H1 _ (Some _) Hv) /=; auto.
Qed.
Lemma alloc_local_update x y mz :
( n, {n} (x ? mz) {n} (x y ? mz)) x ~l~> x y @ mz.
Proof.
split; first done.
intros n mz' _. by rewrite !(comm _ x) !cmra_opM_assoc=> ->.
Qed.
Lemma local_update_total `{CMRADiscrete A} x y mz :
x ~l~> y @ mz
( (x ? mz) (y ? mz))
( mz', (x ? mz) x ? mz x ? mz' y ? mz y ? mz').
Proof.
split.
- destruct 1. split; intros until 0;
rewrite !(cmra_discrete_valid_iff 0) ?(timeless_iff 0); auto.
- intros [??]; split; intros until 0;
rewrite -!cmra_discrete_valid_iff -?timeless_iff; auto.
Qed.
End updates.
(** * Product *)
Lemma prod_local_update {A B : cmraT} (x y : A * B) mz :
x.1 ~l~> y.1 @ fst <$> mz x.2 ~l~> y.2 @ snd <$> mz
x ~l~> y @ mz.
Proof.
intros [Hv1 H1] [Hv2 H2]; split.
- intros n [??]; destruct mz; split; auto.
- intros n mz' [??] [??].
specialize (H1 n (fst <$> mz')); specialize (H2 n (snd <$> mz')).
destruct mz, mz'; split; naive_solver.
Qed.
(** * Option *)
Lemma option_local_update {A : cmraT} (x y : A) mmz :
x ~l~> y @ mjoin mmz
Some x ~l~> Some y @ mmz.
Proof.
intros [Hv H]; split; first destruct mmz as [[?|]|]; auto.
intros n mmz'. specialize (H n (mjoin mmz')).
destruct mmz as [[]|], mmz' as [[]|]; inversion_clear 2; constructor; auto.
Qed.
(** * Natural numbers *)
Lemma nat_local_update (x y : nat) mz : x ~l~> y @ mz.
Proof.
split; first done.
compute -[plus]; destruct mz as [z|]; intros n [z'|]; lia.
Qed.
Lemma mnat_local_update (x y : mnat) mz : x y x ~l~> y @ mz.
Proof.
split; first done.
compute -[max]; destruct mz as [z|]; intros n [z'|]; lia.
Qed.
From iris.algebra Require Export cmra.
(** * Local updates *)
Record local_update {A : cmraT} (mz : option A) (x y : A) := {
local_update_valid n : {n} (x ? mz) {n} (y ? mz);
local_update_go n mz' :
{n} (x ? mz) x ? mz {n} x ? mz' y ? mz {n} y ? mz'
}.
Notation "x ~l~> y @ mz" := (local_update mz x y) (at level 70).
Instance: Params (@local_update) 1.
(** * Frame preserving updates *)
(* This quantifies over [option A] for the frame. That is necessary to
make the following hold:
......@@ -24,18 +15,10 @@ Definition cmra_update {A : cmraT} (x y : A) := ∀ n mz,
Infix "~~>" := cmra_update (at level 70).
Instance: Params (@cmra_update) 1.
(** ** CMRAs *)
Section cmra.
Section updates.
Context {A : cmraT}.
Implicit Types x y : A.
Global Instance local_update_proper :
Proper (() ==> () ==> () ==> iff) (@local_update A).
Proof.
cut (Proper (() ==> () ==> () ==> impl) (@local_update A)).
{ intros Hproper; split; by apply Hproper. }
intros mz mz' Hmz x x' Hx y y' Hy [Hv Hup]; constructor; setoid_subst; auto.
Qed.
Global Instance cmra_updateP_proper :
Proper (() ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
Proof.
......@@ -48,51 +31,6 @@ Proof.
rewrite /cmra_update=> x x' Hx y y' Hy; split=> ? n mz ?; setoid_subst; auto.
Qed.
(** ** Local updates *)
Global Instance local_update_preorder mz : PreOrder (@local_update A mz).
Proof.
split.
- intros x; by split.
- intros x1 x2 x3 [??] [??]; split; eauto.
Qed.
Lemma exclusive_local_update `{!Exclusive x} y mz : y x ~l~> y @ mz.
Proof.
split; intros n.
- move=> /exclusiveN_opM ->. by apply cmra_valid_validN.
- intros mz' ? Hmz.
by rewrite (exclusiveN_opM n x mz) // (exclusiveN_opM n x mz') -?Hmz.
Qed.
Lemma op_local_update x1 x2 y mz :
x1 ~l~> x2 @ Some (y ? mz) x1 y ~l~> x2 y @ mz.
Proof.
intros [Hv1 H1]; split.
- intros n. rewrite !cmra_opM_assoc. move=> /Hv1 /=; auto.
- intros n mz'. rewrite !cmra_opM_assoc. move=> Hv /(H1 _ (Some _) Hv) /=; auto.
Qed.
Lemma alloc_local_update x y mz :
( n, {n} (x ? mz) {n} (x y ? mz)) x ~l~> x y @ mz.
Proof.
split; first done.
intros n mz' _. by rewrite !(comm _ x) !cmra_opM_assoc=> ->.
Qed.
(** ** Local updates for discrete CMRAs *)
Lemma local_update_total `{CMRADiscrete A} x y mz :
x ~l~> y @ mz
( (x ? mz) (y ? mz))
( mz', (x ? mz) x ? mz x ? mz' y ? mz y ? mz').
Proof.
split.
- destruct 1. split; intros until 0;
rewrite !(cmra_discrete_valid_iff 0) ?(timeless_iff 0); auto.
- intros [??]; split; intros until 0;
rewrite -!cmra_discrete_valid_iff -?timeless_iff; auto.
Qed.
(** ** Frame preserving updates *)
Lemma cmra_update_updateP x y : x ~~> y x ~~>: (y =).
Proof. split=> Hup n z ?; eauto. destruct (Hup n z) as (?&<-&?); auto. Qed.
Lemma cmra_updateP_id (P : A Prop) x : P x x ~~>: P.
......@@ -176,7 +114,7 @@ Section total_updates.
naive_solver eauto using 0.
Qed.
End total_updates.
End cmra.
End updates.
(** * Transport *)
Section cmra_transport.
......@@ -195,17 +133,6 @@ Section prod.
Context {A B : cmraT}.
Implicit Types x : A * B.
Lemma prod_local_update x y mz :
x.1 ~l~> y.1 @ fst <$> mz x.2 ~l~> y.2 @ snd <$> mz
x ~l~> y @ mz.
Proof.
intros [Hv1 H1] [Hv2 H2]; split.
- intros n [??]; destruct mz; split; auto.
- intros n mz' [??] [??].
specialize (H1 n (fst <$> mz')); specialize (H2 n (snd <$> mz')).
destruct mz, mz'; split; naive_solver.
Qed.
Lemma prod_updateP P1 P2 (Q : A * B Prop) x :
x.1 ~~>: P1 x.2 ~~>: P2 ( a b, P1 a P2 b Q (a,b)) x ~~>: Q.
Proof.
......@@ -229,15 +156,6 @@ Section option.
Context {A : cmraT}.
Implicit Types x y : A.
Lemma option_local_update x y mmz :
x ~l~> y @ mjoin mmz
Some x ~l~> Some y @ mmz.
Proof.
intros [Hv H]; split; first destruct mmz as [[?|]|]; auto.
intros n mmz'. specialize (H n (mjoin mmz')).
destruct mmz as [[]|], mmz' as [[]|]; inversion_clear 2; constructor; auto.
Qed.
Lemma option_updateP (P : A Prop) (Q : option A Prop) x :
x ~~>: P ( y, P y Q (Some y)) Some x ~~>: Q.
Proof.
......@@ -252,16 +170,3 @@ Section option.
Lemma option_update x y : x ~~> y Some x ~~> Some y.
Proof. rewrite !cmra_update_updateP; eauto using option_updateP with subst. Qed.
End option.
(** * Natural numbers *)
Lemma nat_local_update (x y : nat) mz : x ~l~> y @ mz.
Proof.
split; first done.
compute -[plus]; destruct mz as [z|]; intros n [z'|]; lia.
Qed.
Lemma mnat_local_update (x y : mnat) mz : x y x ~l~> y @ mz.
Proof.
split; first done.
compute -[max]; destruct mz as [z|]; intros n [z'|]; lia.
Qed.
From iris.prelude Require Export coPset.
From iris.algebra Require Export upred_big_op.
From iris.algebra Require Export upred_big_op updates.
From iris.program_logic Require Export model.
From iris.program_logic Require Import ownership wsat.
Local Hint Extern 10 (_ _) => omega.
......
From iris.prelude Require Export coPset.
From iris.program_logic Require Export model.
From iris.algebra Require Export cmra_big_op cmra_tactics.
From iris.algebra Require Import updates.
Local Hint Extern 10 (_ _) => omega.
Local Hint Extern 10 ({_} _) => solve_validN.
Local Hint Extern 1 ({_} gst _) => apply gst_validN.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment