The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

I am a afraid my message from yesterday night was a bit confusing, 
because a few sentences were
missing.
> Coq's inferred recursion principle for X is not the "reference".  The 
> mechanism at work inside
> the verification of guards for recursive definition is the reference.  
> The inferred recursion principle
> that is given by Coq for an arbitrary inductive definition is a 
> helper, but it does not capture the
> whole expressive power.
>
> This is why you can devise your own recursion principles that may turn 
> out to be more powerful
> than the ones provided by default by Coq.

Here, I wanted to say:

If you define a map function in the following way:
> Fixpoint map1 (A B:Type)(f:A->B) (l:list A) : list B :=
>  match l with nil => nil | a::tl => f a::map1 A B f tl end.
>
> You don't get the same value as if you write
>
> Section map_def.
>
> Variables (A B:Type)(f:A->B).
>
> Fixpoint map2 (l:list A) : list B :=
>  match l with nil => nil | a::tl => f a::map2 tl end.
>
> End map_def.

The function map1 contains recursive calls where f occurs without being 
applied
to an argument, while map2 contains no such recursive call.  For this 
reason,
> a recursive function on your type X based on map2 will pass the guard 
> checking test,
> while a recursive function on the same type based on map1 will not.

Now, we can verify that the map function defined in the List library is 
defined like map1,
not like map2, just by typing the following lines:

Require Import List.
Print map.

or by browsing the sources.
> One more explanation: when performing guard-checking, the Coq system 
> will unfold
> functions as necessary to expose recursive calls and check that they 
> are always applied,
> and that they are always applied to structural sub-terms,
> where structural sub-terms are defined through a recursive process:
>
> - a variable obtained by pattern-matching from a structural sub-term 
> is a structural sub-term,
> - a variable obtained by pattern-matching from the initial structural 
> argument is a structural sub-term,
> - the structural variable of a fix expression, when this fix 
> expression is applied to a structural sub-term,
>   is a structural subterm,
> - a pattern-matching construct where all branches are structural 
> subterm is a structural sub-term,
>
> My explanation here may be slightly flawed, but I hope you get an 
> idea.  Note that your use of map
> falls in 3rd point above, while well-founded recursion works mainly 
> because of the 4th point.
>
> In principle, this allows for "match (t:False) with end" to be 
> accepted as a structural sub-term in any
> function.  I use this a lot.
>
> I hope this helps,
>
> Yves
I am afraid my message from yesterday did not help: I was in a hurry to 
leave and fetch my kid out of school.

Yves