Redefine big ops to get more definitional equalities.

opam.pins

-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 0ac2b4db07bdc471421c5a4c47789087b3df074c
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp a0ce0937cfabe16a184af2d92c0466ebacecbca2

theories/algebra/cmra_tactics.v

@@ -23,15 +23,15 @@ Module ra_reflection. Section ra_reflection.
     | EOp e1 e2 => flatten e1 ++ flatten e2
     end.
   Lemma eval_flatten Σ e :
-    eval Σ e ≡ big_op ((λ n, from_option id ∅ (Σ !! n)) <$> flatten e).
+    eval Σ e ≡ [⋅ list] n ∈ flatten e, from_option id ∅ (Σ !! n).
   Proof.
     induction e as [| |e1 IH1 e2 IH2]; rewrite /= ?right_id //.
-    by rewrite fmap_app IH1 IH2 big_op_app.
+    by rewrite IH1 IH2 big_opL_app.
   Qed.
   Lemma flatten_correct Σ e1 e2 :
     flatten e1 ⊆+ flatten e2 → eval Σ e1 ≼ eval Σ e2.
   Proof.
-    by intros He; rewrite !eval_flatten; apply big_op_submseteq; rewrite ->He.
+    by intros He; rewrite !eval_flatten; apply big_opL_submseteq; rewrite ->He.
   Qed.
 
   Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.

theories/base_logic/big_op.v

@@ -85,27 +85,28 @@ Arguments uPredR : clear implicits.
 Arguments uPredUR : clear implicits.
 
 (* Notations *)
-Notation "'[∗]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope.
-
-Notation "'[∗' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ k x, P))
+Notation "'[∗' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) (λ k x, P) l)
   (at level 200, l at level 10, k, x at level 1, right associativity,
    format "[∗  list ]  k ↦ x  ∈  l ,  P") : uPred_scope.
-Notation "'[∗' 'list' ] x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ _ x, P))
+Notation "'[∗' 'list' ] x ∈ l , P" := (big_opL (M:=uPredUR _) (λ _ x, P) l)
   (at level 200, l at level 10, x at level 1, right associativity,
    format "[∗  list ]  x  ∈  l ,  P") : uPred_scope.
 
-Notation "'[∗' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ k x, P))
+Notation "'[∗]' Ps" :=
+  (big_opL (M:=uPredUR _) (λ _ x, x) Ps) (at level 20) : uPred_scope.
+
+Notation "'[∗' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) (λ k x, P) m)
   (at level 200, m at level 10, k, x at level 1, right associativity,
    format "[∗  map ]  k ↦ x  ∈  m ,  P") : uPred_scope.
-Notation "'[∗' 'map' ] x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ _ x, P))
+Notation "'[∗' 'map' ] x ∈ m , P" := (big_opM (M:=uPredUR _) (λ _ x, P) m)
   (at level 200, m at level 10, x at level 1, right associativity,
    format "[∗  map ]  x  ∈  m ,  P") : uPred_scope.
 
-Notation "'[∗' 'set' ] x ∈ X , P" := (big_opS (M:=uPredUR _) X (λ x, P))
+Notation "'[∗' 'set' ] x ∈ X , P" := (big_opS (M:=uPredUR _) (λ x, P) X)
   (at level 200, X at level 10, x at level 1, right associativity,
    format "[∗  set ]  x  ∈  X ,  P") : uPred_scope.
 
-Notation "'[∗' 'mset' ] x ∈ X , P" := (big_opMS (M:=uPredUR _) X (λ x, P))
+Notation "'[∗' 'mset' ] x ∈ X , P" := (big_opMS (M:=uPredUR _) (λ x, P) X)
   (at level 200, X at level 10, x at level 1, right associativity,
    format "[∗  mset ]  x  ∈  X ,  P") : uPred_scope.
 
@@ -126,24 +127,6 @@ Context {M : ucmraT}.
 Implicit Types Ps Qs : list (uPred M).
 Implicit Types A : Type.
 
