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 
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

Reply via email to