Commit 562b2c2b authored by Robbert Krebbers's avatar Robbert Krebbers

Reorganize big ops for CMRA based on those for uPred.

parent d1ef32dd
......@@ -244,7 +244,7 @@ Global Instance cmra_pcore_proper' : Proper ((≡) ==> (≡)) (@pcore A _).
Proof. apply (ne_proper _). Qed.
Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _).
Proof. intros x1 x2 Hx y1 y2 Hy. by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed.
Global Instance ra_op_proper' : Proper (() ==> () ==> ()) (@op A _).
Global Instance cmra_op_proper' : Proper (() ==> () ==> ()) (@op A _).
Proof. apply (ne_proper_2 _). Qed.
Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
Proof. by split; apply cmra_validN_ne. Qed.
......
From iris.algebra Require Export cmra list.
From iris.prelude Require Import gmap.
From iris.prelude Require Import functions gmap.
Fixpoint big_op {A : ucmraT} (xs : list A) : A :=
(** The operator [ [⋅] Ps ] folds [⋅] over the list [Ps]. This operator is not a
quantifier, so it binds strongly.
Apart from that, we define the following big operators with binders build in:
- The operator [ [⋅ list] k ↦ x ∈ l, P ] folds over a list [l]. The binder [x]
refers to each element at index [k].
- The operator [ [⋅ map] k ↦ x ∈ m, P ] folds over a map [m]. The binder [x]
refers to each element at index [k].
- The operator [ [⋅ set] x ∈ X, P ] folds over a set [m]. The binder [x] refers
to each element.
Since these big operators are like quantifiers, they have the same precedence as
[∀] and [∃]. *)
(** * Big ops over lists *)
(* This is the basic building block for other big ops *)
Fixpoint big_op {M : ucmraT} (xs : list M) : M :=
match xs with [] => | x :: xs => x big_op xs end.
Arguments big_op _ !_ /.
Instance: Params (@big_op) 1.
Definition big_opM `{Countable K} {A : ucmraT} (m : gmap K A) : A :=
big_op (snd <$> map_to_list m).
Instance: Params (@big_opM) 4.
Notation "'[⋅]' xs" := (big_op xs) (at level 20) : C_scope.
(** * Other big ops *)
Definition big_opL {M : ucmraT} {A} (l : list A) (f : nat A M) : M :=
[] (imap f l).
Instance: Params (@big_opL) 2.
Typeclasses Opaque big_opL.
Notation "'[⋅' 'list' ] k ↦ x ∈ l , P" := (big_opL l (λ k x, P))
(at level 200, l at level 10, k, x at level 1, right associativity,
format "[⋅ list ] k ↦ x ∈ l , P") : C_scope.
Notation "'[⋅' 'list' ] x ∈ l , P" := (big_opL l (λ _ x, P))
(at level 200, l at level 10, x at level 1, right associativity,
format "[⋅ list ] x ∈ l , P") : C_scope.
Definition big_opM {M : ucmraT} `{Countable K} {A}
(m : gmap K A) (f : K A M) : M :=
[] (curry f <$> map_to_list m).
Instance: Params (@big_opM) 6.
Typeclasses Opaque big_opM.
Notation "'[⋅' 'map' ] k ↦ x ∈ m , P" := (big_opM m (λ k x, P))
(at level 200, m at level 10, k, x at level 1, right associativity,
format "[⋅ map ] k ↦ x ∈ m , P") : C_scope.
Definition big_opS {M : ucmraT} `{Countable A}
(X : gset A) (f : A M) : M := [] (f <$> elements X).
Instance: Params (@big_opS) 5.
Typeclasses Opaque big_opS.
Notation "'[⋅' 'set' ] x ∈ X , P" := (big_opS X (λ x, P))
(at level 200, X at level 10, x at level 1, right associativity,
format "[⋅ set ] x ∈ X , P") : C_scope.
(** * Properties about big ops *)
Section big_op.
Context {A : ucmraT}.
Implicit Types xs : list A.
Context {M : ucmraT}.
Implicit Types xs : list M.
(** * Big ops *)
Lemma big_op_nil : big_op (@nil A) = .
Global Instance big_op_ne n : Proper (dist n ==> dist n) (@big_op M).
Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
Global Instance big_op_proper : Proper (() ==> ()) (@big_op M) := ne_proper _.
Lemma big_op_nil : [] (@nil M) = .
Proof. done. Qed.
Lemma big_op_cons x xs : big_op (x :: xs) = x big_op xs.
Lemma big_op_cons x xs : [] (x :: xs) = x [] xs.
Proof. done. Qed.
Global Instance big_op_permutation : Proper (() ==> ()) (@big_op A).
Lemma big_op_app xs ys : [] (xs ++ ys) [] xs [] ys.
Proof.
induction xs as [|x xs IH]; simpl; first by rewrite ?left_id.
by rewrite IH assoc.
Qed.
Lemma big_op_mono xs ys : Forall2 () xs ys [] xs [] ys.
Proof. induction 1 as [|x y xs ys Hxy ? IH]; simpl; eauto using cmra_mono. Qed.
Global Instance big_op_permutation : Proper (() ==> ()) (@big_op M).
Proof.
induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
- by rewrite IH.
- by rewrite !assoc (comm _ x).
- by trans (big_op xs2).
Qed.
Global Instance big_op_ne n : Proper (dist n ==> dist n) (@big_op A).
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.
by rewrite IH assoc.
Qed.
Lemma big_op_contains xs ys : xs `contains` ys big_op xs big_op ys.
Lemma big_op_contains xs ys : xs `contains` ys [] xs [] ys.
Proof.
intros [xs' ->]%contains_Permutation.
rewrite big_op_app; apply cmra_included_l.
Qed.
Lemma big_op_delete xs i x :
xs !! i = Some x x big_op (delete i xs) big_op xs.
Lemma big_op_delete xs i x : xs !! i = Some x x [] delete i xs [] xs.
Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed.
Context `{Countable K}.
Implicit Types m : gmap K A.
Lemma big_opM_empty : big_opM ( : gmap K A) .
Proof. unfold big_opM. by rewrite map_to_list_empty. Qed.
Lemma big_opM_insert m i x :
m !! i = None big_opM (<[i:=x]> m) x big_opM m.
Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed.
Lemma big_opM_delete m i x :
m !! i = Some x x big_opM (delete i m) big_opM m.
Proof.
intros. rewrite -{2}(insert_id m i x) // -insert_delete.
by rewrite big_opM_insert ?lookup_delete.
Qed.
Lemma big_opM_singleton i x : big_opM ({[i := x]} : gmap K A) x.
Lemma big_sep_elem_of xs x : x xs x [] xs.
Proof.
rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty.
by rewrite big_opM_empty right_id.
Qed.
Global Instance big_opM_proper : Proper (() ==> ()) (big_opM : gmap K 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 //.
rewrite (IH (delete i m2)); last by rewrite -Hm2 delete_insert.
destruct (map_equiv_lookup_l (<[i:=x]> m1) m2 i x)
as (y&?&Hxy); auto using lookup_insert.
rewrite Hxy -big_opM_insert; last auto using lookup_delete.
by rewrite insert_delete insert_id.
Qed.
Lemma big_opM_lookup_valid n m i x : {n} big_opM m m !! i = Some x {n} x.
Proof.
intros Hm ?; revert Hm; rewrite -(big_opM_delete _ i x) //.
apply cmra_validN_op_l.
intros [i ?]%elem_of_list_lookup. rewrite -big_op_delete //.
apply cmra_included_l.
Qed.
(** ** Big ops over lists *)
Section list.
Context {A : Type}.
Implicit Types l : list A.
Implicit Types f g : nat A M.
Lemma big_opL_mono f g l :
( k y, l !! k = Some y f k y g k y)
([ list] k y l, f k y) [ list] k y l, g k y.
Proof.
intros Hf. apply big_op_mono.
revert f g Hf. induction l as [|x l IH]=> f g Hf; first constructor.
rewrite !imap_cons; constructor; eauto.
Qed.
Lemma big_opL_proper f g l :
( k y, l !! k = Some y f k y g k y)
([ list] k y l, f k y) ([ list] k y l, g k y).
Proof.
intros Hf; apply big_op_proper.
revert f g Hf. induction l as [|x l IH]=> f g Hf; first constructor.
rewrite !imap_cons; constructor; eauto.
Qed.
Global Instance big_opL_ne l n :
Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
(big_opL (M:=M) l).
Proof.
intros f g Hf. apply big_op_ne.
revert f g Hf. induction l as [|x l IH]=> f g Hf; first constructor.
rewrite !imap_cons; constructor. by apply Hf. apply IH=> n'; apply Hf.
Qed.
Global Instance big_opL_proper' l :
Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
(big_opL (M:=M) l).
Proof. intros f1 f2 Hf. by apply big_opL_proper; intros; last apply Hf. Qed.
Global Instance big_opL_mono' l :
Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
(big_opL (M:=M) l).
Proof. intros f1 f2 Hf. by apply big_opL_mono; intros; last apply Hf. Qed.
Lemma big_opL_nil f : ([ list] ky nil, f k y) = .
Proof. done. Qed.
Lemma big_opL_cons f x l :
([ list] ky x :: l, f k y) = f 0 x [ list] ky l, f (S k) y.
Proof. by rewrite /big_opL imap_cons. Qed.
Lemma big_opL_singleton f x : ([ list] ky [x], f k y) f 0 x.
Proof. by rewrite big_opL_cons big_opL_nil right_id. Qed.
Lemma big_opL_app f l1 l2 :
([ list] ky l1 ++ l2, f k y)
([ list] ky l1, f k y) ([ list] ky l2, f (length l1 + k) y).
Proof. by rewrite /big_opL imap_app big_op_app. Qed.
Lemma big_opL_lookup f l i x :
l !! i = Some x f i x [ list] ky l, f k y.
Proof.
intros. rewrite -(take_drop_middle l i x) // big_opL_app big_opL_cons.
rewrite Nat.add_0_r take_length_le; eauto using lookup_lt_Some, Nat.lt_le_incl.
eapply transitivity, cmra_included_r; eauto using cmra_included_l.
Qed.
Lemma big_opL_elem_of (f : A M) l x : x l f x [ list] y l, f y.
Proof.
intros [i ?]%elem_of_list_lookup; eauto using (big_opL_lookup (λ _, f)).
Qed.
Lemma big_opL_fmap {B} (h : A B) (f : nat B M) l :
([ list] ky h <$> l, f k y) ([ list] ky l, f k (h y)).
Proof. by rewrite /big_opL imap_fmap. Qed.
Lemma big_opL_opL f g l :
([ list] kx l, f k x g k x)
([ list] kx l, f k x) ([ list] kx l, g k x).
Proof.
revert f g; induction l as [|x l IH]=> f g.
{ by rewrite !big_opL_nil left_id. }
rewrite !big_opL_cons IH.
by rewrite -!assoc (assoc _ (g _ _)) [(g _ _ _)]comm -!assoc.
Qed.
End list.
(** ** Big ops over finite maps *)
Section gmap.
Context `{Countable K} {A : Type}.
Implicit Types m : gmap K A.
Implicit Types f g : K A M.
Lemma big_opM_mono f g m1 m2 :
m1 m2 ( k x, m2 !! k = Some x f k x g k x)
([ map] k x m1, f k x) [ map] k x m2, g k x.
Proof.
intros HX Hf. trans ([ map] kx m2, f k x).
- by apply big_op_contains, fmap_contains, map_to_list_contains.
- apply big_op_mono, Forall2_fmap, Forall_Forall2.
apply Forall_forall=> -[i x] ? /=. by apply Hf, elem_of_map_to_list.
Qed.
Lemma big_opM_proper f g m :
( k x, m !! k = Some x f k x g k x)
([ map] k x m, f k x) ([ map] k x m, g k x).
Proof.
intros Hf. apply big_op_proper, equiv_Forall2, Forall2_fmap, Forall_Forall2.
apply Forall_forall=> -[i x] ? /=. by apply Hf, elem_of_map_to_list.
Qed.
Global Instance big_opM_ne m n :
Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
(big_opM (M:=M) m).
Proof.
intros f1 f2 Hf. apply big_op_ne, Forall2_fmap.
apply Forall_Forall2, Forall_true=> -[i x]; apply Hf.
Qed.
Global Instance big_opM_proper' m :
Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
(big_opM (M:=M) m).
Proof. intros f1 f2 Hf. by apply big_opM_proper; intros; last apply Hf. Qed.
Global Instance big_opM_mono' m :
Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
(big_opM (M:=M) m).
Proof. intros f1 f2 Hf. by apply big_opM_mono; intros; last apply Hf. Qed.
Lemma big_opM_empty f : ([ map] kx , f k x) = .
Proof. by rewrite /big_opM map_to_list_empty. Qed.
Lemma big_opM_insert f m i x :
m !! i = None
([ map] ky <[i:=x]> m, f k y) f i x [ map] ky m, f k y.
Proof. intros ?. by rewrite /big_opM map_to_list_insert. Qed.
Lemma big_opM_delete f m i x :
m !! i = Some x
([ map] ky m, f k y) f i x [ map] ky delete i m, f k y.
Proof.
intros. rewrite -big_opM_insert ?lookup_delete //.
by rewrite insert_delete insert_id.
Qed.
Lemma big_opM_lookup f m i x :
m !! i = Some x f i x [ map] ky m, f k y.
Proof. intros. rewrite big_opM_delete //. apply cmra_included_l. Qed.
Lemma big_opM_singleton f i x : ([ map] ky {[i:=x]}, f k y) f i x.
Proof.
rewrite -insert_empty big_opM_insert/=; last auto using lookup_empty.
by rewrite big_opM_empty right_id.
Qed.
Lemma big_opM_fmap {B} (h : A B) (f : K B M) m :
([ map] ky h <$> m, f k y) ([ map] ky m, f k (h y)).
Proof.
rewrite /big_opM map_to_list_fmap -list_fmap_compose.
f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done.
Qed.
Lemma big_opM_insert_override (f : K M) m i x y :
m !! i = Some x
([ map] k_ <[i:=y]> m, f k) ([ map] k_ m, f k).
Proof.
intros. rewrite -insert_delete big_opM_insert ?lookup_delete //.
by rewrite -big_opM_delete.
Qed.
Lemma big_opM_fn_insert {B} (g : K A B M) (f : K B) m i (x : A) b :
m !! i = None
([ map] ky <[i:=x]> m, g k y (<[i:=b]> f k))
(g i x b [ map] ky m, g k y (f k)).
Proof.
intros. rewrite big_opM_insert // fn_lookup_insert.
apply cmra_op_proper', big_opM_proper; auto=> k y ?.
by rewrite fn_lookup_insert_ne; last set_solver.
Qed.
Lemma big_opM_fn_insert' (f : K M) m i x P :
m !! i = None
([ map] ky <[i:=x]> m, <[i:=P]> f k) (P [ map] ky m, f k).
Proof. apply (big_opM_fn_insert (λ _ _, id)). Qed.
Lemma big_opM_opM f g m :
([ map] kx m, f k x g k x)
([ map] kx m, f k x) ([ map] kx m, g k x).
Proof.
rewrite /big_opM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
by rewrite IH -!assoc (assoc _ (g _ _)) [(g _ _ _)]comm -!assoc.
Qed.
End gmap.
(** ** Big ops over finite sets *)
Section gset.
Context `{Countable A}.
Implicit Types X : gset A.
Implicit Types f : A M.
Lemma big_opS_mono f g X Y :
X Y ( x, x Y f x g x)
([ set] x X, f x) [ set] x Y, g x.
Proof.
intros HX Hf. trans ([ set] x Y, f x).
- by apply big_op_contains, fmap_contains, elements_contains.
- apply big_op_mono, Forall2_fmap, Forall_Forall2.
apply Forall_forall=> x ? /=. by apply Hf, elem_of_elements.
Qed.
Lemma big_opS_proper f g X Y :
X Y ( x, x X x Y f x g x)
([ set] x X, f x) ([ set] x Y, g x).
Proof.
intros HX Hf. trans ([ set] x Y, f x).
- apply big_op_permutation. by rewrite HX.
- apply big_op_proper, equiv_Forall2, Forall2_fmap, Forall_Forall2.
apply Forall_forall=> x ? /=.
apply Hf; first rewrite HX; by apply elem_of_elements.
Qed.
Lemma big_opS_ne X n :
Proper (pointwise_relation _ (dist n) ==> dist n) (big_opS (M:=M) X).
Proof.
intros f1 f2 Hf. apply big_op_ne, Forall2_fmap.
apply Forall_Forall2, Forall_true=> x; apply Hf.
Qed.
Lemma big_opS_proper' X :
Proper (pointwise_relation _ () ==> ()) (big_opS (M:=M) X).
Proof. intros f1 f2 Hf. apply big_opS_proper; naive_solver. Qed.
Lemma big_opS_mono' X :
Proper (pointwise_relation _ () ==> ()) (big_opS (M:=M) X).
Proof. intros f1 f2 Hf. apply big_opS_mono; naive_solver. Qed.
Lemma big_opS_empty f : ([ set] x , f x) = .
Proof. by rewrite /big_opS elements_empty. Qed.
Lemma big_opS_insert f X x :
x X ([ set] y {[ x ]} X, f y) (f x [ set] y X, f y).
Proof. intros. by rewrite /big_opS elements_union_singleton. Qed.
Lemma big_opS_fn_insert {B} (f : A B M) h X x b :
x X
([ set] y {[ x ]} X, f y (<[x:=b]> h y))
(f x b [ set] y X, f y (h y)).
Proof.
intros. rewrite big_opS_insert // fn_lookup_insert.
apply cmra_op_proper', big_opS_proper; auto=> y ??.
by rewrite fn_lookup_insert_ne; last set_solver.
Qed.
Lemma big_opS_fn_insert' f X x P :
x X ([ set] y {[ x ]} X, <[x:=P]> f y) (P [ set] y X, f y).
Proof. apply (big_opS_fn_insert (λ y, id)). Qed.
Lemma big_opS_delete f X x :
x X ([ set] y X, f y) f x [ set] y X {[ x ]}, f y.
Proof.
intros. rewrite -big_opS_insert; last set_solver.
by rewrite -union_difference_L; last set_solver.
Qed.
Lemma big_opS_elem_of f X x : x X f x [ set] y X, f y.
Proof. intros. rewrite big_opS_delete //. apply cmra_included_l. Qed.
Lemma big_opS_singleton f x : ([ set] y {[ x ]}, f y) f x.
Proof. intros. by rewrite /big_opS elements_singleton /= right_id. Qed.
Lemma big_opS_opS f g X :
([ set] y X, f y g y) ([ set] y X, f y) ([ set] y X, g y).
Proof.
rewrite /big_opS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
by rewrite IH -!assoc (assoc _ (g _)) [(g _ _)]comm -!assoc.
Qed.
End gset.
End big_op.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment