From 1bbe5d155fcb19288edd3d27b8dd0496af2cf0ca Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 30 Sep 2016 09:55:45 +0200
Subject: [PATCH] Unfolding lemmas for big ops over lists with Z indices.

---
 algebra/cmra_big_op.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 6fe6cda19..96b7c11e2 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -160,6 +160,13 @@ Section list.
            (big_opL (M:=M) l).
   Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
 
+  Lemma big_opL_consZ_l (f : Z → A → M) x l :
+    ([⋅ list] k↦y ∈ x :: l, f k y) = f 0 x ⋅ [⋅ list] k↦y ∈ l, f (1 + k)%Z y.
+  Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
+  Lemma big_opL_consZ_r (f : Z → A → M) x l :
+    ([⋅ list] k↦y ∈ x :: l, f k y) = f 0 x ⋅ [⋅ list] k↦y ∈ l, f (k + 1)%Z y.
+  Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
+
   Lemma big_opL_lookup f l i x :
     l !! i = Some x → f i x ≼ [⋅ list] k↦y ∈ l, f k y.
   Proof.
-- 
GitLab