The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Le 26 mai 08 à 21:46, Ezra Cooper a écrit :

> Hi folks,

Hi Ezra,

> Does the "Program Fixpoint" feature correctly bind the function- 
> being-defined within the proof obligations? It seems to be bind it  
> differently between the proof-editing mode and in the type-checking  
> mode, which would seem to be a bug--or perhaps I'm missing something.
>
> Here's an example program:
>
>   Require Import Arith.
>
>   Program Fixpoint f (n:nat) : {m | n < m} :=
>     match n with
>     | 0 => 1
>     | S n => S(f n)
>     end.
>   Next Obligation.
>    induction n0.
>     apply lt_n_S; destruct (f 0); trivial.
>    destruct (f (S n0)); simpl; apply lt_n_S; trivial.
>   Show Proof.
>   Qed.
>
>
> Upon hitting Qed, I get the following:
>
>   Error:
>   Recursive definition of f is ill-formed.
>   In environment
>   f : forall n : nat, {m : nat | n < m}
>   n : nat
>   n0 : nat
>   H : S n0 = n
>   Recursive call to f had not enough arguments
>
>
> The result of "Show Proof" is this:
>
>   LOC:
>   Subgoals
>   Proof: fun (f : forall n : nat, {m : nat | n < m}) (n n0 : nat)
>            (H : S n0 = n) =>
>          eq_ind (S n0) (fun n1 : nat => n1 < S (proj1_sig (f n0)))
>            (nat_ind (fun n1 : nat => S n1 < S (proj1_sig (f n1)))
>               (lt_n_S 0 (proj1_sig (f 0))
>                  (let s := f 0 in
>                   let (x, l) as s0 return (0 < proj1_sig s0) := s in  
> l))
>               (fun (n1 : nat) (_ : S n1 < S (proj1_sig (f n1))) =>
>                let s := f (S n1) in
>                let (x, l) as s0 return (S (S n1) < S (proj1_sig s0))
>   := s in
>                lt_n_S (S n1) x l) n0) n H
>
>
> which typechecks ok; but perhaps this is not the term that is being  
> typechecked at Qed.
>
> Is this a bug or am I misunderstanding what's going on? Is it  
> possible to refer to the function-being-defined within the proof  
> obligations?

This is not a bug, but a common (documented) problem with structurally  
recursive definitions made with Program. If you finish an obligation  
in which the recursive prototype appears you should not use Qed but  
Defined, making the proof transparent so that the guardness check can  
be done. If you do that, you will find that you are actually doing non- 
structurally smaller calls in your obligation (calling [f (S n1)] at  
some point, or [f 0]).
The problem here is that you have a recursive call in your goal, which  
you should destruct before trying to solve the goal, using [destruct  
(f n0)] for example. After fixing that, your definition goes through.

The forthcoming version has a [Preterm] command that shows the real  
term fed to Coq for debugging cases like this. It also makes  
everything transparent by default to avoid this sort of problems and  
let proofs reduce. It cannot force the use of Defined instead of Qed  
though :)
--
Matthieu Sozeau
http://www.lri.fr/~sozeau