cmra_big_op.v 1.55 KB
Newer Older
1
From stdpp Require Import gmap gmultiset.
2
From iris.algebra Require Export big_op cmra.
3
Set Default Proof Using "Type*".
4

Robbert Krebbers's avatar
Robbert Krebbers committed
5 6
(** Option *)
Lemma big_opL_None {M : cmraT} {A} (f : nat  A  option M) l :
7
  ([^op list] kx  l, f k x) = None   k x, l !! k = Some x  f k x = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
Proof.
9
  revert f. induction l as [|x l IH]=> f //=. rewrite op_None IH. split.
Robbert Krebbers's avatar
Robbert Krebbers committed
10 11 12 13
  - intros [??] [|k] y ?; naive_solver.
  - intros Hl. split. by apply (Hl 0). intros k. apply (Hl (S k)).
Qed.
Lemma big_opM_None {M : cmraT} `{Countable K} {A} (f : K  A  option M) m :
14
  ([^op map] kx  m, f k x) = None   k x, m !! k = Some x  f k x = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
15 16 17 18 19 20 21 22 23
Proof.
  induction m as [|i x m ? IH] using map_ind=> //=.
  rewrite -equiv_None big_opM_insert // equiv_None op_None IH. split.
  { intros [??] k y. rewrite lookup_insert_Some; naive_solver. }
  intros Hm; split.
  - apply (Hm i). by simplify_map_eq.
  - intros k y ?. apply (Hm k). by simplify_map_eq.
Qed.
Lemma big_opS_None {M : cmraT} `{Countable A} (f : A  option M) X :
24
  ([^op set] x  X, f x) = None   x, x  X  f x = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
25
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
  induction X as [|x X ? IH] using set_ind_L; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
27 28
  rewrite -equiv_None big_opS_insert // equiv_None op_None IH. set_solver.
Qed.
29
Lemma big_opMS_None {M : cmraT} `{Countable A} (f : A  option M) X :
30
  ([^op mset] x  X, f x) = None   x, x  X  f x = None.
31 32 33
Proof.
  induction X as [|x X IH] using gmultiset_ind.
  { rewrite big_opMS_empty. set_solver. }
34
  rewrite -equiv_None big_opMS_disj_union big_opMS_singleton equiv_None op_None IH.
35
  set_solver.
36
Qed.