96 lines
3.4 KiB
Text
96 lines
3.4 KiB
Text
import data.nat
|
||
open nat
|
||
|
||
lemma addl_eq_add [simp] (n m : nat) : (:n ⊕ m:) = n + m :=
|
||
!add_eq_addl
|
||
|
||
-- Casting notation
|
||
notation `⟨`:max a `⟩`:0 := cast (by inst_simp) a
|
||
|
||
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
|
||
|
||
variable {A : Type}
|
||
|
||
private definition append_aux : Π {n m : nat}, vector A n → vector A m → vector A (n ⊕ m)
|
||
| 0 m [] w := w
|
||
| (succ n) m (a::v) w := a :: (append_aux v w)
|
||
|
||
theorem append_aux_nil_left [simp] {n : nat} (v : vector A n) : append_aux [] v == v :=
|
||
!heq.refl
|
||
|
||
theorem append_aux_cons [simp] {n m : nat} (h : A) (t : vector A n) (v : vector A m) : append_aux (h::t) v == h :: (append_aux t v) :=
|
||
!heq.refl
|
||
|
||
definition append {n m : nat} (v : vector A n) (w : vector A m) : vector A (n + m) :=
|
||
⟨append_aux v w⟩
|
||
|
||
section
|
||
|
||
theorem append_nil_left [simp] {n : nat} (v : vector A n) : append [] v == v :=
|
||
by unfold append ; inst_simp
|
||
|
||
theorem append_cons [simp] {n m : nat} (h : A) (t : vector A n) (v : vector A m) : (: append (h::t) v :) == (: h::(append t v) :) :=
|
||
by unfold append ; inst_simp
|
||
end
|
||
|
||
theorem append_nil_right [simp] {n : nat} (v : vector A n) : append v [] == v :=
|
||
by rec_inst_simp
|
||
|
||
attribute succ_add [simp]
|
||
|
||
theorem append_assoc [simp] {n₁ n₂ n₃ : nat} (v₁ : vector A n₁) (v₂ : vector A n₂) (v₃ : vector A n₃) : append v₁ (append v₂ v₃) == append (append v₁ v₂) v₃ :=
|
||
by rec_inst_simp
|
||
|
||
definition concat : Π {n : nat}, vector A n → A → vector A (succ n)
|
||
| concat [] a := [a]
|
||
| concat (b::v) a := b :: concat v a
|
||
|
||
theorem concat_nil [simp] (a : A) : concat [] a = [a] :=
|
||
rfl
|
||
|
||
theorem concat_cons [simp] {n : nat} (b : A) (v : vector A n) (a : A) : concat (b :: v) a = b :: concat v a :=
|
||
rfl
|
||
|
||
definition reverse : Π {n : nat}, vector A n → vector A n
|
||
| 0 [] := []
|
||
| (n+1) (x :: xs) := concat (reverse xs) x
|
||
|
||
theorem reverse_nil [simp] : reverse [] = @nil A :=
|
||
rfl
|
||
|
||
theorem reverse_cons [simp] {n : nat} (a : A) (v : vector A n) : reverse (a::v) = concat (reverse v) a :=
|
||
rfl
|
||
|
||
theorem reverse_concat [simp] : ∀ {n : nat} (xs : vector A n) (a : A), reverse (concat xs a) = a :: reverse xs :=
|
||
by rec_inst_simp
|
||
|
||
theorem reverse_reverse [simp] : ∀ {n : nat} (xs : vector A n), reverse (reverse xs) = xs :=
|
||
by rec_inst_simp
|
||
|
||
theorem append_reverse_cons [simp] {n : nat} (v : vector A n) : ∀ (m : ℕ) (w : vector A m) (a : A),
|
||
append v (reverse (cons a w)) == concat (append v (reverse w)) a :=
|
||
by induction v; inst_simp; inst_simp
|
||
|
||
theorem reverse_append [simp] : ∀ {n m : nat} (v : vector A n) (w : vector A m),
|
||
reverse (append v w) == append (reverse w) (reverse v) :=
|
||
by rec_inst_simp
|
||
|
||
definition vplus : Π {n : ℕ} (v₁ v₂ : vector ℕ n), vector ℕ n
|
||
| nat.zero [] [] := []
|
||
| (nat.succ m) (x::xs) (y::ys) := (x + y) :: vplus xs ys
|
||
|
||
lemma vplus.def1 [simp] : vplus [] [] = @nil ℕ := rfl
|
||
lemma vplus.def2 [simp] {n : ℕ} (v₁ v₂ : vector ℕ n) (a₁ a₂ : ℕ) : (: vplus (a₁ :: v₁) (a₂ :: v₂) :) = (a₁ + a₂) :: vplus v₁ v₂ := rfl
|
||
|
||
lemma vplus_weird {n₁ n₂ : ℕ} (v₁ : vector ℕ n₁) (v₂ : vector ℕ n₂) (a b : ℕ) :
|
||
vplus (a :: append v₁ v₂) ⟨b :: append v₂ v₁⟩ == (a + b) :: vplus (append v₁ v₂) ⟨append v₂ v₁⟩ :=
|
||
by inst_simp
|
||
|
||
end vector
|