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:
Proofpower mailing list