cmra_big_op.v 3 KB
Newer Older
1
From iris.algebra Require Export cmra list.
2
From iris.prelude Require Import gmap.
3

4
Fixpoint big_op {A : ucmraT} (xs : list A) : A :=
5
  match xs with [] =>  | x :: xs => x  big_op xs end.
6 7 8
Arguments big_op _ !_ /.
Instance: Params (@big_op) 1.
Definition big_opM `{Countable K} {A : ucmraT} (m : gmap K A) : A :=
9
  big_op (snd <$> map_to_list m).
10
Instance: Params (@big_opM) 4.
11 12 13

(** * Properties about big ops *)
Section big_op.
14 15
Context {A : ucmraT}.
Implicit Types xs : list A.
16 17 18 19 20 21

(** * Big ops *)
Lemma big_op_nil : big_op (@nil A) = .
Proof. done. Qed.
Lemma big_op_cons x xs : big_op (x :: xs) = x  big_op xs.
Proof. done. Qed.
22
Global Instance big_op_permutation : Proper (() ==> ()) (@big_op A).
23 24
Proof.
  induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
25 26
  - by rewrite IH.
  - by rewrite !assoc (comm _ x).
27
  - by trans (big_op xs2).
28
Qed.
29
Global Instance big_op_ne n : Proper (dist n ==> dist n) (@big_op A).
30
Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
31
Global Instance big_op_proper : Proper (() ==> ()) big_op := ne_proper _.
32 33
Lemma big_op_app xs ys : big_op (xs ++ ys)  big_op xs  big_op ys.
Proof.
34 35
  induction xs as [|x xs IH]; simpl; first by rewrite ?left_id.
  by rewrite IH assoc.
36 37 38
Qed.
Lemma big_op_contains xs ys : xs `contains` ys  big_op xs  big_op ys.
Proof.
39 40
  intros [xs' ->]%contains_Permutation.
  rewrite big_op_app; apply cmra_included_l.
41 42 43 44 45
Qed.
Lemma big_op_delete xs i x :
  xs !! i = Some x  x  big_op (delete i xs)  big_op xs.
Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed.

46 47 48
Context `{Countable K}.
Implicit Types m : gmap K A.
Lemma big_opM_empty : big_opM ( : gmap K A)  .
49
Proof. unfold big_opM. by rewrite map_to_list_empty. Qed.
50
Lemma big_opM_insert m i x :
51 52
  m !! i = None  big_opM (<[i:=x]> m)  x  big_opM m.
Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed.
53
Lemma big_opM_delete m i x :
54 55
  m !! i = Some x  x  big_opM (delete i m)  big_opM m.
Proof.
56 57
  intros. rewrite -{2}(insert_id m i x) // -insert_delete.
  by rewrite big_opM_insert ?lookup_delete.
58
Qed.
59
Lemma big_opM_singleton i x : big_opM ({[i := x]} : gmap K A)  x.
60 61
Proof.
  rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty.
62
  by rewrite big_opM_empty right_id.
63
Qed.
64
Global Instance big_opM_proper : Proper (() ==> ()) (big_opM : gmap K A  _).
65 66 67 68 69
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 //.
  rewrite (IH (delete i m2)); last by rewrite -Hm2 delete_insert.
70
  destruct (map_equiv_lookup_l (<[i:=x]> m1) m2 i x)
71 72
    as (y&?&Hxy); auto using lookup_insert.
  rewrite Hxy -big_opM_insert; last auto using lookup_delete.
73
  by rewrite insert_delete insert_id.
74
Qed.
75
Lemma big_opM_lookup_valid n m i x : {n} big_opM m  m !! i = Some x  {n} x.
76 77 78 79 80
Proof.
  intros Hm ?; revert Hm; rewrite -(big_opM_delete _ i x) //.
  apply cmra_validN_op_l.
Qed.
End big_op.