The Coq mailing list

[Clement Renard <Clement.Renard AT inria.fr>]

On Fri, 7 Sep 2001, Carlos.SIMPSON wrote:

> Hi.
> Is it possible that Pablo Alberto's question basically comes down to
> the following problem:? in the Cases ... of construction, 
> Coq doesn't know that the variable is set to the value that you say.
> However, this is of course crucial for defining any recursive object,
> and in fact it has to work to get for example even nat_rec. This leads to 
> the
> situation where if you print out nat_rec and then try to
> write that same definition it is rejected. Hmmm...

I think the problem is a little different. In fact, your Cases ... of
expression is a dependent elimination and Coq cannot always infer the
predicate for dependent elimination. That means that Coq won't succeed in
unifying the types of the two branches of pattern matching. But if you
give the predicate it works :
 
> If you type 
> 
> 
> Coq < Inductive mynat : Set :=
> Coq < O : mynat | S : mynat -> mynat.
> 
> mynat_ind is defined
> mynat_rec is defined
> mynat_rect is defined
> mynat is defined
> 
> 
> Coq < Print mynat_rec
> Coq < .
> mynat_rec = 
> [P:(mynat->Set); f:(P O); f0:((m:mynat)(P m)->(P (S m)))]
>  Fix F
>    {F [m:mynat] : (P m) :=
>       Cases m of
>         O => f
>       | (S m0) => (f0 m0 (F m0))
>       end}
>      : (P:(mynat->Set))
>         (P O)->((m:mynat)(P m)->(P (S m)))->(m:mynat)(P m)
> 
> 
> Coq < 
> 
> now we recopy the supposed definition:
> 
> Coq < Definition new_mynat_rec :=     
> Coq < [P:(mynat->Set); f:(P O); f0:((m:mynat)(P m)->(P (S m)))]
>  Fix F
>    {F [m:mynat] : (P m) :=
>       Cases m of
>         O => f
>       | (S m0) => (f0 m0 (F m0))
>       end} .

Ok, now try :

Coq < Definition new_mynat_rec :=
[P:(mynat->Set); f:(P O); f0:((m:mynat)(P m)->(P (S m)))]
 Fix F
   {F [m:mynat] : (P m) :=
      < [p:mynat] (P p)>
      Cases m of
        O => f
      | (S m0) => (f0 m0 (F m0))
      end} .
new_mynat_rec is defined

 
> I tried this on a version 7 from last spring and it still produced
> an error message. I don't know if it now works in more recent versions.
> 
> The short version of this story is that inside a 
> Cases m of O => ??? etc.
> Coq doesn't "know" that here m is equal to O;
> however, of course that is essential to defining mynat_rec etc.
> and in fact if you use the proof engine you can obtain this type
> of definition, because it uses the result ..._rec rather than
> the Cases...of... expression. 
> 
> What's the latest scoop on this?

So, the problem is that type inference is too hard for Coq in such a
case. But I admit that Coq should not print term it cannot understand. We
will try to fix this in the next release.

Clement Renard