Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq

algebra/coPset.v

 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From iris.prelude Require Export collections coPset.
-
 (** This is pretty much the same as algebra/gset, but I was not able to
 generalize the construction without breaking canonical structures. *)
 
+(* The union CMRA *)
+Section coPset.
+  Implicit Types X Y : coPset.
+
+  Canonical Structure coPsetC := leibnizC coPset.
+
+  Instance coPset_valid : Valid coPset := λ _, True.
+  Instance coPset_op : Op coPset := union.
+  Instance coPset_pcore : PCore coPset := λ _, Some ∅.
+
+  Lemma coPset_op_union X Y : X ⋅ Y = X ∪ Y.
+  Proof. done. Qed.
+  Lemma coPset_core_empty X : core X = ∅.
+  Proof. done. Qed.
+  Lemma coPset_included X Y : X ≼ Y ↔ X ⊆ Y.
+  Proof.
+    split.
+    - intros [Z ->]. rewrite coPset_op_union. set_solver.
+    - intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z.
+  Qed.
+
+  Lemma coPset_ra_mixin : RAMixin coPset.
+  Proof.
+    apply ra_total_mixin; eauto.
+    - solve_proper.
+    - solve_proper.
+    - solve_proper.
+    - intros X1 X2 X3. by rewrite !coPset_op_union assoc_L.
+    - intros X1 X2. by rewrite !coPset_op_union comm_L.
+    - intros X. by rewrite coPset_op_union coPset_core_empty left_id_L.
+    - intros X1 X2 _. by rewrite coPset_included !coPset_core_empty.
+  Qed.
+  Canonical Structure coPsetR := discreteR coPset coPset_ra_mixin.
+
+  Lemma coPset_ucmra_mixin : UCMRAMixin coPset.
+  Proof. split. done. intros X. by rewrite coPset_op_union left_id_L. done. Qed.
+  Canonical Structure coPsetUR :=
+    discreteUR coPset coPset_ra_mixin coPset_ucmra_mixin.
+
+  Lemma coPset_opM X mY : X ⋅? mY = X ∪ from_option id ∅ mY.
+  Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
+
+  Lemma coPset_update X Y : X ~~> Y.
+  Proof. done. Qed.
+
+  Lemma coPset_local_update X Y mXf : X ⊆ Y → X ~l~> Y @ mXf.
+  Proof.
+    intros (Z&->&?)%subseteq_disjoint_union_L.
+    intros; apply local_update_total; split; [done|]; simpl.
+    intros mZ _. rewrite !coPset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX.
+  Qed.
+End coPset.
+
+(* The disjoiny union CMRA *)
 Inductive coPset_disj :=
   | CoPset : coPset → coPset_disj
   | CoPsetBot : coPset_disj.
 
-Section coPset.
+Section coPset_disj.
   Arguments op _ _ !_ !_ /.
   Canonical Structure coPset_disjC := leibnizC coPset_disj.
 
@@ -27,7 +80,7 @@ Section coPset.
     repeat (simpl || case_decide);
     first [apply (f_equal CoPset)|done|exfalso]; set_solver by eauto.
 
-  Lemma coPset_included X Y : CoPset X ≼ CoPset Y ↔ X ⊆ Y.
+  Lemma coPset_disj_included X Y : CoPset X ≼ CoPset Y ↔ X ⊆ Y.
   Proof.
     split.
     - move=> [[Z|]]; simpl; try case_decide; set_solver.
@@ -60,4 +113,4 @@ Section coPset.
   Proof. split; try apply _ || done. intros [X|]; coPset_disj_solve. Qed.
   Canonical Structure coPset_disjUR :=
     discreteUR coPset_disj coPset_disj_ra_mixin coPset_disj_ucmra_mixin.
-End coPset.
+End coPset_disj.

algebra/gset.v

@@ -2,13 +2,68 @@ From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From iris.prelude Require Export collections gmap.
 
