Commit 481c49d6 by Dmitry Khalanskiy

### Make `big_op{L,M}_gen_proper_2` stronger

```The existing versions did not allow the two structures to be over
different types.```
parent 446bc644
 ... ... @@ -101,7 +101,8 @@ Section list. Lemma big_opL_unit l : ([^o list] k↦y ∈ l, monoid_unit) ≡ (monoid_unit : M). Proof. induction l; rewrite /= ?left_id //. Qed. Lemma big_opL_gen_proper_2 (R : relation M) f g l1 l2 : Lemma big_opL_gen_proper_2 {B} (R : relation M) f (g : nat → B → M) l1 (l2 : list B) : R monoid_unit monoid_unit → Proper (R ==> R ==> R) o → (∀ k, ... ... @@ -207,28 +208,31 @@ Proof. Qed. (** ** Big ops over finite maps *) Lemma big_opM_empty `{Countable K} {B} (f : K → B → M) : ([^o map] k↦x ∈ ∅, f k x) = monoid_unit. Proof. by rewrite big_opM_eq /big_opM_def map_to_list_empty. Qed. Lemma big_opM_insert `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x : m !! i = None → ([^o map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ m, f k y. Proof. intros ?. by rewrite big_opM_eq /big_opM_def map_to_list_insert. Qed. Lemma big_opM_delete `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x : m !! i = Some x → ([^o map] k↦y ∈ m, f k y) ≡ f i x `o` [^o map] k↦y ∈ delete i m, f k y. Proof. intros. rewrite -big_opM_insert ?lookup_delete //. by rewrite insert_delete insert_id. Qed. Section gmap. Context `{Countable K} {A : Type}. Implicit Types m : gmap K A. Implicit Types f g : K → A → M. Lemma big_opM_empty f : ([^o map] k↦x ∈ ∅, f k x) = monoid_unit. Proof. by rewrite big_opM_eq /big_opM_def map_to_list_empty. Qed. Lemma big_opM_insert f m i x : m !! i = None → ([^o map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ m, f k y. Proof. intros ?. by rewrite big_opM_eq /big_opM_def map_to_list_insert. Qed. Lemma big_opM_delete f m i x : m !! i = Some x → ([^o map] k↦y ∈ m, f k y) ≡ f i x `o` [^o map] k↦y ∈ delete i m, f k y. Proof. intros. rewrite -big_opM_insert ?lookup_delete //. by rewrite insert_delete insert_id. Qed. Lemma big_opM_gen_proper_2 (R : relation M) f g m1 m2 : Lemma big_opM_gen_proper_2 {B} (R : relation M) f (g : K → B → M) m1 (m2 : gmap K B) : subrelation (≡) R → Equivalence R → Proper (R ==> R ==> R) o → (∀ k, ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!