From 2b96b14d9e335a6342163e0f5a29ce5dc2b32dba Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 21 Mar 2016 16:32:13 +0100
Subject: [PATCH] Make use of COFE on lists in big ops.

---
 algebra/cmra_big_op.v  | 5 +++--
 algebra/upred_big_op.v | 8 +++-----
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index a2c6dd5da..65f9f9256 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export cmra.
+From iris.algebra Require Export cmra list.
 From iris.prelude Require Import gmap.
 
 Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
@@ -25,8 +25,9 @@ Proof.
   - by rewrite !assoc (comm _ x).
   - by trans (big_op xs2).
 Qed.
-Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op.
+Global Instance big_op_ne n : Proper (dist n ==> dist n) big_op.
 Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
+Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op := ne_proper _.
 Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
 Proof.
   induction xs as [|x xs IH]; simpl; first by rewrite ?left_id.
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index f7fd01d7d..fe35a51e6 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export upred.
+From iris.algebra Require Export upred list.
 From iris.prelude Require Import gmap fin_collections.
 Import uPred.
 
@@ -44,11 +44,9 @@ Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 Global Instance big_sep_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_sep M).
 Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
-Global Instance big_and_ne n :
-  Proper (Forall2 (dist n) ==> dist n) (@uPred_big_and M).
+Global Instance big_and_ne n : Proper (dist n ==> dist n) (@uPred_big_and M).
 Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-Global Instance big_sep_ne n :
-  Proper (Forall2 (dist n) ==> dist n) (@uPred_big_sep M).
+Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M).
 Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
 Global Instance big_and_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_and M).
-- 
GitLab