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

chore(library/data/vector): cleanup vector proofs

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-06 17:37:03 -08:00
parent 1490bdad49
commit 4fdac068b0
1 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
library/data/vector.lean
View file

@ -84,8 +84,8 @@ namespace vector
-- Remark: why do we need to provide indices? -- Remark: why do we need to provide indices?
definition append : Π {n m : nat}, vector A n → vector A m → vector A (n ⊕ m) definition append : Π {n m : nat}, vector A n → vector A m → vector A (n ⊕ m)
| @append 0 m nil w := w | 0 m nil w := w
| @append (succ n) m (a::v) w := a :: (append v w) | (succ n) m (a::v) w := a :: (append v w)
theorem append_nil {n : nat} (v : vector A n) : append nil v = v := theorem append_nil {n : nat} (v : vector A n) : append nil v = v :=
rfl rfl
@ -117,16 +117,16 @@ namespace vector
rfl rfl
theorem unzip_zip : ∀ {n : nat} (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂) 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 | 0 nil nil := rfl
| @unzip_zip (succ n) (a::va) (b::vb) := calc | (succ n) (a::va) (b::vb) := calc
unzip (zip (a :: va) (b :: vb)) unzip (zip (a :: va) (b :: vb))
= (a :: pr₁ (unzip (zip va vb)), b :: pr₂ (unzip (zip va vb))) : rfl = (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 :: pr₁ (va, vb), b :: pr₂ (va, vb)) : {unzip_zip va vb}
... = (a :: va, b :: vb) : rfl ... = (a :: va, b :: vb) : rfl
theorem zip_unzip : ∀ {n : nat} (v : vector (A × B) n), zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v theorem zip_unzip : ∀ {n : nat} (v : vector (A × B) n), zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v
| @zip_unzip 0 nil := rfl | 0 nil := rfl
| @zip_unzip (succ n) ((a, b) :: v) := calc | (succ n) ((a, b) :: v) := calc
zip (pr₁ (unzip ((a, b) :: v))) (pr₂ (unzip ((a, b) :: v))) zip (pr₁ (unzip ((a, b) :: v))) (pr₂ (unzip ((a, b) :: v)))
= (a, b) :: zip (pr₁ (unzip v)) (pr₂ (unzip v)) : rfl = (a, b) :: zip (pr₁ (unzip v)) (pr₂ (unzip v)) : rfl
... = (a, b) :: v : {zip_unzip v} ... = (a, b) :: v : {zip_unzip v}
@ -144,8 +144,8 @@ namespace vector
rfl rfl
theorem last_concat : ∀ {n : nat} (v : vector A n) (a : A), last (concat v a) = a theorem last_concat : ∀ {n : nat} (v : vector A n) (a : A), last (concat v a) = a
| @last_concat 0 nil a := rfl | 0 nil a := rfl
| @last_concat (succ n) (b::v) a := calc | (succ n) (b::v) a := calc
last (concat (b::v) a) = last (concat v a) : rfl last (concat (b::v) a) = last (concat v a) : rfl
... = a : last_concat v a ... = a : last_concat v a
end vector end vector