diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-11-11 15:17:20 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-11-11 15:17:27 -0500 |
commit | 37167250d6f02a187c91702ecbfb66f6ca19f925 (patch) | |
tree | 130ff98cc9e7856541409fa41ee17b77dd49d848 /src | |
parent | a8b24296018ccd736e49ed764b942cbc79c9dfcf (diff) |
prove admits in Util.Tuple
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/ListUtil.v | 98 | ||||
-rw-r--r-- | src/Util/Tuple.v | 127 |
2 files changed, 175 insertions, 50 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 9131a0d20..88fb815b2 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1485,34 +1485,36 @@ Proof. Qed. Local Hint Resolve map2_nil_r map2_nil_l. -Opaque map2. +Ltac simpl_list_lengths := repeat match goal with + | H : appcontext[length (@nil ?A)] |- _ => rewrite (@nil_length0 A) in H + | H : appcontext[length (_ :: _)] |- _ => rewrite length_cons in H + | |- appcontext[length (@nil ?A)] => rewrite (@nil_length0 A) + | |- appcontext[length (_ :: _)] => rewrite length_cons + end. -Lemma map2_length : forall A B C (f : A -> B -> C) ls1 ls2, - length (map2 f ls1 ls2) = min (length ls1) (length ls2). -Proof. - induction ls1, ls2; intros; try solve [cbv; auto]. - rewrite map2_cons, !length_cons, IHls1. - auto. -Qed. -Hint Rewrite @map2_length : distr_length. +Section OpaqueMap2. + Local Opaque map2. + Lemma map2_length : forall A B C (f : A -> B -> C) ls1 ls2, + length (map2 f ls1 ls2) = min (length ls1) (length ls2). + Proof. + induction ls1, ls2; intros; try solve [cbv; auto]. + rewrite map2_cons, !length_cons, IHls1. + auto. + Qed. + Hint Rewrite @map2_length : distr_length. -Ltac simpl_list_lengths := repeat match goal with - | H : appcontext[length (@nil ?A)] |- _ => rewrite (@nil_length0 A) in H - | H : appcontext[length (_ :: _)] |- _ => rewrite length_cons in H - | |- appcontext[length (@nil ?A)] => rewrite (@nil_length0 A) - | |- appcontext[length (_ :: _)] => rewrite length_cons - end. -Lemma map2_app : forall A B C (f : A -> B -> C) ls1 ls2 ls1' ls2', - (length ls1 = length ls2) -> - map2 f (ls1 ++ ls1') (ls2 ++ ls2') = map2 f ls1 ls2 ++ map2 f ls1' ls2'. -Proof. - induction ls1, ls2; intros; rewrite ?map2_nil_r, ?app_nil_l; try congruence; - simpl_list_lengths; try omega. - rewrite <-!app_comm_cons, !map2_cons. - rewrite IHls1; auto. -Qed. + Lemma map2_app : forall A B C (f : A -> B -> C) ls1 ls2 ls1' ls2', + (length ls1 = length ls2) -> + map2 f (ls1 ++ ls1') (ls2 ++ ls2') = map2 f ls1 ls2 ++ map2 f ls1' ls2'. + Proof. + induction ls1, ls2; intros; rewrite ?map2_nil_r, ?app_nil_l; try congruence; + simpl_list_lengths; try omega. + rewrite <-!app_comm_cons, !map2_cons. + rewrite IHls1; auto. + Qed. +End OpaqueMap2. Lemma firstn_update_nth {A} : forall f m n (xs : list A), firstn m (update_nth n f xs) = update_nth n f (firstn m xs). @@ -1622,3 +1624,51 @@ Lemma skipn_repeat : forall {A} x n k, skipn k (@repeat A x n) = repeat x (n - k Proof. induction n, k; boring. Qed. Hint Rewrite @skipn_repeat : push_skipn. + +Global Instance Proper_map {A B} {RA RB} {Equivalence_RB:Equivalence RB} + : Proper ((RA==>RB) ==> eqlistA RA ==> eqlistA RB) (@List.map A B). +Proof. + repeat intro. + match goal with [H:eqlistA _ _ _ |- _ ] => induction H end; [reflexivity|]. + cbv [respectful] in *; econstructor; eauto. +Qed. + +Lemma pointwise_map {A B} : Proper ((pointwise_relation _ eq) ==> eq ==> eq) (@List.map A B). +Proof. + repeat intro; cbv [pointwise_relation] in *; subst. + match goal with [H:list _ |- _ ] => induction H as [|? IH] end; [reflexivity|]. + simpl. rewrite IHIH. congruence. +Qed. + +Lemma map_map2 {A B C D} (f:A -> B -> C) (g:C -> D) (xs:list A) (ys:list B) : List.map g (map2 f xs ys) = map2 (fun (a : A) (b : B) => g (f a b)) xs ys. +Proof. + revert ys; induction xs; intros; [reflexivity|]. + destruct ys; [reflexivity|]. + simpl. rewrite IHxs. reflexivity. +Qed. + +Lemma map2_fst {A B C} (f:A -> C) (xs:list A) : forall (ys:list B), length xs = length ys -> + map2 (fun (a : A) (_ : B) => f a) xs ys = List.map f xs. +Proof. + induction xs; intros; [reflexivity|]. + destruct ys; [simpl in *; discriminate|]. + simpl. rewrite IHxs by eauto. reflexivity. +Qed. + +Lemma map2_flip {A B C} (f:A -> B -> C) (xs:list A) : forall (ys: list B), + map2 (fun b a => f a b) ys xs = map2 f xs ys. +Proof. + induction xs; destruct ys; try reflexivity; []. + simpl. rewrite IHxs. reflexivity. +Qed. + +Lemma map2_snd {A B C} (f:B -> C) (xs:list A) : forall (ys:list B), length xs = length ys -> + map2 (fun (_ : A) (b : B) => f b) xs ys = List.map f ys. +Proof. intros. rewrite map2_flip. eauto using map2_fst. Qed. + +Lemma map2_map {A B C A' B'} (f:A -> B -> C) (g:A' -> A) (h:B' -> B) (xs:list A') (ys:list B') + : map2 f (List.map g xs) (List.map h ys) = map2 (fun a b => f (g a) (h b)) xs ys. +Proof. + revert ys; induction xs; destruct ys; intros; try reflexivity; []. + simpl. rewrite IHxs. reflexivity. +Qed.
\ No newline at end of file diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index d1dcbca30..af9d9816c 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -188,17 +188,6 @@ Definition on_tuple {A B} (f:list A -> list B) Definition map {n A B} (f:A -> B) (xs:tuple A n) : tuple B n := on_tuple (List.map f) (fun _ => eq_trans (map_length _ _)) xs. -Lemma map_S {n A B} (f:A -> B) (xs:tuple' A n) (x:A) - : map (n:=S (S n)) f (xs, x) = (map (n:=S n) f xs, f x). -Proof. - unfold map, on_tuple. - simpl @List.map. -Admitted. - -Lemma map_to_list {A B n ts} (f : A -> B) - : List.map f (@to_list A n ts) = @to_list B n (map f ts). -Proof. Admitted. - Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat} (Hlength : forall la lb, length la = a -> length lb = b -> length (f la lb) = c) (ta:tuple A a) (tb:tuple B b) : tuple C c @@ -208,40 +197,127 @@ Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat} Definition map2 {n A B C} (f:A -> B -> C) (xs:tuple A n) (ys:tuple B n) : tuple C n := on_tuple2 (map2 f) (fun la lb pfa pfb => eq_trans (@map2_length _ _ _ _ la lb) (eq_trans (f_equal2 _ pfa pfb) (Min.min_idempotent _))) xs ys. -Lemma map2_S {n A B C} (f:A -> B -> C) (xs:tuple' A n) (ys:tuple' B n) (x:A) (y:B) - : map2 (n:=S (S n)) f (xs, x) (ys, y) = (map2 (n:=S n) f xs ys, f x y). +Lemma to_list'_ext {n A} (xs ys:tuple' A n) : to_list' n xs = to_list' n ys -> xs = ys. +Proof. + induction n; simpl in *; [cbv; congruence|]; destruct_head' prod. + intro Hp; injection Hp; clear Hp; intros; subst; eauto using f_equal2. +Qed. + +Lemma to_list_ext {n A} (xs ys:tuple A n) : to_list n xs = to_list n ys -> xs = ys. +Proof. + destruct n; simpl in *; destruct_head unit; eauto using to_list'_ext. +Qed. + +Lemma from_list'_complete {A n} (xs:tuple' A n) : exists x ls pf, xs = from_list' x n ls pf. Proof. -Admitted. + destruct n; simpl in xs. + { exists xs. exists nil. exists eq_refl. reflexivity. } + { destruct xs as [xs' x]. exists x. exists (to_list' _ xs'). eexists (length_to_list' _ _ _). + symmetry; eapply from_list'_to_list'. reflexivity. } +Qed. + +Lemma from_list_complete {A n} (xs:tuple A n) : exists ls pf, xs = from_list n ls pf. +Proof. + exists (to_list n xs). exists (length_to_list _). symmetry; eapply from_list_to_list. +Qed. + +Ltac tuples_from_lists := + repeat match goal with + | [xs:tuple ?A _ |- _] => + let ls := fresh "l" xs in + destruct (from_list_complete xs) as [ls [? ?]]; subst + | [xs:tuple' ?A _ |- _] => + let a := fresh A in + let ls := fresh "l" xs in + destruct (from_list'_complete xs) as [a [ls [? ?]]]; subst + end. + +Lemma map_to_list {A B n ts} (f : A -> B) + : List.map f (@to_list A n ts) = @to_list B n (map f ts). +Proof. + tuples_from_lists; unfold map, on_tuple. + repeat (rewrite to_list_from_list || rewrite from_list_to_list). + reflexivity. +Qed. + +Lemma to_list_map2 {A B C n xs ys} (f : A -> B -> C) + : ListUtil.map2 f (@to_list A n xs) (@to_list B n ys) = @to_list C n (map2 f xs ys). +Proof. + tuples_from_lists; unfold map2, on_tuple2. + repeat (rewrite to_list_from_list || rewrite from_list_to_list). + reflexivity. +Qed. + +Ltac tuple_maps_to_list_maps := + try eapply to_list_ext; + tuples_from_lists; + repeat (rewrite <-map_to_list || rewrite <-to_list_map2 || + rewrite to_list_from_list || rewrite from_list_to_list). Lemma map_map2 {n A B C D} (f:A -> B -> C) (g:C -> D) (xs:tuple A n) (ys:tuple B n) : map g (map2 f xs ys) = map2 (fun a b => g (f a b)) xs ys. Proof. -Admitted. + tuple_maps_to_list_maps; eauto using ListUtil.map_map2. +Qed. Lemma map2_fst {n A B C} (f:A -> C) (xs:tuple A n) (ys:tuple B n) : map2 (fun a b => f a) xs ys = map f xs. Proof. -Admitted. + tuple_maps_to_list_maps; eauto using ListUtil.map2_fst. +Qed. Lemma map2_snd {n A B C} (f:B -> C) (xs:tuple A n) (ys:tuple B n) : map2 (fun a b => f b) xs ys = map f ys. Proof. -Admitted. - -Lemma map_id {n A} (xs:tuple A n) - : map (fun x => x) xs = xs. -Proof. -Admitted. + tuple_maps_to_list_maps; eauto using ListUtil.map2_snd. +Qed. Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n) : (forall x, f x = x) -> map f xs = xs. Proof. -Admitted. + intros; tuple_maps_to_list_maps. + transitivity (List.map (fun x => x) lxs). + { eapply ListUtil.pointwise_map; cbv [pointwise_relation]; eauto. } + { eapply List.map_id. } +Qed. + +Lemma map_id {n A} (xs:tuple A n) + : map (fun x => x) xs = xs. +Proof. eapply map_id_ext; intros; reflexivity. Qed. Lemma map2_map {n A B C A' B'} (f:A -> B -> C) (g:A' -> A) (h:B' -> B) (xs:tuple A' n) (ys:tuple B' n) : map2 f (map g xs) (map h ys) = map2 (fun a b => f (g a) (h b)) xs ys. Proof. -Admitted. + tuple_maps_to_list_maps; eauto using ListUtil.map2_map. +Qed. + +Lemma map_S' {n A B} (f:A -> B) (xs:tuple A (S n)) (x:A) + : map (n:=S (S n)) f (xs, x) = (map (n:=S n) f xs, f x). +Proof. + tuple_maps_to_list_maps. + destruct lxs as [|x' lxs']; [simpl in *; discriminate|]. + change ( f x :: List.map f (to_list (S n) (from_list (S n) (x' :: lxs') x0)) = f x :: to_list (S n) (map f (from_list (S n) (x' :: lxs') x0)) ). + tuple_maps_to_list_maps. + reflexivity. +Qed. + +Definition map_S {n A B} (f:A -> B) (xs:tuple' A n) (x:A) + : map (n:=S (S n)) f (xs, x) = (map (n:=S n) f xs, f x) := map_S' _ _ _. + +Lemma map2_S' {n A B C} (f:A -> B -> C) (xs:tuple A (S n)) (ys:tuple B (S n)) (x:A) (y:B) + : map2 (n:=S (S n)) f (xs, x) (ys, y) = (map2 (n:=S n) f xs ys, f x y). +Proof. + tuple_maps_to_list_maps. + destruct lxs as [|x' lxs']; [simpl in *; discriminate|]. + destruct lys as [|y' lys']; [simpl in *; discriminate|]. + change ( f x y :: ListUtil.map2 f (to_list (S n) (from_list (S n) (x' :: lxs') x1)) + (to_list (S n) (from_list (S n) (y' :: lys') x0)) = f x y :: to_list (S n) (map2 f (from_list (S n) (x' :: lxs') x1) (from_list (S n) (y' :: lys') x0)) ). + tuple_maps_to_list_maps. + reflexivity. +Qed. + +Definition map2_S {n A B C} (f:A -> B -> C) (xs:tuple' A n) (ys:tuple' B n) (x:A) (y:B) + : map2 (n:=S (S n)) f (xs, x) (ys, y) = (map2 (n:=S n) f xs ys, f x y) := map2_S' _ _ _ _ _. Lemma map2_map_fst {n A B C A'} (f:A -> B -> C) (g:A' -> A) (xs:tuple A' n) (ys:tuple B n) : map2 f (map g xs) ys = map2 (fun a b => f (g a) b) xs ys. @@ -257,8 +333,7 @@ Qed. Lemma map_map {n A B C} (g : B -> C) (f : A -> B) (xs:tuple A n) : map g (map f xs) = map (fun x => g (f x)) xs. -Proof. -Admitted. +Proof. tuple_maps_to_list_maps; eapply List.map_map. Qed. Section monad. Context (M : Type -> Type) (bind : forall X Y, M X -> (X -> M Y) -> M Y) (ret : forall X, X -> M X). |