In-order Flatcat

練習用 dependent pair 表示 constraints or subtypes 。以下是 scm 老師的定義：

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

然後我寫了這個 proposition，其中 List 來自 Data.List module：

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)

然後寫一個 function，給定長度 n 就成為一個 predicate：

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

寫一個證明 length-preserving 的 list concatenation 很容易。

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)

接著 function in-flatcat 是把一個 Braun tree 以 in-order 走訪打平成一個 list 後接在給定的 list 前面，並附 length-preserving 的證明。

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))，但我暫時兜不出來…

--
今天先到這裡 XD。