Big ops on RAs.

iris/ra.v

-Require Export prelude.collections prelude.relations.
+Require Export prelude.collections prelude.relations prelude.fin_maps.
 
 Class Valid (A : Type) := valid : A → Prop.
 Instance: Params (@valid) 2.
@@ -11,6 +11,14 @@ Instance: Params (@op) 2.
 Infix "⋅" := op (at level 50, left associativity) : C_scope.
 Notation "(⋅)" := op (only parsing) : C_scope.
 
+Fixpoint big_op `{Op A, Empty A} (xs : list A) : A :=
+  match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end.
+Arguments big_op _ _ _ !_ /.
+Instance: Params (@big_op) 3.
+Definition big_opM `{FinMapToList K A M, Op A, Empty A} (m : M) : A :=
+  big_op (snd <$> map_to_list m).
+Instance: Params (@big_opM) 4.
+
 Class Included (A : Type) := included : relation A.
 Instance: Params (@included) 2.
 Infix "≼" := included (at level 70) : C_scope.
@@ -58,6 +66,7 @@ Instance: Params (@ra_update) 3.
 Section ra.
 Context `{RA A}.
 Implicit Types x y z : A.
+Implicit Types xs ys zs : list A.
 
 Global Instance ra_valid_proper' : Proper ((≡) ==> iff) valid.
 Proof. by intros ???; split; apply ra_valid_proper. Qed.
@@ -120,4 +129,43 @@ Lemma ra_unit_empty x : unit ∅ ≡ ∅.
 Proof. by rewrite <-(ra_unit_l ∅) at 2; rewrite (right_id _ _). Qed.
 Lemma ra_empty_least x : ∅ ≼ x.
 Proof. by rewrite ra_included_spec; exists x; rewrite (left_id _ _). Qed.
+
+(** * Big ops *)
+Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
+Proof.
+  induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
+  * by rewrite IH.
+  * by rewrite !(associative _), (commutative _ x).
+  * by transitivity (big_op xs2).
+Qed.
+Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op.
+Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
+Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
+Proof.
+  induction xs as [|x xs IH]; simpl; [by rewrite ?(left_id _ _)|].
+  by rewrite IH, (associative _).
+Qed.
+
+Context `{FinMap K M}.
+Lemma big_opM_empty : big_opM (∅ : M A) ≡ ∅.
+Proof. unfold big_opM. by rewrite map_to_list_empty. Qed.
+Lemma big_opM_insert (m : M A) i x :
+  m !! i = None → big_opM (<[i:=x]> m) ≡ x ⋅ big_opM m.
+Proof. intros ?; unfold big_opM. by rewrite map_to_list_insert by done. Qed.
+Lemma big_opM_singleton i x : big_opM ({[i,x]} : M A) ≡ x.
+Proof.
+  unfold singleton, map_singleton.
+  rewrite big_opM_insert by auto using lookup_empty; simpl.
+  by rewrite big_opM_empty, (right_id _ _).
+Qed.
+Global Instance big_opM_proper : Proper ((≡) ==> (≡)) (big_opM : M A → _).
+Proof.
+  intros m1; induction m1 as [|i x m1 ? IH] using map_ind.
+  { by intros m2; rewrite (symmetry_iff (≡)), map_equiv_empty; intros ->. }
+  intros m2 Hm2; rewrite big_opM_insert by done.
+  rewrite (IH (delete i m2)) by (by rewrite <-Hm2, delete_insert).
+  destruct (map_equiv_lookup (<[i:=x]> m1) m2 i x)
+    as (y&?&Hxy); auto using lookup_insert.
+  by rewrite Hxy, <-big_opM_insert, insert_delete by auto using lookup_delete.
+Qed.
 End ra.