Commit eab2b27a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Tweaks.

parent 27628a0a
Pipeline #66432 passed with stage
in 11 minutes and 56 seconds
......@@ -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.
......
......@@ -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. *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment