Library iris.algebra.upred_big_op
From iris.algebra Require Export upred list.
From iris.prelude Require Import gmap fin_collections functions.
Import uPred.
From iris.prelude Require Import gmap fin_collections functions.
Import uPred.
We define the following big operators:
- The operators [★] Ps and [∧] Ps fold ★ and ∧ over the list Ps. This operator is not a quantifier, so it binds strongly.
- The operator [★ map] k ↦ x ∈ m, P asserts that P holds separately for each k ↦ x in the map m. This operator is a quantifier, and thus has the same precedence as ∀ and ∃.
- The operator [★ set] x ∈ X, P asserts that P holds separately for each x in the set X. This operator is a quantifier, and thus has the same precedence as ∀ and ∃.
Big ops over lists
Fixpoint uPred_big_and {M} (Ps : list (uPred M)) : uPred M :=
match Ps with [] ⇒ True | P :: Ps ⇒ P ∧ uPred_big_and Ps end%I.
Instance: Params (@uPred_big_and) 1.
Notation "'[∧]' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) : uPred M :=
match Ps with [] ⇒ Emp | P :: Ps ⇒ P ★ uPred_big_sep Ps end%I.
Instance: Params (@uPred_big_sep) 1.
Notation "'[★]' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
match Ps with [] ⇒ True | P :: Ps ⇒ P ∧ uPred_big_and Ps end%I.
Instance: Params (@uPred_big_and) 1.
Notation "'[∧]' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) : uPred M :=
match Ps with [] ⇒ Emp | P :: Ps ⇒ P ★ uPred_big_sep Ps end%I.
Instance: Params (@uPred_big_sep) 1.
Notation "'[★]' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
Definition uPred_big_sepM {M: ucmraT} `{Countable K} {A}
(m : gmap K A) (Φ : K → A → uPred M) : uPred M :=
[★] (curry Φ <$> map_to_list m).
Instance: Params (@uPred_big_sepM) 6.
Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (uPred_big_sepM m (λ k x, P))
(at level 200, m at level 10, k, x at level 1, right associativity,
format "[★ map ] k ↦ x ∈ m , P") : uPred_scope.
Definition uPred_big_sepS {M} `{Countable A}
(X : gset A) (Φ : A → uPred M) : uPred M := [★] (Φ <$> elements X).
Instance: Params (@uPred_big_sepS) 5.
Notation "'[★' 'set' ] x ∈ X , P" := (uPred_big_sepS X (λ x, P))
(at level 200, X at level 10, x at level 1, right associativity,
format "[★ set ] x ∈ X , P") : uPred_scope.
(m : gmap K A) (Φ : K → A → uPred M) : uPred M :=
[★] (curry Φ <$> map_to_list m).
Instance: Params (@uPred_big_sepM) 6.
Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (uPred_big_sepM m (λ k x, P))
(at level 200, m at level 10, k, x at level 1, right associativity,
format "[★ map ] k ↦ x ∈ m , P") : uPred_scope.
Definition uPred_big_sepS {M} `{Countable A}
(X : gset A) (Φ : A → uPred M) : uPred M := [★] (Φ <$> elements X).
Instance: Params (@uPred_big_sepS) 5.
Notation "'[★' 'set' ] x ∈ X , P" := (uPred_big_sepS X (λ x, P))
(at level 200, X at level 10, x at level 1, right associativity,
format "[★ set ] x ∈ X , P") : uPred_scope.
Class RelevantL {M} (Ps : list (uPred M)) :=
relevantL : Forall RelevantP Ps.
Arguments relevantL {_} _ {_}.
Class AffineL {M} (Ps : list (uPred M)) :=
affineL : Forall AffineP Ps.
Arguments affineL {_} _ {_}.
relevantL : Forall RelevantP Ps.
Arguments relevantL {_} _ {_}.
Class AffineL {M} (Ps : list (uPred M)) :=
affineL : Forall AffineP Ps.
Arguments affineL {_} _ {_}.
Section big_op.
Context {M : ucmraT}.
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.
Context {M : ucmraT}.
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.
Global Instance big_and_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_and M).
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 (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 (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).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_and M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
- by rewrite IH.
- by rewrite !assoc (comm _ P).
- etrans; eauto.
Qed.
Global Instance big_sep_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_sep M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
- by rewrite IH.
- by rewrite !assoc (comm _ P).
- etrans; eauto.
Qed.
Lemma big_and_app Ps Qs : [∧] (Ps ++ Qs) ⊣⊢ [∧] Ps ∧ [∧] Qs.
Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ [★] Ps ★ [★] Qs.
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_and_contains Ps Qs : Qs `contains` Ps → [∧] Ps ⊢ [∧] Qs.
Proof.
intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
Qed.
Lemma big_sep_permutation Ps Qs : Permutation Qs Ps → [★] Ps ⊢ [★] Qs.
Proof.
by intros →.
Qed.
Lemma big_and_elem_of Ps P : P ∈ Ps → [∧] Ps ⊢ P.
Proof. induction 1; simpl; auto with I. Qed.
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 (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 (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).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_and M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
- by rewrite IH.
- by rewrite !assoc (comm _ P).
- etrans; eauto.
Qed.
Global Instance big_sep_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_sep M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
- by rewrite IH.
- by rewrite !assoc (comm _ P).
- etrans; eauto.
Qed.
Lemma big_and_app Ps Qs : [∧] (Ps ++ Qs) ⊣⊢ [∧] Ps ∧ [∧] Qs.
Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ [★] Ps ★ [★] Qs.
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_and_contains Ps Qs : Qs `contains` Ps → [∧] Ps ⊢ [∧] Qs.
Proof.
intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
Qed.
Lemma big_sep_permutation Ps Qs : Permutation Qs Ps → [★] Ps ⊢ [★] Qs.
Proof.
by intros →.
Qed.
Lemma big_and_elem_of Ps P : P ∈ Ps → [∧] Ps ⊢ P.
Proof. induction 1; simpl; auto with I. Qed.
Section gmap.
Context `{Countable K} {A : Type}.
Implicit Types m : gmap K A.
Implicit Types Φ Ψ : K → A → uPred M.
Lemma big_sepM_proper Φ Ψ m :
(∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) →
([★ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m, Ψ k x).
Proof.
intros HΦ. apply (anti_symm (⊢)).
- trans ([★ map] k ↦ x ∈ m, Φ k x)%I.
× apply big_sep_permutation, fmap_Permutation.
apply (anti_symm contains); apply map_to_list_contains; set_solver.
× apply big_sep_mono', Forall2_fmap, Forall_Forall2.
apply Forall_forall⇒ -[i x] ? /=. rewrite -HΦ; auto; apply elem_of_map_to_list; set_solver.
- trans ([★ map] k ↦ x ∈ m, Ψ k x)%I.
× apply big_sep_permutation, fmap_Permutation.
apply (anti_symm contains); apply map_to_list_contains; set_solver.
× apply big_sep_mono', Forall2_fmap, Forall_Forall2.
apply Forall_forall⇒ -[i x] ? /=. rewrite -HΦ; auto; apply elem_of_map_to_list; set_solver.
Qed.
Global Instance big_sepM_ne m n :
Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
(uPred_big_sepM (M:=M) m).
Proof.
intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
apply Forall_Forall2, Forall_true⇒ -[i x]; apply HΦ.
Qed.
Global Instance big_sepM_proper' m :
Proper (pointwise_relation _ (pointwise_relation _ (⊣⊢)) ==> (⊣⊢))
(uPred_big_sepM (M:=M) m).
Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_proper; intros; last apply HΦ. Qed.
Lemma big_sepM_empty Φ : ([★ map] k↦x ∈ ∅, Φ k x) ⊣⊢ Emp.
Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
Lemma big_sepM_insert Φ m i x :
m !! i = None →
([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ m, Φ k y.
Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
Lemma big_sepM_delete Φ m i x :
m !! i = Some x →
([★ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y.
Proof.
intros. rewrite -big_sepM_insert ?lookup_delete //.
by rewrite insert_delete insert_id.
Qed.
Lemma big_sepM_singleton Φ i x : ([★ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x.
Proof.
rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
by rewrite big_sepM_empty right_id.
Qed.
Lemma big_sepM_fmap {B} (f : A → B) (Φ : K → B → uPred M) m :
([★ map] k↦y ∈ f <$> m, Φ k y) ⊣⊢ ([★ map] k↦y ∈ m, Φ k (f y)).
Proof.
rewrite /uPred_big_sepM map_to_list_fmap -list_fmap_compose.
f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done.
Qed.
Lemma big_sepM_insert_override (Φ : K → uPred M) m i x y :
m !! i = Some x →
([★ map] k↦_ ∈ <[i:=y]> m, Φ k) ⊣⊢ ([★ map] k↦_ ∈ m, Φ k).
Proof.
intros. rewrite -insert_delete big_sepM_insert ?lookup_delete //.
by rewrite -big_sepM_delete.
Qed.
Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → uPred M) (f : K → B) m i x b :
m !! i = None →
([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=b]> f k))
⊣⊢ (Ψ i x b ★ [★ map] k↦y ∈ m, Ψ k y (f k)).
Proof.
intros. rewrite big_sepM_insert // fn_lookup_insert.
apply sep_proper, big_sepM_proper; auto⇒ k y ?.
by rewrite fn_lookup_insert_ne; last set_solver.
Qed.
Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P :
m !! i = None →
([★ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ★ [★ map] k↦y ∈ m, Φ k).
Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed.
Lemma big_sepM_sepM Φ Ψ m :
([★ map] k↦x ∈ m, Φ k x ★ Ψ k x)
⊣⊢ ([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc.
Qed.
Lemma map_to_list_union m1 m2:
dom (gset K) m1 ∩ dom (gset K) m2 ≡ ∅ →
Permutation (map_to_list (m1 ∪ m2)) (map_to_list m1 ++ map_to_list m2).
Proof.
intros Hdom.
apply (anti_symm (contains)).
- apply NoDup_contains; auto using NoDup_map_to_list.
intros (x, a). rewrite elem_of_map_to_list.
rewrite lookup_union_Some_raw.
set_unfold.
intros [?|?].
× left. apply elem_of_map_to_list; naive_solver.
× right. apply elem_of_map_to_list; naive_solver.
- apply NoDup_contains. apply NoDup_app.
× split_and!; auto using NoDup_map_to_list.
intros (x, a). rewrite ?elem_of_map_to_list.
intros Hin1 Hin2.
assert (x ∈ dom (gset K) m1).
{ apply elem_of_dom; eauto. }
assert (x ∈ dom (gset K) m2).
{ apply elem_of_dom; eauto. }
set_solver.
× intros (x, a). set_unfold.
rewrite ?elem_of_map_to_list.
intros [Hleft|Hright]; apply lookup_union_Some_raw.
** naive_solver.
** specialize (Hdom x). rewrite ?elem_of_dom Hright in Hdom *=>Hdom'.
assert (m1 !! x = None).
{ destruct (m1 !! x); auto. exfalso. naive_solver. }
naive_solver.
Qed.
Lemma big_sepM_union Φ m1 m2 :
dom (gset K) m1 ∩ dom (gset K) m2 ≡ ∅ →
([★ map] k↦x ∈ m1, Φ k x) ★ ([★ map] k↦x ∈ m2, Φ k x)
⊣⊢ [★ map] k↦x ∈ (m1 ∪ m2), Φ k x.
Proof.
intros Hdom. rewrite /uPred_big_sepM //.
rewrite map_to_list_union; eauto.
induction (map_to_list m1).
- by rewrite //= left_id.
- simpl. rewrite -assoc. apply sep_proper; auto.
Qed.
Lemma map_union_least m1 m2 m3:
m1 ⊆ m3 →
m2 ⊆ m3 →
m1 ∪ m2 ⊆ m3.
Proof.
intros Hsub1 Hsub2.
apply map_subseteq_spec.
intros i x Hlook%lookup_union_Some_raw.
destruct Hlook as [Hlook1|(?&Hlook2)].
- eapply (map_subseteq_spec m1); eauto.
- eapply (map_subseteq_spec m2); eauto.
Qed.
Lemma big_sepM_split Φ m m1 m2 :
m1 ⊆ m →
m2 ⊆ m →
dom (gset K) m1 ∩ dom (gset K) m2 ≡ ∅ →
∃ m3,
([★ map] k↦x ∈ m, Φ k x)
⊣⊢ ([★ map] k↦x ∈ m1, Φ k x) ★
([★ map] k↦x ∈ m2, Φ k x) ★
([★ map] k↦x ∈ m3, Φ k x).
Proof.
intros Hsub1 Hsub2 Hdom.
pose (m3 := (map_of_list (filter (λ p, p.1 ∉ dom (gset K) m1 ∧ p.1 ∉ dom (gset K) m2)
(map_to_list m)) : gmap K A)).
∃ m3.
rewrite assoc.
rewrite big_sepM_union; auto.
rewrite big_sepM_union; auto.
- cut (m = m1 ∪ m2 ∪ m3).
{ by intros <-. }
assert (m3 ⊆ m) as Hsub3.
{ apply map_subseteq_spec⇒ x a.
rewrite /m3. intros Hlook3.
apply elem_of_map_of_list_2, elem_of_list_filter in Hlook3.
rewrite elem_of_map_to_list in Hlook3 ×. naive_solver.
}
apply (anti_symm (⊆)).
× apply map_subseteq_spec⇒x a Hlook.
apply lookup_union_Some.
** apply map_disjoint_dom.
set_unfold⇒x'. rewrite dom_union_L⇒Hin_12.
rewrite ?elem_of_dom //=.
inversion 1 as (a'&Hlook3).
rewrite /m3 in Hlook3.
apply elem_of_map_of_list_2, elem_of_list_filter in Hlook3.
set_unfold. naive_solver.
** rewrite lookup_union_Some; last first.
{ apply map_disjoint_dom. set_unfold. set_solver. }
case_eq (m1 !! x).
{ intros ? Hlook'%map_subseteq_spec; eauto.
rewrite Hlook in Hlook'. inversion Hlook'. naive_solver. }
intros Hnone1. case_eq (m2 !! x).
{ intros ? Hlook'%map_subseteq_spec; eauto.
rewrite Hlook in Hlook'. inversion Hlook'. naive_solver. }
intros Hnone2.
assert (is_Some (m3 !! x)) as (a'&Hlook').
{ rewrite /is_Some. case_eq (m3 !! x); first eauto.
rewrite /m3. intros Hnot%not_elem_of_map_of_list_2.
exfalso; apply Hnot. apply elem_of_list_fmap.
∃ (x, a); split; auto.
apply elem_of_list_filter. rewrite elem_of_map_to_list; split; auto.
rewrite ?not_elem_of_dom. naive_solver. }
rewrite Hlook'. eapply map_subseteq_spec in Hlook'; eauto.
rewrite Hlook in Hlook'. inversion Hlook'. naive_solver.
× apply map_union_least; auto.
apply map_union_least; auto.
- set_unfold⇒x'. rewrite dom_union_L. intros (Hin_12&Hin_3).
rewrite elem_of_dom //= in Hin_3 ×.
inversion 1 as (a'&Hlook3).
rewrite /m3 in Hlook3.
apply elem_of_map_of_list_2, elem_of_list_filter in Hlook3.
set_unfold. naive_solver.
Qed.
End gmap.
Context `{Countable K} {A : Type}.
Implicit Types m : gmap K A.
Implicit Types Φ Ψ : K → A → uPred M.
Lemma big_sepM_proper Φ Ψ m :
(∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) →
([★ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m, Ψ k x).
Proof.
intros HΦ. apply (anti_symm (⊢)).
- trans ([★ map] k ↦ x ∈ m, Φ k x)%I.
× apply big_sep_permutation, fmap_Permutation.
apply (anti_symm contains); apply map_to_list_contains; set_solver.
× apply big_sep_mono', Forall2_fmap, Forall_Forall2.
apply Forall_forall⇒ -[i x] ? /=. rewrite -HΦ; auto; apply elem_of_map_to_list; set_solver.
- trans ([★ map] k ↦ x ∈ m, Ψ k x)%I.
× apply big_sep_permutation, fmap_Permutation.
apply (anti_symm contains); apply map_to_list_contains; set_solver.
× apply big_sep_mono', Forall2_fmap, Forall_Forall2.
apply Forall_forall⇒ -[i x] ? /=. rewrite -HΦ; auto; apply elem_of_map_to_list; set_solver.
Qed.
Global Instance big_sepM_ne m n :
Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
(uPred_big_sepM (M:=M) m).
Proof.
intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
apply Forall_Forall2, Forall_true⇒ -[i x]; apply HΦ.
Qed.
Global Instance big_sepM_proper' m :
Proper (pointwise_relation _ (pointwise_relation _ (⊣⊢)) ==> (⊣⊢))
(uPred_big_sepM (M:=M) m).
Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_proper; intros; last apply HΦ. Qed.
Lemma big_sepM_empty Φ : ([★ map] k↦x ∈ ∅, Φ k x) ⊣⊢ Emp.
Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
Lemma big_sepM_insert Φ m i x :
m !! i = None →
([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ m, Φ k y.
Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
Lemma big_sepM_delete Φ m i x :
m !! i = Some x →
([★ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y.
Proof.
intros. rewrite -big_sepM_insert ?lookup_delete //.
by rewrite insert_delete insert_id.
Qed.
Lemma big_sepM_singleton Φ i x : ([★ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x.
Proof.
rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
by rewrite big_sepM_empty right_id.
Qed.
Lemma big_sepM_fmap {B} (f : A → B) (Φ : K → B → uPred M) m :
([★ map] k↦y ∈ f <$> m, Φ k y) ⊣⊢ ([★ map] k↦y ∈ m, Φ k (f y)).
Proof.
rewrite /uPred_big_sepM map_to_list_fmap -list_fmap_compose.
f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done.
Qed.
Lemma big_sepM_insert_override (Φ : K → uPred M) m i x y :
m !! i = Some x →
([★ map] k↦_ ∈ <[i:=y]> m, Φ k) ⊣⊢ ([★ map] k↦_ ∈ m, Φ k).
Proof.
intros. rewrite -insert_delete big_sepM_insert ?lookup_delete //.
by rewrite -big_sepM_delete.
Qed.
Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → uPred M) (f : K → B) m i x b :
m !! i = None →
([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=b]> f k))
⊣⊢ (Ψ i x b ★ [★ map] k↦y ∈ m, Ψ k y (f k)).
Proof.
intros. rewrite big_sepM_insert // fn_lookup_insert.
apply sep_proper, big_sepM_proper; auto⇒ k y ?.
by rewrite fn_lookup_insert_ne; last set_solver.
Qed.
Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P :
m !! i = None →
([★ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ★ [★ map] k↦y ∈ m, Φ k).
Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed.
Lemma big_sepM_sepM Φ Ψ m :
([★ map] k↦x ∈ m, Φ k x ★ Ψ k x)
⊣⊢ ([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc.
Qed.
Lemma map_to_list_union m1 m2:
dom (gset K) m1 ∩ dom (gset K) m2 ≡ ∅ →
Permutation (map_to_list (m1 ∪ m2)) (map_to_list m1 ++ map_to_list m2).
Proof.
intros Hdom.
apply (anti_symm (contains)).
- apply NoDup_contains; auto using NoDup_map_to_list.
intros (x, a). rewrite elem_of_map_to_list.
rewrite lookup_union_Some_raw.
set_unfold.
intros [?|?].
× left. apply elem_of_map_to_list; naive_solver.
× right. apply elem_of_map_to_list; naive_solver.
- apply NoDup_contains. apply NoDup_app.
× split_and!; auto using NoDup_map_to_list.
intros (x, a). rewrite ?elem_of_map_to_list.
intros Hin1 Hin2.
assert (x ∈ dom (gset K) m1).
{ apply elem_of_dom; eauto. }
assert (x ∈ dom (gset K) m2).
{ apply elem_of_dom; eauto. }
set_solver.
× intros (x, a). set_unfold.
rewrite ?elem_of_map_to_list.
intros [Hleft|Hright]; apply lookup_union_Some_raw.
** naive_solver.
** specialize (Hdom x). rewrite ?elem_of_dom Hright in Hdom *=>Hdom'.
assert (m1 !! x = None).
{ destruct (m1 !! x); auto. exfalso. naive_solver. }
naive_solver.
Qed.
Lemma big_sepM_union Φ m1 m2 :
dom (gset K) m1 ∩ dom (gset K) m2 ≡ ∅ →
([★ map] k↦x ∈ m1, Φ k x) ★ ([★ map] k↦x ∈ m2, Φ k x)
⊣⊢ [★ map] k↦x ∈ (m1 ∪ m2), Φ k x.
Proof.
intros Hdom. rewrite /uPred_big_sepM //.
rewrite map_to_list_union; eauto.
induction (map_to_list m1).
- by rewrite //= left_id.
- simpl. rewrite -assoc. apply sep_proper; auto.
Qed.
Lemma map_union_least m1 m2 m3:
m1 ⊆ m3 →
m2 ⊆ m3 →
m1 ∪ m2 ⊆ m3.
Proof.
intros Hsub1 Hsub2.
apply map_subseteq_spec.
intros i x Hlook%lookup_union_Some_raw.
destruct Hlook as [Hlook1|(?&Hlook2)].
- eapply (map_subseteq_spec m1); eauto.
- eapply (map_subseteq_spec m2); eauto.
Qed.
Lemma big_sepM_split Φ m m1 m2 :
m1 ⊆ m →
m2 ⊆ m →
dom (gset K) m1 ∩ dom (gset K) m2 ≡ ∅ →
∃ m3,
([★ map] k↦x ∈ m, Φ k x)
⊣⊢ ([★ map] k↦x ∈ m1, Φ k x) ★
([★ map] k↦x ∈ m2, Φ k x) ★
([★ map] k↦x ∈ m3, Φ k x).
Proof.
intros Hsub1 Hsub2 Hdom.
pose (m3 := (map_of_list (filter (λ p, p.1 ∉ dom (gset K) m1 ∧ p.1 ∉ dom (gset K) m2)
(map_to_list m)) : gmap K A)).
∃ m3.
rewrite assoc.
rewrite big_sepM_union; auto.
rewrite big_sepM_union; auto.
- cut (m = m1 ∪ m2 ∪ m3).
{ by intros <-. }
assert (m3 ⊆ m) as Hsub3.
{ apply map_subseteq_spec⇒ x a.
rewrite /m3. intros Hlook3.
apply elem_of_map_of_list_2, elem_of_list_filter in Hlook3.
rewrite elem_of_map_to_list in Hlook3 ×. naive_solver.
}
apply (anti_symm (⊆)).
× apply map_subseteq_spec⇒x a Hlook.
apply lookup_union_Some.
** apply map_disjoint_dom.
set_unfold⇒x'. rewrite dom_union_L⇒Hin_12.
rewrite ?elem_of_dom //=.
inversion 1 as (a'&Hlook3).
rewrite /m3 in Hlook3.
apply elem_of_map_of_list_2, elem_of_list_filter in Hlook3.
set_unfold. naive_solver.
** rewrite lookup_union_Some; last first.
{ apply map_disjoint_dom. set_unfold. set_solver. }
case_eq (m1 !! x).
{ intros ? Hlook'%map_subseteq_spec; eauto.
rewrite Hlook in Hlook'. inversion Hlook'. naive_solver. }
intros Hnone1. case_eq (m2 !! x).
{ intros ? Hlook'%map_subseteq_spec; eauto.
rewrite Hlook in Hlook'. inversion Hlook'. naive_solver. }
intros Hnone2.
assert (is_Some (m3 !! x)) as (a'&Hlook').
{ rewrite /is_Some. case_eq (m3 !! x); first eauto.
rewrite /m3. intros Hnot%not_elem_of_map_of_list_2.
exfalso; apply Hnot. apply elem_of_list_fmap.
∃ (x, a); split; auto.
apply elem_of_list_filter. rewrite elem_of_map_to_list; split; auto.
rewrite ?not_elem_of_dom. naive_solver. }
rewrite Hlook'. eapply map_subseteq_spec in Hlook'; eauto.
rewrite Hlook in Hlook'. inversion Hlook'. naive_solver.
× apply map_union_least; auto.
apply map_union_least; auto.
- set_unfold⇒x'. rewrite dom_union_L. intros (Hin_12&Hin_3).
rewrite elem_of_dom //= in Hin_3 ×.
inversion 1 as (a'&Hlook3).
rewrite /m3 in Hlook3.
apply elem_of_map_of_list_2, elem_of_list_filter in Hlook3.
set_unfold. naive_solver.
Qed.
End gmap.
Section gset.
Context `{Countable A}.
Implicit Types X : gset A.
Implicit Types Φ : A → uPred M.
Lemma big_sepS_proper Φ Ψ X Y :
X ≡ Y → (∀ x, x ∈ X → x ∈ Y → Φ x ⊣⊢ Ψ x) →
([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ Y, Ψ x).
Proof.
intros HX HΦ. apply (anti_symm (⊢)).
- trans ([★ set] x ∈ Y, Φ x)%I.
× apply big_sep_permutation, fmap_Permutation.
apply (anti_symm contains); set_solver.
× apply big_sep_mono', Forall2_fmap, Forall_Forall2.
apply Forall_forall⇒ x ? /=. rewrite HΦ; eauto.
** rewrite HX; by apply elem_of_elements.
** by apply elem_of_elements.
- trans ([★ set] x ∈ X, Ψ x)%I.
× apply big_sep_permutation, fmap_Permutation.
apply (anti_symm contains); set_solver.
× apply big_sep_mono', Forall2_fmap, Forall_Forall2.
apply Forall_forall⇒ x ? /=. rewrite HΦ; eauto.
** by apply elem_of_elements.
** rewrite -HX; by apply elem_of_elements.
Qed.
Lemma big_sepS_ne X n :
Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
Proof.
intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
apply Forall_Forall2, Forall_true⇒ x; apply HΦ.
Qed.
Lemma big_sepS_proper' X :
Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (uPred_big_sepS (M:=M) X).
Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed.
Lemma big_sepS_empty Φ : ([★ set] x ∈ ∅, Φ x) ⊣⊢ Emp.
Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
Lemma big_sepS_insert Φ X x :
x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X, Φ y).
Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
Lemma big_sepS_delete Φ X x :
x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y.
Proof.
intros. rewrite -big_sepS_insert; last set_solver.
by rewrite -union_difference_L; last set_solver.
Qed.
Lemma big_sepS_singleton Φ x : ([★ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
Lemma big_sepS_sepS Φ Ψ X :
([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ ([★ set] y ∈ X, Φ y) ★ ([★ set] y ∈ X, Ψ y).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc.
Qed.
End gset.
Context `{Countable A}.
Implicit Types X : gset A.
Implicit Types Φ : A → uPred M.
Lemma big_sepS_proper Φ Ψ X Y :
X ≡ Y → (∀ x, x ∈ X → x ∈ Y → Φ x ⊣⊢ Ψ x) →
([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ Y, Ψ x).
Proof.
intros HX HΦ. apply (anti_symm (⊢)).
- trans ([★ set] x ∈ Y, Φ x)%I.
× apply big_sep_permutation, fmap_Permutation.
apply (anti_symm contains); set_solver.
× apply big_sep_mono', Forall2_fmap, Forall_Forall2.
apply Forall_forall⇒ x ? /=. rewrite HΦ; eauto.
** rewrite HX; by apply elem_of_elements.
** by apply elem_of_elements.
- trans ([★ set] x ∈ X, Ψ x)%I.
× apply big_sep_permutation, fmap_Permutation.
apply (anti_symm contains); set_solver.
× apply big_sep_mono', Forall2_fmap, Forall_Forall2.
apply Forall_forall⇒ x ? /=. rewrite HΦ; eauto.
** by apply elem_of_elements.
** rewrite -HX; by apply elem_of_elements.
Qed.
Lemma big_sepS_ne X n :
Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
Proof.
intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
apply Forall_Forall2, Forall_true⇒ x; apply HΦ.
Qed.
Lemma big_sepS_proper' X :
Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (uPred_big_sepS (M:=M) X).
Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed.
Lemma big_sepS_empty Φ : ([★ set] x ∈ ∅, Φ x) ⊣⊢ Emp.
Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
Lemma big_sepS_insert Φ X x :
x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X, Φ y).
Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
Lemma big_sepS_delete Φ X x :
x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y.
Proof.
intros. rewrite -big_sepS_insert; last set_solver.
by rewrite -union_difference_L; last set_solver.
Qed.
Lemma big_sepS_singleton Φ x : ([★ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
Lemma big_sepS_sepS Φ Ψ X :
([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ ([★ set] y ∈ X, Φ y) ★ ([★ set] y ∈ X, Ψ y).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc.
Qed.
End gset.
Global Instance big_sep_relevant Ps : RelevantL Ps → RelevantP ([★] Ps).
Proof. induction 1; apply _. Qed.
Global Instance big_sep_affine Ps : AffineL Ps → AffineP ([★] Ps).
Proof. induction 1; apply _. Qed.
Global Instance nil_relevant : RelevantL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_relevant P Ps :
RelevantP P → RelevantL Ps → RelevantL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_relevant Ps Ps' :
RelevantL Ps → RelevantL Ps' → RelevantL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.
Global Instance zip_with_relevant {A B} (f : A → B → uPred M) xs ys :
(∀ x y, RelevantP (f x y)) → RelevantL (zip_with f xs ys).
Proof.
unfold RelevantL⇒ ?; revert ys; induction xs⇒ -[|??]; constructor; auto.
Qed.
Global Instance nil_affine : AffineL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_affine P Ps :
AffineP P → AffineL Ps → AffineL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_affine Ps Ps' :
AffineL Ps → AffineL Ps' → AffineL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.
Global Instance zip_with_affine {A B} (f : A → B → uPred M) xs ys :
(∀ x y, AffineP (f x y)) → AffineL (zip_with f xs ys).
Proof.
unfold AffineL⇒ ?; revert ys; induction xs⇒ -[|??]; constructor; auto.
Qed.
End big_op.
Proof. induction 1; apply _. Qed.
Global Instance big_sep_affine Ps : AffineL Ps → AffineP ([★] Ps).
Proof. induction 1; apply _. Qed.
Global Instance nil_relevant : RelevantL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_relevant P Ps :
RelevantP P → RelevantL Ps → RelevantL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_relevant Ps Ps' :
RelevantL Ps → RelevantL Ps' → RelevantL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.
Global Instance zip_with_relevant {A B} (f : A → B → uPred M) xs ys :
(∀ x y, RelevantP (f x y)) → RelevantL (zip_with f xs ys).
Proof.
unfold RelevantL⇒ ?; revert ys; induction xs⇒ -[|??]; constructor; auto.
Qed.
Global Instance nil_affine : AffineL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_affine P Ps :
AffineP P → AffineL Ps → AffineL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_affine Ps Ps' :
AffineL Ps → AffineL Ps' → AffineL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.
Global Instance zip_with_affine {A B} (f : A → B → uPred M) xs ys :
(∀ x y, AffineP (f x y)) → AffineL (zip_with f xs ys).
Proof.
unfold AffineL⇒ ?; revert ys; induction xs⇒ -[|??]; constructor; auto.
Qed.
End big_op.