Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

algebra/cmra_big_op.v

 From algebra Require Export cmra.
-From prelude Require Import fin_maps.
+From prelude Require Import gmap.
 
 Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
   match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end.
 Arguments big_op _ _ !_ /.
 Instance: Params (@big_op) 2.
-Definition big_opM {A : cmraT} `{FinMapToList K A M, Empty A} (m : M) : A :=
+Definition big_opM `{Countable K} {A : cmraT} `{Empty A} (m : gmap K A) : A :=
   big_op (snd <$> map_to_list m).
 Instance: Params (@big_opM) 5.
 
@@ -34,33 +34,31 @@ Proof.
 Qed.
 Lemma big_op_contains xs ys : xs `contains` ys → big_op xs ≼ big_op ys.
 Proof.
-  induction 1 as [|x xs ys|x y xs|x xs ys|xs ys zs]; rewrite //=.
-  - by apply cmra_preserving_l.
-  - by rewrite !assoc (comm _ y).
-  - by transitivity (big_op ys); last apply cmra_included_r.
-  - by transitivity (big_op ys).
+  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.
 Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed.
 
-Context `{FinMap K M}.
-Lemma big_opM_empty : big_opM (∅ : M A) ≡ ∅.
+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 : M A) i x :
+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 : M A) i x :
+Lemma big_opM_delete m i x :
   m !! i = Some x → x ⋅ big_opM (delete i m) ≡ big_opM m.
 Proof.
   intros. by rewrite -{2}(insert_delete m i x) // big_opM_insert ?lookup_delete.
 Qed.
-Lemma big_opM_singleton i x : big_opM ({[i := x]} : M A) ≡ x.
+Lemma big_opM_singleton i x : big_opM ({[i := x]} : gmap K A) ≡ x.
 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 : M A → _).
+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 ->. }

algebra/upred_big_op.v

 From algebra Require Export upred.
-From prelude Require Import fin_maps fin_collections.
+From prelude Require Import gmap fin_collections.
 
 (** * Big ops over lists *)
 (* These are the basic building blocks for other big ops *)
@@ -14,14 +14,16 @@ Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
 
 (** * Other big ops *)
 (** We use a type class to obtain overloaded notations *)
-Definition uPred_big_sepM {M} `{FinMapToList K A MA}
-    (m : MA) (P : K → A → uPred M) : uPred M :=
+Definition uPred_big_sepM {M} `{Countable K} {A}
+    (m : gmap K A) (P : K → A → uPred M) : uPred M :=
   uPred_big_sep (curry P <$> map_to_list m).
+Instance: Params (@uPred_big_sepM) 6.
 Notation "'Π★{map' m } P" := (uPred_big_sepM m P)
   (at level 20, m at level 10, format "Π★{map  m }  P") : uPred_scope.
 
-Definition uPred_big_sepS {M} `{Elements A C}
-  (X : C) (P : A → uPred M) : uPred M := uPred_big_sep (P <$> elements X).
+Definition uPred_big_sepS {M} `{Countable A}
+  (X : gset A) (P : A → uPred M) : uPred M := uPred_big_sep (P <$> elements X).
+Instance: Params (@uPred_big_sepS) 5.
 Notation "'Π★{set' X } P" := (uPred_big_sepS X P)
   (at level 20, X at level 10, format "Π★{set  X }  P") : uPred_scope.
 
@@ -32,7 +34,6 @@ Arguments always_stableL {_} _ {_}.
 
 Section big_op.
 Context {M : cmraT}.
-Implicit Types P Q : uPred M.
 Implicit Types Ps Qs : list (uPred M).
 Implicit Types A : Type.
 
