The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

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