Commit 499512ba authored by Robbert Krebbers's avatar Robbert Krebbers

Patch for std++ MR !93.

parent 066354af
......@@ -196,7 +196,7 @@ Global Instance lookup_op_homomorphism :
MonoidHomomorphism op op () (lookup i : gmap K A option A).
Proof. split; [split|]; try apply _. intros m1 m2; by rewrite lookup_op. done. Qed.
Lemma lookup_opM m1 mm2 i : (m1 ? mm2) !! i = m1 !! i (mm2 = (!! i)).
Lemma lookup_opM m1 mm2 i : (m1 ? mm2) !! i = m1 !! i (mm2 = (.!! i)).
Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
Lemma lookup_validN_Some n m i x : {n} m m !! i {n} Some x {n} x.
......
......@@ -52,7 +52,7 @@ Section gmultiset.
Global Instance gmultiset_cancelable X : Cancelable X.
Proof.
apply: discrete_cancelable=> Y Z _ ?. fold_leibniz. by apply (inj (X )).
apply: discrete_cancelable=> Y Z _ ?. fold_leibniz. by apply (inj (X .)).
Qed.
Lemma gmultiset_opM X mY : X ? mY = X default mY.
......@@ -64,7 +64,7 @@ Section gmultiset.
Lemma gmultiset_local_update X Y X' Y' : X Y' = X' Y (X,Y) ~l~> (X', Y').
Proof.
intros HXY. rewrite local_update_unital_discrete=> Z' _. intros ->%leibniz_equiv.
split; first done. apply leibniz_equiv_iff, (inj ( Y)).
split; first done. apply leibniz_equiv_iff, (inj (. Y)).
rewrite -HXY !gmultiset_op_disj_union.
by rewrite -(comm_L _ Y) (comm_L _ Y') assoc_L.
Qed.
......
......@@ -278,7 +278,7 @@ Section properties.
Local Arguments cmra_op _ !_ !_ / : simpl nomatch.
Local Arguments ucmra_op _ !_ !_ / : simpl nomatch.
Lemma list_lookup_opM l mk i : (l ? mk) !! i = l !! i (mk = (!! i)).
Lemma list_lookup_opM l mk i : (l ? mk) !! i = l !! i (mk = (.!! i)).
Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed.
Global Instance list_op_nil_l : LeftId (=) (@nil A) op.
......@@ -426,7 +426,7 @@ Section properties.
(* FIXME
Lemma list_middle_local_update l1 l2 x y ml :
x ~l~> y @ ml ≫= (!! length l1) →
x ~l~> y @ ml ≫= (.!! length l1) →
l1 ++ x :: l2 ~l~> l1 ++ y :: l2 @ ml.
Proof.
intros [Hxy Hxy']; split.
......@@ -446,7 +446,7 @@ Section properties.
rewrite !list_lookup_opM !lookup_app_r !app_length //=; lia.
Qed.
Lemma list_singleton_local_update i x y ml :
x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
x ~l~> y @ ml ≫= (.!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
*)
......
......@@ -32,7 +32,7 @@ Proof.
rewrite /cmra_update=> x x' Hx y y' Hy; split=> ? n mz ?; setoid_subst; auto.
Qed.
Lemma cmra_update_updateP x y : x ~~> y x ~~>: (y =).
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.
Proof. intros ? n mz ?; eauto. Qed.
......@@ -42,7 +42,7 @@ Proof. intros Hx Hy n mz ?. destruct (Hx n mz) as (y&?&?); naive_solver. Qed.
Lemma cmra_updateP_compose_l (Q : A Prop) x y : x ~~> y y ~~>: Q x ~~>: Q.
Proof.
rewrite cmra_update_updateP.
intros; apply cmra_updateP_compose with (y =); naive_solver.
intros; apply cmra_updateP_compose with (y =.); naive_solver.
Qed.
Lemma cmra_updateP_weaken (P Q : A Prop) x :
x ~~>: P ( y, P y Q y) x ~~>: Q.
......
......@@ -55,7 +55,7 @@ Proof.
Qed.
Lemma bupd_ownM_update x y : x ~~> y uPred_ownM x |==> uPred_ownM y.
Proof.
intros; rewrite (bupd_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
intros; rewrite (bupd_ownM_updateP _ (y =.)); last by apply cmra_update_updateP.
by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
Qed.
......
......@@ -220,7 +220,7 @@ Qed.
Lemma box_empty E f P :
N E
map_Forall (λ _, (true =)) f
map_Forall (λ _, (true =.)) f
box N f P ={E}= P box N (const false <$> f) P.
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
......
......@@ -53,7 +53,7 @@ Qed.
Lemma inv_alloc N E P : P ={E}= inv N P.
Proof.
rewrite inv_eq /inv_def uPred_fupd_eq. iIntros "HP [Hw $]".
iMod (ownI_alloc ( (N : coPset)) P with "[$HP $Hw]")
iMod (ownI_alloc (. (N : coPset)) P with "[$HP $Hw]")
as (i ?) "[$ ?]"; auto using fresh_inv_name.
do 2 iModIntro. iExists i, P. rewrite -(iff_refl True%I). auto.
Qed.
......@@ -62,7 +62,7 @@ Lemma inv_alloc_open N E P :
N E (|={E, E∖↑N}=> inv N P (P ={E∖↑N, E}= True))%I.
Proof.
rewrite inv_eq /inv_def uPred_fupd_eq. iIntros (Sub) "[Hw HE]".
iMod (ownI_alloc_open ( (N : coPset)) P with "Hw")
iMod (ownI_alloc_open (. (N : coPset)) P with "Hw")
as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
iAssert (ownE {[i]} ownE ( N {[i]}) ownE (E N))%I
with "[HE]" as "(HEi & HEN\i & HE\N)".
......
......@@ -185,7 +185,7 @@ Qed.
Lemma own_update γ a a' : a ~~> a' own γ a == own γ a'.
Proof.
intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
intros; rewrite (own_updateP (a' =.)); last by apply cmra_update_updateP.
by apply bupd_mono, exist_elim=> a''; apply pure_elim_l=> ->.
Qed.
Lemma own_update_2 γ a1 a2 a' :
......
......@@ -657,7 +657,7 @@ Inductive head_step : expr → state → list observation → expr → state →
p σ.(used_proph_id)
head_step NewProph σ
[]
(Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ) σ)
(Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} .) σ)
[]
| ResolveS p v e σ w σ' κs ts :
head_step e σ κs (Val v) σ' ts
......@@ -698,7 +698,7 @@ Qed.
Lemma new_proph_id_fresh σ :
let p := fresh σ.(used_proph_id) in
head_step NewProph σ [] (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ) σ) [].
head_step NewProph σ [] (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} .) σ) [].
Proof. constructor. apply is_fresh. Qed.
Lemma heap_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
......
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