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

[Ulf Norell]

On Thu, Mar 20, 2008 at 9:13 AM, Shin-Cheng Mu <scm at iis.sinica.edu.tw>
wrote:

> Hi,
>
> Why does this function not pass the termination check,
> and is there a work around?
>
> The function f, defined below, is defined inductively
> on its input, in principle. The twist is that I would
> like to wrap the list in a type constructor Wrap, carrying
> some extra information about the list in the type:
>
>   data Wrap : ℕ -> Set where
>     W : (xs : [ ℕ ]) -> (bnd : ℕ) -> Wrap bnd
>
>   lemma : ℕ -> ℕ
>   lemma = {! !}    -- definition not relevant and omitted
>
> The following (simplified) function f merely returns 0.
>
>   f : forall {i} -> Wrap i -> ℕ
>   f {i} (W [] .i) = 0
>   f {i} (W (x ∷ xs) .i) with lemma i
>   ... | j with f {j} (W xs j)
>   ...        | _ = 0
>
> When the argument is x ∷ xs, one recursive call is made
> on xs and j, some information computed from i. Although
> the argument of f does reduce (from x ∷ xs to xs), Agda
> cannot determine its termination. Is it because xs is
> wrapped in W?
>

Yes, kind of. The real problem is the with. When you say "with lemma i", it
translates to a call to an auxiliary function "aux {i} x xs (lemma i)". In
the body of aux you then call "f {j} (W xs j)", so the calls you make are
(simplified): "f (W (x :: xs)) --> aux xs --> f (W xs)". The detour through
"aux xs" is what throws the termination checker off.


> Is there a work around?


I suppose you could try to unwrap. Maybe something like

data Wrap : List N -> N -> Set where
  W : forall {xs} bnd -> Wrap xs bnd

f : forall {i} -> (xs : [ N ]) -> Wrap xs i -> N
f {i} [] _ = []
f {i} (x :: xs) (W .i) with lemma i
... | j with f {j} xs (W j)
...     | _ = 0

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080320/b0b51d2c/attachment.html