Email Gateway (Aug 18 2022 at 17:22): Email Gateway (Aug 18 2022 at 17:22):From: Kevin Van Horn <kevin@ksvanhorn.com>
I'm trying to figure out if Isabelle is the right theorem prover /
proof assistant for my needs, or if I should use something else. I'm
writing a Bayesian model compiler, something that will turn a
specification of a joint probability distribution plus indication of
what variables are observed into Markov chain Monte Carlo code for
estimating the parameters. There are existing software packages that
do something similar -- WinBUGS/OpenBUGS, JAGS, and hbc -- but they
all have limitations that are unacceptable for my purposes, and it
appears that I'll need some sort of theorem proving to overcome those
limitations.
Here are the features I'm looking for:
Interactive theorem proving (Isabelle seems to do this very well).
Ability to write new proof tactics.
Ability to do derivational proofs where I know the form of what I
want to prove but don't know exactly what I'm proving until I reach
the end. For example, I'm doing a chain of A1 = A2 = ... An, and only
when I reach an An that has the form I want do I know I'm done and
know that A1 = An is what I'm proving. Likewise, I might be trying to
find a usable upper bound: B1 <= B2 <= ... Bn.
Ability to call the theorem prover as a software module in a larger
system (no user interaction). This would be for tasks simple enough to
fully automate with appropriate tactics, or to spit out subgoals for
which the user will need to provide proofs in harder cases.
How does Isabelle rate on these? Would a different theorem prover /
proof assistant better fill these requirements?
(BTW I'm also looking at HOL Light and HOL 4, which appear have the
last three features above, but my impression is that Isabelle is
easier to use for interactive proof and that the finished proofs are
easier to read.)
Email Gateway (Aug 18 2022 at 17:22):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Dienstag, den 15.03.2011, 09:11 -0600 schrieb Kevin Van Horn:
I'm trying to figure out if Isabelle is the right theorem prover /
proof assistant for my needs, or if I should use something else. I'm
writing a Bayesian model compiler, something that will turn a
specification of a joint probability distribution plus indication of
what variables are observed into Markov chain Monte Carlo code for
estimating the parameters. There are existing software packages that
do something similar -- WinBUGS/OpenBUGS, JAGS, and hbc -- but they
all have limitations that are unacceptable for my purposes, and it
appears that I'll need some sort of theorem proving to overcome those
limitations.
Which mathematical background theories do you need? We have measure /
probability theory but no theorems about MCMC.
Here are the features I'm looking for:
- Interactive theorem proving (Isabelle seems to do this very well).
- Ability to write new proof tactics.
I only developed two small tactics in Isabelle, so I'm not very
experienced. But I think it is very easy to do in the interactive mode
in ProofGeneral. Open a new theory and write
theory test imports Main begin
ML {*
fun .....
*}
theorem "..."
apply (tactic {* ML code *})
This is a very nice playground for ideas, later you can of course move
your code to its own ML-file.
A introduction on how to write tactics is found in the Isabelle
Cookbook:
http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/isabelle-cookbook/raw-file/tip/progtutorial.pdf
For further information take a look at the reference manuals
http://isabelle.in.tum.de/documentation.html
- Ability to do derivational proofs where I know the form of what I
want to prove but don't know exactly what I'm proving until I reach
the end. For example, I'm doing a chain of A1 = A2 = ... An, and only
when I reach an An that has the form I want do I know I'm done and
know that A1 = An is what I'm proving. Likewise, I might be trying to
find a usable upper bound: B1 <= B2 <= ... Bn.
- Ability to call the theorem prover as a software module in a larger
system (no user interaction). This would be for tasks simple enough to
fully automate with appropriate tactics, or to spit out subgoals for
which the user will need to provide proofs in harder cases.
Some proof methods in Isabelle work in this way. The most often used
proof method (simp) works in this way. The user states a goal, applies
the simplifier and gets back the simplified goal where he can apply
further tactics. (This should also answer the previous question.)
How does Isabelle rate on these? Would a different theorem prover /
proof assistant better fill these requirements?(BTW I'm also looking at HOL Light and HOL 4, which appear have the
last three features above, but my impression is that Isabelle is
easier to use for interactive proof and that the finished proofs are
easier to read.)
I have no experiences with HOL Light or HOL 4. When you write your
proofs in Isar (Isabelle's proof language) they are more readable.
However I assume the OCaml / ML internals of HOL Light / HOL 4 are
easier to understand.
Greetings,
Johannes
Email Gateway (Aug 18 2022 at 17:22):From: Makarius <makarius@sketis.net>
On Tue, 15 Mar 2011, Kevin Van Horn wrote:
- Ability to call the theorem prover as a software module in a larger
system (no user interaction). This would be for tasks simple enough to
fully automate with appropriate tactics, or to spit out subgoals for
which the user will need to provide proofs in harder cases.
It is not as simple as I would like it to have, but it works, and people
have done it before, e.g. in the Isabelle/TLA+ IDE. (The technology for
Isabelle integration is about to change substantially in the coming
years.)
How does Isabelle rate on these? Would a different theorem prover /
proof assistant better fill these requirements?(BTW I'm also looking at HOL Light and HOL 4, which appear have the last
three features above, but my impression is that Isabelle is easier to
use for interactive proof and that the finished proofs are easier to
read.)
The HOL systems are not fundamentally different. There is mainly a
tendency towards more frugal system infrastructure -- HOL Light is
especially minimalistic.
The main alternative to Isabelle is actually Coq, but there are quite
different logical foundations, and less system manuals.
Makarius
Email Gateway (Aug 18 2022 at 17:22):From: Lawrence Paulson <lp15@cam.ac.uk>
Mike Gordon has a snappy description of the differences between the systems: Isabelle provide a better out-of-the-box experience, while HOL is better as an API for writing code that performs inference.
The various versions of HOL are much simpler internally than Isabelle, which simplifies programming. On the other hand, HOL provides less automation and its proof scripts are unintelligible.
Larry Paulson
Email Gateway (Aug 18 2022 at 17:22):From: Makarius <makarius@sketis.net>
Lets say these systems are closer to the bare metal, so it is easier to
read through the full sources and get an impression how it works.
In contrast, Isabelle is more like a Linux kernel over the bare logic, so
you need to understand some higher structuring principles. I would
nonetheless call it simple, in the same way a modern operating system is
"simple".
BTW, the APIs of Isabelle have been cleaned up a lot in recent years, so
the simplicity is now easier to see, without the historical baggage
getting in the way.
Makarius
Email Gateway (Aug 18 2022 at 17:23):From: Kevin Van Horn <kevin@ksvanhorn.com>
On Mar 16, 2011, at 4:14 AM, Johannes Hölzl wrote:
Am Dienstag, den 15.03.2011, 09:11 -0600 schrieb Kevin Van Horn:
... I'm writing a Bayesian model compiler, something that will
turn a
specification of a joint probability distribution plus indication of
what variables are observed into Markov chain Monte Carlo code for
estimating the parameters. ... it appears that I'll need some sort
of theorem proving...Which mathematical background theories do you need? We have measure /
probability theory but no theorems about MCMC.
In addition to measure / probability theory, I'll need some linear
algebra (matrix/vector multiplication, inverse, determinants) and
standard probability density functions (gamma, normal, multivariate
normal, etc.). A lot of what I'll be doing looks a lot more like
computer algebra (transforming a function into an equivalent function,
where equivalent means the same up to a constant of proportionality,
and deriving gradients of multivariate functions), along with
establishing some upper bounds and proving some arithmetic results on
array indices.
I don't expect to be proving anything very deep. Mostly, I'm looking
to automate (at least partially) a process that is currently done by
doing the math by hand following some pretty standard patterns; I need
to be able to automate new patterns as they arise; and I need to be
highly confident that the results are correct.
A introduction on how to write tactics is found in the Isabelle
Cookbook:
http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/isabelle-cookbook/raw-file/tip/progtutorial.pdf
Great! This seems to have a lot of the missing pieces I couldn't find
in the tutorial and reference manual.
-- Kevin
Email Gateway (Aug 18 2022 at 17:23):From: Makarius <makarius@sketis.net>
You should also look at the "implementation" manual.
Makarius
Email Gateway (Aug 18 2022 at 17:23):From: Timothy McKenzie <tjm1983@gmail.com>
I'm a little surprised that no-one has yet mentioned the "also ...
also ... finally ..." constructions in Isabelle/Isar. There's an
example in isar-overview in the documentation provided with
Isabelle, and more technical documentation in isar-ref. It can be
used with both = and <= (and, I think, even mixing the two), but
it behaves unusually with >=, because this is an abbreviation for
<=, and the abbreviation seems to be expanded before Isabelle
decides which is the left-hand side and which is the right-hand
side for the purposes of the next step.
And if you don't know exactly what you want to prove before you've
proven it, you can make the statement of the lemma almost
arbitrary until you've figured out what you want to prove, and
then go back and change it. I haven't used the other HOLs, but I
understand that they work backwards, manipulating the goal until
it becomes "True", so in those you'd need to state the lemma
correctly before you begin.
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 17:23):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Timothy McKenzie wrote:
Well, in either system you can always start with a goal of the form
P1 ==> P2 ==> ... ==> Pn ==> X
where Pi are your real assumptions, and X is literally just "X", a
placeholder,
while you see what you can get from P1 to Pn - when you have decided
what X should be you go back and repeat the same proof
Jeremy
Email Gateway (Aug 18 2022 at 17:23):From: Makarius <makarius@sketis.net>
Isar calculations are parameterized by a collection of rules that are
declared as "trans" and can be inspected via print_trans_rules. This is a
very general mechanism to combine relations in a forward manner. It also
works with substitution of equalities or inequalities (with some care
about higher-order unification).
The >= abbreviations indeed do not fit in here. There were added as adhoc
feature when I was not looking, and still await to be integrated properly.
Makarius
Email Gateway (Aug 18 2022 at 17:23):From: Makarius <makarius@sketis.net>
Maybe the recent 'notepad' is also of some interest here, it nicely shows
how Isabelle/Isar works without goal states getting in the way:
notepad
begin
fix x y z :: 'a
assume "x = y"
also assume "... = z"
finally have "x = z" .
end
Makarius
Last updated: Apr 25 2024 at 04:18 UTC