Re: [isabelle] question


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”.


On 01/24/2014 06:14 PM, Elsa L Gunter wrote:
> 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
> On 1/24/14 10:54 AM, John Wickerson 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.