+(* The union CMRA *)
+Section gset.
+  Context `{Countable K}.
+  Implicit Types X Y : gset K.
+
+  Canonical Structure gsetC := leibnizC (gset K).
+
+  Instance gset_valid : Valid (gset K) := λ _, True.
+  Instance gset_op : Op (gset K) := union.
+  Instance gset_pcore : PCore (gset K) := λ _, Some ∅.
+
+  Lemma gset_op_union X Y : X ⋅ Y = X ∪ Y.
+  Proof. done. Qed.
+  Lemma gset_core_empty X : core X = ∅.
+  Proof. done. Qed.
+  Lemma gset_included X Y : X ≼ Y ↔ X ⊆ Y.
+  Proof.
+    split.
+    - intros [Z ->]. rewrite gset_op_union. set_solver.
+    - intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z.
+  Qed.
+
+  Lemma gset_ra_mixin : RAMixin (gset K).
+  Proof.
+    apply ra_total_mixin; eauto.
+    - solve_proper.
+    - solve_proper.
+    - solve_proper.
+    - intros X1 X2 X3. by rewrite !gset_op_union assoc_L.
+    - intros X1 X2. by rewrite !gset_op_union comm_L.
+    - intros X. by rewrite gset_op_union gset_core_empty left_id_L.
+    - intros X1 X2 _. by rewrite gset_included !gset_core_empty.
+  Qed.
+  Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.
+
+  Lemma gset_ucmra_mixin : UCMRAMixin (gset K).
+  Proof. split. done. intros X. by rewrite gset_op_union left_id_L. done. Qed.
+  Canonical Structure gsetUR :=
+    discreteUR (gset K) gset_ra_mixin gset_ucmra_mixin.
+
+  Lemma gset_opM X mY : X ⋅? mY = X ∪ from_option id ∅ mY.
+  Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
+
+  Lemma gset_update X Y : X ~~> Y.
+  Proof. done. Qed.
+
+  Lemma gset_local_update X Y mXf : X ⊆ Y → X ~l~> Y @ mXf.
+  Proof.
+    intros (Z&->&?)%subseteq_disjoint_union_L.
+    intros; apply local_update_total; split; [done|]; simpl.
+    intros mZ _. rewrite !gset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX.
+  Qed.
+End gset.
+
+(* The disjoint union CMRA *)
 Inductive gset_disj K `{Countable K} :=
   | GSet : gset K → gset_disj K
   | GSetBot : gset_disj K.
 Arguments GSet {_ _ _} _.
 Arguments GSetBot {_ _ _}.
 
