Re: [isabelle] Calculational reasoning proof structure



That pops up sometimes if you've flipped one of the inequalities e.g.

have "a = b" .
also have "c = b" .

Dave

On 20/08/14 08:21, Vadim Zaliva wrote:
Somehow related question:

Why switching from second form to calculation one (using "also have")
I ocaasionally get "*** Vacuous calculation result" error. Any common
reasons for such problem?

Vadim



On Aug 19, 2014, at 11:35 , Vadim Zaliva <vzaliva at cmu.edu> wrote:

Hi!

I am doing a proof which includes series of steps. Something like this:

have "x0 = x1"
also have "... = x2"
also have "... = x3"
...
finally have "x0=xN"

The proof is rather long and sometimes I need to prove some intermediate facts
between the steps to get to the next one. This breaks the computation chain and I could not
use "..." in the next step. What is the common way of dealing with such proofs?
Right now I am forced to do something like this:


have "x0 = x1"
hence s2:"x0=x2"

have "some fact"

hence "x0 = x3" using s2
...
hence "x0=xN"

Thanks!

Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva


Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.