The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

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

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

In our old 6.2.4 this produced the error expression : 

Toplevel input, characters 28-195
> [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} 
Error: The term
  [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 dum_m0) => (f0 dum_m0 (F dum_m0))
        end} failed to typecheck:
 Expansion strategy failed to build a well typed case expression.
 There is a branch that mistmatches the expected type.
 The risen type error on the result of expansion was:
  In Cases expression on term m the branch 1 has type (P O)
  which should be: (P m)

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?
---Carlos Simpson