-Global Instance big_sep_mono' :
-  Proper (Forall2 (⊢) ==> (⊢)) (big_op (M:=uPredUR M)).
-Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-
-Lemma big_sep_app Ps Qs : [∗] (Ps ++ Qs) ⊣⊢ [∗] Ps ∗ [∗] Qs.
-Proof. by rewrite big_op_app. Qed.
-
-Lemma big_sep_submseteq Ps Qs : Qs ⊆+ Ps → [∗] Ps ⊢ [∗] Qs.
-Proof. intros. apply uPred_included. by apply: big_op_submseteq. Qed.
-Lemma big_sep_elem_of Ps P : P ∈ Ps → [∗] Ps ⊢ P.
-Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
-Lemma big_sep_elem_of_acc Ps P : P ∈ Ps → [∗] Ps ⊢ P ∗ (P -∗ [∗] Ps).
-Proof. intros [k ->]%elem_of_Permutation. by apply sep_mono_r, wand_intro_l. Qed.
-
-(** ** Persistence *)
-Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([∗] Ps).
-Proof. induction 1; apply _. Qed.
-
 Global Instance nil_persistent : PersistentL (@nil (uPred M)).
 Proof. constructor. Qed.
 Global Instance cons_persistent P Ps :
@@ -163,9 +146,7 @@ Proof.
 Qed.
 Global Instance imap_persistent {A} (f : nat → A → uPred M) xs :
   (∀ i x, PersistentP (f i x)) → PersistentL (imap f xs).
-Proof.
-  rewrite /PersistentL /imap=> ?. generalize 0. induction xs; constructor; auto.
-Qed.
+Proof. revert f. induction xs; simpl; constructor; naive_solver. Qed.
 
 (** ** Timelessness *)
 Global Instance big_sep_timeless Ps : TimelessL Ps → TimelessP ([∗] Ps).
@@ -190,9 +171,7 @@ Proof.
 Qed.
 Global Instance imap_timeless {A} (f : nat → A → uPred M) xs :
   (∀ i x, TimelessP (f i x)) → TimelessL (imap f xs).
-Proof.
-  rewrite /TimelessL /imap=> ?. generalize 0. induction xs; constructor; auto.
-Qed.
+Proof. revert f. induction xs; simpl; constructor; naive_solver. Qed.
 
 (** ** Big ops over lists *)
 Section list.
@@ -226,17 +205,21 @@ Section list.
     l1 ⊆+ l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y.
   Proof. intros ?. apply uPred_included. by apply: big_opL_submseteq. Qed.
 
-  Global Instance big_sepL_mono' l :
-    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢))
-           (big_opL (M:=uPredUR M) l).
-  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
+  Global Instance big_sepL_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
+           (big_opL (M:=uPredUR M) (A:=A)).
+  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
+  Global Instance big_sep_mono' :
+    Proper (Forall2 (⊢) ==> (⊢)) (big_opL (M:=uPredUR M) (λ _ P, P)).
+  Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
   Lemma big_sepL_lookup_acc Φ l i x :
     l !! i = Some x →
     ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x ∗ (Φ i x -∗ ([∗ list] k↦y ∈ l, Φ k y)).
   Proof.
-    intros Hli. apply big_sep_elem_of_acc, (elem_of_list_lookup_2 _ i).
-    by rewrite list_lookup_imap Hli.
+    intros Hli. rewrite -(take_drop_middle l i x) // big_sepL_app /=.
+    rewrite Nat.add_0_r take_length_le; eauto using lookup_lt_Some, Nat.lt_le_incl.
+    rewrite assoc -!(comm _ (Φ _ _)) -assoc. by apply sep_mono_r, wand_intro_l.
   Qed.
 
   Lemma big_sepL_lookup Φ l i x :
@@ -303,16 +286,21 @@ Section list.
 
   Global Instance big_sepL_nil_persistent Φ :
     PersistentP ([∗ list] k↦x ∈ [], Φ k x).
-  Proof. rewrite /big_opL. apply _. Qed.
+  Proof. apply _. Qed.
   Global Instance big_sepL_persistent Φ l :
     (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ list] k↦x ∈ l, Φ k x).
-  Proof. rewrite /big_opL. apply _. Qed.
+  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Global Instance big_sepL_persistent_id Ps : PersistentL Ps → PersistentP ([∗] Ps).
+  Proof. induction 1; apply _. Qed.
+
   Global Instance big_sepL_nil_timeless Φ :
     TimelessP ([∗ list] k↦x ∈ [], Φ k x).
-  Proof. rewrite /big_opL. apply _. Qed.
+  Proof. apply _. Qed.
   Global Instance big_sepL_timeless Φ l :
     (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ list] k↦x ∈ l, Φ k x).
-  Proof. rewrite /big_opL. apply _. Qed.
+  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Global Instance big_sepL_timeless_id Ps : TimelessL Ps → TimelessP ([∗] Ps).
+  Proof. induction 1; apply _. Qed.
 End list.
 
 Section list2.
@@ -325,13 +313,13 @@ Section list2.
     ([∗ list] k↦x ∈ zip_with f l1 l2, Φ k x)
     ⊣⊢ ([∗ list] k↦x ∈ l1, ∀ y, ⌜l2 !! k = Some y⌝ → Φ k (f x y)).
   Proof.
