Commit 4a3a6cc7 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump stdpp/Iris.

parent 1dfbaa66
Pipeline #20685 passed with stage
in 14 minutes and 27 seconds
......@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "dev.2019-08-13.5.c1d6ef7f") | (= "dev") }
"coq-iris" { (= "dev.2019-09-20.0.b958d569") | (= "dev") }
]
......@@ -184,7 +184,7 @@ Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types x y : A.
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.
......@@ -341,7 +341,7 @@ Section freshness.
End freshness.
Lemma insert_local_update m i x y mf :
x ~l~> y @ mf = (!! i) <[i:=x]>m ~l~> <[i:=y]>m @ mf.
x ~l~> y @ mf = (.!! i) <[i:=x]>m ~l~> <[i:=y]>m @ mf.
Proof.
intros [Hxy Hxy']; split.
- intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
......@@ -354,7 +354,7 @@ Proof.
Qed.
Lemma singleton_local_update i x y mf :
x ~l~> y @ mf = (!! i) {[ i := x ]} ~l~> {[ i := y ]} @ mf.
x ~l~> y @ mf = (.!! i) {[ i := x ]} ~l~> {[ i := y ]} @ mf.
Proof. apply insert_local_update. Qed.
Lemma alloc_singleton_local_update m i x mf :
......@@ -369,7 +369,7 @@ Proof.
Qed.
Lemma alloc_unit_singleton_local_update i x mf :
mf = (!! i) = None x ~l~> {[ i := x ]} @ mf.
mf = (.!! i) = None x ~l~> {[ i := x ]} @ mf.
Proof.
intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi.
Qed.
......
......@@ -235,7 +235,7 @@ Section properties.
Local Arguments op _ _ !_ !_ / : simpl nomatch.
Local Arguments cmra_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.
Lemma list_op_app l1 l2 l3 :
......@@ -332,7 +332,7 @@ Section properties.
Qed.
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.
......@@ -353,7 +353,7 @@ Section properties.
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.
End properties.
......
......@@ -42,7 +42,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.
......@@ -52,7 +52,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.
......
......@@ -133,7 +133,7 @@ Qed.
Lemma own_update γ a a' E : a ~~> a' own γ a ={E}=> 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 pvs_mono, exist_elim=> a''; apply pure_elim_l=> ->.
Qed.
End global.
......@@ -224,7 +224,7 @@ Qed.
Lemma owne_update a a' E : a ~~> a' owne a (|={E}=> owne a').
Proof.
intros; rewrite (owne_updateP (a' =)); last by apply cmra_update_updateP.
intros; rewrite (owne_updateP (a' =.)); last by apply cmra_update_updateP.
by apply pvs_mono, exist_elim=> a''; apply pure_elim_l=> ->.
Qed.
......
......@@ -258,7 +258,7 @@ Proof. auto using pvs_mask_frame'. Qed.
Lemma pvs_ownG_update E m m' : m ~~> m' ownG m ={E}=> ownG m'.
Proof.
intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
intros; rewrite (pvs_ownG_updateP E _ (m' =.)); last by apply cmra_update_updateP.
by apply pvs_mono, uPred.exist_elim=> m''; apply pure_elim_l=> ->.
Qed.
......
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