refactor(library/data): cleanup vector and list modules
This commit is contained in:
Leonardo de Moura
parent
f6f2c499ae
commit
27e58dc534
2 changed files with 148 additions and 148 deletions
|
|
@ -17,50 +17,50 @@ inductive list (T : Type) : Type :=
|
|||
|
||||
namespace list
|
||||
notation h :: t := cons h t
|
||||
notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
|
||||
notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l
|
||||
|
||||
variable {T : Type}
|
||||
|
||||
/- append -/
|
||||
|
||||
definition append : list T → list T → list T
|
||||
| append nil l := l
|
||||
| append (h :: s) t := h :: (append s t)
|
||||
| [] l := l
|
||||
| (h :: s) t := h :: (append s t)
|
||||
|
||||
notation l₁ ++ l₂ := append l₁ l₂
|
||||
|
||||
theorem append_nil_left (t : list T) : nil ++ t = t
|
||||
theorem append_nil_left (t : list T) : [] ++ t = t
|
||||
|
||||
theorem append_cons (x : T) (s t : list T) : (x::s) ++ t = x::(s ++ t)
|
||||
|
||||
theorem append_nil_right : ∀ (t : list T), t ++ nil = t
|
||||
| append_nil_right nil := rfl
|
||||
| append_nil_right (a :: l) := calc
|
||||
(a :: l) ++ nil = a :: (l ++ nil) : rfl
|
||||
... = a :: l : append_nil_right l
|
||||
theorem append_nil_right : ∀ (t : list T), t ++ [] = t
|
||||
| [] := rfl
|
||||
| (a :: l) := calc
|
||||
(a :: l) ++ [] = a :: (l ++ []) : rfl
|
||||
... = a :: l : append_nil_right l
|
||||
|
||||
|
||||
theorem append.assoc : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u)
|
||||
| append.assoc nil t u := rfl
|
||||
| append.assoc (a :: l) t u :=
|
||||
| [] t u := rfl
|
||||
| (a :: l) t u :=
|
||||
show a :: (l ++ t ++ u) = (a :: l) ++ (t ++ u),
|
||||
by rewrite (append.assoc l t u)
|
||||
|
||||
/- length -/
|
||||
|
||||
definition length : list T → nat
|
||||
| length nil := 0
|
||||
| length (a :: l) := length l + 1
|
||||
| [] := 0
|
||||
| (a :: l) := length l + 1
|
||||
|
||||
theorem length_nil : length (@nil T) = 0
|
||||
|
||||
theorem length_cons (x : T) (t : list T) : length (x::t) = length t + 1
|
||||
|
||||
theorem length_append : ∀ (s t : list T), length (s ++ t) = length s + length t
|
||||
| length_append nil t := calc
|
||||
length (nil ++ t) = length t : rfl
|
||||
... = length nil + length t : zero_add
|
||||
| length_append (a :: s) t := calc
|
||||
| [] t := calc
|
||||
length ([] ++ t) = length t : rfl
|
||||
... = length [] + length t : zero_add
|
||||
| (a :: s) t := calc
|
||||
length (a :: s ++ t) = length (s ++ t) + 1 : rfl
|
||||
... = length s + length t + 1 : length_append
|
||||
... = (length s + 1) + length t : add.succ_left
|
||||
|
|
@ -71,17 +71,17 @@ theorem length_append : ∀ (s t : list T), length (s ++ t) = length s + length
|
|||
/- concat -/
|
||||
|
||||
definition concat : Π (x : T), list T → list T
|
||||
| concat a nil := [a]
|
||||
| concat a (b :: l) := b :: concat a l
|
||||
| a [] := [a]
|
||||
| a (b :: l) := b :: concat a l
|
||||
|
||||
theorem concat_nil (x : T) : concat x nil = [x]
|
||||
theorem concat_nil (x : T) : concat x [] = [x]
|
||||
|
||||
theorem concat_cons (x y : T) (l : list T) : concat x (y::l) = y::(concat x l)
|
||||
|
||||
theorem concat_eq_append (a : T) : ∀ (l : list T), concat a l = l ++ [a]
|
||||
| concat_eq_append nil := rfl
|
||||
| concat_eq_append (b :: l) :=
|
||||
show b :: (concat a l) = (b :: l) ++ (a :: nil),
|
||||
| [] := rfl
|
||||
| (b :: l) :=
|
||||
show b :: (concat a l) = (b :: l) ++ (a :: []),
|
||||
by rewrite concat_eq_append
|
||||
|
||||
-- add_rewrite append_nil append_cons
|
||||
|
|
@ -89,21 +89,21 @@ theorem concat_eq_append (a : T) : ∀ (l : list T), concat a l = l ++ [a]
|
|||
/- reverse -/
|
||||
|
||||
definition reverse : list T → list T
|
||||
| reverse nil := nil
|
||||
| reverse (a :: l) := concat a (reverse l)
|
||||
| [] := []
|
||||
| (a :: l) := concat a (reverse l)
|
||||
|
||||
theorem reverse_nil : reverse (@nil T) = nil
|
||||
theorem reverse_nil : reverse (@nil T) = []
|
||||
|
||||
theorem reverse_cons (x : T) (l : list T) : reverse (x::l) = concat x (reverse l)
|
||||
|
||||
theorem reverse_singleton (x : T) : reverse [x] = [x]
|
||||
|
||||
theorem reverse_append : ∀ (s t : list T), reverse (s ++ t) = (reverse t) ++ (reverse s)
|
||||
| reverse_append nil t2 := calc
|
||||
reverse (nil ++ t2) = reverse t2 : rfl
|
||||
... = (reverse t2) ++ nil : append_nil_right
|
||||
... = (reverse t2) ++ (reverse nil) : {reverse_nil⁻¹}
|
||||
| reverse_append (a2 :: s2) t2 := calc
|
||||
| [] t2 := calc
|
||||
reverse ([] ++ t2) = reverse t2 : rfl
|
||||
... = (reverse t2) ++ [] : append_nil_right
|
||||
... = (reverse t2) ++ (reverse []) : by rewrite reverse_nil
|
||||
| (a2 :: s2) t2 := calc
|
||||
reverse ((a2 :: s2) ++ t2) = concat a2 (reverse (s2 ++ t2)) : rfl
|
||||
... = concat a2 (reverse t2 ++ reverse s2) : reverse_append
|
||||
... = (reverse t2 ++ reverse s2) ++ [a2] : concat_eq_append
|
||||
|
|
@ -112,8 +112,8 @@ theorem reverse_append : ∀ (s t : list T), reverse (s ++ t) = (reverse t) ++ (
|
|||
... = reverse t2 ++ reverse (a2 :: s2) : rfl
|
||||
|
||||
theorem reverse_reverse : ∀ (l : list T), reverse (reverse l) = l
|
||||
| reverse_reverse nil := rfl
|
||||
| reverse_reverse (a :: l) := calc
|
||||
| [] := rfl
|
||||
| (a :: l) := calc
|
||||
reverse (reverse (a :: l)) = reverse (concat a (reverse l)) : rfl
|
||||
... = reverse (reverse l ++ [a]) : concat_eq_append
|
||||
... = reverse [a] ++ reverse (reverse l) : reverse_append
|
||||
|
|
@ -128,39 +128,39 @@ calc
|
|||
/- head and tail -/
|
||||
|
||||
definition head [h : inhabited T] : list T → T
|
||||
| head nil := arbitrary T
|
||||
| head (a :: l) := a
|
||||
| [] := arbitrary T
|
||||
| (a :: l) := a
|
||||
|
||||
theorem head_cons [h : inhabited T] (a : T) (l : list T) : head (a::l) = a
|
||||
|
||||
theorem head_concat [h : inhabited T] (t : list T) : ∀ {s : list T}, s ≠ nil → head (s ++ t) = head s
|
||||
| @head_concat nil H := absurd rfl H
|
||||
| @head_concat (a :: s) H :=
|
||||
theorem head_concat [h : inhabited T] (t : list T) : ∀ {s : list T}, s ≠ [] → head (s ++ t) = head s
|
||||
| [] H := absurd rfl H
|
||||
| (a :: s) H :=
|
||||
show head (a :: (s ++ t)) = head (a :: s),
|
||||
by rewrite head_cons
|
||||
|
||||
definition tail : list T → list T
|
||||
| tail nil := nil
|
||||
| tail (a :: l) := l
|
||||
| [] := []
|
||||
| (a :: l) := l
|
||||
|
||||
theorem tail_nil : tail (@nil T) = nil
|
||||
theorem tail_nil : tail (@nil T) = []
|
||||
|
||||
theorem tail_cons (a : T) (l : list T) : tail (a::l) = l
|
||||
|
||||
theorem cons_head_tail [h : inhabited T] {l : list T} : l ≠ nil → (head l)::(tail l) = l :=
|
||||
theorem cons_head_tail [h : inhabited T] {l : list T} : l ≠ [] → (head l)::(tail l) = l :=
|
||||
list.cases_on l
|
||||
(assume H : nil ≠ nil, absurd rfl H)
|
||||
(take x l, assume H : x::l ≠ nil, rfl)
|
||||
(assume H : [] ≠ [], absurd rfl H)
|
||||
(take x l, assume H : x::l ≠ [], rfl)
|
||||
|
||||
/- list membership -/
|
||||
|
||||
definition mem : T → list T → Prop
|
||||
| mem a nil := false
|
||||
| mem a (b :: l) := a = b ∨ mem a l
|
||||
| a [] := false
|
||||
| a (b :: l) := a = b ∨ mem a l
|
||||
|
||||
notation e ∈ s := mem e s
|
||||
|
||||
theorem mem_nil (x : T) : x ∈ nil ↔ false :=
|
||||
theorem mem_nil (x : T) : x ∈ [] ↔ false :=
|
||||
iff.rfl
|
||||
|
||||
theorem mem_cons (x y : T) (l : list T) : x ∈ y::l ↔ (x = y ∨ x ∈ l) :=
|
||||
|
|
@ -195,13 +195,13 @@ local attribute mem [reducible]
|
|||
local attribute append [reducible]
|
||||
theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x::t) :=
|
||||
list.induction_on l
|
||||
(take H : x ∈ nil, false.elim (iff.elim_left !mem_nil H))
|
||||
(take H : x ∈ [], false.elim (iff.elim_left !mem_nil H))
|
||||
(take y l,
|
||||
assume IH : x ∈ l → ∃s t : list T, l = s ++ (x::t),
|
||||
assume H : x ∈ y::l,
|
||||
or.elim H
|
||||
(assume H1 : x = y,
|
||||
exists.intro nil (!exists.intro (H1 ▸ rfl)))
|
||||
exists.intro [] (!exists.intro (H1 ▸ rfl)))
|
||||
(assume H1 : x ∈ l,
|
||||
obtain s (H2 : ∃t : list T, l = s ++ (x::t)), from IH H1,
|
||||
obtain t (H3 : l = s ++ (x::t)), from H2,
|
||||
|
|
@ -241,16 +241,16 @@ variable [H : decidable_eq T]
|
|||
include H
|
||||
|
||||
definition find : T → list T → nat
|
||||
| find a nil := 0
|
||||
| find a (b :: l) := if a = b then 0 else succ (find a l)
|
||||
| a [] := 0
|
||||
| a (b :: l) := if a = b then 0 else succ (find a l)
|
||||
|
||||
theorem find_nil (x : T) : find x nil = 0
|
||||
theorem find_nil (x : T) : find x [] = 0
|
||||
|
||||
theorem find_cons (x y : T) (l : list T) : find x (y::l) = if x = y then 0 else succ (find x l)
|
||||
|
||||
theorem find.not_mem {l : list T} {x : T} : ¬x ∈ l → find x l = length l :=
|
||||
list.rec_on l
|
||||
(assume P₁ : ¬x ∈ nil, _)
|
||||
(assume P₁ : ¬x ∈ [], _)
|
||||
(take y l,
|
||||
assume iH : ¬x ∈ l → find x l = length l,
|
||||
assume P₁ : ¬x ∈ y::l,
|
||||
|
|
@ -266,9 +266,9 @@ end
|
|||
/- nth element -/
|
||||
|
||||
definition nth [h : inhabited T] : list T → nat → T
|
||||
| nth nil n := arbitrary T
|
||||
| nth (a :: l) 0 := a
|
||||
| nth (a :: l) (n+1) := nth l n
|
||||
| [] n := arbitrary T
|
||||
| (a :: l) 0 := a
|
||||
| (a :: l) (n+1) := nth l n
|
||||
|
||||
theorem nth_zero [h : inhabited T] (a : T) (l : list T) : nth (a :: l) 0 = a
|
||||
|
||||
|
|
@ -276,10 +276,10 @@ theorem nth_succ [h : inhabited T] (a : T) (l : list T) (n : nat) : nth (a::l) (
|
|||
|
||||
open decidable
|
||||
definition decidable_eq {A : Type} [H : decidable_eq A] : ∀ l₁ l₂ : list A, decidable (l₁ = l₂)
|
||||
| decidable_eq nil nil := inl rfl
|
||||
| decidable_eq nil (b::l₂) := inr (λ H, list.no_confusion H)
|
||||
| decidable_eq (a::l₁) nil := inr (λ H, list.no_confusion H)
|
||||
| decidable_eq (a::l₁) (b::l₂) :=
|
||||
| [] [] := inl rfl
|
||||
| [] (b::l₂) := inr (λ H, list.no_confusion H)
|
||||
| (a::l₁) [] := inr (λ H, list.no_confusion H)
|
||||
| (a::l₁) (b::l₂) :=
|
||||
match H a b with
|
||||
| inl Hab :=
|
||||
match decidable_eq l₁ l₂ with
|
||||
|
|
@ -293,44 +293,44 @@ section combinators
|
|||
variables {A B C : Type}
|
||||
|
||||
definition map (f : A → B) : list A → list B
|
||||
| map nil := nil
|
||||
| map (a :: l) := f a :: map l
|
||||
| [] := []
|
||||
| (a :: l) := f a :: map l
|
||||
|
||||
theorem map_nil (f : A → B) : map f nil = nil
|
||||
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_map (g : B → C) (f : A → B) : ∀ l : list A, map g (map f l) = map (g ∘ f) l
|
||||
| map_map nil := rfl
|
||||
| map_map (a :: l) :=
|
||||
| [] := rfl
|
||||
| (a :: l) :=
|
||||
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
|
||||
| len_map nil := rfl
|
||||
| len_map (a :: l) :=
|
||||
| [] := rfl
|
||||
| (a :: l) :=
|
||||
show length (map f l) + 1 = length l + 1,
|
||||
by rewrite (len_map l)
|
||||
|
||||
definition foldl (f : A → B → A) : A → list B → A
|
||||
| foldl a nil := a
|
||||
| foldl a (b :: l) := foldl (f a b) l
|
||||
| a [] := a
|
||||
| a (b :: l) := foldl (f a b) l
|
||||
|
||||
definition foldr (f : A → B → B) : B → list A → B
|
||||
| foldr b nil := b
|
||||
| foldr b (a :: l) := f a (foldr b l)
|
||||
| b [] := b
|
||||
| b (a :: l) := f a (foldr b l)
|
||||
|
||||
definition all (p : A → Prop) : list A → Prop
|
||||
| all nil := true
|
||||
| all (a :: l) := p a ∧ all l
|
||||
| [] := true
|
||||
| (a :: l) := p a ∧ all l
|
||||
|
||||
definition any (p : A → Prop) : list A → Prop
|
||||
| any nil := false
|
||||
| any (a :: l) := p a ∨ any l
|
||||
| [] := false
|
||||
| (a :: l) := p a ∨ any l
|
||||
|
||||
definition decidable_all (p : A → Prop) [H : decidable_pred p] : ∀ l, decidable (all p l)
|
||||
| decidable_all nil := decidable_true
|
||||
| decidable_all (a :: l) :=
|
||||
| [] := decidable_true
|
||||
| (a :: l) :=
|
||||
match H a with
|
||||
| inl Hp₁ :=
|
||||
match decidable_all l with
|
||||
|
|
@ -341,8 +341,8 @@ definition decidable_all (p : A → Prop) [H : decidable_pred p] : ∀ l, decida
|
|||
end
|
||||
|
||||
definition decidable_any (p : A → Prop) [H : decidable_pred p] : ∀ l, decidable (any p l)
|
||||
| decidable_any nil := decidable_false
|
||||
| decidable_any (a :: l) :=
|
||||
| [] := decidable_false
|
||||
| (a :: l) :=
|
||||
match H a with
|
||||
| inl Hp := inl (or.inl Hp)
|
||||
| inr Hn₁ :=
|
||||
|
|
@ -353,25 +353,25 @@ definition decidable_any (p : A → Prop) [H : decidable_pred p] : ∀ l, decida
|
|||
end
|
||||
|
||||
definition zip : list A → list B → list (A × B)
|
||||
| zip nil _ := nil
|
||||
| zip _ nil := nil
|
||||
| zip (a :: la) (b :: lb) := (a, b) :: zip la lb
|
||||
| [] _ := []
|
||||
| _ [] := []
|
||||
| (a :: la) (b :: lb) := (a, b) :: zip la lb
|
||||
|
||||
definition unzip : list (A × B) → list A × list B
|
||||
| unzip nil := (nil, nil)
|
||||
| unzip ((a, b) :: l) :=
|
||||
| [] := ([], [])
|
||||
| ((a, b) :: l) :=
|
||||
match unzip l with
|
||||
| (la, lb) := (a :: la, b :: lb)
|
||||
end
|
||||
|
||||
theorem unzip_nil : unzip (@nil (A × B)) = (nil, nil)
|
||||
theorem unzip_nil : unzip (@nil (A × B)) = ([], [])
|
||||
|
||||
theorem unzip_cons (a : A) (b : B) (l : list (A × B)) :
|
||||
unzip ((a, b) :: l) = match unzip l with (la, lb) := (a :: la, b :: lb) end
|
||||
|
||||
theorem zip_unzip : ∀ (l : list (A × B)), zip (pr₁ (unzip l)) (pr₂ (unzip l)) = l
|
||||
| zip_unzip nil := rfl
|
||||
| zip_unzip ((a, b) :: l) :=
|
||||
| [] := rfl
|
||||
| ((a, b) :: l) :=
|
||||
begin
|
||||
rewrite unzip_cons,
|
||||
have r : zip (pr₁ (unzip l)) (pr₂ (unzip l)) = l, from zip_unzip l,
|
||||
|
|
|
|||
|
|
@ -14,22 +14,22 @@ inductive vector (A : Type) : nat → Type :=
|
|||
|
||||
namespace vector
|
||||
notation a :: b := cons a b
|
||||
notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
|
||||
notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l
|
||||
|
||||
variables {A B C : Type}
|
||||
|
||||
protected definition is_inhabited [instance] [h : inhabited A] : ∀ (n : nat), inhabited (vector A n)
|
||||
| is_inhabited 0 := inhabited.mk nil
|
||||
| is_inhabited (n+1) := inhabited.mk (inhabited.value h :: inhabited.value (is_inhabited n))
|
||||
| 0 := inhabited.mk []
|
||||
| (n+1) := inhabited.mk (inhabited.value h :: inhabited.value (is_inhabited n))
|
||||
|
||||
theorem vector0_eq_nil : ∀ (v : vector A 0), v = nil
|
||||
| vector0_eq_nil nil := rfl
|
||||
theorem vector0_eq_nil : ∀ (v : vector A 0), v = []
|
||||
| [] := rfl
|
||||
|
||||
definition head : Π {n : nat}, vector A (succ n) → A
|
||||
| head (a::v) := a
|
||||
| n (a::v) := a
|
||||
|
||||
definition tail : Π {n : nat}, vector A (succ n) → vector A n
|
||||
| tail (a::v) := v
|
||||
| n (a::v) := v
|
||||
|
||||
theorem head_cons {n : nat} (h : A) (t : vector A n) : head (h :: t) = h :=
|
||||
rfl
|
||||
|
|
@ -38,50 +38,50 @@ namespace vector
|
|||
rfl
|
||||
|
||||
theorem eta : ∀ {n : nat} (v : vector A (succ n)), head v :: tail v = v
|
||||
| eta (a::v) := rfl
|
||||
| n (a::v) := rfl
|
||||
|
||||
definition last : Π {n : nat}, vector A (succ n) → A
|
||||
| last (a::nil) := a
|
||||
| last (a::v) := last v
|
||||
| last [a] := a
|
||||
| last (a::v) := last v
|
||||
|
||||
theorem last_singleton (a : A) : last (a :: nil) = a :=
|
||||
theorem last_singleton (a : A) : last [a] = a :=
|
||||
rfl
|
||||
|
||||
theorem last_cons {n : nat} (a : A) (v : vector A (succ n)) : last (a :: v) = last v :=
|
||||
rfl
|
||||
|
||||
definition const : Π (n : nat), A → vector A n
|
||||
| const 0 a := nil
|
||||
| const (succ n) a := a :: const n a
|
||||
| 0 a := []
|
||||
| (succ n) a := a :: const n a
|
||||
|
||||
theorem head_const (n : nat) (a : A) : head (const (succ n) a) = a :=
|
||||
rfl
|
||||
|
||||
theorem last_const : ∀ (n : nat) (a : A), last (const (succ n) a) = a
|
||||
| last_const 0 a := rfl
|
||||
| last_const (succ n) a := last_const n a
|
||||
| 0 a := rfl
|
||||
| (n+1) a := last_const n a
|
||||
|
||||
definition nth : Π {n : nat}, vector A n → fin n → A
|
||||
| ⌞succ n⌟ (h :: t) (fz n) := h
|
||||
| ⌞succ n⌟ (h :: t) (fs f) := nth t f
|
||||
| ⌞n+1⌟ (h :: t) (fz n) := h
|
||||
| ⌞n+1⌟ (h :: t) (fs f) := nth t f
|
||||
|
||||
definition tabulate : Π {n : nat}, (fin n → A) → vector A n
|
||||
| 0 f := nil
|
||||
| (succ n) f := f (fz n) :: tabulate (λ i : fin n, f (fs i))
|
||||
| 0 f := []
|
||||
| (n+1) f := f (fz n) :: tabulate (λ i : fin n, f (fs i))
|
||||
|
||||
theorem nth_tabulate : ∀ {n : nat} (f : fin n → A) (i : fin n), nth (tabulate f) i = f i
|
||||
| (succ n) f (fz n) := rfl
|
||||
| (succ n) f (fs i) :=
|
||||
| (n+1) f (fz n) := rfl
|
||||
| (n+1) f (fs i) :=
|
||||
begin
|
||||
change (nth (tabulate (λ i : fin n, f (fs i))) i = f (fs i)),
|
||||
rewrite nth_tabulate
|
||||
end
|
||||
|
||||
definition map (f : A → B) : Π {n : nat}, vector A n → vector B n
|
||||
| map nil := nil
|
||||
| map [] := []
|
||||
| map (a::v) := f a :: map v
|
||||
|
||||
theorem map_nil (f : A → B) : map f nil = nil :=
|
||||
theorem map_nil (f : A → B) : map f [] = [] :=
|
||||
rfl
|
||||
|
||||
theorem map_cons {n : nat} (f : A → B) (h : A) (t : vector A n) : map f (h :: t) = f h :: map f t :=
|
||||
|
|
@ -96,10 +96,10 @@ namespace vector
|
|||
end
|
||||
|
||||
definition map2 (f : A → B → C) : Π {n : nat}, vector A n → vector B n → vector C n
|
||||
| map2 nil nil := nil
|
||||
| map2 [] [] := []
|
||||
| map2 (a::va) (b::vb) := f a b :: map2 va vb
|
||||
|
||||
theorem map2_nil (f : A → B → C) : map2 f nil nil = nil :=
|
||||
theorem map2_nil (f : A → B → C) : map2 f [] [] = [] :=
|
||||
rfl
|
||||
|
||||
theorem map2_cons {n : nat} (f : A → B → C) (h₁ : A) (h₂ : B) (t₁ : vector A n) (t₂ : vector B n) :
|
||||
|
|
@ -107,23 +107,23 @@ namespace vector
|
|||
rfl
|
||||
|
||||
definition append : Π {n m : nat}, vector A n → vector A m → vector A (n ⊕ m)
|
||||
| 0 m nil w := w
|
||||
| 0 m [] w := w
|
||||
| (succ n) m (a::v) w := a :: (append v w)
|
||||
|
||||
theorem nil_append {n : nat} (v : vector A n) : append nil v = v :=
|
||||
theorem nil_append {n : nat} (v : vector A n) : append [] v = v :=
|
||||
rfl
|
||||
|
||||
theorem append_cons {n m : nat} (h : A) (t : vector A n) (v : vector A m) :
|
||||
append (h::t) v = h :: (append t v) :=
|
||||
rfl
|
||||
|
||||
theorem append_nil : Π {n : nat} (v : vector A n), append v nil == v
|
||||
| zero nil := !heq.refl
|
||||
| (succ n) (h::t) :=
|
||||
theorem append_nil : Π {n : nat} (v : vector A n), append v [] == v
|
||||
| 0 [] := !heq.refl
|
||||
| (n+1) (h::t) :=
|
||||
begin
|
||||
change (h :: append t nil == h :: t),
|
||||
have H₁ : append t nil == t, from append_nil t,
|
||||
revert H₁, generalize (append t nil),
|
||||
change (h :: append t [] == h :: t),
|
||||
have H₁ : append t [] == t, from append_nil t,
|
||||
revert H₁, generalize (append t []),
|
||||
rewrite [-add_eq_addl, add_zero],
|
||||
intros (w, H₁),
|
||||
rewrite [heq.to_eq H₁],
|
||||
|
|
@ -131,18 +131,18 @@ namespace vector
|
|||
end
|
||||
|
||||
theorem map_append (f : A → B) : ∀ {n m : nat} (v : vector A n) (w : vector A m), map f (append v w) = append (map f v) (map f w)
|
||||
| zero m nil w := rfl
|
||||
| (succ n) m (h :: t) w :=
|
||||
| 0 m [] w := rfl
|
||||
| (n+1) m (h :: t) w :=
|
||||
begin
|
||||
change (f h :: map f (append t w) = f h :: append (map f t) (map f w)),
|
||||
rewrite map_append
|
||||
end
|
||||
|
||||
definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n
|
||||
| unzip nil := (nil, nil)
|
||||
| unzip [] := ([], [])
|
||||
| unzip ((a, b) :: v) := (a :: pr₁ (unzip v), b :: pr₂ (unzip v))
|
||||
|
||||
theorem unzip_nil : unzip (@nil (A × B)) = (nil, nil) :=
|
||||
theorem unzip_nil : unzip (@nil (A × B)) = ([], []) :=
|
||||
rfl
|
||||
|
||||
theorem unzip_cons {n : nat} (a : A) (b : B) (v : vector (A × B) n) :
|
||||
|
|
@ -150,7 +150,7 @@ namespace vector
|
|||
rfl
|
||||
|
||||
definition zip : Π {n : nat}, vector A n → vector B n → vector (A × B) n
|
||||
| zip nil nil := nil
|
||||
| zip [] [] := []
|
||||
| zip (a::va) (b::vb) := ((a, b) :: zip va vb)
|
||||
|
||||
theorem zip_nil_nil : zip (@nil A) (@nil B) = nil :=
|
||||
|
|
@ -161,16 +161,16 @@ namespace vector
|
|||
rfl
|
||||
|
||||
theorem unzip_zip : ∀ {n : nat} (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂)
|
||||
| 0 nil nil := rfl
|
||||
| (succ n) (a::va) (b::vb) := calc
|
||||
| 0 [] [] := rfl
|
||||
| (n+1) (a::va) (b::vb) := calc
|
||||
unzip (zip (a :: va) (b :: vb))
|
||||
= (a :: pr₁ (unzip (zip va vb)), b :: pr₂ (unzip (zip va vb))) : rfl
|
||||
... = (a :: pr₁ (va, vb), b :: pr₂ (va, vb)) : by rewrite unzip_zip
|
||||
... = (a :: va, b :: vb) : rfl
|
||||
|
||||
theorem zip_unzip : ∀ {n : nat} (v : vector (A × B) n), zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v
|
||||
| 0 nil := rfl
|
||||
| (succ n) ((a, b) :: v) := calc
|
||||
| 0 [] := rfl
|
||||
| (n+1) ((a, b) :: v) := calc
|
||||
zip (pr₁ (unzip ((a, b) :: v))) (pr₂ (unzip ((a, b) :: v)))
|
||||
= (a, b) :: zip (pr₁ (unzip v)) (pr₂ (unzip v)) : rfl
|
||||
... = (a, b) :: v : by rewrite zip_unzip
|
||||
|
|
@ -178,38 +178,38 @@ namespace vector
|
|||
/- Concat -/
|
||||
|
||||
definition concat : Π {n : nat}, vector A n → A → vector A (succ n)
|
||||
| concat nil a := a :: nil
|
||||
| concat [] a := [a]
|
||||
| concat (b::v) a := b :: concat v a
|
||||
|
||||
theorem concat_nil (a : A) : concat nil a = a :: nil :=
|
||||
theorem concat_nil (a : A) : concat [] a = [a] :=
|
||||
rfl
|
||||
|
||||
theorem concat_cons {n : nat} (b : A) (v : vector A n) (a : A) : concat (b :: v) a = b :: concat v a :=
|
||||
rfl
|
||||
|
||||
theorem last_concat : ∀ {n : nat} (v : vector A n) (a : A), last (concat v a) = a
|
||||
| 0 nil a := rfl
|
||||
| (succ n) (b::v) a := calc
|
||||
| 0 [] a := rfl
|
||||
| (n+1) (b::v) a := calc
|
||||
last (concat (b::v) a) = last (concat v a) : rfl
|
||||
... = a : last_concat v a
|
||||
|
||||
/- Reverse -/
|
||||
|
||||
definition reverse : Π {n : nat}, vector A n → vector A n
|
||||
| zero nil := nil
|
||||
| (succ n) (x :: xs) := concat (reverse xs) x
|
||||
| 0 [] := []
|
||||
| (n+1) (x :: xs) := concat (reverse xs) x
|
||||
|
||||
theorem reverse_concat : Π {n : nat} (xs : vector A n) (a : A), reverse (concat xs a) = a :: reverse xs
|
||||
| zero nil a := rfl
|
||||
| (succ n) (x :: xs) a :=
|
||||
| 0 [] a := rfl
|
||||
| (n+1) (x :: xs) a :=
|
||||
begin
|
||||
change (concat (reverse (concat xs a)) x = a :: reverse (x :: xs)),
|
||||
rewrite reverse_concat
|
||||
end
|
||||
|
||||
theorem reverse_reverse : Π {n : nat} (xs : vector A n), reverse (reverse xs) = xs
|
||||
| zero nil := rfl
|
||||
| (succ n) (x :: xs) :=
|
||||
| 0 [] := rfl
|
||||
| (n+1) (x :: xs) :=
|
||||
begin
|
||||
change (reverse (concat (reverse xs) x) = x :: xs),
|
||||
rewrite [reverse_concat, reverse_reverse]
|
||||
|
|
@ -218,12 +218,12 @@ namespace vector
|
|||
/- list <-> vector -/
|
||||
|
||||
definition of_list {A : Type} : Π (l : list A), vector A (list.length l)
|
||||
| list.nil := nil
|
||||
| list.nil := []
|
||||
| (list.cons a l) := a :: (of_list l)
|
||||
|
||||
definition to_list {A : Type} : Π {n : nat}, vector A n → list A
|
||||
| zero nil := list.nil
|
||||
| (succ n) (a :: vs) := list.cons a (to_list vs)
|
||||
| 0 [] := list.nil
|
||||
| (n+1) (a :: vs) := list.cons a (to_list vs)
|
||||
|
||||
theorem to_list_of_list {A : Type} : ∀ (l : list A), to_list (of_list l) = l
|
||||
| list.nil := rfl
|
||||
|
|
@ -234,16 +234,16 @@ namespace vector
|
|||
end
|
||||
|
||||
theorem length_to_list {A : Type} : ∀ {n : nat} (v : vector A n), list.length (to_list v) = n
|
||||
| zero nil := rfl
|
||||
| (succ n) (a :: vs) :=
|
||||
| 0 [] := rfl
|
||||
| (n+1) (a :: vs) :=
|
||||
begin
|
||||
change (succ (list.length (to_list vs)) = succ n),
|
||||
rewrite length_to_list
|
||||
end
|
||||
|
||||
theorem of_list_to_list {A : Type} : ∀ {n : nat} (v : vector A n), of_list (to_list v) == v
|
||||
| zero nil := !heq.refl
|
||||
| (succ n) (a :: vs) :=
|
||||
| 0 [] := !heq.refl
|
||||
| (n+1) (a :: vs) :=
|
||||
begin
|
||||
change (a :: of_list (to_list vs) == a :: vs),
|
||||
have H₁ : of_list (to_list vs) == vs, from of_list_to_list vs,
|
||||
|
|
@ -259,8 +259,8 @@ namespace vector
|
|||
/- decidable equality -/
|
||||
open decidable
|
||||
definition decidable_eq [H : decidable_eq A] : ∀ {n : nat} (v₁ v₂ : vector A n), decidable (v₁ = v₂)
|
||||
| ⌞zero⌟ nil nil := inl rfl
|
||||
| ⌞succ n⌟ (a::v₁) (b::v₂) :=
|
||||
| ⌞zero⌟ [] [] := inl rfl
|
||||
| ⌞n+1⌟ (a::v₁) (b::v₂) :=
|
||||
match H a b with
|
||||
| inl Hab :=
|
||||
match decidable_eq v₁ v₂ with
|
||||
|
|
|
|||
Loading…
Reference in a new issue