diff --git a/theories/fin_sets.v b/theories/fin_sets.v index 19a114cddfb3560297663f53e09c78fb11e52c10..43a4d66aa8987056bfc0c083c67042046216e38b 100644 --- a/theories/fin_sets.v +++ b/theories/fin_sets.v @@ -29,11 +29,10 @@ Global Instance: Params (@set_map) 8 := {}. Definition set_map_2 `{Elements A SA, Elements B SB, Singleton C SC, Empty SC, Union SC} (f : A → B → C) (X : SA) (Y : SB) : SC := - list_to_set (list_ap (f <$> elements X) (elements Y)). + list_to_set (x ↠elements X; y ↠elements Y; [f x y]). Typeclasses Opaque set_map_2. Global Instance: Params (@set_map_2) 12 := {}. - Global Instance set_fresh `{Elements A C, Fresh A (list A)} : Fresh A C := fresh ∘ elements. Typeclasses Opaque set_fresh. @@ -561,78 +560,61 @@ End fin_set. (* Properties of [set_map_2] *) Section map2. - Context `{FinSet A C}. - Context `{FinSet B D}. - Context `{Set_ K E}. - - Lemma elem_of_set_map_2 (f : A → B → K) (X : C) (Y : D) (z : K) : - z ∈ set_map_2 (SC:=E) f X Y ↔ ∃ x y, z = f x y ∧ x ∈ X ∧ y ∈ Y. - Proof. - unfold set_map_2, list_ap. - rewrite elem_of_list_to_set. - rewrite list_fmap_bind. - rewrite elem_of_list_bind. set_unfold. - firstorder. - Qed. - Global Instance set_unfold_map_2 (f : A → B → K) (X : C) (Y : D) (P : A → Prop) (Q : B → Prop) z : - (∀ x, SetUnfoldElemOf x X (P x)) → - (∀ y, SetUnfoldElemOf y Y (Q y)) → - SetUnfoldElemOf z (set_map_2 (SC:=E) f X Y) (∃ x y, z = f x y ∧ P x ∧ Q y). + Context `{FinSet A SA, FinSet B SB, Set_ C SC}. + Local Notation set_map_2 := (set_map_2 (SA:=SA) (SB:=SB) (SC:=SC)). + Implicit Types X : SA. + Implicit Types Y : SB. + + Lemma elem_of_set_map_2 (f : A → B → C) X Y z : + z ∈ set_map_2 f X Y ↔ ∃ x y, z = f x y ∧ x ∈ X ∧ y ∈ Y. + Proof. unfold set_map_2. set_solver. Qed. + Global Instance set_unfold_map_2 (f : A → B → C) X Y + (P : A → Prop) (Q : B → Prop) z : + (∀ x, SetUnfoldElemOf x X (P x)) → (∀ y, SetUnfoldElemOf y Y (Q y)) → + SetUnfoldElemOf z (set_map_2 f X Y) (∃ x y, z = f x y ∧ P x ∧ Q y). Proof. constructor. rewrite elem_of_set_map_2; naive_solver. Qed. Global Instance set_map_2_proper : - Proper (pointwise_relation _ (pointwise_relation _ (=)) ==> (≡) ==> (≡) ==> (≡)) (set_map_2 (SA:=C) (SB:=D) (SC:=E)). - Proof. intros f g Hfg X1 X2 HX Y1 Y2 HY. set_unfold. intros z. by repeat f_equiv. Qed. + Proper (pointwise_relation _ (pointwise_relation _ (=)) ==> (≡) ==> (≡) ==> (≡)) + set_map_2. + Proof. unfold pointwise_relation. repeat intro; set_solver. Qed. Global Instance set_map_2_mono : - Proper (pointwise_relation _ (pointwise_relation _ (=)) ==> (⊆) ==> (⊆) ==> (⊆)) (set_map_2 (SA:=C) (SB:=D) (SC:=E)). - Proof. - intros f g Hfg X1 X2 HX Y1 Y2 HY. set_unfold. - intros z. intros [x [y [-> [Hx Hy]]]]. - exists x, y. split; eauto. - apply Hfg. - Qed. + Proper (pointwise_relation _ (pointwise_relation _ (=)) ==> (⊆) ==> (⊆) ==> (⊆)) + set_map_2. + Proof. unfold pointwise_relation. repeat intro; set_solver. Qed. - Lemma set_map_2_empty_1 (f : A → B → K) (Y : D) : - set_map_2 (SA:=C) (SB:=D) (SC:=E) f ∅ Y = ∅. + Lemma set_map_2_empty_1 (f : A → B → C) Y : set_map_2 f ∅ Y = ∅. Proof. unfold set_map_2. rewrite elements_empty. done. Qed. - Lemma set_map_2_empty_2 (f : A → B → K) (X : C) : - set_map_2 (SA:=C) (SB:=D) (SC:=E) f X ∅ = ∅. + Lemma set_map_2_empty_2 (f : A → B → C) X : set_map_2 f X ∅ = ∅. Proof. unfold set_map_2. rewrite elements_empty. - unfold list_ap. rewrite list_fmap_bind. simpl. induction (elements X); simpl; eauto. Qed. - Lemma set_map_2_union_1 (f : A → B → K) (X1 X2 : C) (Y : D) : - set_map_2 (SA:=C) (SB:=D) (SC:=E) f (X1 ∪ X2) Y - ≡ set_map_2 (SA:=C) (SB:=D) (SC:=E) f X1 Y - ∪ set_map_2 (SA:=C) (SB:=D) (SC:=E) f X2 Y. + Lemma set_map_2_union_1 (f : A → B → C) X1 X2 Y : + set_map_2 f (X1 ∪ X2) Y ≡ set_map_2 f X1 Y ∪ set_map_2 f X2 Y. Proof. set_solver. Qed. - Lemma set_map_2_union_2 (f : A → B → K) (X : C) (Y1 Y2 : D) : - set_map_2 (SA:=C) (SB:=D) (SC:=E) f X (Y1 ∪ Y2) - ≡ set_map_2 (SA:=C) (SB:=D) (SC:=E) f X Y1 - ∪ set_map_2 (SA:=C) (SB:=D) (SC:=E) f X Y2. + Lemma set_map_2_union_2 (f : A → B → C) X Y1 Y2 : + set_map_2 f X (Y1 ∪ Y2) ≡ set_map_2 f X Y1 ∪ set_map_2 f X Y2. Proof. set_solver. Qed. - (** This cannot be using [=] because [list_to_set_singleton] does not hold for [=]. *) - Lemma set_map_2_singleton (f : A → B → K) (x : A) (y : B): - set_map_2 (SA:=C) (SB:=D) (SC:=E) f {[x]} {[y]} ≡ {[f x y]}. + (** The following lemma does not hold using [=] because [list_to_set_singleton] + does not hold for [=]. *) + Lemma set_map_2_singleton (f : A → B → C) x y : + set_map_2 f {[x]} {[y]} ≡ {[f x y]}. Proof. set_solver. Qed. - - Lemma set_map_2_union_1_L `{!LeibnizEquiv E} (f : A → B → K) (X1 X2 : C) (Y : D) : - set_map_2 (SA:=C) (SB:=D) (SC:=E) f (X1 ∪ X2) Y - = set_map_2 (SA:=C) (SB:=D) (SC:=E) f X1 Y - ∪ set_map_2 (SA:=C) (SB:=D) (SC:=E) f X2 Y. + Lemma set_map_2_union_1_L `{!LeibnizEquiv SC} (f : A → B → C) X1 X2 Y : + set_map_2 f (X1 ∪ X2) Y = set_map_2 f X1 Y ∪ set_map_2 f X2 Y. Proof. unfold_leibniz. apply set_map_2_union_1. Qed. - Lemma set_map_2_union_2_L `{!LeibnizEquiv E} (f : A → B → K) (X : C) (Y1 Y2 : D) : - set_map_2 (SA:=C) (SB:=D) (SC:=E) f X (Y1 ∪ Y2) - = set_map_2 (SA:=C) (SB:=D) (SC:=E) f X Y1 - ∪ set_map_2 (SA:=C) (SB:=D) (SC:=E) f X Y2. + Lemma set_map_2_union_2_L `{!LeibnizEquiv SC} (f : A → B → C) X Y1 Y2 : + set_map_2 f X (Y1 ∪ Y2) = set_map_2 f X Y1 ∪ set_map_2 f X Y2. Proof. unfold_leibniz. apply set_map_2_union_2. Qed. + Lemma set_map_2_singleton_L `{!LeibnizEquiv SC} (f : A → B → C) x y : + set_map_2 f {[x]} {[y]} = {[f x y]}. + Proof. unfold_leibniz. apply set_map_2_singleton. Qed. End map2. - Lemma size_set_seq `{FinSet nat C} start len : size (set_seq (C:=C) start len) = len. Proof. diff --git a/theories/list.v b/theories/list.v index e2e2fa4be974cabcceb97ee6ef1f9e305eac26a2..20135cbb3ab043b6d794a29029cb8106c27ada73 100644 --- a/theories/list.v +++ b/theories/list.v @@ -231,10 +231,6 @@ Global Instance list_join: MJoin list := Definition mapM `{MBind M, MRet M} {A B} (f : A → M B) : list A → M (list B) := fix go l := match l with [] => mret [] | x :: l => y ↠f x; k ↠go l; mret (y :: k) end. -Definition list_ap {A B} (fs : list (A → B)) (xs : list A) : list B := - f ↠fs; - x ↠xs; - [f x]. (** We define stronger variants of the map function that allow the mapped function to use the index of the elements. *)