diff options
author | 2013-07-24 15:44:13 +0000 | |
---|---|---|
committer | 2013-07-24 15:44:13 +0000 | |
commit | 64789ead3540e37983759b25de39233dcbf82b23 (patch) | |
tree | 10df75a0c4ba85e550752f1f9650dd6d25d6998f /theories/Lists/List.v | |
parent | f5bbb5ce34bb1ee2165086b0fdb3ee5f3d96a44e (diff) |
Added a concat function to List theory. Strangely, it was missing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16633 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists/List.v')
-rw-r--r-- | theories/Lists/List.v | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index ae6dde711..66c536a40 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -812,6 +812,33 @@ Section ListOps. End Reverse_Induction. + (*************************) + (** ** Concatenation *) + (*************************) + + Fixpoint concat (l : list (list A)) : list A := + match l with + | nil => nil + | cons x l => x ++ concat l + end. + + Lemma concat_nil : concat nil = nil. + Proof. + reflexivity. + Qed. + + Lemma concat_cons : forall x l, concat (cons x l) = x ++ concat l. + Proof. + reflexivity. + Qed. + + Lemma concat_app : forall l1 l2, concat (l1 ++ l2) = concat l1 ++ concat l2. + Proof. + intros l1; induction l1 as [|x l1 IH]; intros l2; simpl. + + reflexivity. + + rewrite IH; apply app_assoc. + Qed. + (***********************************) (** ** Decidable equality on lists *) (***********************************) @@ -916,6 +943,21 @@ Section Map. End Map. +Lemma flat_map_concat_map : forall A B (f : A -> list B) l, + flat_map f l = concat (map f l). +Proof. +intros A B f l; induction l as [|x l IH]; simpl. ++ reflexivity. ++ rewrite IH; reflexivity. +Qed. + +Lemma concat_map : forall A B (f : A -> B) l, map f (concat l) = concat (map (map f) l). +Proof. +intros A B f l; induction l as [|x l IH]; simpl. ++ reflexivity. ++ rewrite map_app, IH; reflexivity. +Qed. + Lemma map_id : forall (A :Type) (l : list A), map (fun x => x) l = l. Proof. |