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

algebra/auth.v

@@ -3,7 +3,7 @@ From iris.algebra Require Import upred updates.
 Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
 
-Record auth (A : Type) := Auth { authoritative : option (excl A); auth_own : A }.
+Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
 Add Printing Constructor auth.
 Arguments Auth {_} _ _.
 Arguments authoritative {_} _.
@@ -14,7 +14,7 @@ Notation "● a" := (Auth (Excl' a) ∅) (at level 20).
 (* COFE *)
 Section cofe.
 Context {A : cofeT}.
-Implicit Types a : option (excl A).
+Implicit Types a : excl' A.
 Implicit Types b : A.
 Implicit Types x y : auth A.
 

algebra/cmra.v

@@ -520,6 +520,64 @@ Section ucmra.
 End ucmra.
 Hint Immediate cmra_unit_total.
 
+
+(** * Properties about CMRAs with Leibniz equality *)
+Section cmra_leibniz.
+  Context {A : cmraT} `{!LeibnizEquiv A}.
+  Implicit Types x y : A.
+
+  Global Instance cmra_assoc_L : Assoc (=) (@op A _).
+  Proof. intros x y z. unfold_leibniz. by rewrite assoc. Qed.
+  Global Instance cmra_comm_L : Comm (=) (@op A _).
+  Proof. intros x y. unfold_leibniz. by rewrite comm. Qed.
+
+  Lemma cmra_pcore_l_L x cx : pcore x = Some cx → cx ⋅ x = x.
+  Proof. unfold_leibniz. apply cmra_pcore_l'. Qed.
+  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.
+
+  (** ** Core *)
+  Lemma cmra_pcore_r_L x cx : pcore x = Some cx → x ⋅ cx = x.
+  Proof. unfold_leibniz. apply cmra_pcore_r'. Qed.
+  Lemma cmra_pcore_dup_L x cx : pcore x = Some cx → cx = cx ⋅ cx.
+  Proof. unfold_leibniz. apply cmra_pcore_dup'. Qed.
+
+  (** ** Persistent elements *)
+  Lemma persistent_dup_L x `{!Persistent x} : x ≡ x ⋅ x.
+  Proof. unfold_leibniz. by apply persistent_dup. Qed.
+
+  (** ** Total core *)
+  Section total_core.
+    Context `{CMRATotal A}.
+
+    Lemma cmra_core_r_L x : x ⋅ core x = x.
+    Proof. unfold_leibniz. apply cmra_core_r. Qed.
+    Lemma cmra_core_l_L x : core x ⋅ x = x.
+    Proof. unfold_leibniz. apply cmra_core_l. Qed.
+    Lemma cmra_core_idemp_L x : core (core x) = core x.
+    Proof. unfold_leibniz. apply cmra_core_idemp. Qed.
+    Lemma cmra_core_dup_L x : core x = core x ⋅ core x.
+    Proof. unfold_leibniz. apply cmra_core_dup. Qed.
+    Lemma persistent_total_L x : Persistent x ↔ core x = x.
+    Proof. unfold_leibniz. apply persistent_total. Qed.
+    Lemma persistent_core_L x `{!Persistent x} : core x = x.
+    Proof. by apply persistent_total_L. Qed.
+  End total_core.
+End cmra_leibniz.
+
+Section ucmra_leibniz.
+  Context {A : ucmraT} `{!LeibnizEquiv A}.
+  Implicit Types x y z : A.
+
+  Global Instance ucmra_unit_left_id_L : LeftId (=) ∅ (@op A _).
+  Proof. intros x. unfold_leibniz. by rewrite left_id. Qed.
+  Global Instance ucmra_unit_right_id_L : RightId (=) ∅ (@op A _).
+  Proof. intros x. unfold_leibniz. by rewrite right_id. Qed.
+End ucmra_leibniz.
+
 (** * Constructing a CMRA with total core *)
 Section cmra_total.
   Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}.
@@ -1005,7 +1063,7 @@ Section option.
   Proof. by destruct my. Qed.
 
   Lemma option_included (mx my : option A) :
-    mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ (x ≼ y ∨ x ≡ y).
+    mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ (x ≡ y ∨ x ≼ y).
   Proof.
     split.
     - intros [mz Hmz].
@@ -1013,10 +1071,10 @@ Section option.
       destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
       destruct mz as [z|]; inversion_clear Hmz; split_and?; auto;
         setoid_subst; eauto using cmra_included_l.
-    - intros [->|(x&y&->&->&[[z Hz]|Hz])].
+    - intros [->|(x&y&->&->&[Hz|[z Hz]])].
       + exists my. by destruct my.
-      + exists (Some z); by constructor.
       + exists None; by constructor.
+      + exists (Some z); by constructor.
   Qed.
 
   Lemma option_cmra_mixin : CMRAMixin (option A).
@@ -1036,10 +1094,10 @@ Section option.
       destruct (pcore x) as [cx|] eqn:?; simpl; eauto using cmra_pcore_idemp.
     - intros mx my; setoid_rewrite option_included.
       intros [->|(x&y&->&->&[?|?])]; simpl; eauto.
-      + destruct (pcore x) as [cx|] eqn:?; eauto.
-        destruct (cmra_pcore_mono x y cx) as (?&?&?); eauto 10.
       + destruct (pcore x) as [cx|] eqn:?; eauto.
         destruct (cmra_pcore_proper x y cx) as (?&?&?); eauto 10.
+      + destruct (pcore x) as [cx|] eqn:?; eauto.
+        destruct (cmra_pcore_mono x y cx) as (?&?&?); eauto 10.
     - intros n [x|] [y|]; rewrite /validN /option_validN /=;
         eauto using cmra_validN_op_l.
     - intros n mx my1 my2.
@@ -1084,6 +1142,13 @@ Section option.
   Lemma exclusiveN_Some_r n x `{!Exclusive x} my :
     ✓{n} (my ⋅ Some x) → my = None.
   Proof. rewrite comm. by apply exclusiveN_Some_l. Qed.
+
+  Lemma Some_included x y : Some x ≼ Some y ↔ x ≡ y ∨ x ≼ y.
+  Proof. rewrite option_included; naive_solver. Qed.
+  Lemma Some_included' `{CMRATotal A} x y : Some x ≼ Some y ↔ x ≡ y ∨ x ≼ y.
+  Proof. rewrite Some_included; naive_solver. Qed.
+  Lemma is_Some_included mx my : mx ≼ my → is_Some mx → is_Some my.
+  Proof. rewrite -!not_eq_None_Some option_included. naive_solver. Qed.
 End option.
 
 Arguments optionR : clear implicits.
@@ -1095,8 +1160,8 @@ Proof.
   split; first apply _.
   - intros n [x|] ?; rewrite /cmra_validN //=. by apply (validN_preserving f).
   - intros mx my; rewrite !option_included.
-    intros [->|(x&y&->&->&[?|Hxy])]; simpl; eauto 10 using @cmra_monotone.
-    right; exists (f x), (f y). by rewrite {4}Hxy; eauto.
+    intros [->|(x&y&->&->&[Hxy|?])]; simpl; eauto 10 using @cmra_monotone.
+    right; exists (f x), (f y). by rewrite {3}Hxy; eauto.
 Qed.
 Program Definition optionURF (F : rFunctor) : urFunctor := {|
   urFunctor_car A B := optionUR (rFunctor_car F A B);

algebra/coPset.v

@@ -27,6 +27,13 @@ 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.
+  Proof.
+    split.
+    - move=> [[Z|]]; simpl; try case_decide; set_solver.
+    - intros (Z&->&?)%subseteq_disjoint_union_L.
+      exists (CoPset Z). coPset_disj_solve.
+  Qed.
   Lemma coPset_disj_valid_inv_l X Y :
     ✓ (CoPset X ⋅ Y) → ∃ Y', Y = CoPset Y' ∧ X ⊥ Y'.
   Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.

algebra/excl.v

@@ -9,6 +9,7 @@ Inductive excl (A : Type) :=
 Arguments Excl {_} _.
 Arguments ExclBot {_}.
 
+Notation excl' A := (option (excl A)).
 Notation Excl' x := (Some (Excl x)).
 Notation ExclBot' := (Some ExclBot).
 

algebra/gmap.v

@@ -258,12 +258,6 @@ Proof.
       * by rewrite Hi lookup_op lookup_singleton lookup_delete.
       * by rewrite lookup_op lookup_singleton_ne // lookup_delete_ne // left_id.
 Qed.
-Lemma dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) = dom _ m1 ∪ dom _ m2.
-Proof.
-  apply elem_of_equiv_L=> i; rewrite elem_of_union !elem_of_dom.
-  unfold is_Some; setoid_rewrite lookup_op.
-  destruct (m1 !! i), (m2 !! i); naive_solver.
-Qed.
 
 Lemma insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x :
   x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q.
@@ -298,6 +292,17 @@ Proof.
   - move: (Hm j). by rewrite !lookup_op lookup_delete_ne.
 Qed.
 
+Lemma dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) = dom _ m1 ∪ dom _ m2.
+Proof.
+  apply elem_of_equiv_L=> i; rewrite elem_of_union !elem_of_dom.
+  unfold is_Some; setoid_rewrite lookup_op.
+  destruct (m1 !! i), (m2 !! i); naive_solver.
+Qed.
+Lemma dom_included m1 m2 : m1 ≼ m2 → dom (gset K) m1 ⊆ dom _ m2.
+Proof.
+  rewrite lookup_included=>? i; rewrite !elem_of_dom. by apply is_Some_included.
+Qed.
+
 Section freshness.
   Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
   Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x :

algebra/gset.v

@@ -28,6 +28,13 @@ 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.
+  Proof.
+    split.
+    - move=> [[Z|]]; simpl; try case_decide; set_solver.
+    - intros (Z&->&?)%subseteq_disjoint_union_L.
+      exists (GSet Z). gset_disj_solve.
+  Qed.
   Lemma gset_disj_valid_inv_l X Y : ✓ (GSet X ⋅ Y) → ∃ Y', Y = GSet Y' ∧ X ⊥ Y'.
   Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
   Lemma gset_disj_union X Y : X ⊥ Y → GSet X ⋅ GSet Y = GSet (X ∪ Y).

heap_lang/heap.v

@@ -142,7 +142,7 @@ Section heap.
     iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
     iVs (auth_empty heap_name) as "Hh".
     iVs (auth_open with "[Hh]") as (h) "[Hv [Hh Hclose]]"; eauto.
-    rewrite left_id /heap_inv. iDestruct "Hv" as %?.
+    rewrite left_id_L /heap_inv. iDestruct "Hv" as %?.
     iApply wp_alloc_pst. iFrame "Hh". iNext.
     iIntros (l) "[% Hh] !==>".
     iVs ("Hclose" $! {[ l := (1%Qp, DecAgree v) ]} with "[Hh]").