Email Gateway (Aug 19 2022 at 13:19): Email Gateway (Aug 19 2022 at 13:19):From: John Wickerson <johnwickerson@cantab.net>
Hi all,
I wonder if I might invite comment on the following statement?
"Don't even think about firing up Isabelle until you've completed a really solid pencil-and-paper proof of the theorem you want to mechanise."
Thanks!
John
Email Gateway (Aug 19 2022 at 13:19):From: Alfio Martini <alfio.martini@acm.org>
Hi John,
I can say that I "hate" firing up Isabelle before having made at least a
proof sketch of the statement
I want to prove. I don´t feel comfortable with automation unless I know
what is going on.
Best!
Email Gateway (Aug 19 2022 at 13:19):From: Joachim Breitner <breitner@kit.edu>
Hi,
it is certainly good advice, but Isabelle has its merits also when
exploring and finding a proof. One could also say
„Don’t even think about completing as solid pencil-and-paper
proof of your theorem until you have finalized your
formalisation, your definition, and your theorem.“
Because when you change some of these, fixing a pencil-and-paper-proof
is tedious and error-prone, while Isabelle will easily tell you where
you need to adjust stuff.
So while there were certainly cases where I should have worked on paper
before, I would not make it an absolute rule.
Also, depending on your hand writing, there are good reason to avoid
pen-and-pencil proofs that need to be readable even the next day :-)
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 13:20):From: Tobias Nipkow <nipkow@in.tum.de>
That's easy to refute: Quickcheck and Nitpick may already give you feedback
during development. But your statement becomes monotonically truer with the
complexity of the theory.
Tobias
Email Gateway (Aug 19 2022 at 13:20):From: Elsa L Gunter <egunter@illinois.edu>
Dear John,
I am an old time Isabelle user, and someone with a PhD in math
(abstract algebra), and I always do my work in Isabelle straight out.
It's my scratch pad. I make lots of lemmas and start with a heavy use
of sorry, but the use of Isabelle as a record keeper when you are
thrashing out a proof is considerable. It is true that you will
probably make a very messy proof at best if you try to use Isabelle to
bludgeoned the proof to death or just start failing with the
connectives. Also, I basically never use auto, and only use clarsimp
when I know what I want it to do and what it will do. But through the
use of lemmas and subgoals, you can use Isabelle to help you
interactively discover the proof of theorems you are trying to prove.
---Elsa
Email Gateway (Aug 19 2022 at 13:20):From: Alfio Martini <alfio.martini@acm.org>
I would add that if you are into Isar structured proofs and the structure
of the proof is not trivial then a proof sketch
using pencil and paper (or maybe even using "sorry") seems essential.
Actually, I only accept apply scripts
in proof exploration. In a early version of Tobias tutorial on Isar there
was this nice remark:
"structure does not emerge automatically but needs to
be understood and imposed".
Best!
---------- Forwarded message ----------
From: Alfio Martini <alfio.martini@acm.org>
Date: Fri, Jan 24, 2014 at 3:04 PM
Subject: Re: [isabelle] question
To: John Wickerson <johnwickerson@cantab.net>
Cc: "isabelle-users@cl.cam.ac.uk Mailinglist" <isabelle-users@cl.cam.ac.uk>
Hi John,
I can say that I "hate" firing up Isabelle before having made at least a
proof sketch of the statement
I want to prove. I don´t feel comfortable with automation unless I know
what is going on.
Best!
On Fri, Jan 24, 2014 at 2:54 PM, John Wickerson <johnwickerson@cantab.net>wrote:
Hi all,
I wonder if I might invite comment on the following statement?
"Don't even think about firing up Isabelle until you've completed a
really solid pencil-and-paper proof of the theorem you want to mechanise."Thanks!
John
--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
Email Gateway (Aug 19 2022 at 13:20):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
while I am not an old time Isabelle user (~3 years) and am still at
least four-ish years away from a PhD, I can wholeheartedly agree to what
Elsa said. While formalisation is, of course, much easier when you
already have a solid idea of /why/ the theorem you're trying to prove
holds, I often find it very helpful to just write down a theorem
statement in Isabelle and prove away even if I don't have the first idea
why it should hold.
For instance, in my Bachelor's thesis, I had to prove that some
invariant (that I first had to find, so I wasn't even sure if it was the
right one) is preserved throughout a loop. Isabelle told me precisely
what facts I could use and what I had to prove – which is hard to keep
track of in your head with a large proof such as this – and I proved
everything in a short amount of time; by simply exploring “forward”,
i.e. deriving everything I could think of from the assumptions I had,
and “backwards”, i.e. reducing what I had to prove to simpler
statements, until everything fell into place. It was only much later
that I actually understood /intuitively/ what I had proven.
This is probably a rare case, normally you first understand something
and then formalise it, but Isabelle can help you to develop a proof from
scratch as well. I also found it very useful during homework, most
recently in social choice theory. Nitpick is particularly useful to
avoid wasting time trying to prove things that are simply wrong, and it
is also very useful for exercises such as “Prove or disprove X“ or “Show
that in general, X does not hold”.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 13:20):From: John Wickerson <johnwickerson@cantab.net>
Thanks all for your variety of insightful answers. I thought the statement might well be contentious :).
Email Gateway (Aug 19 2022 at 13:21):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
For my Master's thesis, I formalized in Isabelle a proof of the
independence of the equivalent of the parallels postulate in Tarski's
axioms of geometry [1]. That would have been far too big to do by hand
first (at least at the speed I write). But when I couldn't easily keep
a part of the proof in my head all at once, I'd draw myself a map of
which lemmas were required to prove which other lemmas, and then I could
concentrate one at a time on any lemma such that all of the lemmas it
depended on had already been formalized. I've attached a couple of
examples. Having said that, I did do pen-and-paper working for some of
the lemmas mentioned on those pages, though many of them went straight
from my head into Isabelle, probably including some that were never even
mentioned on the map.
This suited my style well, but I suspect that the best strategy is
highly dependent on the style of the person using it. For me, I
naturally tend to write proofs in more detail than most, so writing
proofs for Isabelle wasn't as much of a hurdle as it probably is for
some other people. And I grew up with computers, too; I often feel more
comfortable writing a letter on a computer, rather than writing it by
hand, but some people prefer to write by hand first, even if they're
going to type up the result in the end.
Tim
<><
[1] http://afp.sourceforge.net/entries/Tarskis_Geometry.shtml
IMG_20140125_125138.jpg
IMG_20140125_125401.jpg
signature.asc
Email Gateway (Aug 19 2022 at 13:21):From: Peter Lammich <lammich@in.tum.de>
For algorithm verification, I usually try to understand the algorithm
intuitively, sketching it on paper. Then I try sketching the
invariants, still on paper. Only then I start formalizing it, and see
how to strengthen the invariants to go through.
For proofs that require more intricate arguments (in my case, decidable
abstract models for parallel programs) I usually have a proof sketch on
paper first, and then try to encode it in Isabelle.
However, as more advanced you get in Isabelle, as more can you prove by
just typing it into Isabelle and follow your "instinct" (supported by
sledgehammer&co) to prove it.
-- Peter
Email Gateway (Aug 19 2022 at 13:21):From: "Jens-D. Doll" <jd@cococo.de>
Hello Tim,
the two-dimensional graphical reasoning (i.e. the images) look fine and
are somehow enjoyable. If programming is like writing a letter to(!) a
computer, I wonder if there is a way of also transmitting diagrams to an
inference machine like Isabelle?
Jens
Last updated: Nov 21 2024 at 12:39 UTC