From fae8176363ab5a2afa66e714d44c9e12d5abe615 Mon Sep 17 00:00:00 2001 From: Haitao Zhang Date: Mon, 13 Jul 2015 14:38:31 -0700 Subject: [PATCH] feat(library/data/list/comb): add map theorems --- library/data/list/comb.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean index c45ddc680..42e1bf5b9 100644 --- a/library/data/list/comb.lean +++ b/library/data/list/comb.lean @@ -19,6 +19,12 @@ theorem map_nil (f : A → B) : map f [] = [] theorem map_cons (f : A → B) (a : A) (l : list A) : map f (a :: l) = f a :: map f l +lemma map_append (f : A → B) : ∀ l₁ l₂, map f (l₁++l₂) = (map f l₁)++(map f l₂) +| nil := take l, rfl +| (a::l) := take l', begin rewrite [append_cons, *map_cons, append_cons, map_append] end + +lemma map_singleton (f : A → B) (a : A) : map f [a] = [f a] := rfl + theorem map_id : ∀ l : list A, map id l = l | [] := rfl | (x::xs) := begin rewrite [map_cons, map_id] end