Commit 87abb52a by Jacques-Henri Jourdan

Lemmas about Big ops and contains.

parent 2407263c
 ... @@ -157,6 +157,9 @@ Section list. ... @@ -157,6 +157,9 @@ Section list. Lemma big_opL_permutation (f : A → M) l1 l2 : Lemma big_opL_permutation (f : A → M) l1 l2 : l1 ≡ₚ l2 → ([⋅ list] x ∈ l1, f x) ≡ ([⋅ list] x ∈ l2, f x). l1 ≡ₚ l2 → ([⋅ list] x ∈ l1, f x) ≡ ([⋅ list] x ∈ l2, f x). Proof. intros Hl. by rewrite /big_opL !imap_const Hl. Qed. Proof. intros Hl. by rewrite /big_opL !imap_const Hl. Qed. Lemma big_opL_contains (f : A → M) l1 l2 : l1 `contains` l2 → ([⋅ list] x ∈ l1, f x) ≼ ([⋅ list] x ∈ l2, f x). Proof. intros Hl. apply big_op_contains. rewrite !imap_const. by rewrite ->Hl. Qed. Global Instance big_opL_ne l n : Global Instance big_opL_ne l n : Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n)) Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n)) ... ...
 ... @@ -219,6 +219,9 @@ Section list. ... @@ -219,6 +219,9 @@ 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_proper. Qed. Proof. apply big_opL_proper. Qed. Lemma big_sepL_contains (Φ : A → uPred M) l1 l2 : l1 `contains` l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y. Proof. intros ?. apply uPred_included. by apply: big_opL_contains. Qed. Global Instance big_sepL_mono' l : Global Instance big_sepL_mono' l : Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢)) Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢)) ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!