Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Semantics of simpl

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Semantics of simpl


chronological Thread 
  • From: Kenneth Roe <kendroe AT hotmail.com>
  • To: Coq-Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Semantics of simpl
  • Date: Mon, 19 Dec 2011 19:30:44 -0800
  • Importance: Normal

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



Archive powered by MhonArc 2.6.16.

Top of Page