Email Gateway (Aug 19 2022 at 10:40): Email Gateway (Aug 19 2022 at 10:40):From: David Greenaway <david.greenaway@nicta.com.au>
Hi all,
In an Isabelle theory file, I can write simple one-line tactics such as
the following:
apply (clarsimp simp: split_def split: prod.splits)
I find, however, when I start writing ML code to automate proofs,
producing a ML tactic object is far more verbose:
clarsimp_tac (Context.proof_map (
Simplifier.map_ss (fold Splitter.add_split @{thms prod.splits})
#> Simplifier.map_ss (fn ss => ss addsimps [@{thm split_def}]))
@{context}) 1
The background is that I am writing tools[1] to automatically convert
C code into an abstract(ish) monadic form with the goal of easing
reasoning. As part of this, I frequently need to write ML code that
dynamically generates theorems and then proceeds to prove them. A simple
way of writing tactics such as the one above would be helpful both in
quick-and-dirty prototyping of ML proof procedures, but ideally would
also be clean enough for "production quality code".
Does anyone have any hints or tips?
(This discussion was originally started at StackOverflow[2], but it was
suggested that I move it over here when the discussion became a little
more involved. It is also part of long-running bigger question as to
"what is the best way to interact with Isabelle at the ML level?", but
perhaps it is better to address this concrete issue for now.)
[1]: http://ssrg.nicta.com.au/projects/TS/autocorres/
[2]: http://stackoverflow.com/questions/15217009/how-can-i-easily-write-simple-tactics-at-the-ml-level-of-isabelle
Thanks so much,
David
Email Gateway (Aug 19 2022 at 10:41):From: Makarius <makarius@sketis.net>
The first hint is off-topic: ML has values and functions over values, not
"objects". Someone else had also used the oo-term "method" for ML
functions, but this is only adding confusion, and working against the
intentions of the oo-guys some decades ago: the idea back then was to have
unusual terminology ("objects", "methods", "classes") for unusual and
groundbreaking concepts.
Back to today's reality and the question how to work effectively and
smoothly with Isabelle/ML, and how to write proof procedures in it. Here
is part of my answer from the Stackoverflow thread again:
ML {*
(*foo_tac -- the payload of what you want to do,
note the dependency on ctxt: Proof.context*)
fun foo_tac ctxt =
let
val my_ctxt =
ctxt |> Simplifier.map_simpset
(fold Splitter.add_split @{thms prod.splits} #>
Simplifier.add_simp @{thm split_def})
in ALLGOALS (clarsimp_tac my_ctxt) end
*}
method_setup foo = {*
(concrete syntax like "clarsimp", "auto" etc.)
Method.sections Clasimp.clasimp_modifiers >>
(Isar method boilerplate)
(fn _ => fn ctxt => SIMPLE_METHOD (CHANGED (foo_tac ctxt)))
*}
Here I had already applied some peep-hole optimization to make your
initial version less awkward. Instead of pasting together big ML
expressions (also with antiquotations) in "apply tactic {* ... *}" you
build up small ML tools like foo_tac and eventually wrap them up in
concrete Isar syntax via method_setup, for example.
We still need to work out, why this direction did not look appealing to
your application. I have browsed through the AutoCorres 0.1 sources, but
did not see the totally unusual problem that requires completely different
approaches to what people are already used to. It might be there
nonetheless, and this is why be have switched to the more interactive
mailing list.
In your second question (actually answer) on Stackoverflow, you've had a
function to parse strings into tactic values like this:
mk_tac "metis Suc_eq_plus1 mult_Suc_right nat_add_commute"
But that is better done at compile-time via ML antiquotations,
speculatively like this:
@{metis Suc_eq_plus1 mult_Suc_right nat_add_commute}
It is reasonably easy to implement such antiquotations -- they are part of
the Isar user space just like methods, attributes etc. -- I can also give
some examples.
Although we first need to sort out what is conceptually the right way to
go. Antiquotations are some kind of ML preprocessor macros, and that is
not something you do without thinking several times about it.
Makarius
Email Gateway (Aug 19 2022 at 10:42):From: David Greenaway <david.greenaway@nicta.com.au>
Hi Makarius,
On 10/03/13 06:47, Makarius wrote:
On Fri, 8 Mar 2013, David Greenaway wrote:
In an Isabelle theory file, I can write simple one-line tactics such
as the following:apply (clarsimp simp: split_def split: prod.splits)
I find, however, when I start writing ML code to automate proofs,
producing a ML tactic object is far more verbose:clarsimp_tac (Context.proof_map (
Simplifier.map_ss (fold Splitter.add_split @{thms prod.splits})
#> Simplifier.map_ss (fn ss => ss addsimps [@{thm split_def}]))
@{context}) 1[...]
The first hint is off-topic: ML has values and functions over values,
not "objects". Someone else had also used the oo-term "method" for ML
functions, but this is only adding confusion, and working against the
intentions of the oo-guys some decades ago: the idea back then was to
have unusual terminology ("objects", "methods", "classes") for unusual
and groundbreaking concepts.
Thank you for the correction. I did understand a tactic is simply a "thm
-> thm Seq.seq", but have the bad habit of being imprecise in my
language.
Back to today's reality and the question how to work effectively and
smoothly with Isabelle/ML, and how to write proof procedures in it.
Here is part of my answer from the Stackoverflow thread again:ML {*
(*foo_tac -- the payload of what you want to do,
note the dependency on ctxt: Proof.context*)
fun foo_tac ctxt =
let
val my_ctxt =
ctxt |> Simplifier.map_simpset
(fold Splitter.add_split @{thms prod.splits} #>
Simplifier.add_simp @{thm split_def})
in ALLGOALS (clarsimp_tac my_ctxt) end
*}method_setup foo = {*
(concrete syntax like "clarsimp", "auto" etc.)
Method.sections Clasimp.clasimp_modifiers >>
(Isar method boilerplate)
(fn _ => fn ctxt => SIMPLE_METHOD (CHANGED (foo_tac ctxt)))
*}Here I had already applied some peep-hole optimization to make your
initial version less awkward. Instead of pasting together big ML
expressions (also with antiquotations) in "apply tactic {* ... *}" you
build up small ML tools like foo_tac and eventually wrap them up in
concrete Isar syntax via method_setup, for example.
Your version is indeed cleaner than mine, but still not quite what I am
looking for.
I think the confusion comes from me not explaining fully what my goal
is. Your solution works well when 1 particular tactic needs to be used
in "n" locations. What I am trying to simplify is having "n" different
tactics each used in 1 single location (with that one location always
being inside an ML function).
In short, I am looking for syntactic sugar to make writing proof scripts
in ML less verbose. While a lot of the heavy lifting of such proof
scripts can be done in Isar and the result used as a "thm", I still find
that I need to carry out proofs inside ML (such as when the proof goal
is not known in advance).
In your second question (actually answer) on Stackoverflow, you've had
a function to parse strings into tactic values like this:mk_tac "metis Suc_eq_plus1 mult_Suc_right nat_add_commute"
But that is better done at compile-time via ML antiquotations,
speculatively like this:@{metis Suc_eq_plus1 mult_Suc_right nat_add_commute}
It is reasonably easy to implement such antiquotations -- they are
part of the Isar user space just like methods, attributes etc. --
I can also give some examples.
An anti-quotation that generates code similar to what I original wrote
(or perhaps what you corrected it to :) would be ideal.
Two problems that I have, though are:
* I can't extract a list of valid methods names (or their associated
tactic) from the "Method" structure;
* Even if I could get a list of method names, I can't see a way of
parsing method arguments into an AST without re-implementing the
parsing logic of every single tactic. (Most tactics are not so
bad, because they use one of three possible argument parsers.
Nevertheless, as far as I can tell these would need to be
reimplemented to produce an AST instead of directly modifying the
proof context directly).
If you have any suggestions for solving these problems, I would be keen
to hear.
Thanks so much,
David
Email Gateway (Aug 19 2022 at 10:42):From: David Greenaway <david.greenaway@nicta.com.au>
On 08/03/13 12:36, David Greenaway wrote:
In an Isabelle theory file, I can write simple one-line tactics such
as the following:apply (clarsimp simp: split_def split: prod.splits)
I find, however, when I start writing ML code to automate proofs,
producing a ML tactic object is far more verbose:
[...]
Does anyone have any hints or tips?
With the help of Thomas Sewell, I came up with the following solution:
The "Method" class provides an interface to both generate a "method"
from a list of tokens, and to generate a "cases_tactic" from a method.
These can be combined as follows:
(*
* Generate an ML tactic object of the given Isar string.
*
* For example,
*
* mk_tac "auto simp: field_simps intro!: ext" @{context}
*
* will generate the corresponding "tactic" object.
*)
fun mk_tac str ctxt =
let
val parsed_str = Outer_Syntax.scan Position.start str
|> filter Token.is_proper
|> Args.name
val meth = Method.method (Proof_Context.theory_of ctxt)
(Args.src (parsed_str, Position.start)) ctxt
in
Method.apply (K meth) ctxt [] #> Seq.map snd
end
or alternatively as an anti-quotation:
(*
* Setup an antiquotation of the form:
*
* @{tactic "auto simp: foo intro!: bar"}
*
* which returns an object of type "context -> tactic".
*
* While this doesn't provide any benefits over a direct call to "mk_tac" just
* yet, in the future it may generate code to avoid parsing the tactic at
* run-time.
*)
val tactic_antiquotation_setup =
let
val parse_string =
((Args.context -- Scan.lift Args.name) >> snd)
#>> ML_Syntax.print_string
#>> (fn s => "mk_tac " ^ s)
#>> ML_Syntax.atomic
in
ML_Antiquote.inline @{binding "tactic"} parse_string
end
and setup in a theory file as follows:
setup {*
tactic_antiquotation_setup
*}
This can then be used in ML code to generate a tactic:
lemma "(a :: nat) * (b + 1) = (a * b) + a"
by (tactic {* @{tactic "metis Suc_eq_plus1 mult_Suc_right nat_add_commute"} @{context} *})
Hopefully this helps somebody other than just me.
Cheers,
David
Email Gateway (Aug 19 2022 at 10:42):From: Makarius <makarius@sketis.net>
On Mon, 11 Mar 2013, David Greenaway wrote:
On 08/03/13 12:36, David Greenaway wrote:
In an Isabelle theory file, I can write simple one-line tactics such
as the following:apply (clarsimp simp: split_def split: prod.splits)
I find, however, when I start writing ML code to automate proofs,
producing a ML tactic object is far more verbose:
[...]
Does anyone have any hints or tips?With the help of Thomas Sewell, I came up with the following solution:
The "Method" class provides an interface
That is the structure Method in Isabelle/ML. SML is free from any
object-oriented concepts. You should do justice to what the oo-guys tried
to do several decades ago by using their terminology properly.
* While this doesn't provide any benefits over a direct call to "mk_tac" just
* yet, in the future it may generate code to avoid parsing the tactic at
* run-time.
*)
val tactic_antiquotation_setup =
let
val parse_string =
((Args.context -- Scan.lift Args.name) >> snd)
#>> ML_Syntax.print_string
#>> (fn s => "mk_tac " ^ s)
#>> ML_Syntax.atomic
in
ML_Antiquote.inline @{binding "tactic"} parse_string
end
Parsing at runtime gets you back to LISP-style dynamic macro programming.
ML_Antiquote.value should do the job statically at compile time.
Sometimes this requires auxiliary data in the context, to transport
abstract values between the runtime/compile time of Isabelle/ML. E.g. see
how the @{thm} antiquotation is done. (To get to its implementation you
write something like ML {* @{thm refl} *} and use hover-click in
Isabelle/jEdit on "thm".)
This can then be used in ML code to generate a tactic:
lemma "(a :: nat) * (b + 1) = (a * b) + a"
by (tactic {* @{tactic "metis Suc_eq_plus1 mult_Suc_right nat_add_commute"} @{context} *})Hopefully this helps somebody other than just me.
The next one will ask for arguments that are not just constants like
Suc_eq_plus1, but ML expressions at run-time.
Makarius
Email Gateway (Aug 19 2022 at 10:42):From: Joachim Breitner <breitner@kit.edu>
Hi,
Nice!
I can use this to somewhat emulate the [1!] feature¹ suggested on
isabelle-dev, without patching Isabelle:
notepad
begin
assume x: "B"
assume y: "A ⟹ B"
assume z: A
have B
apply ((tactic {* SOLVE (@{tactic "rule x"} @{context}) *})[1]) -- "solves the goal, so it works"
done
have B
apply ((tactic {* SOLVE (@{tactic "rule y"} @{context}) *})[1]) -- "does not solve it, hence fails"
sorry
Unfortunately, it does not parse complete method text with , | + ...:
have B
apply ((tactic {* SOLVE (@{tactic "rule y, rule z"} @{context}) *})[1]) -- "should solve, but doesn't parse"
done
Do you think that would be possible as well?
I tried to find a way, but a parsed sequence of proof methods is a
Method.text, which is interpreted by Proof.apply_text, and I did not
find a way to turn a aggregate Method.text to a Method.method to use
with Method.apply.
Thanks,
Joachim
¹ https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-March/003911.html
signature.asc
Last updated: Apr 20 2024 at 01:05 UTC