The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

 Consider the following proof of well-founded induction:

Variable X : Type.
Variable r : X -> X -> Prop.
Variable p : X -> Prop.
Hypothesis H : forall x, (forall y, r y x -> p y) -> p x.
Fixpoint F x (t : Acc r x)  : p x :=
match t with Acc_intro g => H x (fun y R => F y (g y R)) end.

Coq claims that the recursive function F terminates
since it decreases its second argument.  I don't
understand this at all.  Certainly, h is smaller
than t, but why is (h y R) smaller than t?

- What is the intuition / justification behind the
termination argument?
- What are the special properties of the arguments y,R
that justify the claim?
- What paper could I read to understand?
- Where is guarded recursion as implemented in Coq defined?
- Where can I find a corresponding strong normalization proof?

Thanks for considering my questions.  -- Gert

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.

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)