Commit d819164f authored by Ralf Jung's avatar Ralf Jung

bump std++; use \sqsubseteq for stuckness_le

parent c5e25a27
...@@ -12,5 +12,5 @@ remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"] ...@@ -12,5 +12,5 @@ remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [ depends: [
"coq" { (>= "8.6.1" & < "8.8~") | (= "dev") } "coq" { (>= "8.6.1" & < "8.8~") | (= "dev") }
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
"coq-stdpp" { (= "dev.2017-11-29.1") | (= "dev") } "coq-stdpp" { (= "dev.2017-12-04.1") | (= "dev") }
] ]
...@@ -58,7 +58,7 @@ Lemma ht_mono s E P P' Φ Φ' e : ...@@ -58,7 +58,7 @@ Lemma ht_mono s E P P' Φ Φ' e :
(P P') ( v, Φ' v Φ v) {{ P' }} e @ s; E {{ Φ' }} {{ P }} e @ s; E {{ Φ }}. (P P') ( v, Φ' v Φ v) {{ P' }} e @ s; E {{ Φ' }} {{ P }} e @ s; E {{ Φ }}.
Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed. Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
Lemma ht_stuck_mono s1 s2 E P Φ e : Lemma ht_stuck_mono s1 s2 E P Φ e :
stuckness_le s1 s2 {{ P }} e @ s1; E {{ Φ }} {{ P }} e @ s2; E {{ Φ }}. s1 s2 {{ P }} e @ s1; E {{ Φ }} {{ P }} e @ s2; E {{ Φ }}.
Proof. by intros; apply persistently_mono, wand_mono, wp_stuck_mono. Qed. Proof. by intros; apply persistently_mono, wand_mono, wp_stuck_mono. Qed.
Global Instance ht_mono' s E : Global Instance ht_mono' s E :
Proper (flip () ==> eq ==> pointwise_relation _ () ==> ()) (ht s E). Proper (flip () ==> eq ==> pointwise_relation _ () ==> ()) (ht s E).
......
...@@ -22,6 +22,7 @@ Instance: PreOrder stuckness_le. ...@@ -22,6 +22,7 @@ Instance: PreOrder stuckness_le.
Proof. Proof.
split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3. split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3.
Qed. Qed.
Instance: SqSubsetEq stuckness := stuckness_le.
Definition stuckness_to_atomicity (s : stuckness) : atomicity := Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
if s is maybe_stuck then strongly_atomic else weakly_atomic. if s is maybe_stuck then strongly_atomic else weakly_atomic.
...@@ -315,7 +316,7 @@ Proof. ...@@ -315,7 +316,7 @@ Proof.
iIntros "{$H}" (v) "?". by iApply HΦ. iIntros "{$H}" (v) "?". by iApply HΦ.
Qed. Qed.
Lemma wp_stuck_mono s1 s2 E e Φ : Lemma wp_stuck_mono s1 s2 E e Φ :
stuckness_le s1 s2 WP e @ s1; E {{ Φ }} WP e @ s2; E {{ Φ }}. s1 s2 WP e @ s1; E {{ Φ }} WP e @ s2; E {{ Φ }}.
Proof. case: s1; case: s2 => // _. exact: wp_stuck_weaken. Qed. Proof. case: s1; case: s2 => // _. exact: wp_stuck_weaken. Qed.
Lemma wp_mask_mono s E1 E2 e Φ : E1 E2 WP e @ s; E1 {{ Φ }} WP e @ s; E2 {{ Φ }}. Lemma wp_mask_mono s E1 E2 e Φ : E1 E2 WP e @ s; E1 {{ Φ }} WP e @ s; E2 {{ Φ }}.
Proof. iIntros (?) "H"; iApply (wp_strong_mono s E1 E2); auto. iFrame; eauto. Qed. Proof. iIntros (?) "H"; iApply (wp_strong_mono s E1 E2); auto. iFrame; eauto. 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