-    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2]//=.
-    - rewrite big_sepL_nil. apply (anti_symm _), True_intro.
+    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2]//.
+    - apply (anti_symm _), True_intro.
       trans ([∗ list] _↦_ ∈ x :: l1, True : uPred M)%I.
       + rewrite big_sepL_forall. auto using forall_intro, impl_intro_l, True_intro.
       + apply big_sepL_mono=> k y _. apply forall_intro=> z.
         by apply impl_intro_l, pure_elim_l.
-    - rewrite !big_sepL_cons IH. apply sep_proper=> //. apply (anti_symm _).
+    - rewrite /= IH. apply sep_proper=> //. apply (anti_symm _).
       + apply forall_intro=>z /=. by apply impl_intro_r, pure_elim_r=>-[->].
       + rewrite (forall_elim y) /=. by eapply impl_elim, pure_intro.
   Qed.
@@ -348,8 +336,7 @@ Section gmap.
     ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Ψ k x.
   Proof.
     intros Hm HΦ. trans ([∗ map] k↦x ∈ m2, Φ k x)%I.
-    - apply uPred_included. apply: big_op_submseteq.
-      by apply fmap_submseteq, map_to_list_submseteq.
+    - rewrite /big_opM. by apply big_sepL_submseteq, map_to_list_submseteq.
     - apply big_opM_forall; apply _ || auto.
   Qed.
   Lemma big_sepM_proper Φ Ψ m :
@@ -357,10 +344,10 @@ Section gmap.
     ([∗ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([∗ map] k ↦ x ∈ m, Ψ k x).
   Proof. apply big_opM_proper. Qed.
 
-  Global Instance big_sepM_mono' m :
-    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢))
-           (big_opM (M:=uPredUR M) m).
-  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
+  Global Instance big_sepM_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
+           (big_opM (M:=uPredUR M) (A:=A)).
+  Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True.
   Proof. by rewrite big_opM_empty. Qed.
@@ -493,13 +480,13 @@ Section gmap.
   Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
   Global Instance big_sepM_persistent Φ m :
     (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ map] k↦x ∈ m, Φ k x).
-  Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed.
+  Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
   Global Instance big_sepM_nil_timeless Φ :
     TimelessP ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
   Global Instance big_sepM_timeless Φ m :
     (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ map] k↦x ∈ m, Φ k x).
-  Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed.
+  Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
 End gmap.
 
 
@@ -514,8 +501,7 @@ Section gset.
     ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Ψ x.
   Proof.
     intros HX HΦ. trans ([∗ set] x ∈ Y, Φ x)%I.
-    - apply uPred_included. apply: big_op_submseteq.
-      by apply fmap_submseteq, elements_submseteq.
+    - rewrite /big_opM. by apply big_sepL_submseteq, elements_submseteq.
     - apply big_opS_forall; apply _ || auto.
   Qed.
   Lemma big_sepS_proper Φ Ψ X :
@@ -523,9 +509,9 @@ Section gset.
     ([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ set] x ∈ X, Ψ x).
   Proof. apply: big_opS_proper. Qed.
 
-  Global Instance big_sepS_mono' X :
-     Proper (pointwise_relation _ (⊢) ==> (⊢)) (big_opS (M:=uPredUR M) X).
-  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
+  Global Instance big_sepS_mono' :
+     Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opS (M:=uPredUR M) (A:=A)).
+  Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ True.
   Proof. by rewrite big_opS_empty. Qed.
@@ -665,8 +651,7 @@ Section gmultiset.
     ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ Y, Ψ x.
   Proof.
     intros HX HΦ. trans ([∗ mset] x ∈ Y, Φ x)%I.
-    - apply uPred_included. apply: big_op_submseteq.
-      by apply fmap_submseteq, gmultiset_elements_submseteq.
+    - rewrite /big_opM. by apply big_sepL_submseteq, gmultiset_elements_submseteq.
     - apply big_opMS_forall; apply _ || auto.
   Qed.
   Lemma big_sepMS_proper Φ Ψ X :
@@ -674,9 +659,9 @@ Section gmultiset.
     ([∗ mset] x ∈ X, Φ x) ⊣⊢ ([∗ mset] x ∈ X, Ψ x).
   Proof. apply: big_opMS_proper. Qed.
 
