Email Gateway (Aug 18 2022 at 19:52): Email Gateway (Aug 18 2022 at 19:52):From: John Wickerson <jpw48@cam.ac.uk>
Dear Isabelle,
When building an Isabelle script, I often have to come up with names for facts if I am not using them immediately. Coming up with meaningful names all the time is an intellectual burden I could live without when I'm concentrating on a proof. More importantly, even if I did come up with meaningful names all the time, I reckon they would soon get out-of-sync as I modified my script. I briefly tried numbering my steps, but again, the numbers quickly get out-of-order as my script evolves, and I have always to bear in mind which number I used last.
So, my current solution is to have an emacs macro that generates a sequence of 5 random letters when I press "C-c d", which I use to name my facts. I find this works rather well; I've not had a clash yet, and I don't have to engage my brain at all. Here's a little snippet from my current theory, to illustrate:
How do other users approach this issue?
John
ps. One final thought: does there exist a tool that processes an Isabelle script to make it more readable, renaming steps with (say) ascending natural numbers, and removing unused names? I think that would be rather nice.
Email Gateway (Aug 18 2022 at 19:52):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Dienstag, den 22.05.2012, 10:33 +0100 schrieb John Wickerson:
Dear Isabelle,
When building an Isabelle script, I often have to come up with names
for facts if I am not using them immediately. Coming up with
meaningful names all the time is an intellectual burden I could live
without when I'm concentrating on a proof. More importantly, even if I
did come up with meaningful names all the time, I reckon they would
soon get out-of-sync as I modified my script. I briefly tried
numbering my steps, but again, the numbers quickly get out-of-order
as my script evolves, and I have always to bear in mind which number I
used last.So, my current solution is to have an emacs macro that generates a
sequence of 5 random letters when I press "C-c d", which I use to name
my facts. I find this works rather well; I've not had a clash yet, and
I don't have to engage my brain at all. Here's a little snippet from
my current theory, to illustrate:with iecss and "0.prems"(2) have
dakuy: "set S = set (initials (Graph V \<Lambda> E))" and
iuqxi: "set (initials (Graph V \<Lambda> E)) = set V" by auto
from pqshe have wsegy: "set E = {}" by auto
hence hkimj: "E = []" by auto
Uhh, why are 5 random letters better than a slightly out of sync name?
For short theorems like "E = []" or "set E = {}" you can reference it
by E = [] or set E = {}. You can even use patterns if they are
unique:
set S = _
_ = set V
Use the structuring mechanisms of Isar:
have "" ...
moreover have "" ...
moreover have "" ...
ultimately have "" ...
have "x = y"
also have "... < c"
finally have "x < c"
have ""
then have ""
then have ""
then show ""
This avoids names, but also guides the reader through your proof.
I prefer to name collections of assumptions when they specify a
variable:
fix x assume x: "0 < x" "x < 1" ...
Otherwise I think a good idea is to name the theorem after the
constants appearing:
S_eq_initials: "set S = set (initials (Graph V \<Lambda> E))"
initials_eq_V: "set (initials (Graph V \<Lambda> E)) = set V"
This avoids mostly the burden to find good names.
Only sometimes I use , , or for theorems I immediately reuse,
like:
have *: "a b c = 1"
show ?thesis
unfolding *
So please delete your 5 random letters script and use one of these
techniques ;-)
How do other users approach this issue?
John
ps. One final thought: does there exist a tool that processes an
Isabelle script to make it more readable, renaming steps with (say)
ascending natural numbers, and removing unused names? I think that
would be rather nice.
Email Gateway (Aug 18 2022 at 19:52):From: Tobias Nipkow <nipkow@in.tum.de>
Here is the hardliner view: if you need to number your intermediate statements
with more than 0-9, you are doing something wrong. [Unless you want to do
something exotic like recast refutations found by a SAT solver as Isar proofs ;-) ].
Why? Look at a math book, they don't need many labels either. Of course, it
takes a bit of practice and it is a question of style, but Isar has a number of
features that help to avoid names. I find the following most useful:
In your example, drop wsegy: and hkimj: and refer to them as set E = {} and
E = []
use this, then, hence, assms, ?thesis etc
Tobias
Email Gateway (Aug 18 2022 at 19:52):From: Makarius <makarius@sketis.net>
A funny thing that I've seen recently on some non-prover tool is this: use
SHA1 digest on the content and restrict it to a unique prefix according to
the totality of such hashes in a certain context. This gives you 1-3
strange letters in most situations.
Lamport has his own naming scheme, with full paths according to proof
structure, and compressed versions thereof.
In Isabelle/Isar the basic attitude is that explicit names are relatively
rare, so complete naming is avoided by default. You also have implicit
"this" and "calculation" to work with.
Makarius
Email Gateway (Aug 18 2022 at 19:52):From: Tobias Nipkow <nipkow@in.tum.de>
Here is another analogy that I like: try to write proofs as much like Unix pipes
as possible and avoid long-distace cross references.
Tobias
Email Gateway (Aug 18 2022 at 19:52):From: Lawrence Paulson <lp15@cam.ac.uk>
I assume that you are aware of the various chaining facilities that exist, including moreover/ultimately. And the ability to refer to facts using backquotes, as in k>0.
With those, I find that I don't need many labels, so that usually the name of the variable involved is sufficient, for example,
assumes k: "k>0"
Larry Paulson
Email Gateway (Aug 18 2022 at 19:52):From: John Wickerson <jpw48@cam.ac.uk>
Thanks Larry. Yes, I am aware of the chaining features (though not all of the features Johannes helpfully pointed out), and do try not to use my "random-name" trick too often. Regarding your suggestion of conflating variable-names and fact-names, I'm rather uneasy about this practice: doesn't it make the proof rather confusing if, for instance, "[OF k]" and "[of k]" are actually referring to different k's?
John
Email Gateway (Aug 18 2022 at 19:52):From: Lawrence Paulson <lp15@cam.ac.uk>
I suppose it might confuse some people. You can always call it kgt0 if you prefer. Random strings of letters strike me as being the worst option, because they convey no information whatever.
Larry Paulson
Email Gateway (Aug 18 2022 at 19:53):From: "\"Mark\"" <mark@proof-technologies.com>
You are not alone, John. Tom Hales uses a script to generate a random
sequence of 7 letters for the names of the lemmas in his Flyspeck project.
Although this is for HOL Light.
Mark.
on 22/5/12 11:51 AM, John Wickerson <jpw48@cam.ac.uk> wrote:
Thanks Larry. Yes, I am aware of the chaining features (though not all of
the features Johannes helpfully pointed out), and do try not to use my
"random-name" trick too often. Regarding your suggestion of conflating
variable-names and fact-names, I'm rather uneasy about this practice:
doesn't it make the proof rather confusing if, for instance, "[OF k]" and
"[of k]" are actually referring to different k's?John
On 22 May 2012, at 11:33, Lawrence Paulson wrote:
I assume that you are aware of the various chaining facilities that
exist,
including moreover/ultimately. And the ability to refer to facts using
backquotes, as ink>0.With those, I find that I don't need many labels, so that usually the
name
of the variable involved is sufficient, for example,assumes k: "k>0"
Larry Paulson
On 22 May 2012, at 10:33, John Wickerson wrote:
Dear Isabelle,
When building an Isabelle script, I often have to come up with names for
facts if I am not using them immediately. Coming up with meaningful names
all the time is an intellectual burden I could live without when I'm
concentrating on a proof. More importantly, even if I did come up with
meaningful names all the time, I reckon they would soon get out-of-sync as
I
modified my script. I briefly tried numbering my steps, but again, the
numbers quickly get out-of-order as my script evolves, and I have always
to
bear in mind which number I used last.So, my current solution is to have an emacs macro that generates a
sequence of 5 random letters when I press "C-c d", which I use to name my
facts. I find this works rather well; I've not had a clash yet, and I
don't
have to engage my brain at all. Here's a little snippet from my current
theory, to illustrate:with iecss and "0.prems"(2) have
dakuy: "set S = set (initials (Graph V \<Lambda> E))" and
iuqxi: "set (initials (Graph V \<Lambda> E)) = set V" by auto
from pqshe have wsegy: "set E = {}" by auto
hence hkimj: "E = []" by autoHow do other users approach this issue?
John
ps. One final thought: does there exist a tool that processes an
Isabelle
script to make it more readable, renaming steps with (say) ascending
natural
numbers, and removing unused names? I think that would be rather nice.
Last updated: Apr 19 2024 at 20:15 UTC