The Coq mailing list

["Harley D. Eades III" <harley.eades AT gmail.com>]

Hi, everyone.

Currently, I am formalizing some work I did using the hereditary substitution function.  

I have it defined using "Program Fixpoint" along with the experimental "wf" annotation.

The function is definable with every proof obligation satisfied, except for the last obligation

which is to show that my ordering is well-founded.  Now I have a lexicographic ordering consisting

of the strict subexpression ordering on types and then on terms.  I can even prove it well founded.

That is, the following lemma holds:

Lemma lex_acc : forall p, Acc lex p.

However, I still need to push through the final obligation of the function.  Coq generates the following 

proof obligation:

      well_founded

       (MR lex

       (fun recarg : sigT (fun _ : trm => sigT (fun _ : nat => typ * trm)) =>

         projT2 (projT2 recarg))).   

Now if I take this goal and state it as a new lemma:

Lemma lex_wf : 

    well_founded

    (MR lex

      (fun recarg : sigT (fun _ : trm => sigT (fun _ : nat => typ * trm)) =>

        projT2 (projT2 recarg))).   

Coq rejects the definition as being ill-formed.  With the following error:

The term "typ" has type "Set" while it is expected to have type "nat".

Where "typ" is the first occurrence of "typ" in the second argument to MR.

So my question is, is this a bug?  Shouldn't my obligation be a well-formed type even

when I state it as a lemma?

If anyone needs more information about my ordering or function definition please let me know.

Thanks,

Harley