Email Gateway (Aug 22 2022 at 14:27): Email Gateway (Aug 22 2022 at 14:27):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Makarius,
I use "moreover then have" a lot (mostly as the first "moreover"-step).
But in the RC "then" is highlighted in red, which tells me that I
shouldn't do this. Why?
Also
moreover have "..." using 1
is okay, while in
from 1 moreover have "..."
'moreover' and 'have' are highlighted in red. Shouldn't both forms
essentially be the same?
cheers
chris
Email Gateway (Aug 22 2022 at 14:28):From: Makarius <makarius@sketis.net>
Conceptually, Isar has a primary thread of facts called "this" and a
secondary one called "calculation". There are certain policies how
"this" vs. "calculation" are updated, going back to my PhD thesis,
various papers, and the official isar-ref manual.
At some point in history, there was an unfinished experiment that broke
this scheme. It was never documented and I have never seen better proofs
coming from it.
The red markup indicates such "improper Isar" that should be avoided if
you care about doing things properly.
Again, the update to Isar 2016 may be taken as an opportunity to brush
up old proof styles. It will lead to an overall improvement.
Makarius
Email Gateway (Aug 22 2022 at 14:29):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Makarius,
Makarius wrote:
None of the above (nor the remainder of your email) explains what is
wrong with "moreover then have". As I understand it, "moreover" updates
the calculation, and "then" chains the same fact into the next goal.
This is useful. Which principle is violated here?
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 14:29):From: Makarius <makarius@sketis.net>
When the calculational elements were introduced in Isar around
1999/2000, there was certain explicit structure to make sure that the
use of "this" for "calculation" resets the former. This structure was
lost in a later (undocumented) experiment. The highlighting as
"improper" reverses that to some extent, although it would have been
better to remove that feature altogether.
What is particularly bad about "moreover then have" is the implicit fork
of the flow of facts. I find it very hard to read and maintain such
proofs, so they are now formally marked as non-Isar. (The old experiment
to allow that intermittendly was based on the claim "Isar allows
arbitrarily bad proofs anyway".)
Isar is generally based on the principle "structure emerges from taking
arbitrariness away". The brush-up of Isar 2016 was a good opportunity to
emphasize this principle again (and more).
As usual, it might require some efforts to discontinue old habits, but
the Isar 2016 style as a whole leads to better structured and more
concise proofs in all examples that I have cleaned up recently.
It might actually help to proceed under the assumption that Isar 2016 is
a new proof language for Isabelle, not just 10-20 small add-ons and
reforms to the old one.
Makarius
Last updated: Apr 25 2024 at 16:19 UTC