The Coq mailing list

[Judicael Courant <Judicael.Courant AT lri.fr>]

Le 2002.11.18 14:12, Jean-Francois Monin a écrit :
> Beware: my problem is not in the definition of the fixpoint
> but in its use.

Sure, but that is also what Pierre suggests I think.

I hope the following example will help:

Variable A : Set.
Variable a : A.
Inductive accessible : A -> Prop := C : (x:A)(accessible 
x)->(accessible x).

Fixpoint f [x:A; a:(accessible x)] : nat :=
(S (f x (<[a0:A](accessible a0)>Cases a of (C x0 H) => H end))).

The above definition is ok: thanks to the head-constructor condition, 
(f x (C^n H)) will reduce to (S^n (f x H)).

Eval Compute in (C a (wf a)).
Eval Compute in (f a (C a (wf a))).
Eval Compute in (f a (C a (C a (wf a)))).

If you add an inconsistent axiom such as

Axiom wf : (x:A)(accessible x).

and if you remove the head-constructor condition for the decreasing 
argument, then you can build terms that have no normal form:
(f a (wf a)) here.

Best,

Judicaël.
--
Judicael.Courant AT lri.fr,
 http://www.lri.fr/~jcourant/
Tel (+33) (0)1 69 15 64 85
GPG public key: 7C25 D439 9F60 BC68 A131  6267 98B9 98F6 7107 2457