The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Adam,

That was my impression too, until I actually tried it. :)

I think at the very least one has to tell the Program mechanism where to put 
the casts, because, AFAIK, Program only wants to modify terms that it knows 
are supposed to be proofs. For instance, my first attempt was to try to write 
the following:

Program Definition foo (T: Set) (T__eq: T = nat) (f: T -> T) : nat :=
  (rew _ in f) 5

This just tells me that "rew _ in f” is not a function. My second attempt was 
this:

Program Definition foo1 (T: Set) (T__eq: T = nat) (f: T -> T) : nat :=
  ((rew _ in f) : _ -> _) 5.

This gives me an error message that it could not figure out what types to 
cast from what to what…

-Eddy

On Jul 1, 2015, at 10:12 AM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:

> My impression was that the Program mechanism does exactly what you're 
> suggesting.
> 
> On 07/01/2015 01:11 PM, Eddy Westbrook wrote:
>> All,
>> 
>> I am wondering if anyone has any ideas about getting Coq to insert casts 
>> into terms, either fully automatically or with some tactics and/or an 
>> OCaml module to process terms into a form that allows this. I imagine this 
>> sort of thing was part of the deduction modulo work; did this require some 
>> serious changes to the Coq kernel, or is it something that could be done 
>> with an OCaml module? Martin Hofmann also did something like this in his 
>> dissertation, but I am not sure if it has been implemented in a system 
>> like Coq…?
>> 
>> The specific case I am interested in is where I have zero or more 
>> equalities between a free variable and a term that does not contain that 
>> free variable. For example, I would like to be able to enter something 
>> like the following, and have it type-check:
>> 
>> Program Definition foo (T: Set) (T__eq: T = nat) (f: T -> T) : nat :=
>>   f 5.
>> 
>> One idea I had was to replace every occurrence of f with a cast to an 
>> unknown type using evars in place of T, as in something like the following:
>> 
>> ((rew ?e1 in f) : ?T1 -> ?T2)
>> 
>> Any idea if this sort of thing would work? Or does anyone have any other 
>> suggestions?
>> 
>> Any help along these lines would be greatly appreciated.
>> 
>> -Eddy
>