Roger, Thanks for the input. I adjusted the predicate section of my specification to include that precondition requirement, and everything fell right into place.
Regards, Jon On Tue, Nov 6, 2012 at 3:17 PM, Roger Bishop Jones <r...@rbjones.com> wrote: > On Tuesday 06 Nov 2012 01:04, Jon Lockhart wrote: > > > Unfortunately I realized I > > needed to show that the starting and calling floors were > > greater than zero not greater than or equal to zero. > > However, this makes the goal false, so far as I can see. > You need to change the specification if you want this to be > the case. > > > I have modified my goal as such, and was able to prove the > > first sub goal. The third sub goal should be easy to get > > since it is exactly like what I was originally proving. > > I am having trouble though with the second goal, which > > the point I am at can be seen in the error encountered > > document I have provided. > > It looks exactly like goal one, but the linear arithmetic > > tactic fails to solve it, and I tired introducing a > > lemma through LEMMA_T, since I could not get lemma_tac > > working, and I would believe that should give the system > > enough to prove the goal, but apparently not. It > > logically makes since in my head. > > I think the reason linear arithmetic fails is because the > subgoal is false. > > It looks like you don't really understand what lemma_tac and > LEMMA_T do. > They do not do any useful proof work, they just help you to > organise your proof by proving and then using a lemma. > "lemma_tac" assumes you want to use the lemma by adding it > into your assumptions using strip_asm_tac, whereas LEMMA_T > allows you to specify how you are going to use the lemma. > In your proof, you say "asm_tac", which is like > "strip_asm_tac" except that it adds the lemma into the > assumptions without stripping it. > In both cases you have to prove the lemma yourself. > You can do that in the same step using THEN1 if you know a > tactic which will prove it in one step, otherwise THEN1 will > do the first step of the proof and you have to continue on > from there. > In your case, you could have solved that particular subgoal > if you had used linear arithmetic instead of just a rewrite, > but the lemma would not help you to solve goal 2, if (as I > suspect) its not true, > > You need to stipulate in your general operation predicate > the necessary constraints on the allowable input values. > > Roger Jones > > > > > > > > > > >
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
