The Coq mailing list

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

Hi folks,

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?

I'm using
 The Coq Proof Assistant, version 8.1 (Feb. 2007)
 compiled on Jun 08 2007 10:44:46

Thanks in advance,
Ezra


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