Email Gateway (Aug 19 2022 at 16:27): Email Gateway (Aug 19 2022 at 16:27):From: Josh Tilles <merelyapseudonym@gmail.com>
I've come across a few errors that are blocking my progress. I'm not sure
what to do besides trying to become familiar with all of Isabelle's
internals, so I'd appreciate any advice/direction—particularly on the two
specific errors I present below.
Thank you,
--Josh Tilles
These errors have arisen because I've returned to a task that I last
attempted a year or so ago: adapting HOL to make it possible to selectively
"opt-in" to classical logic. I've thought of a few approaches that would
work as initial proof-of-concepts. My intuition is that any of the below
should be possible, but one might be more tractable than the others.
Extract HOL.True_or_False into a locale.
- seems like the ideal solution
- Ultimately, I think the locale should be named classical but I've
currently named it NonIntuitionistic because there's a lemma that's also
named classical and an ML structure named Classical. So if I wanted the
locale usage to stand out in these prototypes, I needed a different name.
- The problem is that the elim rules break:
- on the line "declare NonIntuitionistic.iffCE [elim!]" we see the
message:
exception THM 1 raised (line 332 of "drule.ML"):
RSN: no unifiers
PROP NonIntuitionistic ⟹ ?P = ?Q ⟹ (?P ⟹ ?Q ⟹ ?R) ⟹ (¬ ?P ⟹ ¬ ?Q ⟹
?R) ⟹ ?R
PROP NonIntuitionistic ⟹ (¬ ?P ⟹ ?P) ⟹ ?P
Extract non-classical code into IHOL.thy, which the normal/classical HOL.thy
subsequently imports.
- Took a lot of time the last time I tried it a year ago, so I don't
have a demonstration patch (yet)
- A major problem is that all future theories will need to be split
similarly
- For example, IOrderings.thy for all of the lemmas and theorems that
work in an intuitionistic context, and Orderings.thy as the theory
that contains everything in IOrderings.thy plus any lemmas/theories
that actually depend on classical logic.
Replace the global HOL.True_or_False axiomatization with many local
assumptions/dependencies on the individual lemmas and theorems.
- probably the least amount of broad structural change (effectively,
we're just adding one more assumption to any classical lemmas)
- but tedious to make lots of minor changes to make to the proofs of the
lemmas
- you can see examples of this in my attached patch
- I totally acknowledge that my updated proofs are super-hacky at the
moment.
- needed to move the declarations of a bunch of lemmas as elimination
rules before the Hypsubst and Classical structures, otherwise I get an
error:
- on the line "declare iffCE [elim!]" we see the message:
exception Option raised (line 81 of "General/basics.ML")
- but if those particular errors go away if I relocate the
declarations
- unfortunately, anything elim-related fails with the same error
Email Gateway (Aug 19 2022 at 16:50):From: Makarius <makarius@sketis.net>
There is certainly something to learn from it: how proof assistants were
implemented in the early 1990-ies. See also the famous Handbook article by
Larry Paulson "Designing a theorem prover":
http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-192.html
The newer "Handbook of Practical Logic and Automated Reasoning" by John
Harrison also has a chapter on "Interactive theorem proving", see also
http://www.cl.cam.ac.uk/~jrh13/atp --- it describes HOL-Light, so the
prover architecture is very minimalistic.
That won't help in the project to remove the classical principle from
Isabelle/HOL, which I would consider futile. Why change the logic anyway?
Better use it (and its many ad-on tools) to model your own language and
logic inside it.
Makarius
http://stop-ttip.org 1,152,367 people so far
Email Gateway (Aug 19 2022 at 16:52):From: Makarius <makarius@sketis.net>
On Sat, 20 Dec 2014, Josh Tilles wrote:
On Fri, 21 Nov 2014, Josh Tilles wrote:
P.S. I'm about a hundred pages into ML for the Working Programmer, so I
apologize if all of my questions are just a result of my not yet having
read the chapter about constructing a tactical theorem prover [?]
There is certainly something to learn from it: how proof assistants were
implemented in the early 1990-ies. See also the famous Handbook article by
Larry Paulson "Designing a theorem prover": http://www.cl.cam.ac.uk/
techreports/UCAM-CL-TR-192.htmlAre you being tongue-in-cheek? I can't tell. Like, I wouldn't have
guessed that implementation techniques from twenty years ago are
relevant now...
I did not intend to make jokes about old, but important articles. There
is definitely something to learn from ancient times, where the concepts
are easier to see without all the rest around it that emerged over the
decades. Of course, you need to put things into the historical
perspective, and see the key points of newer prover architecture --
Isabelle is very rich in that respect.
The newer "Handbook of Practical Logic and Automated Reasoning" by John
Harrison also has a chapter on "Interactive theorem proving", see also
http://www.cl.cam.ac.uk/~jrh13/atp --- it describes HOL-Light, so the
prover architecture is very minimalistic.
Note that HOL-Light is interesting in being a minimalistic model of an
LCF-style prover that is in actual use. That is part of its culture, and
in contrast to Isabelle, but contrast also helps to learn something.
Better use it (and its many ad-on tools) to model your own language and
logic inside it.I'm not sure what you mean. Could you elaborate? Or perhaps point me
toward some examples or explanations by other people?
See what Larry said about non-standard analysis. When you want to do
realistic applications, it is better to keep the existing logical
foundations, and build within that huge building what you need in
addition.
Makarius
http://stop-ttip.org 1,218,911 people so far
Last updated: Nov 21 2024 at 12:39 UTC