The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I am running into an issue in that the semantics of simpl change when it is executed alone or within the context of a composite goal.  Here is an abstraction of a portion of a proof derivation: (I am executing three steps, "eapply simplifyPre," "simplifyState," and "simpl" as three separate commands. (For anyone interested in analyzing this problem in more detail, I am more than happy to send complete source files)

______________________________________(1/4)
{{AbsExists AbsNat ...}}
...
{{?54140, NoResult}}

eapply simplifyPre.

simplifyState 0 (AbsExists ...)) ?74918


______________________________________(2/5)
{{?74918}}
...
{{?54140, NoResult}}

simplifyState.

{{removeStateVar (AbsExists ...)}}
...
{{?54140, NoResult}}

simpl.

{{AbsExists ...}}
...
{{?54140, NoResult}}

Notice that in this first case above, that "removeStateVar" is evaluated by the simpl command.  It is a fixpoint function.  The first argument consisting of constructors of the form "Abs..." is a giant constant term. "removeStateVar" recursively traverses the term.

If instead of executing three separate commands, I combine them as follows:

    (eapply simplifyPre; [simplifyState|simpl]).

The resulting goal is:

{{removeStateVar (AbsExists ...)}}
...
{{?54140, NoResult}}

The "removeStateVar" function is not evaluated.  It appears that the behavior of simpl is changing.  What is causing this change?  Is there a way to cause "removeStateVar" to be evaluated in the latter case?

                           - Ken