The Coq mailing list

[Francois Pottier <Francois.Pottier AT inria.fr>]

Dear Jonas,

On Fri, Feb 24, 2012 at 11:19:37PM +0100, Jonas Oberhauser wrote:
> I'm relatively new to coq, so I might not have faced the type of
> problem you're experiencing.
> But when I face similar problems, I use "change" or one of its
> variants to appease simpl/compute (which was more likely to be the
> culprit in my cases anyway).

Thanks for your suggestion. "change" does work, but requires me to mention
the original term and the transformed term. I want to avoid this because I
am in a setting where I am developing a library and the terms are supplied
by the client -- hence, I don't know exactly, when writing this tactic,
what the terms will be.

Let me say a little bit more about what I am trying to do. I have a goal
whose form is roughly:

  f (C x) = ...

where C is a constructor of an inductive data type (say, "term") and where the
function is defined by induction over terms (i.e. it is a Fixpoint). However,
I (the library author) do not have access to the definition of "term", or to
the definition of "f". In fact, I don't even have access to the names "f" and
"C".

What I would like to do at this point is perform one step of reduction, that
is, reduce the application of f to (C x) by appealing to the definition of f
as a Fixpoint.

"simpl" or "simpl f" do this for me, but go too far (they do more than just
one reduction step). Using Opaque to control simpl was one solution I found.
I tried using "cbv", "lazy", etc. but without success. Is there a simple
tactic that allows me to point Coq to this redex and ask "please do just
one reduction step here"?

Thanks,

-- 
François Pottier
Francois.Pottier AT inria.fr
http://gallium.inria.fr/~fpottier/