diff --git a/opam b/opam
index 216f99af02c2af0515f7be13b0a6547f33b47dd5..7d7d4827bb57c4dc66333305faca3050e1e2453a 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.0") | (= "dev") }
+ "coq-iris" { (= "branch.gen_proofmode.2018-01-25.2") | (= "dev") }
]
diff --git a/theories/examples/circ_buffer.v b/theories/examples/circ_buffer.v
index 4d5201437150a2c215f021204a4c89e465991832..299726ccae982158abbc4cb2afa2ab4ab73f4729 100644
--- a/theories/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -287,11 +287,7 @@ Section CircBuffer.
wp_lam. wp_bind ([_]_at)%E. wp_op.
iApply (GPS_SW_Read_ex with "[$kI $pW]"); [done|done|..].
- { iNext.
- (* iIntros (? ?). iViewUp. unfold prodInt. iIntros "#?". *)
- (* iModIntro. by iSplitL. *)
- admit.
- }
+ { rewrite /monPred_all /tc_opaque. iIntros (????) "!> #$ //". }
iNext. iIntros (w) "(pW & #CEs)".
iDestruct "CEs" as "(% & CEs)".
@@ -303,9 +299,7 @@ Section CircBuffer.
with "[$kI $cR]"); [done|done|..].
{ iNext. iSplitL.
- iIntros (?). iIntros "_". iLeft. by iIntros (?) "(? & _)".
- - (* iIntros (? ? ?). iViewUp. iIntros "[? #?]". iModIntro. by iSplit. *)
- admit.
- }
+ - rewrite /monPred_all /tc_opaque. iIntros (?????) "[? #$] //". }
iNext. iIntros (j r) "(% & #cR2 & #PEs)".
iDestruct "PEs" as "(% & PEs)".
@@ -371,7 +365,7 @@ Section CircBuffer.
iApply ("Px"). iPureIntro. lia'.
- iIntros "!#". iIntros (k). iIntros "%".
apply Zlt_succ_le, Zle_lt_or_eq in a as [Lt|Eq].
- + by iApply ("CEs" with "[%]").
+ + by iApply ("CEs" with "[%]").
+ apply Nat2Z.inj in Eq. by rewrite Eq. }
iNext. iIntros "(_ & pW)".
@@ -381,7 +375,7 @@ Section CircBuffer.
iExists γ, (i + 1)%nat, j. iSplitL "".
+ iPureIntro. lia'.
+ rewrite -Nat.add_1_r. iFrame "pW pToks cR2".
- Admitted.
+ Qed.
Lemma tryCons_spec q:
{{{ ⎡PSCtx⎤ ∗ Cons q }}}
@@ -399,7 +393,7 @@ Section CircBuffer.
{ iNext. iSplitL.
- iIntros (?). iIntros (?). iLeft.
iIntros (?) "(? & _)". by auto.
- - (* iIntros (? ? ?). iViewUp. iIntros "[? #?]". iModIntro. by iSplitL. *) admit. }
+ - rewrite /monPred_all /tc_opaque. iIntros (?????) "[? #$] //". }
iNext. iIntros (i w) "(% & pR & #CEs)".
iDestruct "CEs" as "(% & CEs)".
@@ -408,7 +402,7 @@ Section CircBuffer.
iApply (GPS_SW_Read_ex
with "[$kI $cW]"); [done|done|..].
- { iNext. (* iIntros (? ?). iViewUp. iIntros "?". iModIntro. by iSplit. *) admit. }
+ { rewrite /monPred_all /tc_opaque. iIntros (????) "!> #$ //". }
iNext. iIntros (r) "(cW & #PEs)".
iDestruct "PEs" as "(% & PEs)".
@@ -492,7 +486,7 @@ Section CircBuffer.
iExists γ, i, (j + 1)%nat. iSplitL ""; first (iPureIntro; lia').
rewrite -Nat.add_1_r. iFrame "cW cToks pR".
- Admitted.
+ Qed.
End proof.
diff --git a/theories/examples/hashtable.v b/theories/examples/hashtable.v
index b6f46ab514a546ca8993aac322d38154467826ad..edac0e60c6c8acaf2e6d3552456b249c0287a610 100644
--- a/theories/examples/hashtable.v
+++ b/theories/examples/hashtable.v
@@ -1871,7 +1871,7 @@ 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.
- iPoseProof (all_now with "HH") as (HT) "[HH H]".
+ iDestruct (monPred_all_elim with "HH") as (HT) "[HH H]".
iModIntro; iExists HT; iFrame "HH".
iSplit.
{ iIntros "HH".
@@ -2114,7 +2114,7 @@ Section proof.
rewrite Nat.sub_add_distr Hthree Nat.add_1_r seq_S big_sepL_app; simpl.
rewrite Nat.sub_0_r; iFrame.
rewrite Z2Nat.id; [auto | omega].
- + iApply (test_spec with "[-]"); [ | | | iFrame "#"; iFrame |]; try done.
+ + iApply (test_spec with "[-]"); [ | | | by iFrame "# ∗" |]=>//.
* unfold base_mask; rewrite !disjoint_union_l.
split; first by split; apply namespaces.ndot_ne_disjoint.
apply namespaces.ndot_preserve_disjoint_l, namespaces.ndot_ne_disjoint; done.
@@ -2222,7 +2222,7 @@ Section proof.
{ apply namespaces.ndisj_subseteq_difference; last auto.
apply namespaces.ndot_ne_disjoint; done. }
iNext; iIntros (?) "[% Htotal]"; subst.
- iPoseProof (all_now with "Href") as (HT) "[HH Href]".
+ iDestruct (monPred_all_elim with "Href") as (HT) "[HH Href]".
iDestruct "Href" as (hr) "[% Href]".
iDestruct "Href" as (mr) "[% Href]".
assert (i = 3) by omega; subst.
diff --git a/theories/examples/message_passing.v b/theories/examples/message_passing.v
index 2b9feacf073007ae1071301a36a3564b3e4352f8..b4a96e746f22961a4220e017533d0954ca4f0f45 100644
--- a/theories/examples/message_passing.v
+++ b/theories/examples/message_passing.v
@@ -96,9 +96,7 @@ Section proof.
+ iSplitL.
* iNext. iIntros (?). iIntros "_".
iLeft. iIntros (?) "[YP _]". by simpl.
- * iNext.
- (* iIntros (? s v). iViewUp. by iIntros "[? #$]". *)
- admit. (* FIXME *)
+ * rewrite /monPred_all /tc_opaque. iIntros (?????) "!> [_ #$] //".
+ iNext. iIntros (s v) "(_ & #yPRT5 & #YP)".
destruct s.
* iDestruct "YP" as "(% & XE)".
@@ -142,6 +140,6 @@ Section proof.
(* trivial post cond *)
iModIntro. auto.
- Admitted.
+ Qed.
End proof.
diff --git a/theories/examples/msqueue.v b/theories/examples/msqueue.v
index 5ee7dbf4ed986e397e11793d34aeae09cb1fb12c..8dedb7c24539d3839517909d84e4138305bb97c2 100644
--- a/theories/examples/msqueue.v
+++ b/theories/examples/msqueue.v
@@ -230,9 +230,7 @@ Section MSQueue.
[done|done|..].
{ iSplitL "".
- iNext. iIntros ([] ?). iLeft. by iIntros (x) "($ & _)".
- - iNext. admit. (* iIntros (x) "_ (_ & #?)". by iFrame "#". *)
- (* TODO: build infrastructure for É modality :( *)
- }
+ - rewrite /monPred_all /tc_opaque. 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.
@@ -253,10 +251,7 @@ Section MSQueue.
iDestruct "LinkInt" as (γ') "(_ & Link)".
iSplitL ""; first (iPureIntro; lia).
iExists γ'. subst v. iFrame "Link".
- - admit.
- (* iIntros (? s v ?) "_ (_ & #?)". by iFrame "#". *)
- (* TODO: build infrastructure for É modality :( *)
- }
+ - rewrite /monPred_all /tc_opaque. iIntros (????) "_ (_ & #$) //". }
iNext. iIntros (s n') "(% & _ & Q)".
wp_seq. wp_op; case_bool_decide.
@@ -276,7 +271,7 @@ Section MSQueue.
iNext. iIntros "oT2".
wp_seq.
iApply ("Post"); by iLeft.
- Admitted.
+ Qed.
Lemma tryEnq_spec q x:
{{{ ⎡PSCtx⎤ ∗ ⎡PersistorCtx⎤ ∗ Queue q ∗ P x }}}
@@ -296,7 +291,7 @@ Section MSQueue.
wp_let. wp_bind ([_]_na <- _)%E. wp_op.
iApply (na_write with "[$kI $od]"); [done|].
iNext. iIntros "od". wp_seq.
- wp_bind([_]_na <- _)%E. wp_op.
+ wp_bind([_]_na <- _)%E. wp_op.
iMod (own_alloc (Excl ())) as (γ') "Tok"; first done.
iApply (GPS_PP_Init (p:=γ') (Link P γ') Null
@@ -330,9 +325,7 @@ Section MSQueue.
with "kI [P Tok od Link]");
[done|done|..].
{ iFrame "Tok Link". iSplitR "P od"; last iSplitR "P od"; last first.
- - iFrame "P od". iNext. admit.
- (* iIntros (? ? ? ?) "_ (_ & #?)". by iFrame "#". *)
- (* TODO: build infrastructure for É modality :( *)
+ - rewrite /monPred_all /tc_opaque. iIntros "{$P $od}" (????) "!> _ (_ & #$) //".
- iNext. iIntros (??) "(_ & _ & _ & ? & ? & _)". by iFrame.
- iNext. iIntros (s'). iIntros "(_ & LinkInt & P')".
rewrite (unf_int (Link P)).
@@ -368,7 +361,7 @@ Section MSQueue.
+ wp_if_false.
iApply ("Post"); iRight.
by iDestruct "IF" as "[$ ?]".
- Admitted.
+ Qed.
Lemma tryDeq_spec q:
{{{ ⎡PSCtx⎤ ∗ Queue q }}}
@@ -384,9 +377,7 @@ Section MSQueue.
[done|done|..].
{ iNext. iSplitL.
- iIntros ([]) "_". iLeft. by iIntros (x) "($ & _)".
- - (* iIntros (? ? x ?) "_ (_ & #?)". by iFrame "#". *)
- admit.
- }
+ - rewrite /monPred_all /tc_opaque. iIntros (????) "_ (_ & #$) //". }
iNext. iIntros ([] s) "(_ & oH2 & % & os)".
iDestruct "os" as (γ) "os".
@@ -417,9 +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".
- - (* iIntros (????) "_ (_ & #?)". by iFrame "#". *)
- admit.
- }
+ - rewrite /monPred_all /tc_opaque. iIntros (????) "_ [_ #$] //". }
iNext. iIntros (s' n) "(_ & #os & Q')".
wp_seq. wp_op. case_bool_decide.
@@ -434,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.
- - iFrame "oH". iNext. (* iIntros (????) "_ (_ & #?)". by iFrame "#". *) admit.
+ - rewrite /monPred_all /tc_opaque. iIntros "{$oH} !>" (?????) "[_ #$] //".
- iNext. by iIntros (??) "_".
- iNext. iIntros ([]).
iIntros "(_ & Head & _)".
@@ -467,6 +456,6 @@ Section MSQueue.
iApply ("Post" with "[P]"); by iRight.
+ wp_if_false.
iApply ("Post"); by iLeft.
- Admitted.
+ Qed.
End proof.
End MSQueue.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 1acf8cbd6f6f5b78112a7145ae7399ced575055e..6c580f0eaee690267cda4a6666e178108bcf6f3b 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -654,11 +654,8 @@ Section TicketLock.
iLeft. iIntros (z). iIntros "(NSP & _)".
rewrite !(unf_int (NSP P γ)).
by iDestruct "NSP" as "($ & $)".
- - iNext.
- (* iIntros (? s' v). iViewUp. *)
- (* iIntros "(? & #NSP)". by iSplitL "". *)
- admit.
- }
+ - (* TODO : make iAlways able to introduce monPred_all here. *)
+ rewrite /monPred_all /tc_opaque. iIntros (?????) "!> (? & #$) //". }
iNext. iIntros (n z) "(% & #NSR & Q2)".
iDestruct "Q2" as "(% & #ES)".
@@ -716,7 +713,7 @@ Section TicketLock.
iApply ("IH" with "[] [] Post Tkt' Perm").
+ iIntros "!#". iFrame "NS".
+ iIntros "!#". iFrame "TCP".
- Admitted.
+ Qed.
Lemma unlock_spec x :
{{{ ⎡PSCtx⎤ ∗ ▷ P ∗ MayRelease x }}}
@@ -729,10 +726,7 @@ Section TicketLock.
wp_lam. wp_bind ([_]_at)%E. wp_op.
iApply (GPS_SW_Read_ex (NSP P γ) with "[$kI $NSW]"); [done|done|..].
- { iNext.
- (* iIntros (? ?). iViewUp. iIntros "#?". iModIntro. by iSplitL. *)
- admit.
- }
+ { rewrite /monPred_all /tc_opaque. iIntros "!>" (????) "#$ //". }
iNext. iIntros (z) "(NSW & NSP)".
rewrite (unf_int (NSP P γ)).
@@ -769,7 +763,7 @@ Section TicketLock.
iApply ("Post" with "[NS TC Tkt]").
iExists γ, i, (Some $ t). iFrame "Tkt TC".
iIntros "!#". iIntros (?). iIntros "%". by simplify_eq.
- Admitted.
+ Qed.
End proof.
End TicketLock.
diff --git a/theories/examples/tstack.v b/theories/examples/tstack.v
index 5271171f6c7f2c07793e132d478a0789eee6f2b4..296ddec518f167ef2c8c016ab18176e92005b4d5 100644
--- a/theories/examples/tstack.v
+++ b/theories/examples/tstack.v
@@ -206,7 +206,8 @@ Section TreiberStack.
[done|done|..].
{ iNext. iSplitL.
- iIntros (?) "_". iLeft. by iIntros (?) "_".
- - (* iIntros (?[]?) "_ (_ & Head)". by iApply Head_dup. *) admit. }
+ - rewrite /monPred_all /tc_opaque. setoid_rewrite <-Head_dup.
+ iIntros (?????) "[_ $] //". }
iNext. iIntros ([] h) "(_ & Head & _)".
wp_seq. wp_bind ([_]_na <- _)%E. wp_op.
@@ -231,17 +232,15 @@ Section TreiberStack.
+ iExists _, _. iFrame "ol". iNext.
by rewrite /Reachable' (fixpoint_unfold (Reachable' P) _ _).
- iNext. by iIntros (??) "(_ & _ & _ & ?)".
- - iNext.
- (* iIntros (?[]??) "_ (_ & Head)". by iApply Head_dup. *)
- admit.
- - by iFrame.
- }
+ - rewrite /monPred_all /tc_opaque. setoid_rewrite <-Head_dup.
+ iIntros (?????) "!> [_ $] //".
+ - by iFrame. }
iNext. iIntros ([] [] _) "(_ & Head & IF)".
- iApply ("Post" with "[]"); by iLeft.
- iDestruct "IF" as "[P ?]".
iApply ("Post" with "[P]"); by iRight.
- Admitted.
+ Qed.
Lemma tryPop_spec s:
{{{ ⎡PSCtx⎤ ∗ Stack s }}}
@@ -265,9 +264,8 @@ Section TreiberStack.
+ by iDestruct "Head" as "%".
+ iDestruct "Head" as "[$ Head]".
iDestruct "Head" as (q) "[Head _]". by iExists _, _.
- - (* iIntros (?[]??) "_ (_ & Head)". by iApply Head_dup. *)
- admit.
- }
+ - rewrite /monPred_all /tc_opaque. setoid_rewrite <- Head_dup.
+ iIntros (?????) "[_ $] //". }
iNext. iIntros ([] h) "(_ & Head & Q)".
wp_seq. wp_op.
@@ -314,9 +312,8 @@ Section TreiberStack.
iExists A'.
by rewrite /Reachable (fixpoint_unfold (Reachable' P) _ _).
- by iIntros.
- - (* iIntros (?[]??) "_ (_ & Head)". by iApply Head_dup. *)
- admit.
- }
+ - rewrite /monPred_all /tc_opaque. setoid_rewrite <- Head_dup.
+ iIntros (?????) "[_ $] //". }
iNext. iIntros ([] [] _) "(_ & Head & IF)".
+ wp_if_true.
@@ -327,7 +324,7 @@ Section TreiberStack.
iApply ("Post" with "[P]"); by iRight.
+ wp_if_false.
iApply ("Post"); by iLeft.
- Admitted.
+ Qed.
End proof.
End TreiberStack.
diff --git a/theories/invariants.v b/theories/invariants.v
index 117264c350c48245b23eb22d12afcf6331a77b4d..e577bf9e69c463dbc0424951d750cd7eaff201f3 100644
--- a/theories/invariants.v
+++ b/theories/invariants.v
@@ -9,49 +9,24 @@ Section Invariants.
Lemma inv_alloc N (E : coPset) (P : vProp Σ) : â–· (É P) -∗ |={E}=> inv N P.
Proof.
- iStartProof (uPred _). iIntros (V) "H".
- iMod (invariants.inv_alloc with "H") as "H".
- iModIntro. by rewrite monPred_all_eq.
+ iIntros "H". rewrite /monPred_all /tc_opaque -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.
Proof.
- iStartProof (uPred _). iIntros.
- iPoseProof (invariants.inv_alloc_open) as "T"; [done|].
- iMod "T" as "[$ T2]". iModIntro.
- iIntros (V HV) "H". iApply "T2". by rewrite monPred_all_eq.
+ rewrite /monPred_all /tc_opaque -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).
Proof.
- iStartProof (uPred _). iIntros (??) "H".
- iPoseProof (invariants.inv_open with "H") as "T"; [done|].
- rewrite monPred_all_eq /=.
- iMod "T" as "[$ T2]". iModIntro.
- iIntros (V HV) "H".
- by iMod ("T2" with "H").
- Qed.
-
- Lemma all_now (P : vProp Σ) : É P ⊢ P.
- Proof.
- intros; hnf.
- rewrite monPred_all_eq /=.
- split => ?. iIntros "H". iExact "H".
- Qed.
-
- Global Instance all_timeless (P : vProp Σ) {_ : Timeless P} : Timeless (É P).
- Proof.
- revert H; rewrite monPred_all_eq /monPred_all_def.
- rewrite /Timeless /=.
- iStartProof (uPred _); iIntros (H V) "H /=".
- cut (Timeless (∀ i, P i)); [|].
- { by move => ->. }
- apply bi.forall_timeless.
- rewrite /Timeless. rewrite /Timeless in H.
- iIntros (?) "H".
- by iApply H.
+ iIntros (?) "H". rewrite /monPred_all /tc_opaque -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.
@@ -73,16 +48,14 @@ Section Invariants.
split=>H; iIntros (??) "?"; by iApply H.
Qed.
- Global Instance pure_objective P : Objective ⌜PâŒ.
- Proof. iStartProof (uPred _). auto. 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. iStartProof (uPred _). auto. Qed.
+ Proof. apply emb_objective. Qed.
- Global Instance sep_objective P Q `{Objective P} `{Objective Q} : Objective (P ∗ Q).
+ Global Instance sep_objective P Q `{Objective P, Objective Q} : Objective (P ∗ Q).
Proof.
iStartProof (uPred _); iIntros (??) "[HP HQ]".
iSplitL "HP"; by iApply objective.
@@ -103,7 +76,7 @@ Section Invariants.
iExists _. by iApply objective.
Qed.
- Global Instance wand_objective' P Q `{Objective P} `{Objective Q} : Objective (P -∗ Q)%I.
+ 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.
@@ -117,10 +90,9 @@ Section Invariants.
Lemma all_entails (P Q : vProp Σ) : (P -∗ Q) -> bi_valid (É (P -∗ Q))%I.
Proof.
- iIntros.
- iApply objective_all.
- - apply wand_objective; auto.
- - iApply H.
+ iIntros. iApply objective_all.
+ - apply wand_objective; auto.
+ - iApply H.
Qed.
Lemma all_forall {A} (Ψ : A -> vProp Σ) : (É (∀ a, Ψ a))%I ≡ (∀ a, É Î¨ a)%I.
diff --git a/theories/logically_atomic.v b/theories/logically_atomic.v
index 5c4111c8355a4187ee14e453ba9ad5e267705b3c..49831199d4ed0fde778820fe8bf83d12997602f3 100644
--- a/theories/logically_atomic.v
+++ b/theories/logically_atomic.v
@@ -83,7 +83,7 @@ Proof.
iPoseProof (inv_open (↑N ∪ Ei) with "Hinv") as "HR".
{ apply union_subseteq_l. }
iMod "HR" as "[HR HcloseR]".
- iPoseProof (all_now with "HR") as "HR".
+ iDestruct (monPred_all_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. }
@@ -147,7 +147,7 @@ Proof.
iPoseProof (inv_open (↑N ∪ Ei) with "Hinv") as "HR".
{ apply union_subseteq_l. }
iMod "HR" as "[>HR HcloseR]".
- iPoseProof (all_now with "HR") as (a) "HR".
+ iDestruct (monPred_all_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. }