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

## 2007/10/31

### Existential

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)


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


--

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)))


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))


--

Labels: ,

yen311/01/2007 9:39 am 說：