Email Gateway (Aug 19 2022 at 15:28): Email Gateway (Aug 19 2022 at 15:28):From: Vadim Zaliva <vzaliva@cmu.edu>
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
Email Gateway (Aug 19 2022 at 15:28):From: Salomon Sickert <sickert@in.tum.de>
Hi,
In such cases I often use the following pattern:
have "x0 = x1"
by ...
also
have "... = x2"
proof
...
show ?thesis
by ...
qed
also
have "... = x3"
by ...
finally
have "x0 = x3" .
I hope this solves your problem.
Greetings,
Salomon Sickert
signature.asc
smime.p7s
Email Gateway (Aug 19 2022 at 15:29):From: Vadim Zaliva <vzaliva@cmu.edu>
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
Sincerely,
Vadim Zaliva
Email Gateway (Aug 19 2022 at 15:29):From: David Cock <davec@cse.unsw.edu.au>
That pops up sometimes if you've flipped one of the inequalities e.g.
have "a = b" .
also have "c = b" .
Dave
Email Gateway (Aug 19 2022 at 15:29):From: Lars Noschinski <noschinl@in.tum.de>
Of course, the last "..." needs to be replaced by "x2". If you don't want to copy the term, you can also use term bindings with have:
have "t1 = f t2" (is "_ = f ?t")
This binds the term t2 to ?t.
Lars Noschinski <noschinl@in.tum.de> schrieb:
Email Gateway (Aug 19 2022 at 15:29):From: Lars Noschinski <noschinl@in.tum.de>
Hi Vadim,
I often follow the pattern outlined by Salomon or put the intermediate
facts before the calculational chain (actually, one could even put them
at the very end of the proof, using "presume" -- is there anybody using
that?)
BTW, your problem stems not from "..." (which is just an abbreviation
for the last right-hand-side -- you could also enter it manually).
Howevere, there is no sensible place for the "also" (which takes the
facts "calculation" and "this" to produce a new "calculation").
However, you can use "note" to manipulate "this"; but I am not sure I
like this idea (because it destroys the nice calculation sequence).
Something like the following should work:
have "x0 = x1"
also have *: "... = x2"
have "some fact"
note *
also have "... = x3" using s2
...
finally have "x0=xN"
-- Lars
signature.asc
Email Gateway (Aug 19 2022 at 15:29):From: Lars Noschinski <noschinl@in.tum.de>
Your calculation steps are not making any progress. Have a look at the
thread titled "A bug in chained proof mode" (it's not a bug) on this
mailing list, starting 2014-06-11.
-- Lars
Email Gateway (Aug 19 2022 at 15:30):From: Joachim Breitner <breitner@kit.edu>
Hi,
I use {...} for that:
have "A = B" sorry
also
have "… = C" sorry
also
{ have "foo" sorry
hence "bar" sorry
}
hence "… = D" sorry
also
have "… = E" sorry
finally have "A = E".
Greetings,
Joachim
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC