Email Gateway (Aug 22 2022 at 13:01): Email Gateway (Aug 22 2022 at 13:01):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,
at the last section of a proof Isabelle/jEdit show the last proof method in colour, see the attachment. According to
http://stackoverflow.com/questions/22635300/what-do-colour-codes-mean-in-isabelle-jedit
the purple colour means that a prover process is still running.
Despite of this, I can finish the proof by qed and I get
theorem (?Xs::form list) ⇒ (?P::form) ⟹ ∃Ys::form list. Ys cf⇒ ?P
Is this a valid proof? Can I simply ignore this colouring?
I use vanilla Isabelle2016.
Email Gateway (Aug 22 2022 at 13:01):From: Lars Hupel <hupel@in.tum.de>
Hi Gergely,
the purple colour means that a prover process is still running.
proofs in Isar are "forked" by default. That means if you state a
proposition with "have" or "show", it will run the proof (in your
example, using "by") in the background. In order to increase
parallelism, it'll continue processing the remaining theory. It does
that by optimistically assuming that the proof will proceed, hence
"asserting" the statement. To notify the user that there are still some
pending proofs, Isabelle/jEdit uses the purple background.
Is this a valid proof? Can I simply ignore this colouring?
No, you can't. The system continues processing the rest of your theory
so that you can go on with your work, but that doesn't mean you can just
assume that everything still pending is ultimately correct.
Obviously the system doesn't know how long it should wait for the proof
to complete. That's up to the user to decide.
Cheers
Lars
Last updated: Nov 21 2024 at 12:39 UTC