-Section gset.
+Section gset_disj.
   Context `{Countable K}.
   Arguments op _ _ !_ !_ /.
 
@@ -28,7 +83,7 @@ Section gset.
     repeat (simpl || case_decide);
     first [apply (f_equal GSet)|done|exfalso]; set_solver by eauto.
 
-  Lemma coPset_included X Y : GSet X ≼ GSet Y ↔ X ⊆ Y.
+  Lemma gset_disj_included X Y : GSet X ≼ GSet Y ↔ X ⊆ Y.
   Proof.
     split.
     - move=> [[Z|]]; simpl; try case_decide; set_solver.
@@ -63,7 +118,7 @@ Section gset.
 
   Arguments op _ _ _ _ : simpl never.
 
-  Lemma gset_alloc_updateP_strong P (Q : gset_disj K → Prop) X :
+  Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K → Prop) X :
     (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
     (∀ i, i ∉ X → P i → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
   Proof.
@@ -74,43 +129,46 @@ Section gset.
     - apply HQ; set_solver by eauto.
     - apply gset_disj_valid_op. set_solver by eauto.
   Qed.
-  Lemma gset_alloc_updateP_strong' P X :
+  Lemma gset_disj_alloc_updateP_strong' P X :
     (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
     GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X ∧ P i.
-  Proof. eauto using gset_alloc_updateP_strong. Qed.
+  Proof. eauto using gset_disj_alloc_updateP_strong. Qed.
 
-  Lemma gset_alloc_empty_updateP_strong P (Q : gset_disj K → Prop) :
+  Lemma gset_disj_alloc_empty_updateP_strong P (Q : gset_disj K → Prop) :
     (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) →
     (∀ i, P i → Q (GSet {[i]})) → GSet ∅ ~~>: Q.
   Proof.
-    intros. apply (gset_alloc_updateP_strong P); eauto.
+    intros. apply (gset_disj_alloc_updateP_strong P); eauto.
     intros i; rewrite right_id_L; auto.
   Qed.
-  Lemma gset_alloc_empty_updateP_strong' P :
+  Lemma gset_disj_alloc_empty_updateP_strong' P :
     (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) →
     GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]} ∧ P i.
-  Proof. eauto using gset_alloc_empty_updateP_strong. Qed.
+  Proof. eauto using gset_disj_alloc_empty_updateP_strong. Qed.
 
   Section fresh_updates.
     Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
 
-    Lemma gset_alloc_updateP (Q : gset_disj K → Prop) X :
+    Lemma gset_disj_alloc_updateP (Q : gset_disj K → Prop) X :
       (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
     Proof.
-      intro; eapply gset_alloc_updateP_strong with (λ _, True); eauto.
+      intro; eapply gset_disj_alloc_updateP_strong with (λ _, True); eauto.
       intros Y ?; exists (fresh Y); eauto using is_fresh.
     Qed.
-    Lemma gset_alloc_updateP' X : GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.
-    Proof. eauto using gset_alloc_updateP. Qed.
+    Lemma gset_disj_alloc_updateP' X :
+      GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.
+    Proof. eauto using gset_disj_alloc_updateP. Qed.
 
-    Lemma gset_alloc_empty_updateP (Q : gset_disj K → Prop) :
+    Lemma gset_disj_alloc_empty_updateP (Q : gset_disj K → Prop) :
       (∀ i, Q (GSet {[i]})) → GSet ∅ ~~>: Q.
-    Proof. intro. apply gset_alloc_updateP. intros i; rewrite right_id_L; auto. Qed.
-    Lemma gset_alloc_empty_updateP' : GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]}.
-    Proof. eauto using gset_alloc_empty_updateP. Qed.
+    Proof.
+      intro. apply gset_disj_alloc_updateP. intros i; rewrite right_id_L; auto.
+    Qed.
+    Lemma gset_disj_alloc_empty_updateP' : GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]}.
+    Proof. eauto using gset_disj_alloc_empty_updateP. Qed.
   End fresh_updates.
 
-  Lemma gset_alloc_local_update X i Xf :
+  Lemma gset_disj_alloc_local_update X i Xf :
     i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf).
   Proof.
     intros ??; apply local_update_total; split; simpl.
@@ -118,13 +176,13 @@ Section gset.
     - intros mZ ?%gset_disj_valid_op HXf.
       rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver.
   Qed.
-  Lemma gset_alloc_empty_local_update i Xf :
+  Lemma gset_disj_alloc_empty_local_update i Xf :
     i ∉ Xf → GSet ∅ ~l~> GSet {[i]} @ Some (GSet Xf).
   Proof.
     intros. rewrite -(right_id_L _ _ {[i]}).
-    apply gset_alloc_local_update; set_solver.
+    apply gset_disj_alloc_local_update; set_solver.
   Qed.
-End gset.
+End gset_disj.
 
 Arguments gset_disjR _ {_ _}.
 Arguments gset_disjUR _ {_ _}.

algebra/upred.v

@@ -1221,11 +1221,12 @@ Proof.
 Qed.
 Lemma ownM_empty : True ⊢ uPred_ownM ∅.
 Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
-Lemma later_ownM a : Timeless a → ▷ uPred_ownM a ⊢ ▷ False ∨ uPred_ownM a.
+Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
 Proof.
-  unseal=> Ha; split=> -[|n] x ?? /=; [by left|right].
-  apply cmra_included_includedN, cmra_timeless_included_l,
-    cmra_includedN_le with n; eauto using cmra_validN_le.
+  unseal; split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
+  destruct Hax as [y ?].
+  destruct (cmra_extend n x a y) as (a'&y'&Hx&?&?); auto using cmra_validN_S.
+  exists a'. rewrite Hx. eauto using cmra_includedN_l.
 Qed.
 
 (* Valid *)
@@ -1390,7 +1391,12 @@ Global Instance eq_timeless {A : cofeT} (a b : A) :
   Timeless a → TimelessP (a ≡ b : uPred M)%I.
 Proof. intros. rewrite /TimelessP !timeless_eq. apply (timelessP _). Qed.
 Global Instance ownM_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a).
-Proof. apply later_ownM. Qed.
+Proof.
+  intros ?. rewrite /TimelessP later_ownM. apply exist_elim=> b.
+  rewrite (timelessP (a≡b)) (except_last_intro (uPred_ownM b)) -except_last_and.
+  apply except_last_mono. rewrite eq_sym.
+  apply (eq_rewrite b a (uPred_ownM)); first apply _; auto.
+Qed.
 
 (* Persistence *)
 Global Instance pure_persistent φ : PersistentP (■ φ : uPred M)%I.

heap_lang/lib/ticket_lock.v

@@ -141,7 +141,7 @@ Section proof.
     - wp_cas_suc.
       iDestruct "Hainv" as (s) "[Ho %]"; subst.
       iVs (own_update with "Ho") as "Ho".
-      { eapply auth_update_no_frag, (gset_alloc_empty_local_update n).
+      { eapply auth_update_no_frag, (gset_disj_alloc_empty_local_update n).
         rewrite elem_of_seq_set; omega. }
       iDestruct "Ho" as "[Hofull Hofrag]".
       iVs ("Hclose" with "[Hlo' Hln' Haown Hofull]").

program_logic/ownership.v

@@ -156,7 +156,7 @@ Proof.
   iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
   iVs (own_empty (A:=gset_disjUR positive) disabled_name) as "HE".
   iVs (own_updateP with "HE") as "HE".
-  { apply (gset_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
+  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
     intros E. destruct (Hfresh (E ∪ dom _ I))
       as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
   iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?).

program_logic/pviewshifts.v

@@ -31,6 +31,10 @@ Notation "P ={ E }=★ Q" := (P -★ |={E}=> Q)%I
 Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q)
   (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
 
+Notation "|={ E1 , E2 }▷=> Q" := (|={E1%I,E2%I}=> ▷ |={E2,E1}=> Q)%I
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "|={ E1 , E2 }▷=>  Q") : uPred_scope.
+
 Section pvs.
 Context `{irisG Λ Σ}.
 Implicit Types P Q : iProp Σ.

