[Agda] Induction when the argument is wrapped in a constructor?

[Shin-Cheng Mu]

Dear Nils,

Thank you very much! I have not yet studied Logic.Induction.Nat
and <-rec but I shall do soon so and try to understand the code.

After discussion with people in DTP, I was suggested at least
three ways to model terminating unfolds. I hoped to post a
comparison and summary on my blog, but right now I am still
struggling with all these small obstacles here and there.
Hope I will figure them all out soon.

Thanks again!

On Mar 27, 2008, at 12:41 AM, Nils Anders Danielsson wrote:
>
>  open import Logic.Induction.Nat
>
>  data Split (P : Set -> ℕ -> Set) (a : Set) : ℕ -> Set where
>    nul : Split P a 0
>    tip : a -> Split P a 1
>    bin : forall {n l r} -> l <′ 2 + n -> r <′ 2 + n ->
>          P a l -> P a r -> Split P a (2 + n)
>
>  unfold : forall {a} (P : Set -> ℕ -> Set) ->
>           (forall {i} -> P a i -> Split P a i) ->
>           forall {n} -> P a n -> Tree a
>  unfold {a} P f {n} p = <-rec Pred helper n p
>    where
>    Pred = \n -> P a n -> Tree a
>
>    helper : forall n -> <-Rec Pred n -> Pred n
>    helper n             rec p with f p
>    helper zero          rec p | nul               = Nul
>    helper (suc zero)    rec p | tip x             = Tip x
>    helper (suc (suc n)) rec p | bin le₁ le₂ p₁ p₂ =
>      Bin (rec _ le₁ p₁) (rec _ le₂ p₂)
>
> Then you can easily define split:
>
>  split : forall {a n} -> Vec a n -> Split Vec a n
>  split []           = nul
>  split (x ∷ [])     = tip x
>  split (y ∷ z ∷ xs) with split xs
>  ... | nul               = bin ≤′-refl ≤′-refl           (y  
> ∷ [])     (z ∷ [])
>  ... | tip x             = bin ≤′-refl (≤′-step ≤′-refl)  
> (y ∷ x ∷ []) (z ∷ [])
>  ... | bin le₁ le₂ ys zs = bin le₁'    le₂'              (y  
> ∷ ys)     (z ∷ zs)
>    where
>    le₁' = ≤′-step (s≤′s le₁)
>    le₂' = ≤′-step (s≤′s le₂)