diff --git a/opam b/opam
index 7d7d4827bb57c4dc66333305faca3050e1e2453a..83b7b9d2ba48c405e7b4cf9e5f67b0064c9ccb97 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
depends: [
- "coq-iris" { (= "branch.gen_proofmode.2018-01-25.2") | (= "dev") }
+ "coq-iris" { (= "branch.gen_proofmode.2018-02-06.3") | (= "dev") }
]
diff --git a/theories/arith.v b/theories/arith.v
index 331d38d33b11400ac0de093231c13512b748379c..05e074ff5baaf20ea414b7dee41badbb0dbc354f 100644
--- a/theories/arith.v
+++ b/theories/arith.v
@@ -1,7 +1,9 @@
-From mathcomp Require Import ssreflect.
+From Coq.ssr Require Import ssreflect.
From Coq Require Import ZArith.
From Coq Require Import Psatz.
+Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
+
Ltac lia' :=
let rec go :=
try match goal with
diff --git a/theories/blocks.v b/theories/blocks.v
index 9b3226c120be11e1843176e0ceab11cf7e0df402..42377c16a734e860cb14ed0d84e611b80311625e 100644
--- a/theories/blocks.v
+++ b/theories/blocks.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import ssreflect.
From igps Require Import blocks_generic types lang.
From igps.base Require Import ghosts.
diff --git a/theories/blocks_generic.v b/theories/blocks_generic.v
index e15bd7b5b87c1c7e20600c7adf37d961c8722c19..bc13532baf1cbaa3e7711a1908e72650c90895a6 100644
--- a/theories/blocks_generic.v
+++ b/theories/blocks_generic.v
@@ -1,5 +1,4 @@
Require Import Setoid.
-From mathcomp Require Import ssreflect.
From stdpp Require Import gmap.
From iris.base_logic Require Import lib.iprop.
From iris.bi Require Import big_op.
diff --git a/theories/escrows.v b/theories/escrows.v
index 7b7d25389632ff53b0d63719d517abe45e492941..e457d11c30527a7bc05a3a22d64afd792722ba8e 100644
--- a/theories/escrows.v
+++ b/theories/escrows.v
@@ -24,13 +24,13 @@ Section Escrows.
Global Instance exchange_persistent P Q β :
Persistent (exchange P Q β).
- Proof. unfold exchange, tc_opaque. apply _. Qed.
+ Proof. rewrite /exchange /=. apply _. Qed.
Global Instance exchange_ne n: Proper (dist_later n ==> dist_later n ==> (≡) ==> dist n) exchange.
Proof. solve_contractive. Qed.
Definition escrow P Q : vProp Σ :=
- (∃ β, exchange (monPred_ex P) Q β)%I.
+ (∃ β, exchange (∃ᵢ P) Q β)%I.
Global Instance escrow_proper : Proper ((≡) ==> (≡) ==> (≡)) escrow.
Proof. intros ?? H ?? H2. apply: bi.exist_proper => ?. by rewrite H H2. Qed.
@@ -52,16 +52,16 @@ Section proof.
Lemma exchange_in P Q V:
[ex P ↠Q] V ⊢ monPred_in V.
- Proof. rewrite /exchange /tc_opaque. iIntros "[$ _]". Qed.
+ Proof. rewrite /exchange /=. iIntros "[$ _]". Qed.
Lemma exchange_comm P Q V :
[ex P ↠Q] V ⊣⊢ [ex Q ↠P] V.
- Proof. unfold exchange, tc_opaque. by rewrite (comm bi_or). Qed.
+ Proof. rewrite /exchange /=. by rewrite (comm bi_or). Qed.
Lemma exchange_alloc P Q: (▷ (P ∨ Q) ={↑escrowN}=∗ ∃ V, [ex P ↠Q] V)%I.
Proof.
iStartProof (uPred _). iIntros (V) "P".
- iExists V. unfold exchange, tc_opaque. iSplitR; [done|].
+ iExists V. rewrite /exchange /=. iSplitR; [done|].
iApply (inv_alloc escrowN (↑escrowN) (P _ ∨ Q _)%I with "P").
Qed.
@@ -77,7 +77,7 @@ Section proof.
(P ∗ P → False) ⊢ ([ex P0 ↠Q0] V ∗ ▷ ⎡P V⎤ ={↑escrowN}=∗ ▷ ⎡Q V⎤).
Proof.
intros P Q. iStartProof (uPred _). iIntros (V') "ND".
- rewrite /exchange /tc_opaque. iIntros (V0 ?) "(#[% Inv] & P) /=".
+ rewrite /exchange /=. iIntros (V0 ?) "(#[% Inv] & P) /=".
iAssert (inv escrowN (monPred_at P V ∨ monPred_at Q V))%I with "[Inv]" as "#Inv'".
{ destruct b; subst P Q; auto. by rewrite bi.or_comm. }
iClear "Inv". iInv escrowN as "Inv" "HClose".
@@ -104,7 +104,7 @@ Section proof.
{ destruct b; auto. by rewrite exchange_comm. }
iDestruct (exchange_in with "Ex") as "aSeen".
iDestruct (exchange_elim_l with "ND [$Ex' $P]") as ">Q".
- iModIntro. iNext. iApply monPred_in_elim. auto.
+ iModIntro. iNext. iApply monPred_in_elim; auto.
Qed.
Lemma exchange_left P Q V:
@@ -124,13 +124,13 @@ Section proof.
Proof. by apply exchange_alloc_r. Qed.
Lemma escrow_apply_obj P Q:
- (P ∗ P → False) ⊢ ([es P ⇠Q] ∗ ▷ ▲P ={↑escrowN}=∗ ▷ Q).
+ (P ∗ P → False) ⊢ ([es P ⇠Q] ∗ ▷ ∃ᵢ P ={↑escrowN}=∗ ▷ Q).
Proof.
iStartProof (uPred _). iIntros (V0) "ND".
- rewrite /escrow /exchange /tc_opaque /=. iIntros (V ?) "(Esc & oP)".
+ rewrite /escrow /exchange /=. iIntros (V ?) "(Esc & oP)".
iDestruct "Esc" as (V') "[% ?]".
iInv escrowN as "Inv" "HClose".
- iAssert (▷ monPred_at Q V' ∗ ▷ (monPred_at (▲P)%I V' ∨ monPred_at Q V'))%I with "[ND oP Inv]" as "[Q Inv]".
+ iAssert (▷ Q V' ∗ ▷ ((∃ᵢ P)%I V' ∨ Q V'))%I with "[ND oP Inv]" as "[Q Inv]".
{ iNext. iDestruct "Inv" as "[Inv|$]".
- iExFalso.
iDestruct "oP" as (V1) "P1".
diff --git a/theories/examples/circ_buffer.v b/theories/examples/circ_buffer.v
index 299726ccae982158abbc4cb2afa2ab4ab73f4729..8bcf493d9414e84319943a4e5eee4740b160f706 100644
--- a/theories/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -287,7 +287,7 @@ Section CircBuffer.
wp_lam. wp_bind ([_]_at)%E. wp_op.
iApply (GPS_SW_Read_ex with "[$kI $pW]"); [done|done|..].
- { rewrite /monPred_all /tc_opaque. iIntros (????) "!> #$ //". }
+ { rewrite /monPred_absolutely /=. iIntros (????) "!> #$ //". }
iNext. iIntros (w) "(pW & #CEs)".
iDestruct "CEs" as "(% & CEs)".
@@ -299,7 +299,7 @@ Section CircBuffer.
with "[$kI $cR]"); [done|done|..].
{ iNext. iSplitL.
- iIntros (?). iIntros "_". iLeft. by iIntros (?) "(? & _)".
- - rewrite /monPred_all /tc_opaque. iIntros (?????) "[? #$] //". }
+ - rewrite /monPred_absolutely /=. iIntros (?????) "[? #$] //". }
iNext. iIntros (j r) "(% & #cR2 & #PEs)".
iDestruct "PEs" as "(% & PEs)".
@@ -393,7 +393,7 @@ Section CircBuffer.
{ iNext. iSplitL.
- iIntros (?). iIntros (?). iLeft.
iIntros (?) "(? & _)". by auto.
- - rewrite /monPred_all /tc_opaque. iIntros (?????) "[? #$] //". }
+ - rewrite /monPred_absolutely /=. iIntros (?????) "[? #$] //". }
iNext. iIntros (i w) "(% & pR & #CEs)".
iDestruct "CEs" as "(% & CEs)".
@@ -402,7 +402,7 @@ Section CircBuffer.
iApply (GPS_SW_Read_ex
with "[$kI $cW]"); [done|done|..].
- { rewrite /monPred_all /tc_opaque. iIntros (????) "!> #$ //". }
+ { rewrite /monPred_absolutely /=. iIntros (????) "!> #$ //". }
iNext. iIntros (r) "(cW & #PEs)".
iDestruct "PEs" as "(% & PEs)".
diff --git a/theories/examples/hashtable.v b/theories/examples/hashtable.v
index edac0e60c6c8acaf2e6d3552456b249c0287a610..c1b999deee55f994d4ed3a6bee48bfe9639fcb80 100644
--- a/theories/examples/hashtable.v
+++ b/theories/examples/hashtable.v
@@ -601,7 +601,7 @@ Section proof.
iFrame.
iApply ("HP" with "HH").
- iSplit; [|iSplit; auto].
- iNext; iApply objective_all.
+ iNext; iApply absolute_absolutely.
iIntros (? ?) "[? #?]"; iModIntro; iFrame "#". }
iNext. iIntros (s' k') "(% & #Hk' & % & Hpost)"; subst.
iMod "Hpost"; iModIntro.
@@ -670,7 +670,7 @@ Section proof.
eapply Hzero; auto.
eapply lookup_weaken; eauto.
+ iSplit; last auto.
- iNext; iApply objective_all.
+ iNext; iApply absolute_absolutely.
iIntros (? ?) "[? #?]"; iModIntro; iFrame "#". }
iNext. iIntros (s' v) "[% ?]"; auto.
- rewrite bool_decide_false; last done.
@@ -960,7 +960,7 @@ Section proof.
iFrame.
by iMod ("HP" with "HH"); iFrame.
- iSplit; [|iSplit; auto].
- iNext; iApply objective_all.
+ iNext; iApply absolute_absolutely.
iIntros (? ?) "[? #?]"; iModIntro; iFrame "#". }
iNext. iIntros (s' k') "(% & % & Hpost)"; subst.
iMod "Hpost"; iModIntro.
@@ -1062,7 +1062,7 @@ Section proof.
iMod "Hsnap'" as "[% ?]"; subst.
iModIntro; iSplit; [done | iFrame].
iApply "HP"; iFrame; iSplit; done.
- + iNext; iApply objective_all.
+ + iNext; iApply absolute_absolutely.
iIntros (? ?) "[? #?]"; iModIntro; iFrame "#".
+ iFrame; done. }
iNext. iIntros (? b k') "(% & Hpost)".
@@ -1119,7 +1119,7 @@ Section proof.
+ iPoseProof (and_elim_l with "Hrest") as "HP".
by iMod ("HP" with "HH"); iFrame.
- iSplit; [|iSplit; auto].
- iNext; iApply objective_all.
+ iNext; iApply absolute_absolutely.
iIntros (? ?) "[? #?]"; iModIntro; iFrame "#". }
iNext. iIntros (? k'') "(% & % & Hsnap & Hpost)"; subst.
destruct H5; try contradiction; subst k''.
@@ -1378,7 +1378,7 @@ Section proof.
iSplit; last by rewrite (nth_lookup_Some _ _ _ _ H0); auto.
iPureIntro; do 2 eexists; eauto; done.
+ rewrite Hx; auto.
- - iNext; iApply objective_all.
+ - iNext; iApply absolute_absolutely.
iIntros (? ?) "[? #?]"; iModIntro; iFrame "#".
- iFrame; done. }
iNext. iIntros (? b ?) "[% Hpost]".
@@ -1781,15 +1781,15 @@ Section proof.
try (apply Permutation_map; symmetry; eassumption); done.
Qed.
- Instance hashtable_inv_objective : Objective (hashtable_inv gh g lgk lgv H).
+ Instance hashtable_inv_absolute : Absolute (hashtable_inv gh g lgk lgv H).
Proof.
intros; unfold hashtable_inv.
- apply sep_objective, _.
+ apply sep_absolute, _.
unfold hashtable.
- apply exists_objective; intro.
- apply sep_objective; first apply _.
- apply sep_objective; first apply _.
- apply big_sepL_objective; intros ? (?, ?).
+ apply exists_absolute; intro.
+ apply sep_absolute; first apply _.
+ apply sep_absolute; first apply _.
+ apply big_sepL_absolute; intros ? (?, ?).
apply _.
Qed.
@@ -1871,12 +1871,12 @@ Section proof.
iExists _; iSplit; first by iCombine "Hhist Ht" as "H"; iApply "H".
iIntros "!# [>Hhist Ht]".
iMod (inv_open with "Hinv") as "[>HH Hclose]"; first auto.
- iDestruct (monPred_all_elim with "HH") as (HT) "[HH H]".
+ iDestruct (monPred_absolutely_elim with "HH") as (HT) "[HH H]".
iModIntro; iExists HT; iFrame "HH".
iSplit.
{ iIntros "HH".
iMod ("Hclose" with "[HH H]"); last by iFrame.
- iNext; iApply objective_all.
+ iNext; iApply absolute_absolutely.
iExists HT; iFrame. }
iDestruct "H" as (hr) "[% H]"; iDestruct "H" as (mr) "[% Hg]".
iIntros (v) "H"; iDestruct "H" as (b lv) "(Hentries & H & % & HH)"; iDestruct "H" as (T) "[% HA']".
@@ -1897,7 +1897,7 @@ Section proof.
destruct H5 as (? & Hb & Hadd); subst v.
iMod ("Hclose" with "[HH Hg]").
{ iNext.
- iApply objective_all.
+ iApply absolute_absolutely.
iExists (if b then map_upd HT (i + 1) lv else HT); iFrame.
iExists (hr ++ HAdd (i + 1) 1 b :: nil)%list; iSplit.
{ iPureIntro; rewrite apply_hist_app.
@@ -2043,7 +2043,7 @@ Section proof.
set (N := namespaces.ndot namespaces.nroot "N").
iMod (inv_alloc N top (∃H, hashtable_inv gh g lgk lgv H)%I with "[HH Href]") as "#Hinv".
{ iNext.
- iApply objective_all.
+ iApply absolute_absolutely.
iExists (λ _ : Z, None); iFrame.
iExists nil; iSplit; first auto.
iExists ∅; rewrite fmap_empty; auto. }
@@ -2177,8 +2177,8 @@ Section proof.
do 2 apply namespaces.ndot_preserve_disjoint_r.
apply namespaces.ndot_ne_disjoint; done. }
iMod "H"; iModIntro; auto.
- * iNext; do 2 (rewrite all_forall; iIntros (?)).
- iApply all_entails.
+ * iNext; do 2 (rewrite monPred_absolutely_forall; iIntros (?)).
+ iApply absolutely_entails.
iIntros "[? #?]"; iModIntro; iFrame "#". }
iNext; iIntros (b ?) "(% & _ & % & Hcond)"; subst.
iExists (Z.b2z b); iSplit; first auto.
@@ -2222,7 +2222,7 @@ Section proof.
{ apply namespaces.ndisj_subseteq_difference; last auto.
apply namespaces.ndot_ne_disjoint; done. }
iNext; iIntros (?) "[% Htotal]"; subst.
- iDestruct (monPred_all_elim with "Href") as (HT) "[HH Href]".
+ iDestruct (monPred_absolutely_elim with "Href") as (HT) "[HH Href]".
iDestruct "Href" as (hr) "[% Href]".
iDestruct "Href" as (mr) "[% Href]".
assert (i = 3) by omega; subst.
@@ -2235,7 +2235,7 @@ Section proof.
replace (_ â‹… _) with 1%Qp.
iPoseProof (own_valid_2 with "Href Hhist") as "%".
iMod ("Hclose" with "[HH Href]").
- { iNext; iApply objective_all.
+ { iNext; iApply absolute_absolutely.
iExists HT; iFrame; auto. }
iModIntro; iApply "Hpost".
iPureIntro.
diff --git a/theories/examples/kvnode.v b/theories/examples/kvnode.v
index 18ce452afcf874adbda27a2124f25ff989350cab..1473982bf11570d0ab85c603a613cc255aede0dc 100644
--- a/theories/examples/kvnode.v
+++ b/theories/examples/kvnode.v
@@ -488,8 +488,8 @@ Section proof.
iSplitR ""; [|iSplit].
- iNext; iIntros (s Hs).
by iLeft; iIntros (?) "[? _]".
- - iNext; do 2 (rewrite all_forall; iIntros (?)).
- iApply all_entails.
+ - iNext; do 2 (rewrite monPred_absolutely_forall; iIntros (?)).
+ iApply absolutely_entails.
iIntros "[? #?]"; iModIntro; iFrame "#".
- iSplit; first auto.
by iDestruct "node_state" as "(? & ? & ?)". }
@@ -548,8 +548,8 @@ Section proof.
destruct H1 as (_ & ? & ?).
eapply log_latest_ord; eauto.
apply fmap_nth_log_latest; eauto.
- + iNext; do 2 (rewrite all_forall; iIntros (?)).
- iApply all_entails.
+ + iNext; do 2 (rewrite monPred_absolutely_forall; iIntros (?)).
+ iApply absolutely_entails.
iIntros "[? #?]"; iModIntro; iFrame "#". }
iNext; iIntros (s d) "(% & Hdi & H)"; iDestruct "H" as (vi) "(% & #kV'')".
iApply wp_fupd.
@@ -658,8 +658,8 @@ Section proof.
specialize (X i); rewrite !lookup_fmap HL1 HL' in X; done.
+ eapply lookup_weaken; last eauto.
destruct Hlatest; done.
- - iNext; do 2 (rewrite all_forall; iIntros (?)).
- iApply all_entails.
+ - iNext; do 2 (rewrite monPred_absolutely_forall; iIntros (?)).
+ iApply absolutely_entails.
iIntros "[? #?]"; iModIntro; iFrame "#".
- iSplit; first auto.
by iDestruct "node_state" as "(? & ? & ?)". }
@@ -731,8 +731,8 @@ Section proof.
iDestruct "node_state" as "(% & kV & oL & data)".
iApply (GPS_SW_Read_ex (versionP n g) with "[$kI $kV]");
[auto | auto | ..].
- { iNext; rewrite all_forall; iIntros (?).
- iApply all_entails.
+ { iNext; rewrite monPred_absolutely_forall; iIntros (?).
+ iApply absolutely_entails.
iIntros "#?"; iModIntro; iFrame "#". }
iNext; iIntros (?) "(kV & Hv)".
rewrite versionP_eq.
diff --git a/theories/examples/message_passing.v b/theories/examples/message_passing.v
index b4a96e746f22961a4220e017533d0954ca4f0f45..73a986d6bea94495690242eaf3bc5faf0b347754 100644
--- a/theories/examples/message_passing.v
+++ b/theories/examples/message_passing.v
@@ -96,7 +96,7 @@ Section proof.
+ iSplitL.
* iNext. iIntros (?). iIntros "_".
iLeft. iIntros (?) "[YP _]". by simpl.
- * rewrite /monPred_all /tc_opaque. iIntros (?????) "!> [_ #$] //".
+ * rewrite /monPred_absolutely /=. iIntros (?????) "!> [_ #$] //".
+ iNext. iIntros (s v) "(_ & #yPRT5 & #YP)".
destruct s.
* iDestruct "YP" as "(% & XE)".
diff --git a/theories/examples/msqueue.v b/theories/examples/msqueue.v
index 8dedb7c24539d3839517909d84e4138305bb97c2..ce3b24713689db681badca56304f214cb13eecaa 100644
--- a/theories/examples/msqueue.v
+++ b/theories/examples/msqueue.v
@@ -230,7 +230,7 @@ Section MSQueue.
[done|done|..].
{ iSplitL "".
- iNext. iIntros ([] ?). iLeft. by iIntros (x) "($ & _)".
- - rewrite /monPred_all /tc_opaque. iIntros (?????) "!> [_ #$] //". }
+ - rewrite /monPred_absolutely /=. iIntros (?????) "!> [_ #$] //". }
iNext. iIntros ([] x) "(_ & _ & % & ox)".
wp_seq. wp_bind ([_]_at)%E. wp_op. wp_op.
rewrite (_ : ZplusPos 0 (Z.to_pos x) = Z.to_pos (x + 0)); last first.
@@ -251,7 +251,7 @@ Section MSQueue.
iDestruct "LinkInt" as (γ') "(_ & Link)".
iSplitL ""; first (iPureIntro; lia).
iExists γ'. subst v. iFrame "Link".
- - rewrite /monPred_all /tc_opaque. iIntros (????) "_ (_ & #$) //". }
+ - rewrite /monPred_absolutely /=. iIntros (????) "_ (_ & #$) //". }
iNext. iIntros (s n') "(% & _ & Q)".
wp_seq. wp_op; case_bool_decide.
@@ -325,7 +325,7 @@ Section MSQueue.
with "kI [P Tok od Link]");
[done|done|..].
{ iFrame "Tok Link". iSplitR "P od"; last iSplitR "P od"; last first.
- - rewrite /monPred_all /tc_opaque. iIntros "{$P $od}" (????) "!> _ (_ & #$) //".
+ - rewrite /monPred_absolutely /=. iIntros "{$P $od}" (????) "!> _ (_ & #$) //".
- iNext. iIntros (??) "(_ & _ & _ & ? & ? & _)". by iFrame.
- iNext. iIntros (s'). iIntros "(_ & LinkInt & P')".
rewrite (unf_int (Link P)).
@@ -377,7 +377,7 @@ Section MSQueue.
[done|done|..].
{ iNext. iSplitL.
- iIntros ([]) "_". iLeft. by iIntros (x) "($ & _)".
- - rewrite /monPred_all /tc_opaque. iIntros (????) "_ (_ & #$) //". }
+ - rewrite /monPred_absolutely /=. iIntros (????) "_ (_ & #$) //". }
iNext. iIntros ([] s) "(_ & oH2 & % & os)".
iDestruct "os" as (γ) "os".
@@ -408,7 +408,7 @@ Section MSQueue.
rewrite (_: Z.to_pos (Z.pos l' + 1) = ZplusPos 1 l'); last first.
{ rewrite /ZplusPos. f_equal. omega. }
iFrame "DEQ Link".
- - rewrite /monPred_all /tc_opaque. iIntros (????) "_ [_ #$] //". }
+ - rewrite /monPred_absolutely /=. iIntros (????) "_ [_ #$] //". }
iNext. iIntros (s' n) "(_ & #os & Q')".
wp_seq. wp_op. case_bool_decide.
@@ -423,7 +423,7 @@ Section MSQueue.
iApply (GPS_PP_CAS (p:=()) (Head P) True%I Q1 (λ _ _, True)%I
with "kI []"); [done|done|..].
{ iSplitL; last iSplitL; last first.
- - rewrite /monPred_all /tc_opaque. iIntros "{$oH} !>" (?????) "[_ #$] //".
+ - rewrite /monPred_absolutely /=. iIntros "{$oH} !>" (?????) "[_ #$] //".
- iNext. by iIntros (??) "_".
- iNext. iIntros ([]).
iIntros "(_ & Head & _)".
diff --git a/theories/examples/ro_test.v b/theories/examples/ro_test.v
index 9ed16d98c8b674e445350f03969b3455124ae754..0dd1a9a99ca6d46007d1bf91d414faee8c5088e2 100644
--- a/theories/examples/ro_test.v
+++ b/theories/examples/ro_test.v
@@ -24,6 +24,6 @@ Proof.
{ etrans; first apply namespaces.nclose_subseteq.
by apply namespaces.ndisj_subseteq_difference. }
iNext; iIntros (?) "[% oL']"; subst.
- iMod ("Hclose" with "[oL]"); first by iApply objective_all.
+ iMod ("Hclose" with "[oL]"); first by iApply absolute_absolutely.
iApply "Hpost"; auto.
Admitted.
\ No newline at end of file
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 6c580f0eaee690267cda4a6666e178108bcf6f3b..87e2178bdf44905dbb99aa896c0e73da0ec44285 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -654,8 +654,8 @@ Section TicketLock.
iLeft. iIntros (z). iIntros "(NSP & _)".
rewrite !(unf_int (NSP P γ)).
by iDestruct "NSP" as "($ & $)".
- - (* TODO : make iAlways able to introduce monPred_all here. *)
- rewrite /monPred_all /tc_opaque. iIntros (?????) "!> (? & #$) //". }
+ - (* TODO : make iAlways able to introduce monPred_absolutely here. *)
+ rewrite /monPred_absolutely /=. iIntros (?????) "!> (? & #$) //". }
iNext. iIntros (n z) "(% & #NSR & Q2)".
iDestruct "Q2" as "(% & #ES)".
@@ -726,7 +726,7 @@ Section TicketLock.
wp_lam. wp_bind ([_]_at)%E. wp_op.
iApply (GPS_SW_Read_ex (NSP P γ) with "[$kI $NSW]"); [done|done|..].
- { rewrite /monPred_all /tc_opaque. iIntros "!>" (????) "#$ //". }
+ { rewrite /monPred_absolutely /=. iIntros "!>" (????) "#$ //". }
iNext. iIntros (z) "(NSW & NSP)".
rewrite (unf_int (NSP P γ)).
diff --git a/theories/examples/tstack.v b/theories/examples/tstack.v
index 296ddec518f167ef2c8c016ab18176e92005b4d5..6926c86f896fa81b524e562caae5639688fc7303 100644
--- a/theories/examples/tstack.v
+++ b/theories/examples/tstack.v
@@ -206,8 +206,8 @@ Section TreiberStack.
[done|done|..].
{ iNext. iSplitL.
- iIntros (?) "_". iLeft. by iIntros (?) "_".
- - rewrite /monPred_all /tc_opaque. setoid_rewrite <-Head_dup.
- iIntros (?????) "[_ $] //". }
+ - rewrite /monPred_absolutely /tc_opaque. setoid_rewrite <-Head_dup.
+ by iIntros (?????) "[_ $]". }
iNext. iIntros ([] h) "(_ & Head & _)".
wp_seq. wp_bind ([_]_na <- _)%E. wp_op.
@@ -232,7 +232,7 @@ Section TreiberStack.
+ iExists _, _. iFrame "ol". iNext.
by rewrite /Reachable' (fixpoint_unfold (Reachable' P) _ _).
- iNext. by iIntros (??) "(_ & _ & _ & ?)".
- - rewrite /monPred_all /tc_opaque. setoid_rewrite <-Head_dup.
+ - rewrite /monPred_absolutely /tc_opaque. setoid_rewrite <-Head_dup.
iIntros (?????) "!> [_ $] //".
- by iFrame. }
@@ -264,7 +264,7 @@ Section TreiberStack.
+ by iDestruct "Head" as "%".
+ iDestruct "Head" as "[$ Head]".
iDestruct "Head" as (q) "[Head _]". by iExists _, _.
- - rewrite /monPred_all /tc_opaque. setoid_rewrite <- Head_dup.
+ - rewrite /monPred_absolutely /tc_opaque. setoid_rewrite <- Head_dup.
iIntros (?????) "[_ $] //". }
iNext. iIntros ([] h) "(_ & Head & Q)".
@@ -312,7 +312,7 @@ Section TreiberStack.
iExists A'.
by rewrite /Reachable (fixpoint_unfold (Reachable' P) _ _).
- by iIntros.
- - rewrite /monPred_all /tc_opaque. setoid_rewrite <- Head_dup.
+ - rewrite /monPred_absolutely /tc_opaque. setoid_rewrite <- Head_dup.
iIntros (?????) "[_ $] //". }
iNext. iIntros ([] [] _) "(_ & Head & IF)".
diff --git a/theories/gps/fractional.v b/theories/gps/fractional.v
index e0aee6227945b9f23aeae95215bb6e6e93791b52..4c43e02094606381062b671c381015e38c52d828 100644
--- a/theories/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -126,7 +126,7 @@ Section Fractional.
{{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌠→
(∀ v, F_past l s' v ∗ P ∗ vGPS_FP l s' q ={E}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
={E ∖ ↑fracN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
∗ P ∗ vGPS_FP l s q }}}
([ #(LitLoc l) ]_at) @ E
@@ -178,7 +178,7 @@ Section Fractional.
⎡PSCtx⎤ ⊢ {{{ (▷ ∀ s', ⌜s ⊑ s'⌠→
(∀ v, F_past l s' v ∗ P ={E ∖ ↑fracN .@ l}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
={E ∖ ↑fracN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
∗ P ∗ vGPS_FP l s q }}}
([ #(LitLoc l) ]_at) @ E
@@ -199,7 +199,7 @@ Section Fractional.
{{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌠→
(∀ v, F_past l s' v ∗ P ∗ ⎡vGPS_FP l s q V⎤ ={E}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
={E ∖ ↑fracN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
∗ P ∗ ⎡vGPS_FP l s q V⎤ ∗ monPred_in V }}}
([ #(LitLoc l) ]_at) @ E
@@ -244,7 +244,7 @@ Section Fractional.
⎡PSCtx⎤ ⊢ {{{ (▷ ∀ s', ⌜s ⊑ s'⌠→
(∀ v, F_past l s' v ∗ P ={E ∖ ↑fracN .@ l}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
={E ∖ ↑fracN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
∗ P ∗ ⎡vGPS_FP l s q V⎤ ∗ monPred_in V }}}
([ #(LitLoc l) ]_at) @ E
@@ -369,7 +369,7 @@ Section Fractional.
∗ (vGPS_FP l s'' q ={E}=∗ Q s''))
∗ ▷ (∀ s' v, ⌜s ⊑ s'⌠∗ ⌜v ≠v_o⌠∗ ▷ F_past l s' v ∗ P ∗ vGPS_FP l s' q
={E}=∗ R s' v)
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v ={E ∖ ↑fracN .@ l}=∗
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v ={E ∖ ↑fracN .@ l}=∗
F_past l s' v ∗ F_past l s' v )
∗ P ∗ vGPS_FP l s q }}}
(CAS #(LitLoc l) #(LitInt v_o) #(LitInt v_n)) @ E
@@ -446,7 +446,7 @@ Section Fractional.
∗ Q s'' ∗ ▷ (F l s'' v_n) ∗ ▷ F_past l s'' v_n)
∗ ▷ (∀ s' v, ⌜s ⊑ s'⌠∗ ⌜v ≠v_o⌠∗ ▷ F_past l s' v ∗ P
={E ∖ ↑fracN .@ l}=∗ R s' v)
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v ={E ∖ ↑fracN .@ l}=∗
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v ={E ∖ ↑fracN .@ l}=∗
F_past l s' v ∗ F_past l s' v )
∗ P ∗ vGPS_FP l s q }}}
(CAS #(LitLoc l) #(LitInt v_o) #(LitInt v_n)) @ E
diff --git a/theories/gps/plain.v b/theories/gps/plain.v
index 9f8a424b9e8c493ce861d8e727602ae17a3b0504..d221c45425d5947b1d3461602e505464ec13559b 100644
--- a/theories/gps/plain.v
+++ b/theories/gps/plain.v
@@ -136,7 +136,7 @@ Section Plain.
(∀ v, F_past l s' v ∗ vGPS_PP l p s' ∗ P ={E}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F l s'' v ∗ P
={E ∖ ↑persist_locN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
={E ∖ ↑persist_locN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
∗ P ∗ vGPS_PP l p s }}}
[ #l ]_at @ E
@@ -187,7 +187,7 @@ Section Plain.
(∀ v, F_past l s' v ∗ P ={E ∖ ↑persist_locN .@ l}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F l s'' v ∗ P
={E ∖ ↑persist_locN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
={E ∖ ↑persist_locN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
∗ P ∗ vGPS_PP l p s }}}
[ #l ]_at @ E
@@ -257,7 +257,7 @@ Section Plain.
(vGPS_PP l p s'' ={E}=∗ Q s''))
∗ ▷(∀ s' v, ⌜s ⊑ s'⌠∗ ⌜v ≠v_o⌠∗ ▷ F_past l s' v ∗ vGPS_PP l p s' ∗ P
={E}=∗ R s' v)
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
={E ∖ ↑persist_locN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
∗ P ∗ vGPS_PP l p s }}}
(CAS #l #v_o #v_n) @ E
@@ -338,7 +338,7 @@ Section Plain.
∗ Q s'' ∗ ▷ (F l s'' v_n) ∗ ▷ F_past l s'' v_n)
∗ ▷(∀ s' v, ⌜s ⊑ s'⌠∗ ⌜v ≠v_o⌠∗ ▷ F_past l s' v ∗ P
={E ∖ ↑persist_locN .@ l}=∗ R s' v)
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
={E ∖ ↑persist_locN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
∗ P ∗ vGPS_PP l p s }}}
(CAS #l #v_o #v_n) @ E
diff --git a/theories/gps/singlewriter.v b/theories/gps/singlewriter.v
index 0abd730b5f02f772973a5250229ff42ac7ee8608..89ab52e8733ddae108590949acd21b83fb08b130 100644
--- a/theories/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -116,7 +116,7 @@ Section Gname_StrongSW.
Lemma GPS_nFWP_ExRead γ l s q (E : coPset)
(HN : ↑physN ⊆ E) (HNl: ↑fracN .@ l ⊆ E):
- {{{ ⎡PSCtx⎤ ∗ â–· É (∀ v, F_past γ l s v ={E ∖ ↑fracN .@ l}=∗
+ {{{ ⎡PSCtx⎤ ∗ ▷ ∀ᵢ (∀ v, F_past γ l s v ={E ∖ ↑fracN .@ l}=∗
F_past γ l s v ∗ F_past γ l s v ) ∗ vGPS_nFWP γ l s q }}}
([ #l ]_at) @ E
{{{ v, RET #v ;
@@ -382,7 +382,7 @@ Section Gname_StrongSW.
{{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌠→
(∀ v, F_past γ l s' v ∗ P ∗ vGPS_nFRP γ l s' q ={E}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F γ l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past γ l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past γ l s' v
={E ∖ ↑fracN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
∗ P ∗ vGPS_nFRP γ l s q }}}
([ #l ]_at) @ E
@@ -424,7 +424,7 @@ Section Gname_StrongSW.
{{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌠→
(∀ v, F_past γ l s' v ∗ P ={E ∖ ↑fracN .@ l}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F γ l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past γ l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past γ l s' v
={E ∖ ↑fracN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
∗ P ∗ vGPS_nFRP γ l s q }}}
([ #l ]_at) @ E
@@ -446,7 +446,7 @@ Section Gname_StrongSW.
{{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s1 ⊑ s' ∧ s2 ⊑ s'⌠→
(∀ v, F_past γ l s' v ∗ P ∗ ⎡vGPS_nFRP γ l s1 q V⎤ ={E}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F γ l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s1 ⊑ s' ∧ s2 ⊑ s'⌠∗ F_past γ l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s1 ⊑ s' ∧ s2 ⊑ s'⌠∗ F_past γ l s' v
={E ∖ ↑fracN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
∗ P ∗ monPred_in V ∗ ⎡vGPS_nFRP γ l s1 q V⎤ ∗ PrtSeen γ s2 }}}
([ #l ]_at) @ E
@@ -519,7 +519,7 @@ Section Gname_StrongSW.
⎡PSCtx⎤ ⊢ {{{ (▷ ∀ s', ⌜s1 ⊑ s' ∧ s2 ⊑ s'⌠→
(∀ v, F_past γ l s' v ∗ P ={E ∖ ↑fracN .@ l}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F γ l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s1 ⊑ s' ∧ s2 ⊑ s'⌠∗ F_past γ l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s1 ⊑ s' ∧ s2 ⊑ s'⌠∗ F_past γ l s' v
={E ∖ ↑fracN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
∗ P ∗ monPred_in V ∗ ⎡vGPS_nFRP γ l s1 q V⎤ ∗ PrtSeen γ s2 }}}
([ #l ]_at) @ E
@@ -539,7 +539,7 @@ Section Gname_StrongSW.
{{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌠→
(∀ v, F_past γ l s' v ∗ P ∗ ⎡vGPS_nFRP γ l s q V⎤ ={E}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F γ l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past γ l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past γ l s' v
={E ∖ ↑fracN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
∗ P ∗ monPred_in V ∗ ⎡vGPS_nFRP γ l s q V⎤ }}}
([ #l ]_at) @ E
@@ -585,7 +585,7 @@ Section Gname_StrongSW.
⎡PSCtx⎤ ⊢ {{{ (▷ ∀ s', ⌜s ⊑ s'⌠→
(∀ v, F_past γ l s' v ∗ P ={E ∖ ↑fracN .@ l}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F γ l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past γ l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past γ l s' v
={E ∖ ↑fracN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
∗ P ∗ monPred_in V ∗ ⎡vGPS_nFRP γ l s q V⎤ }}}
([ #l ]_at) @ E
@@ -761,7 +761,7 @@ Section Gname_StrongSW_Param.
Lemma GPS_nSW_ExRead l γ p s (E : coPset)
(HN : ↑physN ⊆ E) (HNl: ↑persist_locN .@ l ⊆ E):
- {{{ ⎡PSCtx⎤ ∗ â–· É (∀ v, F_past γ l s v ={E ∖ ↑persist_locN .@ l}=∗
+ {{{ ⎡PSCtx⎤ ∗ ▷ ∀ᵢ (∀ v, F_past γ l s v ={E ∖ ↑persist_locN .@ l}=∗
F_past γ l s v ∗ F_past γ l s v ) ∗ vGPS_nWSP γ l p s }}}
([ #l ]_at) @ E (* TODO: can be non-atomic *)
{{{ v, RET #v ;
@@ -799,7 +799,7 @@ Section Gname_StrongSW_Param.
(∀ v, F_past γ l s' v ∗ P ∗ vGPS_nRSP γ l p s' ={E}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F γ l s'' v ∗ P
={E ∖ ↑persist_locN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past γ l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past γ l s' v
={E ∖ ↑persist_locN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
∗ P ∗ vGPS_nRSP γ l p s }}}
([ #l ]_at) @ E
@@ -842,7 +842,7 @@ Section Gname_StrongSW_Param.
(∀ v, F_past γ l s' v ∗ P ={E ∖ ↑ persist_locN .@ l}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F γ l s'' v ∗ P
={E ∖ ↑persist_locN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past γ l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past γ l s' v
={E ∖ ↑persist_locN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
∗ P ∗ vGPS_nRSP γ l p s }}}
([ #l ]_at) @ E
@@ -1090,7 +1090,7 @@ Section SingleWriter.
Lemma GPS_SW_Read_ex l s (E : coPset)
(HN : ↑physN ⊆ E) (HNl: ↑persist_locN .@ l ⊆ E):
- {{{ ⎡PSCtx⎤ ∗ â–· É (∀ v, F_past l s v ={E ∖ ↑persist_locN .@ l}=∗
+ {{{ ⎡PSCtx⎤ ∗ ▷ ∀ᵢ (∀ v, F_past l s v ={E ∖ ↑persist_locN .@ l}=∗
F_past l s v ∗ F_past l s v ) ∗ vGPS_WSP l s }}}
([ #l ]_at) @ E
{{{ v, RET #v ;
@@ -1161,7 +1161,7 @@ Section SingleWriter.
(∀ v, F_past l s' v ∗ P ∗ vGPS_RSP l s' ={E}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F l s'' v ∗ P
={E ∖ ↑persist_locN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
={E ∖ ↑persist_locN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
∗ P ∗ vGPS_RSP l s }}}
([ #l ]_at) @ E
@@ -1206,7 +1206,7 @@ Section SingleWriter.
(∀ v, F_past l s' v ∗ P ={E ∖ ↑ persist_locN .@ l}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F l s'' v ∗ P
={E ∖ ↑persist_locN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
={E ∖ ↑persist_locN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
∗ P ∗ vGPS_RSP l s }}}
([ #l ]_at) @ E
@@ -1342,7 +1342,7 @@ Section SingleWriter.
{{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌠→
(∀ v, F_past l s' v ∗ P ∗ vGPS_FRP l s' q ={E}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
={E ∖ ↑fracN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
∗ P ∗ vGPS_FRP l s q }}}
([ #l ]_at) @ E
@@ -1387,7 +1387,7 @@ Section SingleWriter.
{{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌠→
(∀ v, F_past l s' v ∗ P ={E ∖ ↑fracN .@ l}=∗ Q s' v)
∨ (∀ s'' v, ⌜s' ⊑ s''⌠→ F l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
- ∗ â–· É (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
+ ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌠∗ F_past l s' v
={E ∖ ↑fracN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
∗ P ∗ vGPS_FRP l s q }}}
([ #l ]_at) @ E
@@ -1405,7 +1405,7 @@ Section SingleWriter.
Lemma GPS_FWP_ExRead l s q (E : coPset)
(HN : ↑physN ⊆ E) (HNl: ↑fracN .@ l ⊆ E):
- {{{ ⎡PSCtx⎤ ∗ â–· É (∀ v, F_past l s v ={E ∖ ↑fracN .@ l}=∗
+ {{{ ⎡PSCtx⎤ ∗ ▷ ∀ᵢ (∀ v, F_past l s v ={E ∖ ↑fracN .@ l}=∗
F_past l s v ∗ F_past l s v ) ∗ vGPS_FWP l s q }}}
([ #l ]_at) @ E
{{{ v, RET #v ;
diff --git a/theories/history.v b/theories/history.v
index 6bb9ac800c101e0925b79907f2f0bc5ce127ebdb..8d2c4722cb5b405b432d2ab91da6fb12e2ffef53 100644
--- a/theories/history.v
+++ b/theories/history.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import ssreflect ssrbool seq.
+From Coq.ssr Require Import ssreflect.
From stdpp Require Export strings list numbers sorting gmap finite set mapset.
Global Generalizable All Variables.
diff --git a/theories/infrastructure.v b/theories/infrastructure.v
index 42a4d0ce72fef6d1845cc5c28182fccedf956efd..03413daecf58a3b7291552a144a6dbd6ad5e497b 100644
--- a/theories/infrastructure.v
+++ b/theories/infrastructure.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import ssreflect ssrbool seq.
+From Coq.ssr Require Export ssreflect.
From stdpp Require Export list numbers set gmap finite mapset fin_collections.
Global Generalizable All Variables.
Global Set Asymmetric Patterns.
@@ -6,6 +6,8 @@ Global Set Bullet Behavior "Strict Subproofs".
From Coq Require Export Utf8.
Require Import Setoid.
+Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
+
Lemma seq_set_size (s n: nat): size (seq_set s n : gset nat) = n.
Proof.
induction n; [done|].
diff --git a/theories/invariants.v b/theories/invariants.v
index e577bf9e69c463dbc0424951d750cd7eaff201f3..93360826ec322875256a63c7d5f3ce81360899c0 100644
--- a/theories/invariants.v
+++ b/theories/invariants.v
@@ -7,105 +7,30 @@ Section Invariants.
Context {Σ : gFunctors} `{fG : !foundationG Σ} `{W : invG.invG Σ}.
Definition inv N (P : vProp Σ) : vProp Σ := ⎡invariants.inv N (∀ V, monPred_at P V)⎤%I.
- Lemma inv_alloc N (E : coPset) (P : vProp Σ) : â–· (É P) -∗ |={E}=> inv N P.
+ Lemma inv_alloc N (E : coPset) (P : vProp Σ) : ▷ (∀ᵢ P) -∗ |={E}=> inv N P.
Proof.
- iIntros "H". rewrite /monPred_all /tc_opaque -sbi_embed_later.
+ iIntros "H". rewrite /monPred_absolutely /= -sbi_embed_later.
by iMod (invariants.inv_alloc with "H") as "$".
Qed.
Lemma inv_alloc_open N (E : coPset) (P : vProp Σ) :
- ↑N ⊆ E → (|={E,E ∖ ↑N}=> inv N P ∗ (â–· (É P) ={E ∖ ↑N,E}=∗ True))%I.
+ ↑N ⊆ E → (|={E,E ∖ ↑N}=> inv N P ∗ (▷ (∀ᵢ P) ={E ∖ ↑N,E}=∗ True))%I.
Proof.
- rewrite /monPred_all /tc_opaque -sbi_embed_later.
+ rewrite /monPred_absolutely /= -sbi_embed_later.
iIntros (?). iMod (invariants.inv_alloc_open) as "[$ Close]"; [done|].
iIntros "!> H". by iMod ("Close" with "H").
Qed.
Lemma inv_open (E : coPset) N (P : vProp Σ) :
- ↑N ⊆ E → inv N P -∗ |={E,E ∖ ↑N}=> â–· (É P) ∗ (â–· (É P) ={E ∖ ↑N,E}=∗ True).
+ ↑N ⊆ E → inv N P -∗ |={E,E ∖ ↑N}=> ▷ (∀ᵢ P) ∗ (▷ (∀ᵢ P) ={E ∖ ↑N,E}=∗ True).
Proof.
- iIntros (?) "H". rewrite /monPred_all /tc_opaque -sbi_embed_later.
+ iIntros (?) "H". rewrite /monPred_absolutely /= -sbi_embed_later.
iMod (invariants.inv_open with "H") as "[$ Close]"; [done|].
iIntros "!> H". by iMod ("Close" with "H").
Qed.
- Class Objective (P : vProp Σ) := objective V1 V2 : P V1 -∗ P V2.
- Arguments Objective _%I.
- Arguments objective _%I {_}.
- Lemma objective_all P `{Objective P} : P ⊢ É P.
- Proof. iStartProof (iProp _). iIntros (V) "HP %". by iApply objective. Qed.
- Lemma objective_ex P `{Objective P} : ▲P ⊢ P.
- Proof.
- iStartProof (iProp _). iIntros (V) "H". iDestruct "H" as (?) "H".
- by iApply objective.
- Qed.
-
- Global Instance as_valid_Objective (P : vProp Σ) (Φ : View → iProp Σ) :
- (∀ V, MakeMonPredAt V P (Φ V)) →
- AsValid (Objective P) (∀ V1 V2, Φ V1 -∗ Φ V2)%I.
- Proof.
- rewrite /Objective /AsValid /MakeMonPredAt=>EQ. setoid_rewrite <-EQ.
- split=>H; iIntros (??) "?"; by iApply H.
- Qed.
-
- Global Instance emb_objective P : Objective ⎡P⎤.
- Proof. iStartProof (uPred _). auto. Qed.
- Global Instance pure_objective P : Objective ⌜PâŒ.
- Proof. apply emb_objective. Qed.
- Global Instance emp_objective : Objective emp.
- Proof. apply emb_objective. Qed.
-
- Global Instance sep_objective P Q `{Objective P, Objective Q} : Objective (P ∗ Q).
- Proof.
- iStartProof (uPred _); iIntros (??) "[HP HQ]".
- iSplitL "HP"; by iApply objective.
- Qed.
-
- Global Instance big_sepL_objective {A} (l : list A) f {Hf : ∀ i x, Objective (f i x)}:
- Objective ([∗ list] i↦x ∈ l, f i x)%I.
- Proof. revert f Hf. induction l=>/=; apply _. Qed.
-
- Global Instance forall_objective {A} P {H : ∀ x : A, Objective (P x)} :
- Objective (∀ x, P x)%I.
- Proof. iStartProof (uPred _). iIntros (??) "H %". by iApply objective. Qed.
-
- Global Instance exists_objective {A} P {H : ∀ x : A, Objective (P x)} :
- Objective (∃ x, P x)%I.
- Proof.
- iStartProof (uPred _). iIntros (??) "H". iDestruct "H" as (x) "H".
- iExists _. by iApply objective.
- Qed.
-
- Global Instance wand_objective' P Q `{Objective P, Objective Q} : Objective (P -∗ Q)%I.
- Proof.
- iStartProof (uPred _). iIntros (??) "H % % HP".
- iApply objective. iApply "H". by iApply objective.
- Qed.
-
- Global Instance fupd_objective E1 E2 P {H : Objective P} : Objective (|={E1,E2}=> P)%I.
- Proof. iStartProof (uPred _). iIntros (??) "H". by iApply objective. Qed.
-
- Global Instance wand_objective P Q (H : P -∗ Q) : Objective (P -∗ Q)%I.
- Proof. iStartProof (uPred _). iIntros (??) "H %% HP". by iApply H. Qed.
-
- Lemma all_entails (P Q : vProp Σ) : (P -∗ Q) -> bi_valid (É (P -∗ Q))%I.
- Proof.
- iIntros. iApply objective_all.
- - apply wand_objective; auto.
- - iApply H.
- Qed.
-
- Lemma all_forall {A} (Ψ : A -> vProp Σ) : (É (∀ a, Ψ a))%I ≡ (∀ a, É Î¨ a)%I.
- Proof.
- iStartProof (uPred _).
- iIntros; iSplit; iIntros "H"; iIntros (??); iApply ("H" $! _ _).
- Qed.
-
+ (* TODO : this should be removed and replaced with the general iAlways
+ tactic. *)
+ Lemma absolutely_entails (P Q : vProp Σ) : (P -∗ Q) -> bi_valid (∀ᵢ (P -∗ Q))%I.
+ Proof. iStartProof (iProp _). iIntros (H V ???). rewrite H. auto. Qed.
End Invariants.
-
-Arguments Objective {_} _%I : simpl never.
-Arguments objective {_} _%I {_}.
-Arguments objective_all {_} _%I {_}.
-Arguments objective_ex {_} _%I {_}.
-Hint Mode Objective + ! : typeclass_instances.
-Instance: Params (@Objective) 1.
diff --git a/theories/logically_atomic.v b/theories/logically_atomic.v
index 49831199d4ed0fde778820fe8bf83d12997602f3..d05b9532d422f393fd1566c35ac494a6662f7d28 100644
--- a/theories/logically_atomic.v
+++ b/theories/logically_atomic.v
@@ -70,7 +70,7 @@ Proof.
iApply "Hclose"; iFrame.
Qed.
-Lemma LA_Inv {A} (α : A -> vProp Σ) β Ei Eo e N R {_ : Objective R}:
+Lemma LA_Inv {A} (α : A -> vProp Σ) β Ei Eo e N R {_ : Absolute R}:
↑N ## Ei ->
atomic_wp (fun x => ▷R ∗ α x)%I (fun x v => ▷R ∗ β x v)%I Ei Eo e -∗
atomic_wp (fun x => inv N R ∗ α x)%I β (↑N ∪ Ei) Eo e.
@@ -83,7 +83,7 @@ Proof.
iPoseProof (inv_open (↑N ∪ Ei) with "Hinv") as "HR".
{ apply union_subseteq_l. }
iMod "HR" as "[HR HcloseR]".
- iDestruct (monPred_all_elim with "HR") as "HR".
+ iDestruct (monPred_absolutely_elim with "HR") as "HR".
assert (Ei = (↑N ∪ Ei) ∖ ↑N) as <-.
{ rewrite difference_union_distr_l_L difference_diag_L union_empty_l_L
difference_disjoint_L; done. }
@@ -91,11 +91,11 @@ Proof.
iExists x; iFrame; iSplit.
- iIntros "[HR Hx]".
iMod ("HcloseR" with "[HR]").
- { by iApply objective_all. }
+ { by iApply absolute_absolutely. }
iApply "Hclose"; auto.
- iIntros (v) "[HR Hv]".
iMod ("HcloseR" with "[HR]").
- { by iApply objective_all. }
+ { by iApply absolute_absolutely. }
iApply "Hclose"; auto.
Qed.
@@ -132,7 +132,7 @@ Proof.
Qed.
Lemma LA_Inv' {A} β Ei Eo e N (R : A -> vProp Σ) Ei'
- {_ : ∀x, Objective (R x)} {_ : ∀x, Timeless (R x)}:
+ {_ : ∀ x, Absolute (R x)} {_ : ∀ x, Timeless (R x)}:
↑N ## Ei -> ↑N ∪ Ei ⊆ Ei' ->
atomic_wp (fun x => R x)%I (fun x v => (∃y, R y) ∗ β x v)%I Ei Eo e -∗
atomic_wp (fun _ : unit => inv N (∃x, R x))%I (fun _ v => ∃x, β x v) Ei' Eo e.
@@ -147,18 +147,18 @@ Proof.
iPoseProof (inv_open (↑N ∪ Ei) with "Hinv") as "HR".
{ apply union_subseteq_l. }
iMod "HR" as "[>HR HcloseR]".
- iDestruct (monPred_all_elim with "HR") as (a) "HR".
+ iDestruct (monPred_absolutely_elim with "HR") as (a) "HR".
assert (Ei = (↑N ∪ Ei) ∖ ↑N) as <-.
{ by rewrite difference_union_distr_l_L difference_diag_L union_empty_l_L
difference_disjoint_L. }
iModIntro. iExists a; iFrame; iSplit.
- iIntros "HR".
iMod ("HcloseR" with "[HR]").
- { by iApply objective_all; iExists a. }
+ { iApply absolute_absolutely; by iExists a. }
iApply "Hclose"; auto.
- iIntros (v) "[HR Hv]".
iMod ("HcloseR" with "[HR]").
- { by iApply objective_all. }
+ { by iApply absolute_absolutely. }
iApply "Hclose"; auto.
Qed.
End LA_rules.
diff --git a/theories/machine.v b/theories/machine.v
index df41efabe9530c9b68ffa8abe9dba220b54af486..2e586b18f05b98b09375fd2d8b252aa13fc9a607 100644
--- a/theories/machine.v
+++ b/theories/machine.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import ssreflect ssrbool seq.
+From Coq.ssr Require Import ssreflect ssrbool.
From stdpp Require Export strings list numbers sorting gmap finite mapset.
Global Generalizable All Variables.
diff --git a/theories/tactics.v b/theories/tactics.v
index 08ee554a0dc3184ca7414ab2f569ae2565907805..3f267492daa7deb215779533c94eee5a7728e60b 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import ssreflect.
From igps Require Export lang.
From iris.program_logic Require Import ectx_language ectxi_language language.
From stdpp Require Import fin_maps.
diff --git a/theories/tactics_vProp.v b/theories/tactics_vProp.v
index d1786641652b04849b1acc7311b0e194591318ef..0169eb4deaa3efb0955f2e0c172f8db69c5d2d9a 100644
--- a/theories/tactics_vProp.v
+++ b/theories/tactics_vProp.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import ssreflect.
From iris.program_logic Require Import ectx_language ectxi_language language.
From stdpp Require Import fin_maps.
From igps Require Export lang.
diff --git a/theories/viewpred.v b/theories/viewpred.v
index 3a5ee4dccc1875a5243abe08db6553c144a6c275..6eef53a4b06b8b608c31457b7a7e763ea44268ce 100644
--- a/theories/viewpred.v
+++ b/theories/viewpred.v
@@ -7,8 +7,3 @@ Export types infrastructure monpred.
Notation vProp Σ := (monPredSI View_bi_index (uPredSI (iResUR Σ))).
Canonical Structure View_ofe : ofeT := leibnizC View.
-
-Notation "'É' P" := (monPred_all P)
- (at level 20, right associativity) : bi_scope.
-Notation "â–² P" := (monPred_ex P)
- (at level 20, right associativity, format "â–² P"): bi_scope.