Email Gateway (Jan 09 2024 at 15:24): Email Gateway (Jan 09 2024 at 15:24):From: David Fuenmayor <davfuenmayor@gmail.com>
Dear experts,
In trying to connect Isabelle with the external world I need to extract a
plain string representation of a term for further processing. However, to
my surprise, the function "Syntax.string_of_term @{context}" still
generates markup. I have tried several other similar functions (e.g.
"Pretty.unformatted_string_of") and all of them keep generating markup
(which I cannot further transform into something external systems would
understand).
Can someone please help me here?
More generally, I would be thankful to anyone indicating me the correct way
to export/import plain text term/thm representations in Isabelle/ML (I
have spent indeed days looking at the documentation and still cannot wrap
my head around how to do such "basic" stuff).
Thanks for your help
David
Email Gateway (Jan 09 2024 at 16:09):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Dear David,
The solution I use in Sledgehammer, and which has served me well, is encapsulated in the following code:
fun hackish_string_of_term ctxt =
Print_Mode.setmp [] (Syntax.string_of_term ctxt)
#> YXML.content_of
#> Sledgehammer_Util.simplify_spaces
I hope this helps.
Best,
Jasmin
Email Gateway (Jan 09 2024 at 17:01):From: Makarius <makarius@sketis.net>
On 09/01/2024 16:24, David Fuenmayor wrote:
In trying to connect Isabelle with the external world I need to extract a
plain string representation of a term for further processing.
Can you say more about this "external world"?
Normally, Isabelle/ML is the "internal world" of Isabelle, and Isabelle/Scala
is the external world. From there you can connect to further outlying islands.
Trying to connect Isabelle/ML to the outside world without Isabelle/Scala is a
bad idea.
More generally, I would be thankful to anyone indicating me the correct way to
export/import plain text term/thm representations in Isabelle/ML
Isabelle/Scala already provides programming interfaces to work e.g. with
Export_Theory material. It corresponds to "isabelle build -o export_theory".
The "system" manual has a brief explanation of "isabelle scala_project", which
simplifies the exploration of Isabelle/Scala sources and APIs e.g. via
IntelliJ IDEA: unfortunately its Scala3 plugin has degraded a lot in recent
years (or I just don't understand how to use it properly).
Next time, I will integrate a proper Isabelle/Scala IDE into Isabelle/PIDE,
bypassing IntelliJ IDEA.
Here is also a recent demo to make an Isabelle command-line tool in
Isabelle/Scala:
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Tools/Demo
--- it should work with Isabelle2023 and will be officially part of
Isabelle2024 (May 2024).
Makarius
Email Gateway (Jan 10 2024 at 00:02):From: David Fuenmayor <davfuenmayor@gmail.com>
Dear Makarius:
Can you say more about this "external world"?
I basically want to use CAS (e.g. Sage) to simplify polynomials in finite
fields (among others).
At first I want to approach the problem in a generic way (see file
attached):
Create a method (via method_setup) that sends the current goal (as a
string) to some CLI tool which transforms it and gives back another string
which shall somehow become the new goal, I assume, by parsing it into a
prop (for an initial PoC I am willing to trust the CAS as an oracle).
The first step of extracting a plain string representation for the goal is
solved (thanks to Jasmin Blanchette suggestion in previous email).
I must now figure out how to 'replace' the current goal with what I am
getting back from the CAS.
Attached is a file with the essential parts of my code. I will be very
grateful if you (or anyone) can make comments/suggestions.
Btw, I apologize if my approach seems too crude. I just started exploring
the solution space (without any knowledge of Isabelle/ML).
Best
David
Email Gateway (Jan 10 2024 at 04:53):From: Wenda Li <wenda.li@ed.ac.uk>
Dear David,
A few years ago, we were using Mathematica to construct checkable certificates to solve univariate polynomial problems: https://github.com/Wenda302/RCF_Decision_Procedures. Much of the pipeline is certainly not idiomatic to today’s standard but may serve as a super crude reference.
Regards,
Wenda
Wenda Li
Lecturer in Hybrid AI
Informatics Forum
University of Edinburgh
Site: https://wenda302.github.io
Email: wli8@ed.ac.uk
On 10 Jan 2024, at 00:01, David Fuenmayor <davfuenmayor@gmail.com> wrote:
Dear Makarius:
Can you say more about this "external world"?
I basically want to use CAS (e.g. Sage) to simplify polynomials in finite fields (among others).
At first I want to approach the problem in a generic way (see file attached):
Create a method (via method_setup) that sends the current goal (as a string) to some CLI tool which transforms it and gives back another string which shall somehow become the new goal, I assume, by parsing it into a prop (for an initial PoC I am willing to trust the CAS as an oracle).
The first step of extracting a plain string representation for the goal is solved (thanks to Jasmin Blanchette suggestion in previous email).
I must now figure out how to 'replace' the current goal with what I am getting back from the CAS.
Attached is a file with the essential parts of my code. I will be very grateful if you (or anyone) can make comments/suggestions.
Btw, I apologize if my approach seems too crude. I just started exploring the solution space (without any knowledge of Isabelle/ML).
Best
David
On Tue, Jan 9, 2024 at 6:01 PM Makarius <makarius@sketis.net<mailto:makarius@sketis.net>> wrote:
On 09/01/2024 16:24, David Fuenmayor wrote:
In trying to connect Isabelle with the external world I need to extract a
plain string representation of a term for further processing.
Can you say more about this "external world"?
Normally, Isabelle/ML is the "internal world" of Isabelle, and Isabelle/Scala
is the external world. From there you can connect to further outlying islands.
Trying to connect Isabelle/ML to the outside world without Isabelle/Scala is a
bad idea.
More generally, I would be thankful to anyone indicating me the correct way to
export/import plain text term/thm representations in Isabelle/ML
Isabelle/Scala already provides programming interfaces to work e.g. with
Export_Theory material. It corresponds to "isabelle build -o export_theory".
The "system" manual has a brief explanation of "isabelle scala_project", which
simplifies the exploration of Isabelle/Scala sources and APIs e.g. via
IntelliJ IDEA: unfortunately its Scala3 plugin has degraded a lot in recent
years (or I just don't understand how to use it properly).
Next time, I will integrate a proper Isabelle/Scala IDE into Isabelle/PIDE,
bypassing IntelliJ IDEA.
Here is also a recent demo to make an Isabelle command-line tool in
Isabelle/Scala:
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Tools/Demo
--- it should work with Isabelle2023 and will be officially part of
Isabelle2024 (May 2024).
Makarius
<Example.thy>
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.
Email Gateway (Jan 10 2024 at 07:48):From: Tobias Nipkow <nipkow@in.tum.de>
Dear David,
I connected Isabelle to Sage a few months ago, the other way around. I generated
code from the AFP article "The Factorization Algorithm of Berlekamp and
Zassenhaus" by Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann and Akihisa
Yamada and wrote a python wrapper for making it a Sage command (i.e. a verified
polynomial factorization command). I am attaching an email I sent to the above
authors in case they were interested in adding my code to their AFP entry (but I
don't think it has happened yet).
I suspect my code will not help you but since your raised the Isabelle-CAS issue
I thought I'd advertise my work ;-)
Tobias
Fact_Poly.thy
Main.hs
factor_polynomial_verified.sage
FactorsPolyZVerified.g
smime.p7s
smime.p7s
Email Gateway (Jan 12 2024 at 12:35):From: David Fuenmayor <davfuenmayor@gmail.com>
Thank you all (Jasmin, Makarius, Wenda, Tobias) for your timely sugestions!
They have been very helpful in getting a better picture of the problem.
In the meanwhile, I have made some progress with interfacing with Sage but
still need help to get through the last mile (I plan to share the stuff in
github in the next days/weeks if I manage get things to work).
I basically need to write the following tactic "replace_goal_tac" that
modifies the proof state by replacing the current goal: a (possibly
equational) term of the form "A (= B)", with a (possibly equational)
'newgoal' term of the form "C (= D)", and also adds the intermediate
subgoal(s): "A = C" (possibly also "B = D").
ML‹ fun replace_goal_tac (ctxt : Proof.context) (current_goal : term)
(new_goal : term) = all_tac ›
Thanks for your help!
David
Email Gateway (Jan 12 2024 at 13:28):From: Makarius <makarius@sketis.net>
On 12/01/2024 13:35, David Fuenmayor wrote:
Thank you all (Jasmin, Makarius, Wenda, Tobias) for your timely sugestions!
They have been very helpful in getting a better picture of the problem.
In the meanwhile, I have made some progress with interfacing with Sage but
still need help to get through the last mile (I plan to share the stuff in
github in the next days/weeks if I manage get things to work).
I did not find time yet to comment further on the material from this thread,
because there were so many deviations from decades of Isabelle culture and
tradition. If you publish your ongoing experiments, I will take another look
eventually.
I basically need to write the following tactic "replace_goal_tac" that
modifies the proof state by replacing the current goal: a (possibly
equational) term of the form "A (= B)", with a (possibly equational) 'newgoal'
term of the form "C (= D)", and also adds the intermediate subgoal(s): "A = C"
(possibly also "B = D").ML‹ fun replace_goal_tac (ctxt : Proof.context) (current_goal : term)
(new_goal : term) = all_tac ›
So what is the logical relationship between the new and old goal?
Tactical theorem proving usually works by backwards refinement of goal
statements, based on previously proven facts (theorems).
If the fact happens to be an equation (equivalence), you can apply it e.g. via
Conv.gconv_rule. (You can do a hypersearch over all *.{ML,thy} files to see
typical uses, including examples and documentation.) If the fact is a rule A1
... ==> An ==> B, you can apply it e.g. via resolve_tac.
There are many more possibilities beyond that. It depends on what you try to
do exactly.
Getting proven equations or rules is another problem. In the scenario of the
external tool, you will probably just "invent" or "postulate" theorems via an
oracle. E.g. see the isar-ref manual, section 5.14 on the 'oracle' Isar
command. (Oracles are by default incorrect and not to be seriously trusted: a
bit too many things can usually go wrong. We will discuss that further, when
you have your concrete implementation.)
Makarius
Last updated: Apr 29 2024 at 04:18 UTC