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

feat(library/data/list/comb): add length_product theorem

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-04 15:09:52 -07:00
parent df69bb4cfc
commit 9a7cff0e89
2 changed files with 11 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -33,11 +33,11 @@ theorem map_map (g : B → C) (f : A → B) : ∀ l, map g (map f l) = map (g
show (g ∘ f) a :: map g (map f l) = map (g ∘ f) (a :: l),
by rewrite (map_map l)
theorem len_map (f : A → B) : ∀ l : list A, length (map f l) = length l
theorem length_map (f : A → B) : ∀ l : list A, length (map f l) = length l
| [] := by esimp
| (a :: l) :=
show length (map f l) + 1 = length l + 1,
by rewrite (len_map l)
by rewrite (length_map l)
theorem mem_map {A B : Type} (f : A → B) : ∀ {a l}, a ∈ l → f a ∈ map f l
| a [] i := absurd i !not_mem_nil
@ -356,6 +356,13 @@ theorem mem_of_mem_product_right {a : A} {b : B} : ∀ {l₁ l₂}, (a, b) ∈ p
mem_of_mem_map_pair₁ abin)
(λ abin : (a, b) ∈ product l₁ l₂,
mem_of_mem_product_right abin)
theorem length_product : ∀ (l₁ : list A) (l₂ : list B), length (product l₁ l₂) = length l₁ * length l₂
| [] l₂ := by rewrite [length_nil, zero_mul]
| (x::l₁) l₂ :=
assert ih : length (product l₁ l₂) = length l₁ * length l₂, from length_product l₁ l₂,
by rewrite [product_cons, length_append, length_cons,
length_map, ih, mul.right_distrib, one_mul, add.comm]
end product
end list

4
library/data/vec.lean
View file

@ -65,7 +65,7 @@ namespace vec
| (tag l h) := list.last l (ne_nil_of_length_eq_succ h)
definition map {n : nat} (f : A → B) : vec A n → vec B n
| (tag l h) := tag (list.map f l) (by clear map; substvars; rewrite len_map)
| (tag l h) := tag (list.map f l) (by clear map; substvars; rewrite length_map)
theorem map_nil (f : A → B) : map f nil = nil :=
rfl
@ -74,7 +74,7 @@ namespace vec
by induction v; reflexivity
theorem map_tag {n : nat} (f : A → B) (l : list A) (h : length l = n)
: map f (tag l h) = tag (list.map f l) (by substvars; rewrite len_map) :=
: map f (tag l h) = tag (list.map f l) (by substvars; rewrite length_map) :=
by reflexivity
theorem map_map {n : nat} (g : B → C) (f : A → B) (v : vec A n) : map g (map f v) = map (g ∘ f) v :=