diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v index 7bc069d253359aa4998aaa2a69aaeed063c9c0fe..6fe6cda19dbd0d5843521b754b9800900c3a29f8 100644 --- a/algebra/cmra_big_op.v +++ b/algebra/cmra_big_op.v @@ -138,6 +138,10 @@ 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_ext f g l : + (∀ 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_proper f g l : (∀ 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). @@ -207,6 +211,10 @@ Section gmap. - by apply big_op_contains, fmap_contains, map_to_list_contains. - apply big_opM_forall; apply _ || auto. Qed. + Lemma big_opM_ext f g m : + (∀ k x, m !! k = Some x → f k x = g k x) → + ([⋅ map] k ↦ x ∈ m, f k x) = ([⋅ map] k ↦ x ∈ m, g k x). + Proof. apply big_opM_forall; apply _. Qed. Lemma big_opM_proper f g m : (∀ k x, m !! k = Some x → f k x ≡ g k x) → ([⋅ map] k ↦ x ∈ m, f k x) ≡ ([⋅ map] k ↦ x ∈ m, g k x). @@ -314,14 +322,14 @@ Section gset. - by apply big_op_contains, fmap_contains, elements_contains. - apply big_opS_forall; apply _ || auto. Qed. - Lemma big_opS_proper f g X Y : - X ≡ Y → (∀ x, x ∈ X → x ∈ Y → f x ≡ g x) → - ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ Y, g x). - Proof. - intros HX Hf. trans ([⋅ set] x ∈ Y, f x). - - apply big_op_permutation. by rewrite HX. - - apply big_opS_forall; try apply _ || set_solver. - Qed. + Lemma big_opS_ext f g X : + (∀ x, x ∈ X → f x = g x) → + ([⋅ set] x ∈ X, f x) = ([⋅ set] x ∈ X, g x). + Proof. apply big_opS_forall; apply _. Qed. + Lemma big_opS_proper f g X : + (∀ x, x ∈ X → f x ≡ g x) → + ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, g x). + Proof. apply big_opS_forall; apply _. Qed. Lemma big_opS_ne X n : Proper (pointwise_relation _ (dist n) ==> dist n) (big_opS (M:=M) X). @@ -345,7 +353,7 @@ Section gset. ≡ (f x b ⋅ [⋅ set] y ∈ X, f y (h y)). Proof. intros. rewrite big_opS_insert // fn_lookup_insert. - apply cmra_op_proper', big_opS_proper; auto=> y ??. + apply cmra_op_proper', big_opS_proper; auto=> y ?. by rewrite fn_lookup_insert_ne; last set_solver. Qed. Lemma big_opS_fn_insert' f X x P : diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v index 8571558e88d5aa2799500a300bb1e27f53d023fd..9f2dded3d0acaa94988f20e10d4ed090ecbe2a2c 100644 --- a/algebra/upred_big_op.v +++ b/algebra/upred_big_op.v @@ -125,7 +125,6 @@ Section list. (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) → ([★ list] k ↦ y ∈ l, Φ k y) ⊢ [★ list] k ↦ y ∈ l, Ψ k y. Proof. apply big_opL_forall; apply _. Qed. - Lemma big_sepL_proper Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) → ([★ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([★ list] k ↦ y ∈ l, Ψ k y). @@ -219,7 +218,6 @@ Section gmap. by apply fmap_contains, map_to_list_contains. - apply big_opM_forall; apply _ || auto. Qed. - 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). @@ -344,16 +342,15 @@ Section gset. by apply fmap_contains, elements_contains. - apply big_opS_forall; apply _ || auto. Qed. + Lemma big_sepS_proper Φ Ψ X : + (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) → + ([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ X, Ψ x). + Proof. apply: big_opS_proper. Qed. - Lemma big_sepS_mono' X : + 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. - Lemma big_sepS_proper Φ Ψ X Y : - X ≡ Y → (∀ x, x ∈ X → x ∈ Y → Φ x ⊣⊢ Ψ x) → - ([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ Y, Ψ x). - Proof. apply: big_opS_proper. Qed. - Lemma big_sepS_empty Φ : ([★ set] x ∈ ∅, Φ x) ⊣⊢ True. Proof. by rewrite big_opS_empty. Qed.