fix validity proof for mono_list

iris/base_logic/lib/mono_list.v

@@ -4,38 +4,40 @@
     list [l]
   - a persistent assertion [mono_list_lb_own γ l] witnessing that the authoritative
     list is at least [l]
-  - a persistent assertion [mono_list_idx_own γ i a] witnessing that the index [i] is
-    [a] in the authoritative list.
-
-The key rules are [mono_list_lb_own_valid], which asserts that an auth at [l] and
-a lower-bound at [l'] imply that [l' `prefix_of` l], and [mono_list_update], which
-allows one to grow the auth element by appending only. At any time the auth list
-can be "snapshotted" with [mono_list_get_lb] to produce a persistent lower-bound. *)
+  - a persistent assertion [mono_list_idx_own γ i a] witnessing that the index [i]
+    is [a] in the authoritative list.
+
+The key rules are [mono_list_lb_own_valid], which asserts that an auth at [l]
+and a lower-bound at [l'] imply that [l' `prefix_of` l], and [mono_list_update],
+which allows one to grow the auth element by appending only. At any time the
+auth list can be "snapshotted" with [mono_list_lb_own_get] to produce a
+persistent lower-bound. *)
 From iris.proofmode Require Import tactics.
 From iris.algebra.lib Require Import mono_list.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Export own.
 From iris.prelude Require Import options.
 
-Class alistG (A: Type) `{EqDecision A} Σ :=
+Class mono_listG (A: Type) `{EqDecision A} Σ :=
   { mono_list_inG :> inG Σ (mono_listR A) }.
-Definition alistΣ (A: Type) `{EqDecision A} : gFunctors :=
+Definition mono_listΣ (A: Type) `{EqDecision A} : gFunctors :=
   #[GFunctor (mono_listR A)].
 
-#[global] Instance subG_alistΣ (A: Type) `{EqDecision A} {Σ} :
-  subG (alistΣ A) Σ → (alistG A) Σ.
+#[global] Instance subG_mono_listΣ (A: Type) `{EqDecision A} {Σ} :
+  subG (mono_listΣ A) Σ → (mono_listG A) Σ.
 Proof. solve_inG. Qed.
 
-Definition mono_list_auth_own_def `{EqDecision A} `{!alistG A Σ}
+(* [mono_list_auth_own] also includes [mono_list_lb_own].  *)
+Definition mono_list_auth_own_def `{EqDecision A} `{!mono_listG A Σ}
     (γ : gname) (q : Qp) (l : list A) : iProp Σ :=
