The Coq mailing list

[AUGER Cedric <sedrikov AT gmail.com>]

Le Sat, 24 Mar 2012 22:34:34 -0500,
"Harley D. Eades III" 
<harley.eades AT gmail.com>
 a écrit :

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

I guess it is simply a notation problem.

'*' has type "nat -> nat -> nat" (usual multiplication, ie. 3*2=6)
'*' has type "Type -> Type -> Type"
    (usual cartesian product, ie. what you meant)

try "(fun _ : nat => (typ * trm)%type)" to enforce the scope notation
or "(fun _ : nat => prod typ trm)" to avoid notation

It is some classical problem, where coq prints stuff it cannot reparse
(often also occurs with implicit arguments).

If you want to copy/paste with less risk of this kind of error,
deactivate printing notations and activate printing of implicit
arguments.

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