From 27e58dc5349a84d027c9837c8bd7768ed40290a6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Mar 2015 22:25:21 -0700 Subject: [PATCH] refactor(library/data): cleanup vector and list modules --- library/data/list/basic.lean | 174 +++++++++++++++++------------------ library/data/vector.lean | 122 ++++++++++++------------ 2 files changed, 148 insertions(+), 148 deletions(-) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 24f6366e7..536830008 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -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, diff --git a/library/data/vector.lean b/library/data/vector.lean index 580d9b67e..c3b6d2dc4 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -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