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

algebra/dec_agree.v

@@ -48,4 +48,20 @@ Qed.
 
 Canonical Structure dec_agreeRA : cmraT := discreteRA dec_agree_ra.
 
-End dec_agree.
+(* Some properties of this CMRA *)
\ No newline at end of file
+Lemma dec_agree_idemp (x : dec_agree A) : x ⋅ x ≡ x.
+Proof.
+  destruct x as [x|]; simpl; repeat (case_match; simpl); try subst; congruence.
+Qed.
+
+Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : ✓ (x1 ⋅ x2) → x1 ≡ x2.
+Proof.
+  destruct x1 as [x1|], x2 as [x2|]; simpl;repeat (case_match; simpl); by subst.
+Qed.
+
+Lemma dec_agree_equivI {M} a b : (DecAgree a ≡ DecAgree b)%I ≡ (a = b : uPred M)%I.
+Proof. split. by case. by destruct 1. Qed.
+Lemma dec_agree_validI {M} (x y : dec_agreeRA) : ✓ (x ⋅ y) ⊑ (x = y : uPred M).
+Proof. intros r n _ ?. by apply: dec_agree_op_inv. Qed.
+
+End dec_agree.

barrier/client.v

@@ -29,11 +29,11 @@ Section ClosedProofs.
 
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
   Proof.
-    apply ht_alt. rewrite (heap_alloc ⊤ (nroot .: "Barrier")); last first.
+    apply ht_alt. rewrite (heap_alloc ⊤ (nroot ..: "Barrier")); last first.
     { (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *)
       by move=>? _. }
     apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
-    rewrite -(client_safe (nroot .: "Heap" ) (nroot .: "Barrier" )) //.
+    rewrite -(client_safe (nroot ..: "Heap" ) (nroot ..: "Barrier" )) //.
     (* This, too, should be automated. *)
     by apply ndot_ne_disjoint.
   Qed.

program_logic/namespaces.v

@@ -7,8 +7,8 @@ Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
   encode x :: N.
 Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
 
-Infix ".:" := ndot (at level 19, left associativity) : C_scope.
-Notation "(.:)" := ndot (only parsing) : C_scope.
+Infix "..:" := ndot (at level 19, left associativity) : C_scope.
+Notation "(..:)" := ndot (only parsing) : C_scope.
 
 Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
 Proof. by intros N1 x1 N2 x2 ?; simplify_eq. Qed.
@@ -16,13 +16,13 @@ Lemma nclose_nroot : nclose nroot = ⊤.
 Proof. by apply (sig_eq_pi _). Qed.
 Lemma encode_nclose N : encode N ∈ nclose N.
 Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed.
-Lemma nclose_subseteq `{Countable A} N x : nclose (N .: x) ⊆ nclose N.
+Lemma nclose_subseteq `{Countable A} N x : nclose (N ..: x) ⊆ nclose N.
 Proof.
   intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->].
-  destruct (list_encode_suffix N (N .: x)) as [q' ?]; [by exists [encode x]|].
+  destruct (list_encode_suffix N (N ..: x)) as [q' ?]; [by exists [encode x]|].
   by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
 Qed.
-Lemma ndot_nclose `{Countable A} N x : encode (N .: x) ∈ nclose N.
+Lemma ndot_nclose `{Countable A} N x : encode (N ..: x) ∈ nclose N.
 Proof. apply nclose_subseteq with x, encode_nclose. Qed.
 
 Instance ndisjoint : Disjoint namespace := λ N1 N2,
@@ -36,16 +36,16 @@ Section ndisjoint.
   Global Instance ndisjoint_comm : Comm iff ndisjoint.
   Proof. intros N1 N2. rewrite /disjoint /ndisjoint; naive_solver. Qed.
 
-  Lemma ndot_ne_disjoint N (x y : A) : x ≠ y → N .: x ⊥ N .: y.
-  Proof. intros Hxy. exists (N .: x), (N .: y); naive_solver. Qed.
+  Lemma ndot_ne_disjoint N (x y : A) : x ≠ y → N ..: x ⊥ N ..: y.
+  Proof. intros Hxy. exists (N ..: x), (N ..: y); naive_solver. Qed.
 
-  Lemma ndot_preserve_disjoint_l N1 N2 x : N1 ⊥ N2 → N1 .: x ⊥ N2.
+  Lemma ndot_preserve_disjoint_l N1 N2 x : N1 ⊥ N2 → N1 ..: x ⊥ N2.
   Proof.
     intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'.
     split_and?; try done; []. by apply suffix_of_cons_r.
   Qed.
 
-  Lemma ndot_preserve_disjoint_r N1 N2 x : N1 ⊥ N2 → N1 ⊥ N2 .: x .
+  Lemma ndot_preserve_disjoint_r N1 N2 x : N1 ⊥ N2 → N1 ⊥ N2 ..: x .
   Proof. rewrite ![N1 ⊥ _]comm. apply ndot_preserve_disjoint_l. Qed.
 
   Lemma ndisj_disjoint N1 N2 : N1 ⊥ N2 → nclose N1 ∩ nclose N2 = ∅.