-  own γ (●ML{#q} l).
+  own γ (●ML{#q} l ⋅ ◯ML l).
 Definition mono_list_auth_own_aux : seal (@mono_list_auth_own_def). Proof. by eexists. Qed.
 Definition mono_list_auth_own := mono_list_auth_own_aux.(unseal).
 Definition mono_list_auth_own_eq :
   @mono_list_auth_own = @mono_list_auth_own_def := mono_list_auth_own_aux.(seal_eq).
 #[global] Arguments mono_list_auth_own {A _ Σ _} γ q l.
 
-Definition mono_list_lb_own_def `{EqDecision A} `{!alistG A Σ}
+Definition mono_list_lb_own_def `{EqDecision A} `{!mono_listG A Σ}
   (γ : gname) (l : list A) : iProp Σ :=
   own γ (◯ML l).
 Definition mono_list_lb_own_aux : seal (@mono_list_lb_own_def). Proof. by eexists. Qed.
@@ -44,7 +46,7 @@ Definition mono_list_lb_own_eq :
   @mono_list_lb_own = @mono_list_lb_own_def := mono_list_lb_own_aux.(seal_eq).
 #[global] Arguments mono_list_lb_own {A _ Σ _} γ l.
 
-Definition mono_list_idx_own `{EqDecision A} `{!alistG A Σ}
+Definition mono_list_idx_own `{EqDecision A} `{!mono_listG A Σ}
   (γ : gname) (i : nat) (a : A) : iProp Σ :=
   ∃ l : list A, ⌜ l !! i = Some a ⌝ ∗ mono_list_lb_own γ l.
 
@@ -53,7 +55,7 @@ Definition mono_list_idx_own `{EqDecision A} `{!alistG A Σ}
   ?mono_list_lb_own_eq /mono_list_lb_own_def.
 
 Section mono_list_own.
-  Context `{EqDecision A} `{!alistG A Σ}.
+  Context `{EqDecision A} `{!mono_listG A Σ}.
   Implicit Types (l : list A) (i : nat) (a : A).
 
   #[global] Instance mono_list_auth_own_timeless γ q l : Timeless (mono_list_auth_own γ q l).
@@ -69,7 +71,11 @@ Section mono_list_own.
 
   #[global] Instance mono_list_auth_own_fractional γ l :
     Fractional (λ q, mono_list_auth_own γ q l).
-  Proof. unseal. intros p q. by rewrite -own_op mono_list_auth_frac_op. Qed.
+  Proof.
+    unseal. intros p q. rewrite -own_op mono_list_auth_frac_op.
+    rewrite (comm _ (●ML{#q} _)) -!assoc (assoc _ (◯ML _)).
+    by rewrite -core_id_dup (comm _ (◯ML _)).
+  Qed.
   #[global] Instance mono_list_auth_own_as_fractional γ q l :
     AsFractional (mono_list_auth_own γ q l) (λ q, mono_list_auth_own γ q l) q.
   Proof. split; [auto|apply _]. Qed.
@@ -80,24 +86,31 @@ Section mono_list_own.
     ⌜(q1 + q2 ≤ 1)%Qp ∧ l1 = l2⌝.
   Proof.
     unseal. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %?%mono_list_auth_frac_op_valid; done.
+    iDestruct (own_valid_2 with "H1 H2") as %Hvalid.
+    iPureIntro.
+    move : Hvalid. rewrite -assoc (comm _ _ (●ML{#q2} _ ⋅ _)) 2!assoc.
+    by intros ?%cmra_valid_op_l%cmra_valid_op_l%mono_list_auth_frac_op_valid.
   Qed.
   Lemma mono_list_auth_own_exclusive γ l1 l2 :
     mono_list_auth_own γ 1 l1 -∗ mono_list_auth_own γ 1 l2 -∗ False.
   Proof.
-    unseal. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %?%mono_list_auth_op_valid; done.
+    iIntros "H1 H2".
+    iDestruct (mono_list_auth_own_agree with "H1 H2") as %[]; done.
   Qed.
 
   Lemma mono_list_lb_own_valid γ q l1 l2 :
-    mono_list_auth_own γ q l1 -∗ mono_list_lb_own γ l2 -∗ ⌜ (q ≤ 1)%Qp ∧ l2 `prefix_of` l1 ⌝.
+    mono_list_auth_own γ q l1 -∗
+    mono_list_lb_own γ l2 -∗
+    ⌜ (q ≤ 1)%Qp ∧ l2 `prefix_of` l1 ⌝.
   Proof.
     unseal. iIntros "Hauth Hlb".
-    iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mono_list_both_dfrac_valid.
-    auto.
+    iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid.
+    iPureIntro.
+    move : Hvalid. rewrite -assoc (comm _ (◯ML _)) assoc.
+    by intros ?%cmra_valid_op_l%mono_list_both_dfrac_valid.
   Qed.
 
-  Lemma mono_list_lb_own_agree γ l1 l2 :
+  Lemma mono_list_lb_own_valid_prefix γ l1 l2 :
     mono_list_lb_own γ l1 -∗
     mono_list_lb_own γ l2 -∗
     ⌜ l1 `prefix_of` l2 ∨ l2 `prefix_of` l1 ⌝.
@@ -111,7 +124,7 @@ Section mono_list_own.
     mono_list_idx_own γ i a1 -∗ mono_list_idx_own γ i a2 -∗ ⌜ a1 = a2 ⌝.
   Proof.
     iDestruct 1 as (l1 Hl1) "H1". iDestruct 1 as (l2 Hl2) "H2".
-    iDestruct (mono_list_lb_own_agree with "H1 H2") as %Hpre.
+    iDestruct (mono_list_lb_own_valid_prefix with "H1 H2") as %Hpre.
     iPureIntro.
     destruct Hpre as [Hpre|Hpre]; eapply prefix_lookup in Hpre; eauto; congruence.
   Qed.
@@ -125,22 +138,17 @@ Section mono_list_own.
     eapply prefix_lookup in Hpre; eauto; congruence.
   Qed.
 
-  (* If mono_list_auth_own is changed such that it also includes mono_list_lb_own, then
-    we won't need a frame-preserving update here. *)
-  Lemma mono_list_lb_own_get γ q l l' :
-    l' `prefix_of` l →
-    mono_list_auth_own γ q l ==∗ mono_list_auth_own γ q l ∗ mono_list_lb_own γ l'.
-  Proof.
-    intros. unseal. rewrite -own_op. by apply own_update, mono_list_update_frag.
-  Qed.
-  Lemma mono_list_lb_own_get_1 γ q l :
-    mono_list_auth_own γ q l ==∗ mono_list_auth_own γ q l ∗ mono_list_lb_own γ l.
-  Proof. by apply mono_list_lb_own_get. Qed.
-
-  Lemma mono_list_lb_own_prefix γ l l' :
+  Lemma mono_list_lb_own_get γ q l :
+    mono_list_auth_own γ q l -∗ mono_list_lb_own γ l.
+  Proof. intros. unseal. rewrite own_op. by iDestruct 1 as "[_ $]". Qed.
+  Lemma mono_list_lb_own_get_prefix γ l l' :
     l' `prefix_of` l →
     mono_list_lb_own γ l -∗ mono_list_lb_own γ l'.
   Proof. unseal. intros. by apply own_mono, mono_list_frag_included. Qed.
+  Lemma mono_list_lb_own_get_1 γ q l l' :
+    l' `prefix_of` l →
+    mono_list_auth_own γ q l -∗ mono_list_lb_own γ l'.
+  Proof. intros. rewrite mono_list_lb_own_get. by apply mono_list_lb_own_get_prefix. Qed.
 
   Lemma mono_list_lb_own_idx_lookup γ l i a :
     l !! i = Some a →
@@ -148,19 +156,15 @@ Section mono_list_own.
   Proof. iIntros (Hli) "Hl". iExists l. by iFrame. Qed.
 
   Lemma mono_list_own_alloc l :
-    ⊢ |==> ∃ γ, mono_list_auth_own γ 1 l ∗ mono_list_lb_own γ l.
-  Proof.
-    unseal. setoid_rewrite <-own_op. by apply own_alloc, mono_list_both_valid.
-  Qed.
+    ⊢ |==> ∃ γ, mono_list_auth_own γ 1 l.
+  Proof. unseal. by apply own_alloc, mono_list_both_valid. Qed.
 
   Lemma mono_list_auth_own_update γ l l' :
     l `prefix_of` l' →
-    mono_list_auth_own γ 1 l ==∗ mono_list_auth_own γ 1 l' ∗ mono_list_lb_own γ l'.
-  Proof.
-    intros. unseal. rewrite -own_op. by apply own_update, mono_list_update_alloc.
-  Qed.
+    mono_list_auth_own γ 1 l ==∗ mono_list_auth_own γ 1 l'.
+  Proof. intros. unseal. by apply own_update, mono_list_update. Qed.
 
   Lemma mono_list_auth_own_update_app γ l l' :
-    mono_list_auth_own γ 1 l ==∗ mono_list_auth_own γ 1 (l ++ l') ∗ mono_list_lb_own γ (l ++ l').
+    mono_list_auth_own γ 1 l ==∗ mono_list_auth_own γ 1 (l ++ l').
   Proof. by apply mono_list_auth_own_update, prefix_app_r. Qed.
 End mono_list_own.