-  Global Instance big_sepMS_mono' X :
-     Proper (pointwise_relation _ (⊢) ==> (⊢)) (big_opMS (M:=uPredUR M) X).
-  Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
+  Global Instance big_sepMS_mono' :
+     Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opMS (M:=uPredUR M) (A:=A)).
+  Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_sepMS_empty Φ : ([∗ mset] x ∈ ∅, Φ x) ⊣⊢ True.
   Proof. by rewrite big_opMS_empty. Qed.

theories/base_logic/tactics.v

@@ -23,17 +23,16 @@ Module uPred_reflection. Section uPred_reflection.
     | ESep e1 e2 => flatten e1 ++ flatten e2
     end.
 
-  Notation eval_list Σ l := ([∗] ((λ n, from_option id True%I (Σ !! n)) <$> l))%I.
+  Notation eval_list Σ l := ([∗ list] n ∈ l, from_option id True (Σ !! n))%I.
+
   Lemma eval_flatten Σ e : eval Σ e ⊣⊢ eval_list Σ (flatten e).
   Proof.
     induction e as [| |e1 IH1 e2 IH2];
-      rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //. 
+      rewrite /= ?right_id ?big_sepL_app ?IH1 ?IH2 //.
   Qed.
   Lemma flatten_entails Σ e1 e2 :
     flatten e2 ⊆+ flatten e1 → eval Σ e1 ⊢ eval Σ e2.
-  Proof.
-    intros. rewrite !eval_flatten. by apply big_sep_submseteq, fmap_submseteq.
-  Qed.
+  Proof. intros. rewrite !eval_flatten. by apply big_sepL_submseteq. Qed.
   Lemma flatten_equiv Σ e1 e2 :
     flatten e2 ≡ₚ flatten e1 → eval Σ e1 ⊣⊢ eval Σ e2.
   Proof. intros He. by rewrite !eval_flatten He. Qed.
@@ -90,7 +89,7 @@ Module uPred_reflection. Section uPred_reflection.
   Proof.
     intros ??. rewrite !eval_flatten.
     rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
-    rewrite !fmap_app !big_sep_app. apply sep_mono_r.
+    rewrite !big_sepL_app. apply sep_mono_r.
   Qed.
 
   Fixpoint to_expr (l : list nat) : expr :=
@@ -110,7 +109,7 @@ Module uPred_reflection. Section uPred_reflection.
     cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ (to_expr ns) ∗ eval Σ e').
   Proof.
     intros He%flatten_cancel.
-    by rewrite eval_flatten He fmap_app big_sep_app eval_to_expr eval_flatten.
+    by rewrite eval_flatten He big_sepL_app eval_to_expr eval_flatten.
   Qed.
   Lemma split_r Σ e ns e' :
     cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ e' ∗ eval Σ (to_expr ns)).

theories/heap_lang/lifting.v

@@ -76,7 +76,7 @@ Lemma wp_fork E e Φ :
   ▷ Φ (LitV LitUnit) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
 Proof.
   rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
-  - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton.
+  - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ (Lit _)) // right_id.
   - intros; inv_head_step; eauto.
 Qed.
 

theories/proofmode/class_instances.v

@@ -354,7 +354,7 @@ Proof. intros. by rewrite /FromAnd big_opL_cons always_and_sep_l. Qed.
 Global Instance from_and_big_sepL_app {A} (Φ : nat → A → uPred M) l1 l2 :
   FromAnd false ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
-Proof. by rewrite /FromAnd big_sepL_app. Qed.
+Proof. by rewrite /FromAnd big_opL_app. Qed.
 Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M) l1 l2 :
   (∀ k y, PersistentP (Φ k y)) →
   FromAnd true ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)

theories/proofmode/coq_tactics.v

@@ -234,14 +234,14 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
     + rewrite (env_app_perm _ _ Γp') //.
-      rewrite big_sep_app always_sep. solve_sep_entails.
+      rewrite big_sepL_app always_sep. solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using env_app_wf.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
-    + rewrite (env_app_perm _ _ Γs') // big_sep_app. solve_sep_entails.
+    + rewrite (env_app_perm _ _ Γs') // big_sepL_app. solve_sep_entails.
 Qed.
 
 Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
@@ -257,14 +257,14 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
     + rewrite (env_replace_perm _ _ Γp') //.
-      rewrite big_sep_app always_sep. solve_sep_entails.
+      rewrite big_sepL_app always_sep. solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
-    + rewrite (env_replace_perm _ _ Γs') // big_sep_app. solve_sep_entails.
+    + rewrite (env_replace_perm _ _ Γs') // big_sepL_app. solve_sep_entails.
 Qed.
 
 Lemma envs_simple_replace_sound Δ Δ' i p P Γ :