The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,


> PS. In Coq Art, there is a similar recursion
> (Acc_iter on page 294), but I could not find a
> single word of explanation why it terminates.


The explanation can be found p 171:

"Defining recursive functions over inductive types where some
constructors have functions as arguments is a natural generalization
of other kinds of structural recursive definitions.  The images of
functions that appear as arguments of the constructors are naturally
subterms of the whole term.  When these images are in the inductive
type, it is natural to allow recursive calls on these images."

This explanation was given in a section about inductive types
with functional fields, which is the case of Acc (with the function
you called g).

Pierre






> PPS. Here is a similar recursion that does
> not terminate (on a). Coq in fact rejects it:
>
> Inductive T : Prop := T_intro : (forall X : Prop, X -> X) -> T.
> Definition a : T := T_intro (fun X x => x).
> Fixpoint F (t : T) : False := match t with T_intro g => F (g T a) end.
>
> (inspired by http://coq.inria.fr/files/adt-2fev10-barras.pdf)