Email Gateway (Aug 22 2022 at 20:55): Email Gateway (Aug 22 2022 at 20:55):From: Joshua Chen <joshua.chen@uibk.ac.at>
Dear list,
Can anyone explain the logic behind the behavior of the Isabelle/jEdit
automatic indentation? I've never been able to figure it out and always
have it disabled, from my point of view it indents and unindents with no
rhyme or reason. I'd be grateful to learn how to use it from those who
have it happily turned on in their daily work...
Best,
Josh
Email Gateway (Aug 22 2022 at 20:55):From: Lawrence Paulson <lp15@cam.ac.uk>
Indentation is a matter of taste, but perhaps you are talking about this phenomenon:
lemma "((P ⟷ Q) ⟷ R) ⟷ (P ⟷ (Q ⟷ R))"
apply (intro iffI)
apply simp_all
apply blast
apply blast
done
For apply-proofs, the indentation varies with the number of subgoals, the point being to inform the reader how many subgoals are present at that point in the proof. In the proof above, we can see that the first line generates many subgoals (six in fact) and the second line proves a bunch of them (four in fact), the remaining two proved one at a time. This information can be valuable when you are confronted with a proof that no longer works.
Larry Paulson
Email Gateway (Aug 22 2022 at 20:55):From: Makarius <makarius@sketis.net>
The Isabelle/jEdit documentation has a few explanations about indentation.
Ultimately this is a computer game, and the dynamics of it depends on
many side-conditions how you work with it.
The results should be crisp and clear for 98% of cases, following the
semantics of the language, especially for proofs, especially structured
proofs in Isar.
The less you invent diverging ideas about it, the better it will work.
Makarius
Email Gateway (Aug 22 2022 at 20:55):From: Joshua Chen <joshua.chen@uibk.ac.at>
The Isabelle/jEdit documentation has a few explanations about indentation.
Indeed, but unfortunately it's really too sketchy to be understandable
to someone who doesn't already have an idea of the answer.
The less you invent diverging ideas about it, the better it will work.
Not to mention that sometimes one works on a new thing, and hence needs
to know the precise workings of things in order to reliably determine if
the pre-existing order is suitable, or if one really needs to diverge
from canon. ;)
Josh
On 11/11/19 1:46 PM, Makarius wrote:
On 11/11/2019 12:14, Joshua Chen wrote:
Can anyone explain the logic behind the behavior of the Isabelle/jEdit
automatic indentation? I've never been able to figure it out and always
have it disabled, from my point of view it indents and unindents with no
rhyme or reason. I'd be grateful to learn how to use it from those who
have it happily turned on in their daily work...
The Isabelle/jEdit documentation has a few explanations about indentation.Ultimately this is a computer game, and the dynamics of it depends on
many side-conditions how you work with it.The results should be crisp and clear for 98% of cases, following the
semantics of the language, especially for proofs, especially structured
proofs in Isar.The less you invent diverging ideas about it, the better it will work.
Makarius
Email Gateway (Aug 22 2022 at 20:55):From: Joshua Chen <joshua.chen@uibk.ac.at>
(No offense intended Makarius, just teasing you a little) :p
Josh
Email Gateway (Aug 22 2022 at 20:56):From: Makarius <makarius@sketis.net>
We also have this mailing list to work out the details that remain unclear.
Which aspects precisely did you find confusing? The dynamics of
indentation, the result, or both? Proofs, specifications, something else?
Makarius
Email Gateway (Aug 22 2022 at 20:56):From: Peter Lammich <lammich@in.tum.de>
lemma "((P ⟷ Q) ⟷ R) ⟷ (P ⟷ (Q ⟷ R))"
apply (intro iffI)
apply simp_all
apply blast
apply blast
doneFor apply-proofs, the indentation varies with the number of subgoals,
the point being to inform the reader how many subgoals are present at
that point in the proof. In the proof above, we can see that the
first line generates many subgoals (six in fact) and the second line
proves a bunch of them (four in fact), the remaining two proved one
at a time. This information can be valuable when you are confronted
with a proof that no longer works.
This apply-indentation is, imho, also a matter of taste. I think it
looks horrible. Unfortunately, the Isabelle indentation cannot be
configured, but if you enable it, you get it all. This is why I do not
use it, though the indentation for the other commands is good. I use
the generic "simple indentation" mode of jedit, which will just indent
a new line to the indentation level of the last line.
Peter
Larry Paulson
On 11 Nov 2019, at 11:14, Joshua Chen <joshua.chen@uibk.ac.at>
wrote:
Can anyone explain the logic behind the behavior of the
Isabelle/jEdit
automatic indentation? I've never been able to figure it out and
always
have it disabled, from my point of view it indents and unindents
with no
rhyme or reason. I'd be grateful to learn how to use it from those
who
have it happily turned on in their daily work...
Email Gateway (Aug 22 2022 at 20:56):From: Makarius <makarius@sketis.net>
This is what the Isabelle/jEdit documentation says:
➧[Semantic indentation] adds additional white space to unstructured
proof
scripts via the number of subgoals. This requires information of ongoing
document processing and may thus lag behind when the user is editing too
quickly; see also option @{system_option_def "jedit_script_indent"} and
@{system_option_def "jedit_script_indent_limit"}.
For me the so-called "apply-style proofs" are not a proper part of the
fine Isar proof language and its high ambitions for style. Nonetheless,
I prefer to have that additional indentation enabled.
Further note that recent updates on Isar (2015/2016) have introduced the
'subgoal' command that gives better structure and less extra indentation
to "unstructured apply scripts".
Makarius
Email Gateway (Aug 22 2022 at 20:56):From: Peter Lammich <lammich@in.tum.de>
This is what the Isabelle/jEdit documentation says:
➧[Semantic indentation] adds additional white space to
unstructured
proof
scripts via the number of subgoals. This requires information of
ongoing
document processing and may thus lag behind when the user is
editing too
quickly; see also option @{system_option_def
"jedit_script_indent"} and
@{system_option_def "jedit_script_indent_limit"}.For me the so-called "apply-style proofs" are not a proper part of
the
fine Isar proof language and its high ambitions for style.
Fully agree, but apply scripts are very useful in certain situations,
where a simple proof can be done in a few straightforward steps, and an
Isar-script would mainly mean to copy around subgoals and thus
introduce redundancy (goal-cases and symbolic names like goal3(42),
imho, is worse than apply scripts).
Another very important part of apply scripts, that I feel is often
under-estimated, is rapid prototyping of proofs. I use apply scripts a
lot for exploring proofs, including all nasty (improper in Isabelle
parlance) features like
"case_tac [!] xs" or "rule_tac x=foo in exI", and even "back". Once I
have found a proof, I refactor it, either extracting lemmas or going to
an Isar-proof.
Side-note: Winning verification competitions like VerifyThis would not
have been possible without very dirty apply-scripts, as they can be
written much faster than Isar-proofs. For ProofGround, which was
focused on a different type of problems, Manuel apparently used Isar
from the beginning on, while I used apply-scripts, and both worked.
Nonetheless,
I prefer to have that additional indentation enabled.
As said, a matter of taste. I prefer a different indentation scheme, in
particular when prototyping.
Further note that recent updates on Isar (2015/2016) have introduced
the
'subgoal' command that gives better structure and less extra
indentation
to "unstructured apply scripts".
I actually use this a lot, and I think it is, next to Eisbach, one of
the greatest features introduced to Isabelle regarding rapid-
prototyping capabilities. The only caveat is that it does not work when
a schematic variable has to be instantiated. Luckily, this will not
occur very often for most proofs.
Email Gateway (Aug 22 2022 at 20:56):From: Lawrence Paulson <lp15@cam.ac.uk>
However, if you want to submit an entry to the AFP, this style is mandatory. We are the guys who usually end up keeping all the entries running :-)
Larry
Email Gateway (Aug 22 2022 at 20:56):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Hi,
I do agree with Peter on this.
The so called apply-style proofs is very useful in identifying proof
patterns that can be hidden behind a method later.
It is very useful in teaching as well, since it make the proofs looks like
a program with transitions steps made over the proof context. Therefore,
it is easier for students with no formal background to learn it (Peter has
a very successful experience by teaching Isabelle that way back in USA)!
Also, it is useful for advanced semantic frameworks with large scale
applications.
For example, projects such as Verisoft and seL4 have very large proofs that
use apply-style proof. The proofs are ugly in this kind of projects because
of the complicated and low level memory models of those systems!
In this kind of projects, you want to save time, and it is easier for
proof engineers to progress the proofs and at the same time identify proof
patterns with the so called "apply-style proofs" that can be hidden behind
a single method later in the development.
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 20:56):From: Makarius <makarius@sketis.net>
On 12 Nov 2019, at 10:06, Peter Lammich <lammich@in.tum.de> wrote:
This apply-indentation is, imho, also a matter of taste. I think it
looks horrible. Unfortunately, the Isabelle indentation cannot be
configured, but if you enable it, you get it all. This is why I do not
use it, though the indentation for the other commands is good. I use
the generic "simple indentation" mode of jedit, which will just indent
a new line to the indentation level of the last line.
Email Gateway (Aug 22 2022 at 20:57):From: Joshua Chen <josh@joshchen.io>
For type theory such a schematic_subgoal command is absolutely
indispensible, so allow me to point you to
https://github.com/jaycech3n/Isabelle-Spartan/blob/master/schematic_subgoal.ML
:)
This is basically the subgoal command code copy-pasted, with a
single-line tweak to change the proof mode to schematic (and possibly a
couple other small changes, I forget by now). It's been working fine for
me so far, though I'm sure more experienced people can tell me if
anything could go wrong...
Josh
Email Gateway (Aug 22 2022 at 20:57):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
I tend to use proof method expressions in such situations. If there are
exactly two methods to apply where the first one introduces “boring”
subgoals which are then discharged by the second one, I usually use
by ⟨first-method⟩ ⟨second-method⟩.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:57):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
This can work nicely on small goals, but if you start looking into verification of larger programs there is no really usable way around apply scripts in my opinion.
I don’t agree at all that apply scripts are less maintainable than Isar proofs in general. It is perfectly possible to write brittle and unmaintainable Isar proofs, and we do have some of these in the AFP (as well as in the seL4 verification). It is also perfectly possible to write nicely stable and maintainable apply scripts. I’ve maintained many of both over the last 15 years, and for both it takes work and some experience to write something maintainable.
Not that our seL4 proofs are shining examples of maintainability, there are many things I’d like to improve, but there are over a million lines of apply scripts in them, and while an Isabelle update usually takes us a few weeks, that is a small amount of time compared to the size of the proof. The entire AFP is only about twice the size, and if you add up the update work the Isabelle team puts in incrementally over time, I bet it will be larger even though the AFP has a much higher percentage of Isar proofs. Isar proofs do not necessarily show a greater resilience to change than apply scripts, they just are vulnerable to different kinds of change.
Isar as a language gives you mechanisms for writing proofs that are readable and understandable (which does tend to help with maintenance), but it is up to the user to actually do that properly, and it may not contribute to the purpose of the proof to be readable. There is often no point in making a proof in software verification specifically readable. There is often nothing interesting going on in vcg-style proofs, and their apply-script structure is usually obvious to someone who is used to them. This is different in mathematical-style proofs or maybe even for proofs about small interesting algorithms of some 10s of lines.
Using goal-based indentation is one of the key things in keeping apply scripts maintainable over time. Unless you extensively use Eisbach or other means to make sure that scripts break when goals are solved/not solved when they should, you will waste a lot of time finding the apply command that went wrong if something breaks after an update (I certainly have wasted such time in proofs that haven’t followed the convention).
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 20:57):From: Makarius <makarius@sketis.net>
When you say "absolutely" my first reflex is to try to disprove that,
and present a proof language with explicit structure and synthesized
parts in the reasoning.
Of course that is non-trivial: it is an open research problem that I
left over in 1999. I did not spend much thought on it in recent years --
in contrast to the other open research problem that is more important:
soft types within Isar proofs.
Just abstractly, scientific progress happens when you stop to accept
well-established workarounds and rethink problems from the ground up.
Makarius
Email Gateway (Aug 22 2022 at 20:58):From: Joshua Chen <joshua.chen@uibk.ac.at>
The main thing is the dynamics—in particular in theory declarations but
outside proofs. This is what happens to me when full indentation is
turned on:
If I never manually insert indents, new lines are never automatically
indented. This is at first fine. However, once I go to manually insert
an indent, say on line n, complete the line, and press RETURN to start
line n+1, PIDE will immediately unindent line n (to the same level as
line (n-1)). I then have to go back up one line to tell it "no, I
actually want line n indented!".
Now, suppose I've indented line n, have an empty line on line (n+1),
and want to start a new definition on line (n+2). Like so:
definition my_def :: "some_type"
where "my_def == defn"
definition I_want_a_new_def_here
...
Now when I first begin definition I_want_..., PIDE automatically
indents to the same level as the "where" statement above it. This
shouldn't happen since I'm starting a completely new logical block with
a new command, but it's not a big deal, I just immediately SHIFT+TAB to
unindent, right? But no, even after doing this, PIDE insists on
indenting (again!) after I RETURN to start line n+3.
All this basically means I have to do a lot of up and down keypressing,
entering content on line (n+1) before PIDE will grudgingly accept the
correct indentation level for line n. This is not a matter of "just
leave the automatic indentation to do its work", because it always
blindly insists on following the indentation level of the previous line,
while making it very difficult to unindent.
Josh
Last updated: Nov 21 2024 at 12:39 UTC