$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2007/10/31

### In-order Flatcat

data _⋮_ (A : Set) (P : (A -> Set)) : Set where
sub : (x : A) -> P x -> A ⋮ P


data HasLength {A : Set} : List A -> Nat -> Set where
len-base : HasLength [] 0
len-step : {xs : List A} {n : Nat} {x : A} ->
HasLength xs n -> HasLength (x :: xs) (suc n)


hasLength : {A : Set} -> Nat -> List A -> Set
hasLength n xs = HasLength xs n


lencat : {A : Set} {m n : Nat} ->
List A ⋮ hasLength m -> List A ⋮ hasLength n ->
List A ⋮ hasLength (m + n)
lencat (sub [] len-base) ys&pf = ys&pf
lencat (sub (x :: xs) (len-step subpf)) ys&pf with lencat (sub xs subpf) ys&pf
... | sub zs zspf = sub (x :: zs) (len-step zspf)


in-flatcat : {A : Set} {n m : Nat} -> Braun A m ->
List A ⋮ hasLength n -> List A ⋮ hasLength (m + n)
in-flatcat nul accum = accum
in-flatcat {A} (bin a p left right) accum with in-flatcat right accum
... | sub ys yslenpf = subst
(\x -> List A ⋮ hasLength x)
{! !}
(in-flatcat left (sub (a :: ys) (len-step yslenpf)))


{! !} 要給的 type 是 (suc (parity p + (.n + .n) + .n) ≡ parity p + .n + suc (.n + .n))，但我暫時兜不出來…

--

Labels: ,