The Coq mailing list

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

Hi, Gert,


Quoting 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?

In your example (definition of F),
g has type forall y, R y x -> Acc R y.
R  has type R y x

thus g y R has type Acc R y.

Since the constructor Acc_intro has a functional argument, g y R is a
subterm of t, and Coq accepts the Fixpoint definition. F is thus defined
by structural recursion on accessiblity proofs.

Pierre






> - 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)