Email Gateway (Aug 22 2022 at 09:54): Email Gateway (Aug 22 2022 at 09:54):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Updating lots of proofs to Isabelle2015-RCx and discussions about submission rules for the AFP inspired me to write up guidelines that may be of more widespread use and interest:
http://proofcraft.org/blog/isabelle-style.html
There’s more to come. Feedback welcome.
Enjoy!
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:56):From: Larry Paulson <lp15@cam.ac.uk>
These are nice guidelines, but there is one difficulty with the idea that “auto” should only be allowed at the end of a proof: it was designed to be used at the start of proofs! It is supposed to solve all the easy parts of the problem, returning the difficult ones to the user.
There is a way out of this paradox: use “auto” to start the proof, but regard the resulting subgoals as separate lemmas that need to be proved first. Combining these proved lemmas with “auto” should solve the problem outright, and you have created a structured proof.
If you have just completed a proof after many hours of effort, it is awfully tempting to leave it in that just-finished state, however messy it may be. But you have already done the hard work, and it’s worth taking another 15 minutes to restructure the proof to make it legible and robust against future changes.
Larry
Email Gateway (Aug 22 2022 at 09:56):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Thanks for putting what I was thinking that a lot more clearly. Peter Gammie had a similar point on the Isar side.
I’ll include your example if that’s fine with you.
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 09:56):From: "C. Diekmann" <diekmann@in.tum.de>
Great guide.
I randomly looked at HOL/MicroJava/Comp/AuxLemmas.thy and
HOL/MicroJava/Comp/Index.thy from the Isabelle2015 distribution.
Those theories definitely need some rework.
Cornelius
Email Gateway (Aug 22 2022 at 09:56):From: Peter Lammich <lammich@in.tum.de>
Very nice styleguide! It very much matches what I am trying to do in my
proofs, too. Except for the apply-indentation scheme, where I use
somewhat different:
If a method produces n new subgoals, the next apply-steps will be
indented one level, and grouped into n blocks by blank lines, where each
block solves one of the subgoals:
apply (intro conjI) // produces 3 subgoals
apply auto [] // Solves first one
apply (cases l) // Solve 2nd one
apply clarsimp // Solve Nil-case
apply force
apply auto [] // Solve Cons-case
apply force // Solve 3rd subgoal
done
Email Gateway (Aug 22 2022 at 09:57):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Good old MicroJava, almost proof archeology now.
At least the type compiler were not my own proofs, otherwise that would be mildly embarrassing :-)
I’ve brushed them off a little in the development repository, but there is easily more modernisation to be done to them if anybody feels like it.
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 09:57):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
On 27.05.2015, at 19:40, Peter Lammich <lammich@in.tum.de> wrote:
Very nice styleguide!
Thanks!
It very much matches what I am trying to do in my
proofs, too. Except for the apply-indentation scheme, where I use
somewhat different:If a method produces n new subgoals, the next apply-steps will be
indented one level, and grouped into n blocks by blank lines, where each
block solves one of the subgoals:apply (intro conjI) // produces 3 subgoals
apply auto [] // Solves first oneapply (cases l) // Solve 2nd one
apply clarsimp // Solve Nil-case
apply forceapply auto [] // Solve Cons-case
apply force // Solve 3rd subgoal
done
I use something like this only when I have a large number of subgoals (> 40 or so). Even then, I use the standard indentation within the blocks (with an offset, basically).
In this case, for the “clarsimp", it’s hard to tell that it solves a goal, and for the “cases", it’s hard to tell how many subgoals it produces. Unless you really always have the comments -- then it’s fine, but I’m way too lazy for that many comments...
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:58):From: Lars Hupel <hupel@in.tum.de>
Is there a reason why MicroJava isn't an AFP entry? (Same question goes
for some other subdirectories in ~~/src/HOL.)
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:58):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
The direct reason is that MicroJava and most of these others predate the AFP by several years.
I think it’s a good idea to have some non-trivial applications directly in the distribution, so people don’t need to download something else before they have larger examples.
Which applications precisely these should be is a different question. The current set is mostly a function of where they came from and how they were developed.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:58):From: Peter Lammich <lammich@in.tum.de>
If a method produces n new subgoals, the next apply-steps will be
indented one level, and grouped into n blocks by blank lines, where each
block solves one of the subgoals:apply (intro conjI) // produces 3 subgoals
apply auto [] // Solves first oneapply (cases l) // Solve 2nd one
apply clarsimp // Solve Nil-case
apply forceapply auto [] // Solve Cons-case
apply force // Solve 3rd subgoal
done
In this case, for the “clarsimp", it’s hard to tell that it solves a goal, and for the “cases", it’s hard to tell how many subgoals it produces. Unless you really always have the comments -- then it’s fine, but I’m way too lazy for that many comments...
Actually, it is simple to see, even without the comments: clarsimp does
not solve any subgoal, as there is a next command (force) below it in
the same block. force solves a subgoal, as it is at the end of a block.
The cases produces two subgoals, as there are two indented blocks
following. For the same reason, the "intro conjI" produces 3 subgoals.
Email Gateway (Aug 22 2022 at 09:58):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Got it. That is indeed enough.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 10:01):From: Makarius <makarius@sketis.net>
This is indeed a quite fitting style guide. The Prover IDE should
gradually formalize more of such fine points, to make it easier to avoid
bad style by default. Just some notes in the order of the text:
There is already formal "bad" markup for 'sorry' and 'back' for some
years, which resulted from earlier AFP recommendations.
The formal indentation of 'apply' steps is also supported by some formal
markup that the referenced BeanShell macro uses. I hope to have
something like that as part of the regular indentation in Isabelle/jEdit
soon, within the Isabelle/Scala codebase. (In Isabelle2015 systematic
supports for text folds is new, but systematic indentation once not
addressed.)
Concerning bad internal names like xa, xb, xaa: Isabelle2015 produces
formal markup for that in the slightly reformed rule_tac family, with
the faint read color scheme of improper material. Maybe we should also
revisit rename_tac at some point, to clarify its meaning in that
respect, or to eliminate the need for rename_tac / rule_tac altogether
due to newly emerging subgoal focus in Isar "scripts".
Use of unrestricted "auto". Some years ago the goal restriction form
apply (cases P)
apply (auto ...)[2]
emerged as a partial solution to old subgoal addressing questions.
In Isabelle2015 more management infrastructure is wrapped around method
application, such that the new combinator ";" for structured combination
could be easily provided (it resembles THEN_ALL_NEW of ML tactics).
Using that, the above can we written in Coq-style like this:
apply (cases P; auto)
A potential disadvantage here is that "auto" is invoked separately on
each new subgoal, not on all of them simultaneously. This can make a
difference, e.g. for implicit proof parallelization inside of "auto".
The difference holds for these two variants:
apply (cases P)
apply (simp_all ...)[2]
apply (cases P; simp)
I am curious to see part 2, and especially part 3 about layout; the latter
category is more easily accessible in the Prover IDE.
High-end IDEs like IntelliJ IDEA have lots of built-in style and
recommendations, although it looks like big efforts to get to this level
of sophistication, and maintain it in the long run.
Makarius
Email Gateway (Aug 22 2022 at 10:02):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
On 28.05.2015, at 22:21, Makarius <makarius@sketis.net> wrote:
On Sat, 23 May 2015, Gerwin Klein wrote:
Updating lots of proofs to Isabelle2015-RCx and discussions about submission rules for the AFP inspired me to write up guidelines that may be of more widespread use and interest:
This is indeed a quite fitting style guide. The Prover IDE should gradually formalize more of such fine points, to make it easier to avoid bad style by default.
I agree, it would be nice to gradually converge to more support for such things over time.
- Concerning bad internal names like xa, xb, xaa: Isabelle2015 produces
formal markup for that in the slightly reformed rule_tac family, with
the faint read color scheme of improper material. Maybe we should also
revisit rename_tac at some point, to clarify its meaning in that
respect, or to eliminate the need for rename_tac / rule_tac altogether
due to newly emerging subgoal focus in Isar "scripts”.
The subgoal focus mechanism sounds promising. I didn’t have enough practical experience with it yet to make it a recommendation, but when it has withstood the test of time for a while, that could indeed become the main way of doing things.
I am curious to see part 2, and especially part 3 about layout; the latter category is more easily accessible in the Prover IDE.
Part 3 will probably be the most controversial one - not because I’m planning to write anything special, but because layout is the easiest to have strong opinions on.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 10:02):From: Makarius <makarius@sketis.net>
It is also the easiest to build converters for it. Have you tried
"isabelle update_cartouches" already?
My impression is that many people just get used to something arbitrary as
a start, and then cannot imagine anything else afterwards.
In the classic times of Isar and Proof General development (in 1998/1999)
a certain canonical indentation emerged and was implemented in the editor,
but in Isabelle/jEdit there is still nothing of it -- it will come one
day. Of course that will be based on the good old standards, although I've
found myself doing a few things differently now, to optimize the content
of the first line of a specification, for the tree-view in SideKick. E.g.
Bad:
definition foo :: T where
"foo = ..."
definition
bar :: T where
"bar = ..."
Good:
definition foobar :: T
where "foobar = ..."
Makarius
Email Gateway (Aug 22 2022 at 10:03):From: "C. Diekmann" <diekmann@in.tum.de>
When definitions get longer, the first bad version (subjectively)
appears more pleasant to me.
definition foo :: T where
"foo = BlaulichtAufDerDatenautobahn"
definition foo :: T
where "foo = BlaulichtAufDerDatenautobahn"
Putting the "where" in the first line saves space for the actual definition.
Cornelius
Email Gateway (Aug 22 2022 at 10:03):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Not even finished writing yet, and we have already started ;-)
‘definition/where' is actually one of the case I'm having most trouble with.
Personally, I like the most line-consuming form:
definition
foo :: T
where
“foo = bar”
because I tend to have long types and long definitions, sometimes both over multiple lines. The where in the same line as the definition adds noise to what I’m most interested in (the definition itself).
The variant
definition foo :: T
where
“foo = bar”
works more nicely with folding.
definition foo :: "T => T => (some, other, 'params) list =>
T"
where
“foo = bar”
forces too much indentation for the line break.
Maybe the solution is simply to have both variants, the folding-friendly variant when everything fits on the line, the multi-line one, when it doesn’t.
What do people think about this one for long types?
definition foo ::
"T => T => (some, other, 'params) list => T"
where
“foo = bar”
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 10:03):From: Peter Lammich <lammich@in.tum.de>
definition foo ::
"T => T => (some, other, 'params) list => T"
where
“foo = bar”
I usually use, for long types and long definition terms:
definition foo
:: "long => (type, yeah) they => (can,get) really => long"
where
"foo a b c = do {
let x = f a;
y <- g (b,c,x);
while (...) do {
...
if ... then
...
else
...
} (s_0)
}"
So I even need apply some indentation inside the definition, and this
simply looks best if the definition term starts at the begining of a
line. I even sometimes think about
"foo a b c =
do {
...
}"
Email Gateway (Aug 22 2022 at 10:12):From: Makarius <makarius@sketis.net>
That is not a counter-example yet: the material after the 'where' can be
broken up further, of course:
definition foo :: T
where
"foo =
let val x = long_material
in multiple_lines x end"
There are many possibilities. The main purpose of the exercise is to
follow these principles:
* The first line is restricted to the most relevant information for
SideKick tree view etc. (keyword 'where' is no relevant information).
* The overall layout follows the structure of nesting and fits into the
strict line length of 80-100 characters.
Makarius
Email Gateway (Aug 22 2022 at 10:13):From: Makarius <makarius@sketis.net>
On Sun, 31 May 2015, Gerwin Klein wrote:
Personally, I like the most line-consuming form:
definition
foo :: T
where
“foo = bar”
This form reminds me of ancient times of Proof General 2.0: head keyword
standing alone, then the body below it. I can't remember why be converged
to that in around 1999. Today I find it wasteful in vertical space, with
these odd 16x9 displays. (Apart from the lack of relevant information in
line 1 for SideKick.)
because I tend to have long types and long definitions, sometimes both
over multiple lines. Thewherein the same line as the definition adds
noise to what I’m most interested in (the definition itself).The variant
definition foo :: T
where
“foo = bar”works more nicely with folding.
I am also using this routinely for anything that is not just very short.
Putting the 'where' and the proposition on the same line is actually not
so frequent, since real specifications don't fit there.
definition foo ::
"T => T => (some, other, 'params) list => T"
where
“foo = bar”
It fits into the principle of having relevant information on line 1, and
breaking the rest according to normal indentation standards.
A definition and a theorem statement are analogous, and we already see
things like this routinely:
theorem a: "short statement"
theorem b:
"long statement
broken into
lines"
theorem c:
fixes ...
assumes ...
shows ...
Makarius
Email Gateway (Aug 22 2022 at 10:17):From: Lars Noschinski <noschinl@in.tum.de>
This is the form I use most. It only uses two lines and keeps as much
space as possible for the actual definition. I don't mind seeing the
unnecessary "where" in the sidekick -- it is at the end of the line,
after all. Also, seeing the name suffices for my purposes, so even the
type is unnecessary (for me).
I mostly use the sidekick to see the section structure. I would like to
see more information about my lemmas there (instead of just the name),
but I almost always state my lemmas in structured form, so I have a line
break after name.
-- Lars
Email Gateway (Aug 22 2022 at 10:18):From: Christine Sherif Rizkallah <christine2711987@gmail.com>
definition
foo :: T
where
“foo = bar”
Its nice to have a line to separate the type and the actual definition.
A more important issue though is recommending always explicitly writing the
types.
Email Gateway (Aug 22 2022 at 10:27):From: Holger Blasum <hbl@sysgo.com>
[..]
The availability of the EURO-MILS deliverable "Used Formal Methods"
http://www.euromils.eu/downloads/Deliverables/Y2/2015-EM-UsedFormalMethods-WhitePaper.pdf
might an on-topic contribution to this thread (discussions on Isabelle style).
best,
Last updated: Nov 21 2024 at 12:39 UTC