coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 |
- [Coq-Club] Semantics of simpl, Kenneth Roe
- Re: [Coq-Club] Semantics of simpl, Stéphane Glondu
Archive powered by MhonArc 2.6.16.