there are nested patterns of dependent type and the
strategy builds a term that is well typed but recursive calls in fix
point are reported as illegal:
-
Error: Recursive call applied to an illegal term ...
This is because the strategy generates a term that is correct w.r.t.
to the initial term but which does not pass the guard condition. In
this situation we recommend the user to transform the nested dependent
patterns into several Cases of simple patterns. Let us
explain this with an example. Consider the following definition of a
function that yields the last element of a list and O if it is
empty:
Coq < Fixpoint last [n:nat; l:(listn n)] : nat :=
Coq < Cases l of
Coq < (consn _ a niln) => a
Coq < | (consn m _ x) => (last m x) | niln => O
Coq < end.
Error during interpretation of command:
Fixpoint last [n:nat; l:(listn n)] : nat :=
Cases l of
(consn _ a niln) => a
| (consn m _ x) => (last m x) | niln => O
end.
Error: Recursive call applied to an illegal term
The recursive definition last :=
[n:nat; l:(listn n)]
Cases l of
niln => O
| (consn n0 a a0) =>
Cases a0 of
niln => a
| (consn t1 t0 t) => (last (S t1) (consn t1 t0 t))
end
end is not well-formed
It fails because of the priority between patterns, we know that this
definition is equivalent to the following more explicit one (which
fails too):
Coq < Fixpoint last [n:nat; l:(listn n)] : nat :=
Coq < Cases l of
Coq < (consn _ a niln) => a
Coq < | (consn n _ (consn m b x)) => (last n (consn m b x))
Coq < | niln => O
Coq < end.
Note that the recursive call (last n (consn m b x)) is not
guarded. When treating with patterns of dependent types the strategy
interprets the first definition of last as the second
one1. Thus it generates a term where the
recursive call is rejected by the guard condition.
You can get rid of this problem by writing the definition with
simple patterns:
Coq < Fixpoint last [n:nat; l:(listn n)] : nat :=
Coq < <[_:nat]nat>Cases l of
Coq < (consn m a x) => Cases x of niln => a | _ => (last m x) end
Coq < | niln => O
Coq < end.
last is recursively defined