Existential

寫兩個關於 existential quantifier 的簡單 functions。

attachLength : {A : Set} -> List A -> ∃ (\n -> List A ⋮ hasLength n)
attachLength [] = ∃-I 0 (sub [] len-base)
attachLength (x :: xs) with attachLength xs
... | ∃-I n (sub xs sublenpf) =
  ∃-I (suc n) (sub (x :: xs) (len-step sublenpf))

in-flatcat' : {A : Set} {m : Nat} ->
                Braun A m -> List A -> ∃ (\n -> List A ⋮ hasLength (m + n))
in-flatcat' b xs with attachLength xs
... | ∃-I n xs&lenpf = ∃-I n (in-flatcat b xs&lenpf)

其實這兩個 functions 的 type 都沒保證什麼，例如 attachLength 的 type 應該要類似這種東西

attachLength : {A : Set} -> (xs : List A) ->
                 ∃ (\n -> List A ⋮ hasLength n /\ equalTo xs)

才比較有意義（同時也帶來很大的 overhead XD）。（equalTo 要另外定義。）

--
今天真的就到這裡 XD。

---

為了不要虎頭蛇尾，還是把 attachLength 寫完 XD。

equalTo : {A : Set} -> (xs : List A) -> (ys : List A) -> Set
equalTo xs ys = ys ≡ xs

_∧_ : {A : Set} -> (A -> Set) -> (A -> Set) -> A -> Set
_∧_ P Q a = P a /\ Q a

attachLength : {A : Set} -> (xs : List A) ->
                 ∃ (\n -> List A ⋮ (hasLength n ∧ equalTo xs))
attachLength [] = ∃-I 0 (sub [] (/\-I len-base refl))
attachLength (x :: xs) with attachLength xs
... | ∃-I n (sub xs (/\-I sublenpf eqpf)) =
  ∃-I (suc n) (sub (x :: xs)
                   (/\-I (len-step sublenpf) (cong (\xs -> x :: xs) eqpf)))

在 Agda interpreter 底下的執行結果：

Main> :typeOf attachLength
(xs : List _401) ->
∃ (\n -> List _401 ⋮ (hasLength n ∧ equalTo xs))
Main> attachLength (7 :: 3 :: 5 :: 1 :: 8 :: 6 :: 4 :: 2 :: [])
∃-I 8
(sub (7 :: 3 :: 5 :: 1 :: 8 :: 6 :: 4 :: 2 :: [])
 (/\-I
  (len-step
   (len-step
    (len-step
     (len-step (len-step (len-step (len-step (len-step len-base))))))))
  refl))

因為我用 _≡_ 證明兩個 lists 相等，所以最後的 proof term 只有 refl，沒有什麼 overhead。（equalTo xs 的重點在於 function definition 裡面的 type conversion。）

--
其實也應該研究一下那些 operator precedence 的數字到底怎麼定？XD