@@ -41,6 +42,19 @@ 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 (Forall2 (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 (Forall2 (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.
@@ -55,34 +69,121 @@ Proof.
   - by rewrite !assoc (comm _ P).
   - etransitivity; eauto.
 Qed.
+
 Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I.
 Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
 Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I ≡ (Π★ Ps ★ Π★ Qs)%I.
 Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
+
+Lemma big_and_contains Ps Qs : Qs `contains` Ps → (Π∧ Ps)%I ⊑ (Π∧ Qs)%I.
+Proof.
+  intros [Ps' ->]%contains_Permutation. by rewrite big_and_app uPred.and_elim_l.
+Qed.
+Lemma big_sep_contains Ps Qs : Qs `contains` Ps → (Π★ Ps)%I ⊑ (Π★ Qs)%I.
+Proof.
+  intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app uPred.sep_elim_l.
+Qed.
+
 Lemma big_sep_and Ps : (Π★ Ps) ⊑ (Π∧ Ps).
 Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
+
 Lemma big_and_elem_of Ps P : P ∈ Ps → (Π∧ Ps) ⊑ P.
 Proof. induction 1; simpl; auto with I. Qed.
 Lemma big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊑ P.
 Proof. induction 1; simpl; auto with I. Qed.
 
 (* Big ops over finite maps *)
-Section fin_map.
-  Context `{FinMap K Ma} {A} (P : K → A → uPred M).
+Section gmap.
+  Context `{Countable K} {A : Type}.
+  Implicit Types m : gmap K A.
+  Implicit Types P : K → A → uPred M.
 
-  Lemma big_sepM_empty : (Π★{map ∅} P)%I ≡ True%I.
-  Proof. by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_empty. Qed.
-  Lemma big_sepM_insert (m : Ma A) i x :
-    m !! i = None → (Π★{map <[i:=x]> m} P)%I ≡ (P i x ★ Π★{map m} P)%I.
+  Lemma big_sepM_mono P Q m1 m2 :
+    m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → P k x ⊑ Q k x) →
+    (Π★{map m1} P) ⊑ (Π★{map m2} Q).
   Proof.
-    intros ?; by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_insert.
+    intros HX HP. transitivity (Π★{map m2} P)%I.
+    - by apply big_sep_contains, fmap_contains, map_to_list_contains.
+    - apply big_sep_mono', Forall2_fmap, Forall2_Forall.
+      apply Forall_forall=> -[i x] ? /=. by apply HP, elem_of_map_to_list.
   Qed.
-  Lemma big_sepM_singleton i x : (Π★{map {[i := x]}} P)%I ≡ (P i x)%I.
+
+  Global Instance big_sepM_ne m n :
+    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
+           (uPred_big_sepM (M:=M) m).
+  Proof.
+    intros P1 P2 HP. apply big_sep_ne, Forall2_fmap.
+    apply Forall2_Forall, Forall_true=> -[i x]; apply HP.
+  Qed.
+  Global Instance big_sepM_proper m :
+    Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡))
+           (uPred_big_sepM (M:=M) m).
+  Proof.
+    intros P1 P2 HP; apply equiv_dist=> n.
+    apply big_sepM_ne=> k x; apply equiv_dist, HP.
+  Qed.
+  Global Instance big_sepM_mono' m :
+    Proper (pointwise_relation _ (pointwise_relation _ (⊑)) ==> (⊑))
+           (uPred_big_sepM (M:=M) m).
+  Proof. intros P1 P2 HP. apply big_sepM_mono; intros; [done|apply HP]. Qed.
+
+  Lemma big_sepM_empty P : (Π★{map ∅} P)%I ≡ True%I.
+  Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
+  Lemma big_sepM_insert P (m : gmap K A) i x :
+    m !! i = None → (Π★{map <[i:=x]> m} P)%I ≡ (P i x ★ Π★{map m} P)%I.
+  Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
+  Lemma big_sepM_singleton P i x : (Π★{map {[i := x]}} P)%I ≡ (P i x)%I.
   Proof.
     rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
     by rewrite big_sepM_empty right_id.
   Qed.
-End fin_map.
+End gmap.
+
+(* Big ops over finite sets *)
+Section gset.
+  Context `{Countable A}.
+  Implicit Types X : gset A.
+  Implicit Types P : A → uPred M.
+
+  Lemma big_sepS_mono P Q X Y :
+    Y ⊆ X → (∀ x, x ∈ Y → P x ⊑ Q x) → (Π★{set X} P) ⊑ (Π★{set Y} Q).
+  Proof.
+    intros HX HP. transitivity (Π★{set Y} P)%I.
+    - by apply big_sep_contains, fmap_contains, elements_contains.
+    - apply big_sep_mono', Forall2_fmap, Forall2_Forall.
+      apply Forall_forall=> x ? /=. by apply HP, 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 P1 P2 HP. apply big_sep_ne, Forall2_fmap.
+    apply Forall2_Forall, Forall_true=> x; apply HP.
+  Qed.
+  Lemma big_sepS_proper X :
+    Proper (pointwise_relation _ (≡) ==> (≡)) (uPred_big_sepS (M:=M) X).
+  Proof.
+    intros P1 P2 HP; apply equiv_dist=> n.
+    apply big_sepS_ne=> x; apply equiv_dist, HP.
+  Qed.
+  Lemma big_sepS_mono' X :
+    Proper (pointwise_relation _ (⊑) ==> (⊑)) (uPred_big_sepS (M:=M) X).
+  Proof. intros P1 P2 HP. apply big_sepS_mono; naive_solver. Qed.
+
+  Lemma big_sepS_empty P : (Π★{set ∅} P)%I ≡ True%I.
+  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
+  Lemma big_sepS_insert P X x :
+    x ∉ X → (Π★{set {[ x ]} ∪ X} P)%I ≡ (P x ★ Π★{set X} P)%I.
+  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
+  Lemma big_sepS_delete P X x :
+    x ∈ X → (Π★{set X} P)%I ≡ (P x ★ Π★{set X ∖ {[ x ]}} P)%I.
+  Proof.
+    intros. rewrite -big_sepS_insert; last solve_elem_of.
+    by rewrite -union_difference_L; last solve_elem_of.
+  Qed.
+  Lemma big_sepS_singleton P x : (Π★{set {[ x ]}} P)%I ≡ (P x)%I.
+  Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
+End gset.
 
 (* Always stable *)
 Local Notation AS := AlwaysStable.

prelude/fin_collections.v

@@ -24,14 +24,35 @@ Proof.
   - apply NoDup_elements.
   - intros. by rewrite !elem_of_elements, E.
 Qed.
+Lemma elements_empty : elements (∅ : C) = [].
+Proof.
+  apply elem_of_nil_inv; intros x.
+  rewrite elem_of_elements, elem_of_empty; tauto.
+Qed.
+Lemma elements_union_singleton (X : C) x :
+  x ∉ X → elements ({[ x ]} ∪ X) ≡ₚ x :: elements X.
+Proof.
+  intros ?; apply NoDup_Permutation.
+  { apply NoDup_elements. }
+  { by constructor; rewrite ?elem_of_elements; try apply NoDup_elements. }
+  intros y; rewrite elem_of_elements, elem_of_union, elem_of_singleton.
+  by rewrite elem_of_cons, elem_of_elements.
+Qed.
+Lemma elements_singleton x : elements {[ x ]} = [x].
+Proof.
+  apply Permutation_singleton. by rewrite <-(right_id ∅ (∪) {[x]}),
+    elements_union_singleton, elements_empty by solve_elem_of.
+Qed.
+Lemma elements_contains X Y : X ⊆ Y → elements X `contains` elements Y.
+Proof.
+  intros; apply NoDup_contains; auto using NoDup_elements.
+  intros x. rewrite !elem_of_elements; auto.
+Qed.
+
 Global Instance collection_size_proper: Proper ((≡) ==> (=)) (@size C _).
 Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
 Lemma size_empty : size (∅ : C) = 0.
-Proof.
-  unfold size, collection_size. simpl.
-  rewrite (elem_of_nil_inv (elements ∅)); [done|intro].
-  rewrite elem_of_elements, elem_of_empty; auto.
-Qed.
+Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed.
 Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅.
 Proof.
   intros; apply equiv_empty; intros x; rewrite <-elem_of_elements.
@@ -42,14 +63,7 @@ Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
 Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅.
 Proof. by rewrite size_empty_iff. Qed.
 Lemma size_singleton (x : A) : size {[ x ]} = 1.
-Proof.
-  change (length (elements {[ x ]}) = length [x]).
-  apply Permutation_length, NoDup_Permutation.
-  - apply NoDup_elements.
-  - apply NoDup_singleton.
-  - intros y.
-    by rewrite elem_of_elements, elem_of_singleton, elem_of_list_singleton.
-Qed.
+Proof. unfold size, collection_size. simpl. by rewrite elements_singleton. Qed.
 Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
 Proof.
   unfold size, collection_size. simpl. rewrite <-!elem_of_elements.

prelude/fin_maps.v

@@ -671,6 +671,12 @@ Proof.
     rewrite elem_of_map_to_list in Hlookup. congruence.
   - by rewrite !map_of_to_list.
 Qed.
+Lemma map_to_list_contains {A} (m1 m2 : M A) :
+  m1 ⊆ m2 → map_to_list m1 `contains` map_to_list m2.
+Proof.
+  intros; apply NoDup_contains; auto using NoDup_map_to_list.
+  intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken.
+Qed.
 Lemma map_of_list_nil {A} : map_of_list (@nil (K * A)) = ∅.
 Proof. done. Qed.
 Lemma map_of_list_cons {A} (l : list (K * A)) i x :