From fe62f378953dbf57b86b810e396d0c10c50974ee Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Tue, 27 Aug 2019 13:36:58 +0200
Subject: [PATCH] added lemmas for list cmra

---
 theories/algebra/list.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 0d3d22a06..d97f640aa 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -359,6 +359,9 @@ Section properties.
   Global Instance list_singleton_core_id i (x : A) :
     CoreId x → CoreId {[ i := x ]}.
   Proof. by rewrite !core_id_total list_core_singletonM=> ->. Qed.
+  Lemma list_singleton_snoc l x:
+    {[length l := x]} ⋅ l ≡ l ++ [x].
+  Proof. elim: l => //= ?? <-. by rewrite left_id. Qed.
 
   (* Update *)
   Lemma list_singleton_updateP (P : A → Prop) (Q : list A → Prop) x :
@@ -446,6 +449,17 @@ Section properties.
     x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
   Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
 *)
+
+  Lemma list_alloc_singleton_local_update x l :
+    ✓ x → (l, ε) ~l~> (l ++ [x], {[length l := x]}).
+  Proof.
+    move => ?.
+    have -> : ({[length l := x]} ≡ {[length l := x]} ⋅ ε) by rewrite right_id.
+    rewrite -list_singleton_snoc. apply op_local_update => ??.
+    rewrite list_singleton_snoc app_validN cons_validN. split_and? => //; [| constructor].
+    by apply cmra_valid_validN.
+  Qed.
+
 End properties.
 
 (** Functor *)
-- 
GitLab