41 lines
1.5 KiB
Text
41 lines
1.5 KiB
Text
import data.nat
|
|
import init.meta.tactic
|
|
open tactic
|
|
-- import init.meta.tactics
|
|
|
|
inductive vector (A : Type) : nat → Type :=
|
|
| nil {} : vector A 0
|
|
| cons : Π {n}, A -> vector A n -> vector A (nat.succ n)
|
|
|
|
definition vmap {A B : Type} (f : A -> B) : Π {n}, vector A n -> vector B n
|
|
| vmap vector.nil := vector.nil
|
|
| vmap (vector.cons x xs) := vector.cons (f x) (vmap xs)
|
|
|
|
definition vappend {A} : Π {n m}, vector A n -> vector A m -> vector A (m + n)
|
|
| vappend vector.nil vector.nil := vector.nil
|
|
| vappend vector.nil (vector.cons x xs) := vector.cons x xs
|
|
| vappend (vector.cons x xs) vector.nil := vector.cons x (vappend xs vector.nil)
|
|
| vappend (vector.cons x xs) (vector.cons y ys) := vector.cons x (vappend xs (vector.cons y ys))
|
|
|
|
check get_local
|
|
|
|
axiom Sorry : ∀ A, A
|
|
|
|
theorem vappend_assoc :
|
|
Π {A : Type} {n m k : nat} (v1 : vector A n) (v2 : vector A m) (v3 : vector A k),
|
|
vappend (vappend v1 v2) v3 == vappend v1 (vappend v2 v3) :=
|
|
by do
|
|
intros,
|
|
v <- get_local "v1",
|
|
induction_core semireducible v ("vector" <.> "rec_on") [],
|
|
v2 ← get_local "v2",
|
|
cases_using v2 ["m", "h2", "t2"],
|
|
trace_state, trace "------",
|
|
-- unfold only the first occurrence (i.e., the one of the form (vappend nil nil)
|
|
unfold_occs_of [1] "vappend",
|
|
trace_state, trace "------",
|
|
mk_const "Sorry" >>= apply,
|
|
-- unfold only the first occurrence (i.e., the one of the form (vappend nil (cons ...))
|
|
unfold_occs_of [1] "vappend",
|
|
trace_state, trace "------",
|
|
repeat $ mk_const "Sorry" >>= apply
|