program_logic/thread_local.v

@@ -56,7 +56,7 @@ Section proofs.
     iVs (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
     iVs (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
     { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
-      apply (gset_alloc_empty_updateP_strong' (λ i, i ∈ nclose N)).
+      apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ nclose N)).
       intros Ef. exists (coPpick (nclose N ∖ coPset.of_gset Ef)).
       rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
       apply coPpick_elem_of=> Hfin.
@@ -83,8 +83,8 @@ Section proofs.
       iIntros "!==>[HP $]".
       iInv tlN as "[[_ >Hdis2]|>Hitok]" "Hclose".
       + iCombine "Hdis" "Hdis2" as "Hdis".
-        iDestruct (own_valid with "Hdis") as %[_ Hval].
-        revert Hval. rewrite gset_disj_valid_op. set_solver.
+        iDestruct (own_valid with "Hdis") as %[_ Hval%gset_disj_valid_op].
+        set_solver.
       + iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
     - iDestruct (tl_own_disjoint tid {[i]} {[i]} with "[-]") as %?; first by iFrame.
       set_solver.

program_logic/weakestpre.v

@@ -134,7 +134,7 @@ Qed.
 
 Lemma wp_frame_step_l E1 E2 e Φ R :
   to_val e = None → E2 ⊆ E1 →
-  (|={E1,E2}=> ▷ |={E2,E1}=> R) ★ WP e @ E2 {{ Φ }} ⊢ WP e @ E1 {{ v, R ★ Φ v }}.
+  (|={E1,E2}▷=> R) ★ WP e @ E2 {{ Φ }} ⊢ WP e @ E1 {{ v, R ★ Φ v }}.
 Proof.
   rewrite !wp_unfold /wp_pre. iIntros (??) "[HR [Hv|[_ H]]]".
   { iDestruct "Hv" as (v) "[% Hv]"; simplify_eq. }
@@ -189,7 +189,7 @@ Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed.
 
 Lemma wp_frame_step_r E1 E2 e Φ R :
   to_val e = None → E2 ⊆ E1 →
-  WP e @ E2 {{ Φ }} ★ (|={E1,E2}=> ▷ |={E2,E1}=> R) ⊢ WP e @ E1 {{ v, Φ v ★ R }}.
+  WP e @ E2 {{ Φ }} ★ (|={E1,E2}▷=> R) ⊢ WP e @ E1 {{ v, Φ v ★ R }}.
 Proof.
   rewrite [(WP _ @ _ {{ _ }} ★ _)%I]comm; setoid_rewrite (comm _ _ R).
   apply wp_frame_step_l.

proofmode/coq_tactics.v

@@ -88,7 +88,7 @@ Definition envs_split {M}
   | true => Some (Envs Γp Γs2, Envs Γp Γs1)
   end.
 
-Definition envs_persistent {M} (Δ : envs M) :=
+Definition env_spatial_is_nil {M} (Δ : envs M) :=
   if env_spatial Δ is Enil then true else false.
 
 Definition envs_clear_spatial {M} (Δ : envs M) : envs M :=
@@ -247,9 +247,10 @@ Proof.
   by rewrite IH wand_curry (comm uPred_sep).
 Qed.
 
-Lemma envs_persistent_persistent Δ : envs_persistent Δ = true → PersistentP Δ.
+Lemma env_spatial_is_nil_persistent Δ :
+  env_spatial_is_nil Δ = true → PersistentP Δ.
 Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
-Hint Immediate envs_persistent_persistent : typeclass_instances.
+Hint Immediate env_spatial_is_nil_persistent : typeclass_instances.
 
 Global Instance envs_Forall2_refl (R : relation (uPred M)) :
   Reflexive R → Reflexive (envs_Forall2 R).
@@ -365,7 +366,7 @@ Lemma tac_next Δ Δ' Q Q' :
 Proof. intros ?? HQ. by rewrite -(from_later Q) into_later_env_sound HQ. Qed.
 
 Lemma tac_löb Δ Δ' i Q :
-  envs_persistent Δ = true →
+  env_spatial_is_nil Δ = true →
   envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
@@ -387,7 +388,7 @@ Proof.
 Qed.
 
 (** * Always *)
-Lemma tac_always_intro Δ Q : envs_persistent Δ = true → (Δ ⊢ Q) → Δ ⊢ □ Q.
+Lemma tac_always_intro Δ Q : env_spatial_is_nil Δ = true → (Δ ⊢ Q) → Δ ⊢ □ Q.
 Proof. intros. by apply (always_intro _ _). Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
@@ -401,7 +402,7 @@ Qed.
 
 (** * Implication and wand *)
 Lemma tac_impl_intro Δ Δ' i P Q :
-  envs_persistent Δ = true →
+  env_spatial_is_nil Δ = true →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.

proofmode/tactics.v

@@ -12,7 +12,7 @@ Declare Reduction env_cbv := cbv [
   bool_eq_dec bool_rec bool_rect bool_dec eqb andb (* bool *)
   assci_eq_dec ascii_to_digits Ascii.ascii_dec Ascii.ascii_rec Ascii.ascii_rect
   string_eq_dec string_rec string_rect (* strings *)
-  env_persistent env_spatial envs_persistent
+  env_persistent env_spatial env_spatial_is_nil
   envs_lookup envs_lookup_delete envs_delete envs_app
     envs_simple_replace envs_replace envs_split envs_clear_spatial].
 Ltac env_cbv :=