refactor(library/data/vector): define vector functions using recursive equations
This commit is contained in:
Leonardo de Moura
parent
87d41e90fc
commit
05e1fc21f6
1 changed files with 87 additions and 132 deletions
|
|
@ -5,192 +5,147 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Module: data.vector
|
||||
Author: Floris van Doorn, Leonardo de Moura
|
||||
-/
|
||||
import data.nat.basic
|
||||
open nat prod
|
||||
|
||||
import data.nat.basic data.empty data.prod
|
||||
open nat eq.ops prod
|
||||
|
||||
inductive vector (T : Type) : ℕ → Type :=
|
||||
nil {} : vector T 0,
|
||||
cons : T → ∀{n}, vector T n → vector T (succ n)
|
||||
inductive vector (A : Type) : nat → Type :=
|
||||
nil {} : vector A zero,
|
||||
cons : Π {n}, A → vector A n → vector A (succ n)
|
||||
|
||||
namespace vector
|
||||
notation a :: b := cons a b
|
||||
notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
|
||||
|
||||
variables {A B C : Type}
|
||||
variables {n m : nat}
|
||||
|
||||
protected definition is_inhabited [instance] (H : inhabited A) (n : nat) : inhabited (vector A n) :=
|
||||
nat.rec_on n
|
||||
(inhabited.mk nil)
|
||||
(λ (n : nat) (iH : inhabited (vector A n)),
|
||||
inhabited.destruct H
|
||||
(λa, inhabited.destruct iH
|
||||
(λv, inhabited.mk (a :: v))))
|
||||
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))
|
||||
|
||||
theorem z_cases_on {C : vector A 0 → Type} (v : vector A 0) (Hnil : C nil) : C v :=
|
||||
begin
|
||||
cases v,
|
||||
apply Hnil
|
||||
end
|
||||
theorem vector0_eq_nil : ∀ (v : vector A 0), v = nil,
|
||||
vector0_eq_nil nil := rfl
|
||||
|
||||
theorem vector0_eq_nil (v : vector A 0) : v = nil :=
|
||||
z_cases_on v rfl
|
||||
definition head : Π {n : nat}, vector A (succ n) → A,
|
||||
head (a::v) := a
|
||||
|
||||
protected definition destruct (v : vector A (succ n)) {P : Π {n : nat}, vector A (succ n) → Type}
|
||||
(H : Π {n : nat} (h : A) (t : vector A n), P (h :: t)) : P v :=
|
||||
begin
|
||||
cases v with (h', n', t'),
|
||||
apply (H h' t')
|
||||
end
|
||||
definition tail : Π {n : nat}, vector A (succ n) → vector A n,
|
||||
tail (a::v) := v
|
||||
|
||||
definition nz_cases_on := @destruct
|
||||
|
||||
definition head (v : vector A (succ n)) : A :=
|
||||
destruct v (λ n h t, h)
|
||||
|
||||
definition tail (v : vector A (succ n)) : vector A n :=
|
||||
destruct v (λ n h t, t)
|
||||
|
||||
theorem head_cons (h : A) (t : vector A n) : head (h :: t) = h :=
|
||||
theorem head_cons {n : nat} (h : A) (t : vector A n) : head (h :: t) = h :=
|
||||
rfl
|
||||
|
||||
theorem tail_cons (h : A) (t : vector A n) : tail (h :: t) = t :=
|
||||
theorem tail_cons {n : nat} (h : A) (t : vector A n) : tail (h :: t) = t :=
|
||||
rfl
|
||||
|
||||
theorem eta (v : vector A (succ n)) : head v :: tail v = v :=
|
||||
destruct v (λ n h t, rfl)
|
||||
theorem eta : ∀ {n : nat} (v : vector A (succ n)), head v :: tail v = v,
|
||||
eta (a::v) := rfl
|
||||
|
||||
definition last : vector A (succ n) → A :=
|
||||
nat.rec_on n
|
||||
(λ (v : vector A (succ zero)), head v)
|
||||
(λ n₁ r v, r (tail v))
|
||||
definition last : Π {n : nat}, vector A (succ n) → A,
|
||||
last (a::nil) := a,
|
||||
last (a::v) := last v
|
||||
|
||||
theorem last_singleton (a : A) : last (a :: nil) = a :=
|
||||
rfl
|
||||
|
||||
theorem last_cons (a : A) (v : vector A (succ n)) : last (a :: v) = last v :=
|
||||
theorem last_cons {n : nat} (a : A) (v : vector A (succ n)) : last (a :: v) = last v :=
|
||||
rfl
|
||||
|
||||
definition const (n : nat) (a : A) : vector A n :=
|
||||
nat.rec_on n
|
||||
nil
|
||||
(λ n₁ r, a :: r)
|
||||
definition const : Π (n : nat), A → vector A n,
|
||||
const 0 a := nil,
|
||||
const (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 :=
|
||||
nat.induction_on n
|
||||
rfl
|
||||
(λ n₁ ih, ih)
|
||||
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
|
||||
|
||||
definition map (f : A → B) (v : vector A n) : vector B n :=
|
||||
nat.rec_on n
|
||||
(λ v, nil)
|
||||
(λ n₁ r v, f (head v) :: r (tail v))
|
||||
v
|
||||
definition map (f : A → B) : Π {n : nat}, vector A n → vector B n,
|
||||
map nil := nil,
|
||||
map (a::v) := f a :: map v
|
||||
|
||||
theorem map_vnil (f : A → B) : map f nil = nil :=
|
||||
theorem map_nil (f : A → B) : map f nil = nil :=
|
||||
rfl
|
||||
|
||||
theorem map_vcons (f : A → B) (h : A) (t : vector A n) : map f (h :: t) = f h :: map f t :=
|
||||
theorem map_cons {n : nat} (f : A → B) (h : A) (t : vector A n) : map f (h :: t) = f h :: map f t :=
|
||||
rfl
|
||||
|
||||
definition map2 (f : A → B → C) (v₁ : vector A n) (v₂ : vector B n) : vector C n :=
|
||||
nat.rec_on n
|
||||
(λ v₁ v₂, nil)
|
||||
(λ n₁ r v₁ v₂, f (head v₁) (head v₂) :: r (tail v₁) (tail v₂))
|
||||
v₁ v₂
|
||||
definition map2 (f : A → B → C) : Π {n : nat}, vector A n → vector B n → vector C n,
|
||||
map2 nil nil := nil,
|
||||
map2 (a::va) (b::vb) := f a b :: map2 va vb
|
||||
|
||||
theorem map2_vnil (f : A → B → C) : map2 f nil nil = nil :=
|
||||
theorem map2_nil (f : A → B → C) : map2 f nil nil = nil :=
|
||||
rfl
|
||||
|
||||
theorem map2_vcons (f : A → B → C) (h₁ : A) (h₂ : B) (t₁ : vector A n) (t₂ : vector B n) :
|
||||
map2 f (h₁ :: t₁) (h₂ :: t₂) = f h₁ h₂ :: map2 f t₁ t₂ :=
|
||||
theorem map2_cons {n : nat} (f : A → B → C) (h₁ : A) (h₂ : B) (t₁ : vector A n) (t₂ : vector B n) :
|
||||
map2 f (h₁ :: t₁) (h₂ :: t₂) = f h₁ h₂ :: map2 f t₁ t₂ :=
|
||||
rfl
|
||||
|
||||
definition append (w : vector A n) (v : vector A m) : vector A (n ⊕ m) :=
|
||||
rec_on w
|
||||
v
|
||||
(λ (a₁ : A) (n₁ : nat) (v₁ : vector A n₁) (r₁ : vector A (n₁ ⊕ m)), a₁ :: r₁)
|
||||
-- Remark: why do we need to provide indices?
|
||||
definition append : Π {n m : nat}, vector A n → vector A m → vector A (n ⊕ m),
|
||||
@append 0 m nil w := w,
|
||||
@append (succ n) m (a::v) w := a :: (append v w)
|
||||
|
||||
theorem append_nil (v : vector A n) : append nil v = v :=
|
||||
theorem append_nil {n : nat} (v : vector A n) : append nil v = v :=
|
||||
rfl
|
||||
|
||||
theorem append_cons (h : A) (t : vector A n) (v : vector A m) :
|
||||
append (h :: t) v = h :: (append t v) :=
|
||||
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
|
||||
|
||||
definition unzip : vector (A × B) n → vector A n × vector B n :=
|
||||
nat.rec_on n
|
||||
(λ v, (nil, nil))
|
||||
(λ a r v,
|
||||
let t := r (tail v) in
|
||||
(pr₁ (head v) :: pr₁ t, pr₂ (head v) :: pr₂ t))
|
||||
definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n,
|
||||
unzip nil := (nil, nil),
|
||||
unzip ((a, b) :: v) := (a :: pr₁ (unzip v), b :: pr₂ (unzip v))
|
||||
|
||||
definition zip : vector A n → vector B n → vector (A × B) n :=
|
||||
nat.rec_on n
|
||||
(λ v₁ v₂, nil)
|
||||
(λ a r v₁ v₂, (head v₁, head v₂) :: r (tail v₁) (tail v₂))
|
||||
|
||||
theorem unzip_zip : ∀ (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂) :=
|
||||
nat.induction_on n
|
||||
(λ (v₁ : vector A zero) (v₂ : vector B zero),
|
||||
z_cases_on v₁ (z_cases_on v₂ rfl))
|
||||
(λ (n₁ : nat) (ih : ∀ (v₁ : vector A n₁) (v₂ : vector B n₁), unzip (zip v₁ v₂) = (v₁, v₂))
|
||||
(v₁ : vector A (succ n₁)) (v₂ : vector B (succ n₁)), calc
|
||||
unzip (zip v₁ v₂) = unzip ((head v₁, head v₂) :: zip (tail v₁) (tail v₂)) : rfl
|
||||
... = (head v₁ :: pr₁ (unzip (zip (tail v₁) (tail v₂))),
|
||||
head v₂ :: pr₂ (unzip (zip (tail v₁) (tail v₂)))) : rfl
|
||||
... = (head v₁ :: pr₁ (tail v₁, tail v₂),
|
||||
head v₂ :: pr₂ (tail v₁, tail v₂)) : ih
|
||||
... = (head v₁ :: tail v₁, head v₂ :: tail v₂) : rfl
|
||||
... = (v₁, head v₂ :: tail v₂) : vector.eta
|
||||
... = (v₁, v₂) : vector.eta)
|
||||
|
||||
theorem zip_unzip : ∀ (v : vector (A × B) n), zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v :=
|
||||
nat.induction_on n
|
||||
(λ (v : vector (A × B) zero),
|
||||
z_cases_on v rfl)
|
||||
(λ (n₁ : nat) (ih : ∀ v, zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v) (v : vector (A × B) (succ n₁)), calc
|
||||
zip (pr₁ (unzip v)) (pr₂ (unzip v)) = zip (pr₁ (head v) :: pr₁ (unzip (tail v)))
|
||||
(pr₂ (head v) :: pr₂ (unzip (tail v))) : rfl
|
||||
... = (pr₁ (head v), pr₂ (head v)) :: zip (pr₁ (unzip (tail v))) (pr₂ (unzip (tail v))) : rfl
|
||||
... = (pr₁ (head v), pr₂ (head v)) :: tail v : ih
|
||||
... = head v :: tail v : prod.eta
|
||||
... = v : vector.eta)
|
||||
|
||||
/- Length -/
|
||||
|
||||
definition length (v : vector A n) :=
|
||||
n
|
||||
|
||||
theorem length_nil : length (@nil A) = 0 :=
|
||||
theorem unzip_nil : unzip (@nil (A × B)) = (nil, nil) :=
|
||||
rfl
|
||||
|
||||
theorem length_cons (a : A) (v : vector A n) : length (a :: v) = succ (length v) :=
|
||||
theorem unzip_cons {n : nat} (a : A) (b : B) (v : vector (A × B) n) :
|
||||
unzip ((a, b) :: v) = (a :: pr₁ (unzip v), b :: pr₂ (unzip v)) :=
|
||||
rfl
|
||||
|
||||
theorem length_append (v₁ : vector A n) (v₂ : vector A m) : length (append v₁ v₂) = length v₁ + length v₂ :=
|
||||
calc length (append v₁ v₂) = length v₁ ⊕ length v₂ : rfl
|
||||
... = length v₁ + length v₂ : add_eq_addl
|
||||
definition zip : Π {n : nat}, vector A n → vector B n → vector (A × B) n,
|
||||
zip nil nil := nil,
|
||||
zip (a::va) (b::vb) := ((a, b) :: zip va vb)
|
||||
|
||||
theorem zip_nil_nil : zip (@nil A) (@nil B) = nil :=
|
||||
rfl
|
||||
|
||||
theorem zip_cons_cons {n : nat} (a : A) (b : B) (va : vector A n) (vb : vector B n) :
|
||||
zip (a::va) (b::vb) = ((a, b) :: zip va vb) :=
|
||||
rfl
|
||||
|
||||
theorem unzip_zip : ∀ {n : nat} (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂),
|
||||
@unzip_zip 0 nil nil := rfl,
|
||||
@unzip_zip (succ n) (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)) : {unzip_zip va vb}
|
||||
... = (a :: va, b :: vb) : rfl
|
||||
|
||||
theorem zip_unzip : ∀ {n : nat} (v : vector (A × B) n), zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v,
|
||||
@zip_unzip 0 nil := rfl,
|
||||
@zip_unzip (succ n) ((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 : {zip_unzip v}
|
||||
|
||||
/- Concat -/
|
||||
|
||||
definition concat (v : vector A n) (a : A) : vector A (succ n) :=
|
||||
vector.rec_on v
|
||||
(a :: nil)
|
||||
(λ h n t r, h :: r)
|
||||
definition concat : Π {n : nat}, vector A n → A → vector A (succ n),
|
||||
concat nil a := a :: nil,
|
||||
concat (b::v) a := b :: concat v a
|
||||
|
||||
theorem concat_nil (a : A) : concat nil a = a :: nil :=
|
||||
rfl
|
||||
|
||||
theorem last_concat (v : vector A n) (a : A) : last (concat v a) = a :=
|
||||
vector.induction_on v
|
||||
rfl
|
||||
(λ h n t ih, calc
|
||||
last (concat (h :: t) a) = last (concat t a) : rfl
|
||||
... = a : ih)
|
||||
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,
|
||||
@last_concat 0 nil a := rfl,
|
||||
@last_concat (succ n) (b::v) a := calc
|
||||
last (concat (b::v) a) = last (concat v a) : rfl
|
||||
... = a : last_concat v a
|
||||
end vector
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue