The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Le 25 mars 09 à 13:11, Adam Koprowski a écrit :

>     Dear all,

Dear Adam,

>   I find the new Program tactic an extremely useful and powerful  
> tool, however I do have some problems with it every once in a while.  
> Let me illustrate it on an example - maybe some of you will be able  
> to shed some light on my problems.
>
>   I want to define a function [check_n n P] that given a natural  
> number [n] and a predicate [P : nat -> bool] checks whether [P]  
> holds for all [i < n]. Easy enough, so to make things more  
> interesting, say I also want to restrict the domain of [P] to  
> numbers smaller than [n]. My first attempt was the following:
>
> Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p :  
> nat) :
>   Exc (forall (p : { i | i < n}), P p = true) :=
>   match le_lt_dec n p with
>   | left _ => value _
>   | right cmp =>
>       if P p then
>         check_n P (S p)
>       else
>         error
>   end.
>
>   Now Program tells me that it cannot infer the termination  
> criteria. Fair enough. So I add the following annotation:
>
> {measure (fun i => n - i) p}
>
>   The first unpleasant effect of this is that this actually changes  
> the arguments of check_n (due to inner workings of handling of  
> termination with measure by Program, I believe) and hence the  
> recursive call needs to be changed. Too bad, but based on the error  
> message it's possible to figure out what is expected and I change  
> the recursive call to:
>
> check_n (S p)
>
>   (Why did P become implicit??).

This is indeed due to the way well-founded definitions are encoded,  
using
a combinator that provides a functional for recursive calls whose first
argument is the recursive argument. The way it is handled right now  
forces
all the previous arguments to stay constant during recursive calls.  
Also,
the measure function may refer only to those arguments, and not the ones
following the recursive argument. These two problems could be fixed  
simply
by curryfying.

> Now the definition is accepted but I realize that to prove the  
> obligations I will need to strengthen the specification of  
> [check_n]. So I finally arrive at:
<snip/>
>   Invoking [intros] doesn't work which is the first indication that  
> something funny is going on, but still it's not difficult to give a  
> proof:
>
>   intro H. intros. apply H0. destruct p0. simpl. omega.
> Qed.

Yes, [intros] failing is a sign of ill-typedness. This (deBruijn) bug  
is due
to some tricky manipulations related to the above problem. Please  
report it.

-- Matthieu