[Agda] Induction when the argument is wrapped in a constructor?
Shin-Cheng Mu
scm at iis.sinica.edu.tw
Thu Mar 20 09:13:18 CET 2008
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?
Is there a work around?
ps. To Nils Anders: if you remember, it is related to
what we discussed a while ago. The function f is what
I would like to use in an unfold. The argument i carries
some size information of xs. In general I would like to
write f of, for example, this type:
f : forall {i} -> Wrap (suc i) -> ⊤ ⊎ (ℕ × Wrap i)
I ran into trouble when f is defined inductively.
sincerely,
Shin
More information about the Agda
mailing list