Community, I started doing the "There Exist" proofs, and as you said they seem quite trivial indeed, but I seem to be stuck after the first two lines. So I have the goal, and it has been rewritten, now I am not sure what is the right question to ask. Do I do the z_"There Exist"_tac or something else? What constitutes a witness for some of the predicate declarations.
Attached is the spec and the output of the goal where I am at. Also the
original proof is in there for now, please just disregard I am leaving it
in there for the moment to show what I originally did to what I am now
going to with these "there exists" proofs. I am currently working on
"Button_State".
Roger,
Thank you for the catch, and I apologize about that. I am using pushed and
pushed everywhere else, I believe. I guess if I missed any they will come
up when I am trying to prove.
Regards,
Jon
On Mon, Sep 24, 2012 at 9:05 AM, Roger Bishop Jones <r...@rbjones.com> wrote:
> Jon,
>
> On Sunday 23 Sep 2012 22:32, Jon Lockhart wrote:
>
> > I tried adding the exclamation point to the end of the
> > pushed' line, but if gave me a paser error saying free
> > types here not allowed. I have provided exactly the what
> > the paragraph looked like I tried to parse and the error
> > that was reported in the errorEncountered document.
>
> The perils of not carefully quoting!
> The exclamation mark was not intended to be in the formal
> text, it was just my exclamation.
>
> The point I was making was just that you had said "push'={}"
> and it should have been "pushed'={}"!
>
> > I went back to just having the two exclamation points on
> > pushed and Button_State, in the predicate and
> > declaration section of the schema box respectively, and
> > this generated a monster of subgoals when I tried the
> > provided proof strategy. Obviously there should not be
> > that much to prove, especially when everything is the
> > same, except for push just being set to the empty set.
>
> Should be "pushed"!
>
> Make sure you have no occurrences of "push" and if you still
> have a problem with the proof post it.
>
> > I
> > have also gone back and reviewed Jacky's "The Way of
> > Zed" and he uses the delta operator to signify there are
> > changes being made to the states, though he never
> > discusses initialization, but there appears to be some
> > disconnect between the authors, though I know Spivey and
> > Woodcock should probably be followed so I like to stick
> > with what they say is best practice.
>
> I don't have access to Jacky's book so I can't comment.
>
> > As for the Init and State blocks that I am trying to and
> > have proven, should there be a change there so that the
> > proof is not of precondition but of consistency? As you
> > have mentioned, and I have agreed with, it is really
> > pointless to do the precondition proofs for the states
> > when they are static and not changing, everything
> > remains the same, and they are only showing the
> > information provided is consistent.
>
> Yes, try proving:
>
> ∃ Init ∙ true
> and
> ∃ State ∙ true
>
> Both should be trivial proofs.
>
> Roger
>
elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
errorEncountered.doc.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
