Commit 834c66e0 by Robbert Krebbers

### Extensionality (for Leibniz equality) of big ops.

parent c3c31e88
 ... @@ -138,6 +138,10 @@ Section list. ... @@ -138,6 +138,10 @@ Section list. (∀ k y, l !! k = Some y → f k y ≼ g k y) → (∀ 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. ([⋅ list] k ↦ y ∈ l, f k y) ≼ [⋅ list] k ↦ y ∈ l, g k y. Proof. apply big_opL_forall; apply _. Qed. 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 : Lemma big_opL_proper f g l : (∀ k y, l !! k = Some y → f k y ≡ g k y) → (∀ 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). ([⋅ list] k ↦ y ∈ l, f k y) ≡ ([⋅ list] k ↦ y ∈ l, g k y). ... @@ -207,6 +211,10 @@ Section gmap. ... @@ -207,6 +211,10 @@ Section gmap. - by apply big_op_contains, fmap_contains, map_to_list_contains. - by apply big_op_contains, fmap_contains, map_to_list_contains. - apply big_opM_forall; apply _ || auto. - apply big_opM_forall; apply _ || auto. Qed. 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 : Lemma big_opM_proper f g m : (∀ k x, m !! k = Some x → f k x ≡ g k x) → (∀ 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). ([⋅ map] k ↦ x ∈ m, f k x) ≡ ([⋅ map] k ↦ x ∈ m, g k x). ... @@ -314,14 +322,14 @@ Section gset. ... @@ -314,14 +322,14 @@ Section gset. - by apply big_op_contains, fmap_contains, elements_contains. - by apply big_op_contains, fmap_contains, elements_contains. - apply big_opS_forall; apply _ || auto. - apply big_opS_forall; apply _ || auto. Qed. Qed. Lemma big_opS_proper f g X Y : Lemma big_opS_ext f g X : X ≡ Y → (∀ x, x ∈ X → x ∈ Y → f x ≡ g x) → (∀ x, x ∈ X → f x = g x) → ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ Y, g x). ([⋅ set] x ∈ X, f x) = ([⋅ set] x ∈ X, g x). Proof. Proof. apply big_opS_forall; apply _. Qed. intros HX Hf. trans ([⋅ set] x ∈ Y, f x). Lemma big_opS_proper f g X : - apply big_op_permutation. by rewrite HX. (∀ x, x ∈ X → f x ≡ g x) → - apply big_opS_forall; try apply _ || set_solver. ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, g x). Qed. Proof. apply big_opS_forall; apply _. Qed. Lemma big_opS_ne X n : Lemma big_opS_ne X n : Proper (pointwise_relation _ (dist n) ==> dist n) (big_opS (M:=M) X). Proper (pointwise_relation _ (dist n) ==> dist n) (big_opS (M:=M) X). ... @@ -345,7 +353,7 @@ Section gset. ... @@ -345,7 +353,7 @@ Section gset. ≡ (f x b ⋅ [⋅ set] y ∈ X, f y (h y)). ≡ (f x b ⋅ [⋅ set] y ∈ X, f y (h y)). Proof. Proof. intros. rewrite big_opS_insert // fn_lookup_insert. 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. by rewrite fn_lookup_insert_ne; last set_solver. Qed. Qed. Lemma big_opS_fn_insert' f X x P : Lemma big_opS_fn_insert' f X x P : ... ...
 ... @@ -125,7 +125,6 @@ Section list. ... @@ -125,7 +125,6 @@ Section list. (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) → (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) → ([★ list] k ↦ y ∈ l, Φ k y) ⊢ [★ list] k ↦ y ∈ l, Ψ k y. ([★ list] k ↦ y ∈ l, Φ k y) ⊢ [★ list] k ↦ y ∈ l, Ψ k y. Proof. apply big_opL_forall; apply _. Qed. Proof. apply big_opL_forall; apply _. Qed. Lemma big_sepL_proper Φ Ψ l : Lemma big_sepL_proper Φ Ψ l : (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) → (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) → ([★ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([★ list] k ↦ y ∈ l, Ψ k y). ([★ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([★ list] k ↦ y ∈ l, Ψ k y). ... @@ -219,7 +218,6 @@ Section gmap. ... @@ -219,7 +218,6 @@ Section gmap. by apply fmap_contains, map_to_list_contains. by apply fmap_contains, map_to_list_contains. - apply big_opM_forall; apply _ || auto. - apply big_opM_forall; apply _ || auto. Qed. Qed. Lemma big_sepM_proper Φ Ψ m : Lemma big_sepM_proper Φ Ψ m : (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) → (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) → ([★ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m, Ψ k x). ([★ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m, Ψ k x). ... @@ -344,16 +342,15 @@ Section gset. ... @@ -344,16 +342,15 @@ Section gset. by apply fmap_contains, elements_contains. by apply fmap_contains, elements_contains. - apply big_opS_forall; apply _ || auto. - apply big_opS_forall; apply _ || auto. Qed. 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). Proper (pointwise_relation _ (⊢) ==> (⊢)) (big_opS (M:=uPredUR M) X). Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed. 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. Lemma big_sepS_empty Φ : ([★ set] x ∈ ∅, Φ x) ⊣⊢ True. Proof. by rewrite big_opS_empty. Qed. Proof. by rewrite big_opS_empty. Qed. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!