The Coq mailing list

[Ezra Cooper <e.e.k.cooper AT sms.ed.ac.uk>]

Matthieu Sozeau wrote:
> 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.

Mattieu--Great tips, thanks. This alternative proof worked out:

   Program Fixpoint f (n:nat) : {m | n < m} :=
     match n with
     | 0 => 1
     | S n => S(f n)
     end.
   Next Obligation.
    destruct (f n0).
    induction n0.
     apply lt_n_S; trivial.
    simpl; apply lt_n_S; trivial.
   Defined.


The original, for reference:

>   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.
>   Qed.

I suppose it was the [destruct (f 0)] in the original that caused 
problems; probably it couldn't determine that 0 was a subterm of the 
argument in that case.

Cheers,
Ezra

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.