michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/list/comb): add map theorems

Browse source
This commit is contained in:
Haitao Zhang 2015-07-13 14:38:31 -07:00 committed by Leonardo de Moura
parent 589f9df103
commit fae8176363
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/list/comb.lean
View file

@ -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 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 theorem map_id : ∀ l : list A, map id l = l
| [] := rfl | [] := rfl
| (x::xs) := begin rewrite [map_cons, map_id] end | (x::xs) := begin rewrite [map_cons, map_id] end