Commit e030bb98 authored by Hai Dang's avatar Hai Dang
Browse files

Fix mono_listR to have a fragment; follows naming convention with max_nat

parent 63e031ca
...@@ -13,14 +13,12 @@ Implicit Type l : list A. ...@@ -13,14 +13,12 @@ Implicit Type l : list A.
Definition mono_listR : cmra := authR (max_listUR A). Definition mono_listR : cmra := authR (max_listUR A).
Definition mono_listUR : ucmra := authUR (max_listUR A). Definition mono_listUR : ucmra := authUR (max_listUR A).
Definition mono_list_auth q l : mono_listR := {q} (MList l). Definition mono_list_auth q l : mono_listR := {q} (MList l) (MList l).
Definition mono_list_frag l : mono_listR := (MList l). Definition mono_list_lb l : mono_listR := (MList l).
End mono_list_defs. End mono_list_defs.
#[global] Arguments mono_list_auth {_ _} _ _. #[global] Arguments mono_list_auth {_ _} _ _.
#[global] Arguments mono_list_frag {_ _} _. #[global] Arguments mono_list_lb {_ _} _.
Typeclasses Opaque mono_list_auth mono_list_frag.
(** FIXME: Refactor these notations using custom entries once Coq bug #13654 (** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *) has been fixed. *)
...@@ -28,7 +26,7 @@ Notation "●ML{ dq } l" := (mono_list_auth dq l) (at level 20, format "●ML{ d ...@@ -28,7 +26,7 @@ Notation "●ML{ dq } l" := (mono_list_auth dq l) (at level 20, format "●ML{ d
Notation "●ML{# q } l" := (mono_list_auth (DfracOwn q) l) (at level 20, format "●ML{# q } l"). Notation "●ML{# q } l" := (mono_list_auth (DfracOwn q) l) (at level 20, format "●ML{# q } l").
Notation "●□ML l" := (mono_list_auth (DfracDiscarded) l) (at level 20). Notation "●□ML l" := (mono_list_auth (DfracDiscarded) l) (at level 20).
Notation "●ML l" := (mono_list_auth (DfracOwn 1) l) (at level 20). Notation "●ML l" := (mono_list_auth (DfracOwn 1) l) (at level 20).
Notation "◯ML l" := (mono_list_frag l) (at level 20). Notation "◯ML l" := (mono_list_lb l) (at level 20).
Section mono_list_props. Section mono_list_props.
Context {A : Type} `{EqDecision A}. Context {A : Type} `{EqDecision A}.
...@@ -37,77 +35,105 @@ Implicit Types x y : authR (max_listUR A). ...@@ -37,77 +35,105 @@ Implicit Types x y : authR (max_listUR A).
Implicit Types q : frac. Implicit Types q : frac.
Implicit Types dq : dfrac. Implicit Types dq : dfrac.
#[global] Instance mono_list_auth_inj : Inj2 (=) (=) () (@mono_list_auth A _). #[global] Instance mono_list_lb_core_id l : CoreId (ML l).
Proof. rewrite /mono_list_auth. by intros ???? [? ?%MList_inj]%auth_auth_inj. Qed. Proof. rewrite /mono_list_lb. apply _. Qed.
#[global] Instance mono_list_frag_inj : Inj (=) () (@mono_list_frag A _).
#[global] Instance mono_list_lb_inj : Inj (=) () (@mono_list_lb A _).
Proof. rewrite /mono_list_auth. by intros ?? ?%auth_frag_inj%MList_inj. Qed. Proof. rewrite /mono_list_auth. by intros ?? ?%auth_frag_inj%MList_inj. Qed.
(** * Operation *)
Lemma mono_list_auth_dfrac_op dq1 dq2 l :
ML{dq1 dq2} l ML{dq1} l ML{dq2} l.
Proof.
rewrite /mono_list_auth auth_auth_dfrac_op.
rewrite (comm _ ({dq2} _)) -!assoc (assoc _ ( _)).
by rewrite -core_id_dup (comm _ ( _)).
Qed.
Lemma mono_list_auth_frac_op q1 q2 l : ML{#(q1 + q2)} l ML{#q1} l ML{#q2} l.
Proof. by rewrite -mono_list_auth_dfrac_op dfrac_op_own. Qed.
Lemma mono_list_lb_op_l l1 l2 :
l1 `prefix_of` l2 ML l1 ML l2 = ML l2.
Proof. intros. by rewrite /mono_list_lb -auth_frag_op max_list_op_l. Qed.
Lemma mono_list_lb_op_r l1 l2 :
l1 `prefix_of` l2 ML l2 ML l1 = ML l2.
Proof. intros. by rewrite /mono_list_lb -auth_frag_op max_list_op_r. Qed.
#[global] Instance mono_list_lb_is_op l :
IsOp' (ML l) (ML l) (ML l).
Proof. by rewrite /IsOp' /IsOp -core_id_dup. Qed.
Lemma mono_list_auth_lb_op dq l :
ML{dq} l ML{dq} l ML l.
Proof.
by rewrite /mono_list_auth /mono_list_lb -!assoc -auth_frag_op -core_id_dup.
Qed.
Lemma mono_list_lb_op_le_l l l' :
l' `prefix_of` l ML l = ML l' ML l.
Proof. intros. by rewrite mono_list_lb_op_l. Qed.
(** * Validity *) (** * Validity *)
Lemma mono_list_auth_dfrac_valid dq l :
(ML{dq} l) dq.
Proof. rewrite /mono_list_auth auth_both_dfrac_valid_discrete. naive_solver. Qed.
Lemma mono_list_auth_valid l : (ML l).
Proof. by apply auth_both_valid. Qed.
Lemma mono_list_auth_dfrac_op_valid dq1 dq2 l1 l2 :
(ML{dq1} l1 ML{dq2} l2) (dq1 dq2) l1 = l2.
Proof.
rewrite /mono_list_auth (comm _ ({dq2} _)) -!assoc (assoc _ ( _)).
rewrite -auth_frag_op (comm _ ( _)) assoc. split.
- move=> /cmra_valid_op_l /auth_auth_dfrac_op_valid. naive_solver.
- intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op.
by apply auth_both_dfrac_valid_discrete.
Qed.
Lemma mono_list_auth_frac_op_valid q1 q2 l1 l2 :
(ML{#q1} l1 ML{#q2} l2) (q1 + q2 1)%Qp l1 = l2.
Proof. by apply mono_list_auth_dfrac_op_valid. Qed.
Lemma mono_list_auth_op_valid l1 l2 : (ML l1 ML l2) False.
Proof. rewrite mono_list_auth_dfrac_op_valid. naive_solver. Qed.
Lemma mono_list_both_dfrac_valid dq l l' : Lemma mono_list_both_dfrac_valid dq l l' :
(ML{dq} l ML l') dq l' `prefix_of` l. (ML{dq} l ML l') dq l' `prefix_of` l.
Proof. rewrite auth_both_dfrac_valid_discrete max_list_included. naive_solver. Qed. Proof.
rewrite /mono_list_auth /mono_list_lb -assoc -auth_frag_op.
rewrite auth_both_dfrac_valid_discrete. split.
- intros (? & Hincl & ?). split;[done|]. apply max_list_included.
etrans; [|exact Hincl]. eexists. by rewrite comm.
- intros [? ?]. by rewrite max_list_op_r.
Qed.
Lemma mono_list_both_valid l l' : Lemma mono_list_both_valid l l' :
(ML l ML l') l' `prefix_of` l. (ML l ML l') l' `prefix_of` l.
Proof. rewrite mono_list_both_dfrac_valid. split; [naive_solver|done]. Qed. Proof. rewrite mono_list_both_dfrac_valid. split; [naive_solver|done]. Qed.
Lemma mono_list_frag_op_valid l l' : Lemma mono_list_lb_op_valid l l' :
(ML l ML l') l `prefix_of` l' l' `prefix_of` l. (ML l ML l') l `prefix_of` l' l' `prefix_of` l.
Proof. by rewrite auth_frag_op_valid max_list_valid_op. Qed. Proof. by rewrite auth_frag_op_valid max_list_valid_op. Qed.
Lemma mono_list_frag_op_valid_1 l l' : Lemma mono_list_lb_op_valid_1 l l' :
(ML l ML l') l `prefix_of` l' l' `prefix_of` l. (ML l ML l') l `prefix_of` l' l' `prefix_of` l.
Proof. by apply mono_list_frag_op_valid. Qed. Proof. by apply mono_list_lb_op_valid. Qed.
Lemma mono_list_frag_op_valid_2 l l' : Lemma mono_list_lb_op_valid_2 l l' :
l `prefix_of` l' l' `prefix_of` l (ML l ML l'). l `prefix_of` l' l' `prefix_of` l (ML l ML l').
Proof. by apply mono_list_frag_op_valid. Qed. Proof. by apply mono_list_lb_op_valid. Qed.
Lemma mono_list_auth_dfrac_op_valid dq1 dq2 l1 l2 :
(ML{dq1} l1 ML{dq2} l2) (dq1 dq2) l1 = l2.
Proof. rewrite /mono_list_auth auth_auth_dfrac_op_valid. naive_solver. Qed.
Lemma mono_list_auth_frac_op_valid q1 q2 l1 l2 :
(ML{#q1} l1 ML{#q2} l2) (q1 + q2 1)%Qp l1 = l2.
Proof. by apply mono_list_auth_dfrac_op_valid. Qed.
Lemma mono_list_auth_op_valid l1 l2 : (ML l1 ML l2) False.
Proof. by apply auth_auth_op_valid. Qed.
(** * Operation *) Lemma mono_list_lb_mono l l' : l `prefix_of` l' ML l ML l'.
Lemma mono_list_auth_dfrac_op dq1 dq2 l : ML{dq1 dq2} l ML{dq1} l ML{dq2} l. Proof. intros. by apply auth_frag_mono, max_list_included. Qed.
Proof. by apply auth_auth_dfrac_op. Qed.
Lemma mono_list_auth_frac_op q1 q2 l : ML{#(q1 + q2)} l ML{#q1} l ML{#q2} l.
Proof. by apply auth_auth_frac_op. Qed.
Lemma mono_list_frag_op_l l1 l2 :
l1 `prefix_of` l2 ML l1 ML l2 = ML l2.
Proof. intros. by rewrite /mono_list_frag -auth_frag_op max_list_op_l. Qed.
Lemma mono_list_frag_op_r l1 l2 :
l1 `prefix_of` l2 ML l2 ML l1 = ML l2.
Proof. intros. by rewrite /mono_list_frag -auth_frag_op max_list_op_r. Qed.
Lemma mono_list_frag_included l l' :
l `prefix_of` l' ML l ML l'.
Proof. intros. exists (ML l'). by rewrite mono_list_frag_op_l. Qed.
#[global] Instance mono_list_frag_core_id l : CoreId (ML l). Lemma mono_list_included dq l : ML l ML{dq} l.
Proof. rewrite /mono_list_frag. apply _. Qed. Proof. apply cmra_included_r. Qed.
#[global] Instance mono_list_frag_is_op l :
IsOp' (ML l) (ML l) (ML l).
Proof. by rewrite /IsOp' /IsOp -core_id_dup. Qed.
(** * Update *) (** * Update *)
Lemma mono_list_update l l1 l' : Lemma mono_list_update {l} l' :
l `prefix_of` l' ML l ML l1 ~~> ML l' ML l'. l `prefix_of` l' ML l ~~> ML l'.
Proof. intros. by apply auth_update, max_list_local_update. Qed. Proof. intros. by apply auth_update, max_list_local_update. Qed.
Lemma mono_list_update_alloc l l' :
l `prefix_of` l' ML l ~~> ML l' ML l'.
Proof. intros. by apply auth_update_alloc, max_list_local_update. Qed.
Lemma mono_list_update_auth_persist dq l : ML{dq} l ~~> ●□ML l. Lemma mono_list_update_auth_persist dq l : ML{dq} l ~~> ●□ML l.
Proof. by apply auth_update_auth_persist. Qed.
Lemma mono_list_update_frag dq l l' :
l' `prefix_of` l ML{dq} l ~~> ML{dq} l ML l'.
Proof. Proof.
intros. apply auth_update_dfrac_alloc; [apply _|by apply max_list_included]. rewrite /mono_list_auth. apply cmra_update_op; [|done].
by apply auth_update_auth_persist.
Qed. Qed.
End mono_list_props. End mono_list_props.
Typeclasses Opaque mono_list_auth mono_list_lb.
...@@ -31,7 +31,7 @@ Inductive max_list_equiv : Equiv (max_list A) := ...@@ -31,7 +31,7 @@ Inductive max_list_equiv : Equiv (max_list A) :=
Existing Instance max_list_equiv. Existing Instance max_list_equiv.
#[local] Instance max_list_equiv_Equivalence : @Equivalence (max_list A) equiv. #[local] Instance max_list_equiv_equivalence : @Equivalence (max_list A) equiv.
Proof. Proof.
split. split.
- move => [|]; by constructor. - move => [|]; by constructor.
...@@ -40,16 +40,16 @@ Proof. ...@@ -40,16 +40,16 @@ Proof.
inversion 1; inversion 1; subst; by constructor. inversion 1; inversion 1; subst; by constructor.
Qed. Qed.
#[global] Instance max_list_leinbniz : LeibnizEquiv (max_list A). #[global] Instance max_list_leibniz : LeibnizEquiv (max_list A).
Proof. intros ??; inversion 1; by subst. Qed. Proof. intros ??; inversion 1; by subst. Qed.
Canonical Structure max_listC : ofe := discreteO (max_list A). Canonical Structure max_listO : ofe := discreteO (max_list A).
(* CMRA *) (* CMRA *)
Local Instance max_list_valid_instance : Valid (max_list A) := #[local] Instance max_list_valid_instance : Valid (max_list A) :=
λ x, match x with MList _ => True | MListBot => False end. λ x, match x with MList _ => True | MListBot => False end.
Local Instance max_list_op_instance : Op (max_list A) := λ x y, #[local] Instance max_list_op_instance : Op (max_list A) := λ x y,
match x, y with match x, y with
| MList l1, MList l2 => | MList l1, MList l2 =>
if (decide (l1 `prefix_of` l2)) if (decide (l1 `prefix_of` l2))
...@@ -61,11 +61,13 @@ Local Instance max_list_op_instance : Op (max_list A) := λ x y, ...@@ -61,11 +61,13 @@ Local Instance max_list_op_instance : Op (max_list A) := λ x y,
| _, _ => MListBot | _, _ => MListBot
end. end.
#[local] Instance max_list_PCore : PCore (max_list A) := Some. #[local] Instance max_list_pcore_instance : PCore (max_list A) := Some.
#[local] Instance max_list_unit_instance : Unit (max_list A) := MList [].
Local Arguments op _ _ !_ !_ /. Local Arguments op _ _ !_ !_ /.
#[global] Instance max_list_op_comm: @Comm _ (max_list A) equiv op. #[global] Instance max_list_op_comm : @Comm _ (max_list A) equiv op.
Proof. Proof.
intros [l1|] [l2|]; auto. simpl. do 2 (case_decide; [|auto]). intros [l1|] [l2|]; auto. simpl. do 2 (case_decide; [|auto]).
constructor. by apply : (anti_symm prefix). constructor. by apply : (anti_symm prefix).
...@@ -82,7 +84,7 @@ Lemma max_list_op_r l1 l2 (Le: l1 `prefix_of` l2) : ...@@ -82,7 +84,7 @@ Lemma max_list_op_r l1 l2 (Le: l1 `prefix_of` l2) :
MList l2 MList l1 = MList l2. MList l2 MList l1 = MList l2.
Proof. by rewrite -leibniz_equiv_iff comm max_list_op_l. Qed. Proof. by rewrite -leibniz_equiv_iff comm max_list_op_l. Qed.
#[global] Instance max_list_op_assoc: @Assoc (max_list A) equiv op. #[global] Instance max_list_op_assoc : @Assoc (max_list A) equiv op.
Proof. Proof.
intros [l1|] [l2|] [l3|]; auto; simpl. intros [l1|] [l2|] [l3|]; auto; simpl.
- case decide => H1; case decide => H2; [|case decide => H3..]; - case decide => H1; case decide => H2; [|case decide => H3..];
...@@ -114,21 +116,9 @@ Proof. ...@@ -114,21 +116,9 @@ Proof.
- intros. exists (MList l2). by rewrite max_list_op_l. - intros. exists (MList l2). by rewrite max_list_op_l.
Qed. Qed.
Lemma max_list_valid_op_1 l1 l2 :
(MList l1 MList l2) l1 `prefix_of` l2 l2 `prefix_of` l1.
Proof. simpl. case_decide; first by left. case_decide; [by right|done]. Qed.
Lemma max_list_valid_op_2 l1 l2 :
l1 `prefix_of` l2 l2 `prefix_of` l1 (MList l1 MList l2).
Proof. intros [?|?]; [by rewrite max_list_op_l|by rewrite max_list_op_r]. Qed.
Lemma max_list_valid_op l1 l2 :
(MList l1 MList l2) l1 `prefix_of` l2 l2 `prefix_of` l1.
Proof. split; [by apply max_list_valid_op_1|by apply max_list_valid_op_2]. Qed.
Lemma max_list_core_self (l : max_list A) : core l = l. Lemma max_list_core_self (l : max_list A) : core l = l.
Proof. done. Qed. Proof. done. Qed.
#[local] Instance max_list_unit : Unit (max_list A) := MList [].
Definition max_list_ra_mixin : RAMixin (max_list A). Definition max_list_ra_mixin : RAMixin (max_list A).
Proof. Proof.
apply ra_total_mixin; eauto. apply ra_total_mixin; eauto.
...@@ -158,6 +148,16 @@ Proof. intros ??; inversion 1; by subst. Qed. ...@@ -158,6 +148,16 @@ Proof. intros ??; inversion 1; by subst. Qed.
#[global] Instance max_list_core_id (x : max_list A) : CoreId x. #[global] Instance max_list_core_id (x : max_list A) : CoreId x.
Proof. by constructor. Qed. Proof. by constructor. Qed.
Lemma max_list_valid_op_1 l1 l2 :
(MList l1 MList l2) l1 `prefix_of` l2 l2 `prefix_of` l1.
Proof. simpl. case_decide; first by left. case_decide; [by right|done]. Qed.
Lemma max_list_valid_op_2 l1 l2 :
l1 `prefix_of` l2 l2 `prefix_of` l1 (MList l1 MList l2).
Proof. intros [?|?]; [by rewrite max_list_op_l|by rewrite max_list_op_r]. Qed.
Lemma max_list_valid_op l1 l2 :
(MList l1 MList l2) l1 `prefix_of` l2 l2 `prefix_of` l1.
Proof. split; [by apply max_list_valid_op_1|by apply max_list_valid_op_2]. Qed.
Lemma max_list_absorb (x y : max_listR) : Lemma max_list_absorb (x y : max_listR) :
x y x y x. x y x y x.
Proof. Proof.
......
...@@ -19,7 +19,7 @@ From iris.base_logic.lib Require Export own. ...@@ -19,7 +19,7 @@ From iris.base_logic.lib Require Export own.
From iris.prelude Require Import options. From iris.prelude Require Import options.
Class mono_listG (A: Type) `{EqDecision A} Σ := Class mono_listG (A: Type) `{EqDecision A} Σ :=
{ mono_list_inG :> inG Σ (mono_listR A) }. MonoListG { mono_list_inG :> inG Σ (mono_listR A) }.
Definition mono_listΣ (A: Type) `{EqDecision A} : gFunctors := Definition mono_listΣ (A: Type) `{EqDecision A} : gFunctors :=
#[GFunctor (mono_listR A)]. #[GFunctor (mono_listR A)].
...@@ -27,10 +27,9 @@ Definition mono_listΣ (A: Type) `{EqDecision A} : gFunctors := ...@@ -27,10 +27,9 @@ Definition mono_listΣ (A: Type) `{EqDecision A} : gFunctors :=
subG (mono_listΣ A) Σ (mono_listG A) Σ. subG (mono_listΣ A) Σ (mono_listG A) Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
(* [mono_list_auth_own] also includes [mono_list_lb_own]. *)
Definition mono_list_auth_own_def `{EqDecision A} `{!mono_listG A Σ} Definition mono_list_auth_own_def `{EqDecision A} `{!mono_listG A Σ}
(γ : gname) (q : Qp) (l : list A) : iProp Σ := (γ : gname) (q : Qp) (l : list A) : iProp Σ :=
own γ (ML{#q} l ML l). own γ (ML{#q} l).
Definition mono_list_auth_own_aux : seal (@mono_list_auth_own_def). Proof. by eexists. Qed. 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 := mono_list_auth_own_aux.(unseal).
Definition mono_list_auth_own_eq : Definition mono_list_auth_own_eq :
...@@ -71,11 +70,7 @@ Section mono_list_own. ...@@ -71,11 +70,7 @@ Section mono_list_own.
#[global] Instance mono_list_auth_own_fractional γ l : #[global] Instance mono_list_auth_own_fractional γ l :
Fractional (λ q, mono_list_auth_own γ q l). Fractional (λ q, mono_list_auth_own γ q l).
Proof. Proof. unseal. intros p q. by rewrite -own_op mono_list_auth_frac_op. Qed.
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 : #[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. AsFractional (mono_list_auth_own γ q l) (λ q, mono_list_auth_own γ q l) q.
Proof. split; [auto|apply _]. Qed. Proof. split; [auto|apply _]. Qed.
...@@ -86,10 +81,8 @@ Section mono_list_own. ...@@ -86,10 +81,8 @@ Section mono_list_own.
(q1 + q2 1)%Qp l1 = l2. (q1 + q2 1)%Qp l1 = l2.
Proof. Proof.
unseal. iIntros "H1 H2". unseal. iIntros "H1 H2".
iDestruct (own_valid_2 with "H1 H2") as %Hvalid. iDestruct (own_valid_2 with "H1 H2") as %Hvalid%mono_list_auth_frac_op_valid;
iPureIntro. done.
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. Qed.
Lemma mono_list_auth_own_exclusive γ l1 l2 : Lemma mono_list_auth_own_exclusive γ l1 l2 :
mono_list_auth_own γ 1 l1 - mono_list_auth_own γ 1 l2 - False. mono_list_auth_own γ 1 l1 - mono_list_auth_own γ 1 l2 - False.
...@@ -104,10 +97,8 @@ Section mono_list_own. ...@@ -104,10 +97,8 @@ Section mono_list_own.
(q 1)%Qp l2 `prefix_of` l1 . (q 1)%Qp l2 `prefix_of` l1 .
Proof. Proof.
unseal. iIntros "Hauth Hlb". unseal. iIntros "Hauth Hlb".
iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid. iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mono_list_both_dfrac_valid;
iPureIntro. done.
move : Hvalid. rewrite -assoc (comm _ (ML _)) assoc.
by intros ?%cmra_valid_op_l%mono_list_both_dfrac_valid.
Qed. Qed.
Lemma mono_list_lb_own_valid_prefix γ l1 l2 : Lemma mono_list_lb_own_valid_prefix γ l1 l2 :
...@@ -116,8 +107,7 @@ Section mono_list_own. ...@@ -116,8 +107,7 @@ Section mono_list_own.
l1 `prefix_of` l2 l2 `prefix_of` l1 . l1 `prefix_of` l2 l2 `prefix_of` l1 .
Proof. Proof.
unseal. iIntros "H1 H2". unseal. iIntros "H1 H2".
iDestruct (own_valid_2 with "H1 H2") as %?%mono_list_frag_op_valid_1. iDestruct (own_valid_2 with "H1 H2") as %?%mono_list_lb_op_valid_1; done.
auto.
Qed. Qed.
Lemma mono_list_idx_own_agree γ i a1 a2 : Lemma mono_list_idx_own_agree γ i a1 a2 :
...@@ -140,15 +130,11 @@ Section mono_list_own. ...@@ -140,15 +130,11 @@ Section mono_list_own.
Lemma mono_list_lb_own_get γ q l : Lemma mono_list_lb_own_get γ q l :
mono_list_auth_own γ q l - mono_list_lb_own γ l. mono_list_auth_own γ q l - mono_list_lb_own γ l.
Proof. intros. unseal. rewrite own_op. by iDestruct 1 as "[_ $]". Qed. Proof. intros. unseal. by apply own_mono, mono_list_included. Qed.
Lemma mono_list_lb_own_get_prefix γ l l' : Lemma mono_list_lb_own_le {γ l} l' :
l' `prefix_of` l l' `prefix_of` l
mono_list_lb_own γ l - mono_list_lb_own γ l'. mono_list_lb_own γ l - mono_list_lb_own γ l'.
Proof. unseal. intros. by apply own_mono, mono_list_frag_included. Qed. Proof. unseal. intros. by apply own_mono, mono_list_lb_mono. 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 : Lemma mono_list_lb_own_idx_lookup γ l i a :
l !! i = Some a l !! i = Some a
...@@ -156,15 +142,22 @@ Section mono_list_own. ...@@ -156,15 +142,22 @@ Section mono_list_own.
Proof. iIntros (Hli) "Hl". iExists l. by iFrame. Qed. Proof. iIntros (Hli) "Hl". iExists l. by iFrame. Qed.
Lemma mono_list_own_alloc l : Lemma mono_list_own_alloc l :
|==> γ, mono_list_auth_own γ 1 l. |==> γ, mono_list_auth_own γ 1 l mono_list_lb_own γ l.
Proof. unseal. by apply own_alloc, mono_list_both_valid. Qed. Proof.
unseal. setoid_rewrite <- own_op. by apply own_alloc, mono_list_both_valid.
Qed.
Lemma mono_list_auth_own_update γ l l' : Lemma mono_list_auth_own_update γ l l' :
l `prefix_of` l' l `prefix_of` l'
mono_list_auth_own γ 1 l == mono_list_auth_own γ 1 l'. mono_list_auth_own γ 1 l == mono_list_auth_own γ 1 l' mono_list_lb_own γ l'.
Proof. intros. unseal. by apply own_update, mono_list_update. Qed. Proof.
iIntros (?) "Hauth".
iAssert (mono_list_auth_own γ 1 l') with "[> Hauth]" as "Hauth".
{ unseal. iApply (own_update with "Hauth"). by apply mono_list_update. }
iModIntro. iSplit; [done|]. by iApply mono_list_lb_own_get.
Qed.
Lemma mono_list_auth_own_update_app γ l l' : Lemma mono_list_auth_own_update_app γ l l' :
mono_list_auth_own γ 1 l == mono_list_auth_own γ 1 (l ++ l'). mono_list_auth_own γ 1 l ==
mono_list_auth_own γ 1 (l ++ l') mono_list_lb_own γ (l ++ l').
Proof. by apply mono_list_auth_own_update, prefix_app_r. Qed. Proof. by apply mono_list_auth_own_update, prefix_app_r. Qed.
End mono_list_own. End mono_list_own.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment