I thought that might come up, the idea that I missed pushed = {}. Since
this is describing an initialization section for the system, would pushed =
{} need to be a precondition? What I mean is is that when the subset pushed
is created or generated, the system may very well fill it with garbage, but
when the system initializes pushed must be set to the empty set. Does this
then still need to be a precondition or does this become just a by product
I have to prove of showing the preconditions of the init operation?


On Wed, Sep 19, 2012 at 5:18 PM, Roger Bishop Jones <> wrote:

> On Wednesday 19 Sep 2012 21:10, Jon Lockhart wrote:
> > I moved on to the next area of my specification, which is
> > the initializations of the states declared earlier, and
> > I am stuck on the first one. No errors or anything, just
> > not sure how to proceed to reduce the goal any further.
> > As of now I actually think what I have done is made the
> > goal more complex. Was using the z_"there exists"_tac to
> > try and eliminate portions so then I could feed the goal
> > a tac proving the last bit which is not a precondition.
> > Unfortunately using the "there exists" tactic increased
> > the goal length and just added more. I have tried
> > setting the values to other items with no avail either
> > in reducing the goal.
> z_exists_tac doesn't actually do much, it just substitutes
> in the witnesses you supplied.
> You have to do something else to actually simplify the
> result, usually rewrite.
> In this case asm_rewrite_tac simplifies the goal, and
> probably would have proved it if it was true.
> Looks to me like you missed a clause in the precondition:
>    pushed={}
> Roger
Proofpower mailing list

Reply via email to