Big op for uPred_sep for finite sets.

With nicely overloaded notations for sets and maps.

algebra/upred_big_op.v

 From algebra Require Export upred.
-From prelude Require Import fin_maps.
+From prelude Require Import fin_maps fin_collections.
 
-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 [] => True | 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.
+(** * Big ops over lists *)
+(* These are the basic building blocks for other big ops *)
+Fixpoint uPred_list_and {M} (Ps : list (uPred M)) : uPred M:=
+  match Ps with [] => True | P :: Ps => P ∧ uPred_list_and Ps end%I.
+Instance: Params (@uPred_list_and) 1.
+Notation "'Π∧' Ps" := (uPred_list_and Ps) (at level 20) : uPred_scope.
+Fixpoint uPred_list_sep {M} (Ps : list (uPred M)) : uPred M :=
+  match Ps with [] => True | P :: Ps => P ★ uPred_list_sep Ps end%I.
+Instance: Params (@uPred_list_sep) 1.
+Notation "'Π★' Ps" := (uPred_list_sep Ps) (at level 20) : uPred_scope.
 
-Definition uPred_big_sepM {M : cmraT} `{FinMapToList K A MA}
-    (P : K → A → uPred M) (m : MA) : uPred M :=
-  uPred_big_sep (curry P <$> map_to_list m).
-Instance: Params (@uPred_big_sepM) 5.
-Notation "'Π★{' P } m" := (uPred_big_sepM P m)
-  (at level 20, P at level 10, m at level 20, format "Π★{ P }  m") : uPred_scope.
+(** * Other big ops *)
+(** We use a type class to obtain overloaded notations *)
+Class UPredBigSep (M : cmraT) (A B : Type) :=
+  uPred_big_sep : A → B → uPred M.
+Instance: Params (@uPred_big_sep) 4.
+Notation "'Π★{' x } P" := (uPred_big_sep x P)
+  (at level 20, x at level 10, format "Π★{ x }  P") : uPred_scope.
 
+Instance uPred_big_sepM {M} `{FinMapToList K A MA} :
+    UPredBigSep M MA (K → A → uPred M) := λ m P,
+  uPred_list_sep (curry P <$> map_to_list m).
+Instance uPred_big_sepC {M} `{Elements A C} :
+  UPredBigSep M C (A → uPred M) := λ X P, uPred_list_sep (P <$> elements X).
+
+(** * Always stability for lists *)
 Class AlwaysStableL {M} (Ps : list (uPred M)) :=
   always_stableL : Forall AlwaysStable Ps.
 Arguments always_stableL {_} _ {_}.
@@ -28,45 +38,47 @@ Implicit Types Ps Qs : list (uPred M).
 Implicit Types A : Type.
 
 (* Big ops *)
-Global Instance big_and_proper : Proper ((≡) ==> (≡)) (@uPred_big_and M).
+Global Instance list_and_proper : Proper ((≡) ==> (≡)) (@uPred_list_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).
+Global Instance list_sep_proper : Proper ((≡) ==> (≡)) (@uPred_list_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).
+Global Instance list_and_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_list_and M).
 Proof.
   induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
   * by rewrite IH.
   * by rewrite !assoc (comm _ P).
   * etransitivity; eauto.
 Qed.
-Global Instance big_sep_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_sep M).
+Global Instance list_sep_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_list_sep M).
 Proof.
   induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
   * by rewrite IH.
   * by rewrite !assoc (comm _ P).
   * etransitivity; eauto.
 Qed.
-Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I.
+Lemma list_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.
+Lemma list_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I ≡ (Π★ Ps ★ Π★ Qs)%I.
 Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
-Lemma big_sep_and Ps : (Π★ Ps) ⊑ (Π∧ Ps).
+Lemma list_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.
+Lemma list_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.
+Lemma list_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).
 
-  Lemma big_sepM_empty : (Π★{P} ∅)%I ≡ True%I.
-  Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
+  Lemma big_sepM_empty : (Π★{∅} 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 → (Π★{P} (<[i:=x]> m))%I ≡ (P i x ★ Π★{P} m)%I.
-  Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
-  Lemma big_sepM_singleton i x : (Π★{P} {[i ↦ x]})%I ≡ (P i x)%I.
+    m !! i = None → (Π★{<[i:=x]> m} P)%I ≡ (P i x ★ Π★{m} P)%I.
+  Proof.
+    intros ?; by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_insert.
+  Qed.
+  Lemma big_sepM_singleton i x : (Π★{{[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.
@@ -76,9 +88,9 @@ End fin_map.
 (* Always stable *)
 Local Notation AS := AlwaysStable.
 Local Notation ASL := AlwaysStableL.
-Global Instance big_and_always_stable Ps : ASL Ps → AS (Π∧ Ps).
+Global Instance list_and_always_stable Ps : ASL Ps → AS (Π∧ Ps).
 Proof. induction 1; apply _. Qed.
-Global Instance big_sep_always_stable Ps : ASL Ps → AS (Π★ Ps).
+Global Instance list_sep_always_stable Ps : ASL Ps → AS (Π★ Ps).
 Proof. induction 1; apply _. Qed.
 
 Global Instance nil_always_stable : ASL (@nil (uPred M)).
@@ -90,4 +102,4 @@ Proof. apply Forall_app_2. Qed.
 Global Instance zip_with_always_stable {A B} (f : A → B → uPred M) xs ys :
   (∀ x y, AS (f x y)) → ASL (zip_with f xs ys).
 Proof. unfold ASL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed.
-End big_op.
\ No newline at end of file
+End big_op.

heap_lang/heap.v

@@ -72,7 +72,7 @@ Section heap.
   Qed.
 
   Lemma heap_alloc N σ :
-    ownP σ ⊑ pvs N N (∃ γ, heap_ctx HeapI γ N ∧ Π★{heap_mapsto HeapI γ} σ).
+    ownP σ ⊑ pvs N N (∃ γ, heap_ctx HeapI γ N ∧ Π★{σ} heap_mapsto HeapI γ).
   Proof.
     rewrite -{1}(from_to_heap σ); etransitivity;
       first apply (auth_alloc (ownP ∘ of_heap) N (to_heap σ)), to_heap_valid.