Merge remote-tracking branch 'origin/master' into gen_proofmode

CHANGELOG.md

@@ -24,6 +24,9 @@ Changes in Coq:
   - `IntoLaterNEnvs` → `MaybeIntoLaterNEnvs`
 * Rename:
   - `frag_auth_op` → `frac_auth_frag_op`
+  - `cmra_opM_assoc` → `cmra_op_opM_assoc`
+  - `cmra_opM_assoc_L` → `cmra_op_opM_assoc_L`
+  - `cmra_opM_assoc'` → `cmra_opM_opM_assoc`
 * `namespaces` has been moved to std++.
 
 ## Iris 3.1.0 (released 2017-12-19)

theories/algebra/cmra.v

@@ -327,7 +327,7 @@ Global Instance IdFree_proper : Proper ((≡) ==> iff) (@IdFree A).
 Proof. intros x y Hxy. rewrite /IdFree. by setoid_rewrite Hxy. Qed.
 
 (** ** Op *)
-Lemma cmra_opM_assoc x y mz : (x ⋅ y) ⋅? mz ≡ x ⋅ (y ⋅? mz).
+Lemma cmra_op_opM_assoc x y mz : (x ⋅ y) ⋅? mz ≡ x ⋅ (y ⋅? mz).
 Proof. destruct mz; by rewrite /= -?assoc. Qed.
 
 (** ** Validity *)
@@ -662,8 +662,8 @@ Section cmra_leibniz.
   Lemma cmra_pcore_idemp_L x cx : pcore x = Some cx → pcore cx = Some cx.
   Proof. unfold_leibniz. apply cmra_pcore_idemp'. Qed.
 
-  Lemma cmra_opM_assoc_L x y mz : (x ⋅ y) ⋅? mz = x ⋅ (y ⋅? mz).
-  Proof. unfold_leibniz. apply cmra_opM_assoc. Qed.
+  Lemma cmra_op_opM_assoc_L x y mz : (x ⋅ y) ⋅? mz = x ⋅ (y ⋅? mz).
+  Proof. unfold_leibniz. apply cmra_op_opM_assoc. Qed.
 
   (** ** Core *)
   Lemma cmra_pcore_r_L x cx : pcore x = Some cx → x ⋅ cx = x.
@@ -1334,8 +1334,14 @@ Section option.
   Lemma op_is_Some ma mb : is_Some (ma ⋅ mb) ↔ is_Some ma ∨ is_Some mb.
   Proof. rewrite -!not_eq_None_Some op_None. destruct ma, mb; naive_solver. Qed.
 
-  Lemma cmra_opM_assoc' a mb mc : a ⋅? mb ⋅? mc ≡ a ⋅? (mb ⋅ mc).
+  Lemma cmra_opM_opM_assoc a mb mc : a ⋅? mb ⋅? mc ≡ a ⋅? (mb ⋅ mc).
   Proof. destruct mb, mc; by rewrite /= -?assoc. Qed.
+  Lemma cmra_opM_opM_assoc_L `{!LeibnizEquiv A} a mb mc : a ⋅? mb ⋅? mc = a ⋅? (mb ⋅ mc).
+  Proof. unfold_leibniz. apply cmra_opM_opM_assoc. Qed.
+  Lemma cmra_opM_opM_swap a mb mc : a ⋅? mb ⋅? mc ≡ a ⋅? mc ⋅? mb.
+  Proof. by rewrite !cmra_opM_opM_assoc (comm _ mb). Qed.
+  Lemma cmra_opM_opM_swap_L `{!LeibnizEquiv A} a mb mc : a ⋅? mb ⋅? mc = a ⋅? mc ⋅? mb.
+  Proof. by rewrite !cmra_opM_opM_assoc_L (comm_L _ mb). Qed.
 
   Global Instance Some_core_id a : CoreId a → CoreId (Some a).
   Proof. by constructor. Qed.

theories/algebra/frac_auth.v

@@ -105,17 +105,4 @@ Section frac_auth.
   Proof.
     intros. by apply auth_update, option_local_update, prod_local_update_2.
   Qed.
-
-  Lemma frac_auth_update_alloc q a b c :
-    (∀ n : nat, ✓{n} a → ✓{n} (c ⋅ a)) →
-    ●! a ⋅ ◯!{q} b ~~> ●! (c ⋅ a) ⋅ ◯!{q} (c ⋅ b).
-  Proof. intros ?. by apply frac_auth_update, op_local_update. Qed.
-
-  Lemma frac_auth_dealloc q a b c `{!Cancelable c} :
-    ●! (c ⋅ a) ⋅ ◯!{q} (c ⋅ b) ~~> ●! a ⋅ ◯!{q} b.
-  Proof.
-    apply frac_auth_update.
-    move=> n [x|] /= Hvalid Heq; split; eauto using cmra_validN_op_r.
-    eapply (cancelableN c); by rewrite ?assoc.
-  Qed.
 End frac_auth.

theories/algebra/local_updates.v

@@ -29,7 +29,7 @@ Section updates.
     (∀ n, ✓{n} x → ✓{n} (z ⋅ x)) → (x,y) ~l~> (z ⋅ x, z ⋅ y).
   Proof.
     intros Hv n mz Hxv Hx; simpl in *; split; [by auto|].
-    by rewrite Hx -cmra_opM_assoc.
+    by rewrite Hx -cmra_op_opM_assoc.
   Qed.
   Lemma op_local_update_discrete `{!CmraDiscrete A} x y z :
     (✓ x → ✓ (z ⋅ x)) → (x,y) ~l~> (z ⋅ x, z ⋅ y).
