diff --git a/opam.pins b/opam.pins index ee2d15f4df23e9a795c02d8d0eea4c6754bacab2..1b5b31d49c1a5dd9680f0cb3a987a575274a1196 100644 --- a/opam.pins +++ b/opam.pins @@ -1 +1 @@ -coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 0ac2b4db07bdc471421c5a4c47789087b3df074c +coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp a0ce0937cfabe16a184af2d92c0466ebacecbca2 diff --git a/theories/algebra/cmra_big_op.v b/theories/algebra/cmra_big_op.v index 206c3ac11af52b5e14249109239c8c3d5dd59884..9fba43e70b02ae2e6a11de157fe36aa7064a71b2 100644 --- a/theories/algebra/cmra_big_op.v +++ b/theories/algebra/cmra_big_op.v @@ -18,50 +18,46 @@ 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. -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). +Fixpoint big_opL {M : ucmraT} {A} (f : nat → A → M) (xs : list A) : M := + match xs with + | [] => ∅ + | x :: xs => f 0 x ⋅ big_opL (λ n, f (S n)) xs + end. Instance: Params (@big_opL) 2. -Typeclasses Opaque big_opL. -Notation "'[⋅' 'list' ] k ↦ x ∈ l , P" := (big_opL l (λ k x, P)) +Arguments big_opL _ _ _ !_ /. +Notation "'[⋅' 'list' ] k ↦ x ∈ l , P" := (big_opL (λ k x, P) l) (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)) +Notation "'[⋅' 'list' ] x ∈ l , P" := (big_opL (λ _ x, P) l) (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). +Notation "'[⋅]' xs" := (big_opL (λ _ x, x) xs) (at level 20) : C_scope. + +Definition big_opM {M : ucmraT} `{Countable K} {A} (f : K → A → M) + (m : gmap K A) : M := big_opL (λ _, 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)) +Notation "'[⋅' 'map' ] k ↦ x ∈ m , P" := (big_opM (λ k x, P) m) (at level 200, m at level 10, k, x at level 1, right associativity, format "[⋅ map ] k ↦ x ∈ m , P") : C_scope. -Notation "'[⋅' 'map' ] x ∈ m , P" := (big_opM m (λ _ x, P)) +Notation "'[⋅' 'map' ] x ∈ m , P" := (big_opM (λ _ x, P) m) (at level 200, m at level 10, x at level 1, right associativity, format "[⋅ map ] x ∈ m , P") : C_scope. -Definition big_opS {M : ucmraT} `{Countable A} - (X : gset A) (f : A → M) : M := [⋅] (f <\$> elements X). +Definition big_opS {M : ucmraT} `{Countable A} (f : A → M) + (X : gset A) : M := big_opL (λ _, f) (elements X). Instance: Params (@big_opS) 5. Typeclasses Opaque big_opS. -Notation "'[⋅' 'set' ] x ∈ X , P" := (big_opS X (λ x, P)) +Notation "'[⋅' 'set' ] x ∈ X , P" := (big_opS (λ x, P) X) (at level 200, X at level 10, x at level 1, right associativity, format "[⋅ set ] x ∈ X , P") : C_scope. -Definition big_opMS {M : ucmraT} `{Countable A} - (X : gmultiset A) (f : A → M) : M := [⋅] (f <\$> elements X). +Definition big_opMS {M : ucmraT} `{Countable A} (f : A → M) + (X : gmultiset A) : M := big_opL (λ _, f) (elements X). Instance: Params (@big_opMS) 5. Typeclasses Opaque big_opMS. -Notation "'[⋅' 'mset' ] x ∈ X , P" := (big_opMS X (λ x, P)) +Notation "'[⋅' 'mset' ] x ∈ X , P" := (big_opMS (λ x, P) X) (at level 200, X at level 10, x at level 1, right associativity, format "[⋅ 'mset' ] x ∈ X , P") : C_scope. @@ -70,52 +66,6 @@ Section big_op. Context {M : ucmraT}. Implicit Types xs : list M. -(** * Big ops *) -Lemma big_op_Forall2 R : - Reflexive R → Proper (R ==> R ==> R) (@op M _) → - Proper (Forall2 R ==> R) (@big_op M). -Proof. rewrite /Proper /respectful. induction 3; eauto. Qed. - -Global Instance big_op_ne : NonExpansive (@big_op M). -Proof. intros ?. apply big_op_Forall2; apply _. 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 : [⋅] (x :: xs) = x ⋅ [⋅] xs. -Proof. done. Qed. -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. - -Lemma big_op_submseteq xs ys : xs ⊆+ ys → [⋅] xs ≼ [⋅] ys. -Proof. - intros [xs' ->]%submseteq_Permutation. - rewrite big_op_app; apply cmra_included_l. -Qed. - -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. - -Lemma big_sep_elem_of xs x : x ∈ xs → x ≼ [⋅] xs. -Proof. - intros [i ?]%elem_of_list_lookup. rewrite -big_op_delete //. - apply cmra_included_l. -Qed. - (** ** Big ops over lists *) Section list. Context {A : Type}. @@ -126,21 +76,24 @@ Section list. Proof. done. Qed. Lemma big_opL_cons f x l : ([⋅ list] k↦y ∈ x :: l, f k y) = f 0 x ⋅ [⋅ list] k↦y ∈ l, f (S k) y. - Proof. by rewrite /big_opL imap_cons. Qed. + Proof. done. Qed. Lemma big_opL_singleton f x : ([⋅ list] k↦y ∈ [x], f k y) ≡ f 0 x. - Proof. by rewrite big_opL_cons big_opL_nil right_id. Qed. + Proof. by rewrite /= right_id. Qed. Lemma big_opL_app f l1 l2 : ([⋅ list] k↦y ∈ l1 ++ l2, f k y) ≡ ([⋅ list] k↦y ∈ l1, f k y) ⋅ ([⋅ list] k↦y ∈ l2, f (length l1 + k) y). - Proof. by rewrite /big_opL imap_app big_op_app. Qed. + Proof. + revert f. induction l1 as [|x l1 IH]=> f /=; first by rewrite left_id. + by rewrite IH assoc. + Qed. Lemma big_opL_forall R f g l : - Reflexive R → Proper (R ==> R ==> R) (@op M _) → + Reflexive R → + Proper (R ==> R ==> R) (@op M _) → (∀ k y, l !! k = Some y → R (f k y) (g k y)) → R ([⋅ list] k ↦ y ∈ l, f k y) ([⋅ list] k ↦ y ∈ l, g k y). Proof. - intros ? Hop. revert f g. induction l as [|x l IH]=> f g Hf; [done|]. - rewrite !big_opL_cons. apply Hop; eauto. + intros ??. revert f g. induction l as [|x l IH]=> f g ? //=; f_equiv; eauto. Qed. Lemma big_opL_mono f g l : @@ -155,25 +108,38 @@ Section list. (∀ 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. apply big_opL_forall; apply _. Qed. + Lemma big_opL_permutation (f : A → M) l1 l2 : l1 ≡ₚ l2 → ([⋅ list] x ∈ l1, f x) ≡ ([⋅ list] x ∈ l2, f x). - Proof. intros Hl. by rewrite /big_opL !imap_const Hl. Qed. + Proof. + induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto. + - by rewrite IH. + - by rewrite !assoc (comm _ (f x)). + - by etrans. + Qed. + Global Instance big_op_permutation (f : A → M) : + Proper ((≡ₚ) ==> (≡)) (big_opL (λ _, f)). + Proof. intros xs1 xs2. apply big_opL_permutation. Qed. + Lemma big_opL_submseteq (f : A → M) l1 l2 : l1 ⊆+ l2 → ([⋅ list] x ∈ l1, f x) ≼ ([⋅ list] x ∈ l2, f x). - Proof. intros Hl. apply big_op_submseteq. rewrite !imap_const. by rewrite ->Hl. 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_opL_forall; apply _ || intros; apply Hf. Qed. - Global Instance big_opL_proper' l : - Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡)) - (big_opL (M:=M) l). - Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed. - Global Instance big_opL_mono' l : - Proper (pointwise_relation _ (pointwise_relation _ (≼)) ==> (≼)) - (big_opL (M:=M) l). - Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed. + Proof. + intros [xs' ->]%submseteq_Permutation. + rewrite big_opL_app; apply cmra_included_l. + Qed. + + Global Instance big_opL_ne n : + Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> + eq ==> dist n) (big_opL (M:=M) (A:=A)). + Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed. + Global Instance big_opL_proper' : + Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> eq ==> (≡)) + (big_opL (M:=M) (A:=A)). + Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed. + Global Instance big_opL_mono' : + Proper (pointwise_relation _ (pointwise_relation _ (≼)) ==> eq ==> (≼)) + (big_opL (M:=M) (A:=A)). + Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed. Lemma big_opL_consZ_l (f : Z → A → M) x l : ([⋅ list] k↦y ∈ x :: l, f k y) = f 0 x ⋅ [⋅ list] k↦y ∈ l, f (1 + k)%Z y. @@ -197,16 +163,14 @@ Section list. Lemma big_opL_fmap {B} (h : A → B) (f : nat → B → M) l : ([⋅ list] k↦y ∈ h <\$> l, f k y) ≡ ([⋅ list] k↦y ∈ l, f k (h y)). - Proof. by rewrite /big_opL imap_fmap. Qed. + Proof. revert f. induction l as [|x l IH]=> f; csimpl=> //. by rewrite IH. Qed. Lemma big_opL_opL f g l : ([⋅ list] k↦x ∈ l, f k x ⋅ g k x) ≡ ([⋅ list] k↦x ∈ l, f k x) ⋅ ([⋅ list] k↦x ∈ 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. + revert f g; induction l as [|x l IH]=> f g /=; first by rewrite left_id. + by rewrite IH -!assoc (assoc _ (g _ _)) [(g _ _ ⋅ _)]comm -!assoc. Qed. End list. @@ -221,8 +185,8 @@ Section gmap. (∀ k x, m !! k = Some x → R (f k x) (g k x)) → R ([⋅ map] k ↦ x ∈ m, f k x) ([⋅ map] k ↦ x ∈ m, g k x). Proof. - intros ?? Hf. apply (big_op_Forall2 R _ _), Forall2_fmap, Forall_Forall2. - apply Forall_forall=> -[i x] ? /=. by apply Hf, elem_of_map_to_list. + intros ?? Hf. apply (big_opL_forall R); auto. + intros k [i x] ?%elem_of_list_lookup_2. by apply Hf, elem_of_map_to_list. Qed. Lemma big_opM_mono f g m1 m2 : @@ -230,7 +194,7 @@ Section gmap. ([⋅ map] k ↦ x ∈ m1, f k x) ≼ [⋅ map] k ↦ x ∈ m2, g k x. Proof. intros Hm Hf. trans ([⋅ map] k↦x ∈ m2, f k x). - - by apply big_op_submseteq, fmap_submseteq, map_to_list_submseteq. + - by apply big_opL_submseteq, map_to_list_submseteq. - apply big_opM_forall; apply _ || auto. Qed. Lemma big_opM_ext f g m : @@ -242,18 +206,18 @@ Section gmap. ([⋅ map] k ↦ x ∈ m, f k x) ≡ ([⋅ map] k ↦ x ∈ m, g k x). Proof. apply big_opM_forall; apply _. Qed. - Global Instance big_opM_ne m n : - Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n)) - (big_opM (M:=M) m). - Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed. - Global Instance big_opM_proper' m : - Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡)) - (big_opM (M:=M) m). - Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed. - Global Instance big_opM_mono' m : - Proper (pointwise_relation _ (pointwise_relation _ (≼)) ==> (≼)) - (big_opM (M:=M) m). - Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed. + Global Instance big_opM_ne n : + Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> eq ==> dist n) + (big_opM (M:=M) (A:=A)). + Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed. + Global Instance big_opM_proper' : + Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> eq ==> (≡)) + (big_opM (M:=M) (A:=A)). + Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed. + Global Instance big_opM_mono' : + Proper (pointwise_relation _ (pointwise_relation _ (≼)) ==> eq ==> (≼)) + (big_opM (M:=M) (A:=A)). + Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed. Lemma big_opM_empty f : ([⋅ map] k↦x ∈ ∅, f k x) = ∅. Proof. by rewrite /big_opM map_to_list_empty. Qed. @@ -287,8 +251,8 @@ Section gmap. Lemma big_opM_fmap {B} (h : A → B) (f : K → B → M) m : ([⋅ map] k↦y ∈ h <\$> m, f k y) ≡ ([⋅ map] k↦y ∈ 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. + rewrite /big_opM map_to_list_fmap big_opL_fmap. + by apply big_opL_proper=> ? [??]. Qed. Lemma big_opM_insert_override (f : K → A → M) m i x x' : @@ -316,12 +280,7 @@ Section gmap. Lemma big_opM_opM f g m : ([⋅ map] k↦x ∈ m, f k x ⋅ g k x) ≡ ([⋅ map] k↦x ∈ m, f k x) ⋅ ([⋅ map] k↦x ∈ m, g k x). - Proof. - induction m as [|i x ?? IH] using map_ind. - { by rewrite !big_opM_empty left_id. } - rewrite !big_opM_insert // IH. - by rewrite -!assoc (assoc _ (g _ _)) [(g _ _ ⋅ _)]comm -!assoc. - Qed. + Proof. rewrite /big_opM -big_opL_opL. by apply big_opL_proper=> ? [??]. Qed. End gmap. @@ -336,8 +295,8 @@ Section gset. (∀ x, x ∈ X → R (f x) (g x)) → R ([⋅ set] x ∈ X, f x) ([⋅ set] x ∈ X, g x). Proof. - intros ?? Hf. apply (big_op_Forall2 R _ _), Forall2_fmap, Forall_Forall2. - apply Forall_forall=> x ? /=. by apply Hf, elem_of_elements. + intros ?? Hf. apply (big_opL_forall R); auto. + intros k x ?%elem_of_list_lookup_2. by apply Hf, elem_of_elements. Qed. Lemma big_opS_mono f g X Y : @@ -345,7 +304,7 @@ Section gset. ([⋅ set] x ∈ X, f x) ≼ [⋅ set] x ∈ Y, g x. Proof. intros HX Hf. trans ([⋅ set] x ∈ Y, f x). - - by apply big_op_submseteq, fmap_submseteq, elements_submseteq. + - by apply big_opL_submseteq, elements_submseteq. - apply big_opS_forall; apply _ || auto. Qed. Lemma big_opS_ext f g X : @@ -357,15 +316,15 @@ Section gset. ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, g x). Proof. apply big_opS_forall; apply _. Qed. - Global Instance big_opS_ne X n : - Proper (pointwise_relation _ (dist n) ==> dist n) (big_opS (M:=M) X). - Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed. - Global Instance big_opS_proper' X : - Proper (pointwise_relation _ (≡) ==> (≡)) (big_opS (M:=M) X). - Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed. - Global Instance big_opS_mono' X : - Proper (pointwise_relation _ (≼) ==> (≼)) (big_opS (M:=M) X). - Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed. + Global Instance big_opS_ne n : + Proper (pointwise_relation _ (dist n) ==> eq ==> dist n) (big_opS (M:=M) (A:=A)). + Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed. + Global Instance big_opS_proper' : + Proper (pointwise_relation _ (≡) ==> eq ==> (≡)) (big_opS (M:=M) (A:=A)). + Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed. + Global Instance big_opS_mono' : + Proper (pointwise_relation _ (≼) ==> eq ==> (≼)) (big_opS (M:=M) (A:=A)). + Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed. Lemma big_opS_empty f : ([⋅ set] x ∈ ∅, f x) = ∅. Proof. by rewrite /big_opS elements_empty. Qed. @@ -411,12 +370,7 @@ Section gset. 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. - induction X as [|x X ? IH] using collection_ind_L. - { by rewrite !big_opS_empty left_id. } - rewrite !big_opS_insert // IH. - by rewrite -!assoc (assoc _ (g _)) [(g _ ⋅ _)]comm -!assoc. - Qed. + Proof. by rewrite /big_opS -big_opL_opL. Qed. End gset. Lemma big_opM_dom `{Countable K} {A} (f : K → M) (m : gmap K A) : @@ -437,8 +391,8 @@ Section gmultiset. (∀ x, x ∈ X → R (f x) (g x)) → R ([⋅ mset] x ∈ X, f x) ([⋅ mset] x ∈ X, g x). Proof. - intros ?? Hf. apply (big_op_Forall2 R _ _), Forall2_fmap, Forall_Forall2. - apply Forall_forall=> x ? /=. by apply Hf, gmultiset_elem_of_elements. + intros ?? Hf. apply (big_opL_forall R); auto. + intros k x ?%elem_of_list_lookup_2. by apply Hf, gmultiset_elem_of_elements. Qed. Lemma big_opMS_mono f g X Y : @@ -446,7 +400,7 @@ Section gmultiset. ([⋅ mset] x ∈ X, f x) ≼ [⋅ mset] x ∈ Y, g x. Proof. intros HX Hf. trans ([⋅ mset] x ∈ Y, f x). - - by apply big_op_submseteq, fmap_submseteq, gmultiset_elements_submseteq. + - by apply big_opL_submseteq, gmultiset_elements_submseteq. - apply big_opMS_forall; apply _ || auto. Qed. Lemma big_opMS_ext f g X : @@ -458,22 +412,22 @@ Section gmultiset. ([⋅ mset] x ∈ X, f x) ≡ ([⋅ mset] x ∈ X, g x). Proof. apply big_opMS_forall; apply _. Qed. - Global Instance big_opMS_ne X n : - Proper (pointwise_relation _ (dist n) ==> dist n) (big_opMS (M:=M) X). - Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed. - Global Instance big_opMS_proper' X : - Proper (pointwise_relation _ (≡) ==> (≡)) (big_opMS (M:=M) X). - Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed. - Global Instance big_opMS_mono' X : - Proper (pointwise_relation _ (≼) ==> (≼)) (big_opMS (M:=M) X). - Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed. + Global Instance big_opMS_ne n : + Proper (pointwise_relation _ (dist n) ==> eq ==> dist n) (big_opMS (M:=M) (A:=A)). + Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed. + Global Instance big_opMS_proper' : + Proper (pointwise_relation _ (≡) ==> eq ==> (≡)) (big_opMS (M:=M) (A:=A)). + Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed. + Global Instance big_opMS_mono' : + Proper (pointwise_relation _ (≼) ==> eq ==> (≼)) (big_opMS (M:=M) (A:=A)). + Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed. Lemma big_opMS_empty f : ([⋅ mset] x ∈ ∅, f x) = ∅. Proof. by rewrite /big_opMS gmultiset_elements_empty. Qed. Lemma big_opMS_union f X Y : ([⋅ mset] y ∈ X ∪ Y, f y) ≡ ([⋅ mset] y ∈ X, f y) ⋅ [⋅ mset] y ∈ Y, f y. - Proof. by rewrite /big_opMS gmultiset_elements_union fmap_app big_op_app. Qed. + Proof. by rewrite /big_opMS gmultiset_elements_union big_opL_app. Qed. Lemma big_opMS_singleton f x : ([⋅ mset] y ∈ {[ x ]}, f y) ≡ f x. Proof. @@ -492,12 +446,7 @@ Section gmultiset. Lemma big_opMS_opMS f g X : ([⋅ mset] y ∈ X, f y ⋅ g y) ≡ ([⋅ mset] y ∈ X, f y) ⋅ ([⋅ mset] y ∈ X, g y). - Proof. - induction X as [|x X IH] using gmultiset_ind. - { by rewrite !big_opMS_empty left_id. } - rewrite !big_opMS_union !big_opMS_singleton IH. - by rewrite -!assoc (assoc _ (g _)) [(g _ ⋅ _)]comm -!assoc. - Qed. + Proof. by rewrite /big_opMS -big_opL_opL. Qed. End gmultiset. End big_op. @@ -505,8 +454,7 @@ End big_op. Lemma big_opL_None {M : cmraT} {A} (f : nat → A → option M) l : ([⋅ list] k↦x ∈ l, f k x) = None ↔ ∀ k x, l !! k = Some x → f k x = None. Proof. - revert f. induction l as [|x l IH]=> f //=. - rewrite big_opL_cons op_None IH. split. + revert f. induction l as [|x l IH]=> f //=. rewrite op_None IH. split. - intros [??] [|k] y ?; naive_solver. - intros Hl. split. by apply (Hl 0). intros k. apply (Hl (S k)). Qed. @@ -540,9 +488,9 @@ Lemma big_opL_commute {M1 M2 : ucmraT} {A} (h : M1 → M2) `{!UCMRAHomomorphism h} (f : nat → A → M1) l : h ([⋅ list] k↦x ∈ l, f k x) ≡ ([⋅ list] k↦x ∈ l, h (f k x)). Proof. - revert f. induction l as [|x l IH]=> f. - - by rewrite !big_opL_nil ucmra_homomorphism_unit. - - by rewrite !big_opL_cons cmra_homomorphism -IH. + revert f. induction l as [|x l IH]=> f /=. + - by rewrite ucmra_homomorphism_unit. + - by rewrite cmra_homomorphism -IH. Qed. Lemma big_opL_commute1 {M1 M2 : ucmraT} {A} (h : M1 → M2) `{!CMRAHomomorphism h} (f : nat → A → M1) l : diff --git a/theories/algebra/cmra_tactics.v b/theories/algebra/cmra_tactics.v index a0d123cc4bc092d54c0248e3a134f7bb56322022..b94b625ad12c646e5a600a12b219bc4dcd70e0d7 100644 --- a/theories/algebra/cmra_tactics.v +++ b/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) := {}. diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v index 8dfa1f9830478f02324404cc9e89a6633cc938da..4259b5f11b6490e5bb5575e0390e02874a4ce26b 100644 --- a/theories/base_logic/big_op.v +++ b/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. diff --git a/theories/base_logic/tactics.v b/theories/base_logic/tactics.v index 0a75c4fb55477da496025bcbe936d97f0116f86d..5452b59979b7f8656b963e3333f8a7d62cc4ff9f 100644 --- a/theories/base_logic/tactics.v +++ b/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)). diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v index 9de570086bb2cd94928159d888e15650f54e0067..7368ecf3d581934b9e659bad700133de90a4aae0 100644 --- a/theories/heap_lang/lifting.v +++ b/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. diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v index a4829ce47f905c49c3797bc03aa44f0be6124bed..310281cf127cb13b93c6f51475711765c2443451 100644 --- a/theories/proofmode/class_instances.v +++ b/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) diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v index 29272ebc49ced480907431fe2e918b16ca289f68..9a17276982d479ad80ecaf9484158bfb8bff8d74 100644 --- a/theories/proofmode/coq_tactics.v +++ b/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 Γ :