@@ -41,15 +41,15 @@ Section updates.
     (x,y) ~l~> (x',y') → (x,y ⋅ yf) ~l~> (x', y' ⋅ yf).
   Proof.
     intros Hup n mz Hxv Hx; simpl in *.
-    destruct (Hup n (Some (yf ⋅? mz))); [done|by rewrite /= -cmra_opM_assoc|].
-    by rewrite cmra_opM_assoc.
+    destruct (Hup n (Some (yf ⋅? mz))); [done|by rewrite /= -cmra_op_opM_assoc|].
+    by rewrite cmra_op_opM_assoc.
   Qed.
 
   Lemma cancel_local_update x y z `{!Cancelable x} :
     (x ⋅ y, x ⋅ z) ~l~> (y, z).
   Proof.
     intros n f ? Heq. split; first by eapply cmra_validN_op_r.
-    apply (cancelableN x); first done. by rewrite -cmra_opM_assoc.
+    apply (cancelableN x); first done. by rewrite -cmra_op_opM_assoc.
   Qed.
 
   Lemma local_update_discrete `{!CmraDiscrete A} (x y x' y' : A) :

theories/algebra/updates.v

@@ -64,10 +64,10 @@ Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
 Proof.
   intros Hx1 Hx2 Hy n mz ?.
   destruct (Hx1 n (Some (x2 ⋅? mz))) as (y1&?&?).
-  { by rewrite /= -cmra_opM_assoc. }
+  { by rewrite /= -cmra_op_opM_assoc. }
   destruct (Hx2 n (Some (y1 ⋅? mz))) as (y2&?&?).
-  { by rewrite /= -cmra_opM_assoc (comm _ x2) cmra_opM_assoc. }
-  exists (y1 ⋅ y2); split; last rewrite (comm _ y1) cmra_opM_assoc; auto.
+  { by rewrite /= -cmra_op_opM_assoc (comm _ x2) cmra_op_opM_assoc. }
+  exists (y1 ⋅ y2); split; last rewrite (comm _ y1) cmra_op_opM_assoc; auto.
 Qed.
 Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 :
   x1 ~~>: P1 → x2 ~~>: P2 →
@@ -79,7 +79,7 @@ Proof.
 Qed.
 
 Lemma cmra_update_op_l x y : x ⋅ y ~~> x.
-Proof. intros n mz. rewrite comm cmra_opM_assoc. apply cmra_validN_op_r. Qed.
+Proof. intros n mz. rewrite comm cmra_op_opM_assoc. apply cmra_validN_op_r. Qed.
 Lemma cmra_update_op_r x y : x ⋅ y ~~> y.
 Proof. rewrite comm. apply cmra_update_op_l. Qed.
 

theories/base_logic/lib/cancelable_invariants.v

@@ -62,12 +62,19 @@ Section proofs.
     - iIntros "?". iApply "HP'". iApply "HP''". done.
   Qed.
 
-  Lemma cinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, cinv N γ P ∗ cinv_own γ 1.
+  Lemma cinv_alloc_strong (G : gset gname) E N :
+    (|={E}=> ∃ γ, ⌜ γ ∉ G ⌝ ∧ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P)%I.
   Proof.
-    iIntros "HP".
-    iMod (own_alloc 1%Qp) as (γ) "H1"; first done.
+    iMod (own_alloc_strong 1%Qp G) as (γ) "[Hfresh Hγ]"; first done.
+    iExists γ; iIntros "!> {$Hγ $Hfresh}" (P) "HP".
     iMod (inv_alloc N _ (P ∨ own γ 1%Qp)%I with "[HP]"); first by eauto.
-    iExists _. iFrame. iExists _. iFrame. iIntros "!> !# !>". iSplit; by iIntros "?".
+    iIntros "!>". iExists P. iSplit; last done. iIntros "!# !>"; iSplit; auto.
+  Qed.
+
+  Lemma cinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, cinv N γ P ∗ cinv_own γ 1.
+  Proof.
+    iIntros "HP". iMod (cinv_alloc_strong ∅ E N) as (γ _) "[Hγ Halloc]".
+    iExists γ. iFrame "Hγ". by iApply "Halloc".
   Qed.
 
   Lemma cinv_cancel E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P.