Email Gateway (Aug 19 2022 at 11:51): Email Gateway (Aug 19 2022 at 11:51):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I have an executable decision procedure, say "frobnicate", that takes
some parameters and yields a result. When I run
value "frobnicate x"
I get some result "y". I would now like to turn this into a proof method
that proves the statement "frobnicate x = y", ideally by deduction,
without relying on oracles. (I dimly remember the "eval" method that, if
I recall correctly, uses the code generator and ML as an oracle, doing
basically the same thing as the "value" command)
What is the best way to do this? At the moment, I use the CONVERSION
tactical and Code_Runtime.static_holds_conv, but I am not sure what this
does internally (oracle or deduction) and it is quite slow.
Additionally, I have to pass a number of constants by hand as a list of
@{code_name … } and I am not sure which of these I really need in order
for it to work reliably.
So, how does one normally do these things? Ifi the conversion with
static_holds_conv is the way to go, is there some way to make it faster?
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 11:52):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,
Florian is the expert on Code_Runtime, but here's what I know. Can you make precise which
execution model evaluates the "frobnicate x" in the value example? In principle, you can
use [code] with the code generator, [nbe] for normalization by evaluation and [simp] for
rewriting with the simplifier. For each of these options, there's a separate method: eval,
normalization and code_simp.
The eval method generates ML code for the statement, runs it and checks that it returns
True. It cannot deal with variables in the statement.
normalization converts the statement into an intermediate language and symbolically
executes it in the intermediate language.
code_simp produces a simpset with only the code equations as rewrite rules and invokes the
simplifier with this simpset on the goal after preprocessing with the code_unfold rules.
This meets your criteria for "no oracle", but is the slowest of the three.
In the code generator tutorial, Code_Runtime.static_holds_conv is listed under the column
code, so I expect that it involves code generation and the ML oracle. Isabelle has no
execution engine for HOL, I only know that the simplifier can be used to normalise
functions, which corresponds to executing when the rewrite system are the code equations.
If this is what you want, then you should try code_simp.
Andreas
Email Gateway (Aug 19 2022 at 11:52):From: Makarius <makarius@sketis.net>
Interestingly Coq has such a builtin execution engine, and the French have
invested a lot of energy into it (conceptually and performance wise).
Nonetheless, some Coq expert users have told me that they like the
Isabelle/HOL approach better for certain applications, e.g. what
Isabelle/IsaFoR does with native Haskell compared to Coq/CoLoR with the
on-board execution engine.
Doing actual LCF proofs via computation is a different thing, though.
Makarius
Email Gateway (Aug 19 2022 at 11:53):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
ah, very good, I did not know about the code generator tutorial.
I tried to use Code_Simp now, but it does not terminate even after quite
some time. I then tried "value [simp]" with some examples and found the
following:
value [simp] "[:1:] - [:1, 2::real :]"
Result: "[:1:] + - [:1, 2:]" :: "real poly"
That is obviously not what I wanted. Does this mean that there is some
problem with the way the code equations in Polynomial.thy are set up?
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 11:53):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,
What Isabelle version are you using? And what are your imports? In Isabelle2013, I get the
following results (imports Complex_Main and Polynomial):
value [code] => "[:0, -2:]"
value [nbe] => "[:0, -2:]"
value [simp] => "[: real_of_rat (1 - 1), real_of_rat (- 2) :]"
With the development version f6629734dd2b, I get:
value [code] => "Poly [0, -2]"
value [nbe] => "Poly [0, -2]"
value [simp] => "[:1:] + - [:1, 2:]"
Two months ago, Florian changed in 3cc46b8cca5e the code setup for polynomials from
explicit constructors 0 and pCons to an abstract type with constructor Poly and destructor
coeffs. This explains why the syntax [: and :] is lost.
Since poly is now an abstract datatype, the code generator transforms the [code abstract]
equations for code generation from "Rep (f x) = ..." to "f x = Abs (...)" where Rep is the
destructor and Abs is the constructor (following the usual typedef terminology). For
code_simp, however, no such preprocessing happens, i.e., the simplifier is fed directly
with "Rep (f x) = ...". Therefore, evaluation with [simp] will be delayed until you
destruct the values. This is only a problem for value [simp], but not for proofs by
code_simp, because code_simp can only be called on terms of type bool, i.e., all
polynomials in the statement will be deconstructed if needed.
Maybe Florian can say more how one could use change value [simp] to address this issue,
possibly before the next release makes all this public.
Best,
Andreas
Email Gateway (Aug 19 2022 at 11:53):From: Manuel Eberl <eberlm@in.tum.de>
Thanks for the explanations so far.
I use the development version because, if I remember correctly, it
contains some theorems that I need.
The reason why I asked about "value [simp]" is that code_simp seems to
take a very, very long time, in fact, so long that I think it either
loops or builds up some enormously big term. Other expressions involving
polynomials also lead to unpleasant results, such as:
value [simp] "gcd [:1, 2::real :] [:3:]"
Result: "smult (real_of_rat (inverse 3)) [:3:]" :: "real poly"
If I try to use Poly instead of [: and :], I get the following error
message.
value "Poly [0::real]"
*** Abstraction violation:
*** constant Poly
Attempting to use any of the evaluation conversions on the ML level
results in the same error message, so apparently, switching from [: … :]
to Poly does not solve the problem either, it seems to make things even
worse.
I can, of course, use evaluation instead of code_simp, but I do prefer
deduction within the logic over trusted prove such as the code
generator, and apart from that, I really would like to understand what
is going wrong here and why.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 11:54):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,
Evaluation in the simplifier is a tricky beast to debug! Recently (8e8941fea278), Florian
added a tracing option code_simp_trace to see what's happening. I expect that in your
application, the abstract datatypes cause the trouble. When you use polynomials of reals,
you have the following types stacked into one another:
Evaluation with the simplifier does not obey the call-by-value strategy of ML. There are
some congruence rules for some functions like op & and op | that prevent execution of the
second argument, but nothing more. For normal code_datatypes like Numerals, int and Reals,
this is OK, because the simplifier works bottom-up, i.e., it will first simplify the
arguments of a constant (from left to right) and only then try to rewrite with the
constant's code equation. For abstract datatypes, this breaks down as can be seen in your
examples:
"inverse 3 :: rat" is not evaluated because rat is an abstract type, a quotient_of
destructor would be necessary to trigger evaluation. Instead, the simplifier continues the
execution with the code equations for outer constants. If these do not destruct "inverse
3", this term will be passed around unevaluated. As may code equation duplicate
parameters, this can yield exponentially large terms. Even worse, the duplicates are not
shared (in terms of execution), i.e., if "inverse 3" is destructed later, it will be
destructed and evaluated each time. In summary: evaluation in the simplifier currently
does not work well for abstract datatypes. Maybe Florian has some ideas to mitigate the issue.
Now to your next question with Poly: 'a poly is an abstract datatype with constructor Poly
and destructor quotient_of. The abstract means that the constructor Poly must not occur in
anything that you execute. Otherwise, you will get an abstraction violation. For normal
code generation, this check is essential for soundness, because the code generator
transforms all the [code abstract] equations from destructor style to constructor style.
For code_simp, however, this check is bogus because it does not do the transformation and
soundness is not endangered. Nevertheless, the check currently is there. Maybe you can
convince Florian to drop this check for code_simp. But this will not stop the blow-up that
I have described above.
Best,
Andreas
Email Gateway (Aug 19 2022 at 11:54):From: Makarius <makarius@sketis.net>
Please, just one more attempt to get rid of this wrong idea of "the ML
level of Isabelle".
The proper terminology is "Isabelle/ML". You don't have to understand the
reasons for that, just use the correct term as a habit.
Makarius
Email Gateway (Aug 19 2022 at 11:54):From: Manuel Eberl <eberlm@in.tum.de>
So all in all, at the moment, the only way to do something like what I
am trying to do is to rely on the code generator? Is this what all the
other decision procedure in Isabelle (such as, off the top of my head,
Presburger arithmetic) do?
Email Gateway (Aug 19 2022 at 11:54):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
So all in all, at the moment, the only way to do something like what I
am trying to do is to rely on the code generator? Is this what all the
other decision procedure in Isabelle (such as, off the top of my head,
Presburger arithmetic) do?
I do not have a complete overview over all the Isabelle decision procedures, but I know of
three approaches:
Formalise the algorithm in Isabelle, prove it correct, compile the algorithm to ML with
the code generator and use it as a decision procedure. I expect that all the proof methods
that use reflection rely on the code generator. Amine and Tobias have describe this
approach for linear arithmetic in [1].
Do the proof search outside the kernel, record it if you find one, and then replay that
prove inside the kernel. IIRC, blast uses this approach and sledgehammer/metis probably,
too. This is only sensible if the proof itself requires much less inferences than the
search. In any case, you do not have to formalise and verify your algorithm for soundness,
the kernel takes care of that.
Do everything within the kernel like the simplifier does. In your case, you could code
your own execution engine for the kernel, but that's probably overkill.
Best,
Andreas
[1] Amine Chaieb and Tobias Nipkow. Proof Synthesis and Reflection for Linear Arithmetic.
Journal of Automated Reasoning, April 2008
Email Gateway (Aug 19 2022 at 11:54):From: Tobias Nipkow <nipkow@in.tum.de>
Am 04/09/2013 17:31, schrieb Manuel Eberl:
So all in all, at the moment, the only way to do something like what I
am trying to do is to rely on the code generator?
If you want the execution speed of ML, you use the code generator. If you want
to go through the kernel, you use some form of the simplifier.
Is this what all the
other decision procedure in Isabelle (such as, off the top of my head,
Presburger arithmetic) do?
All the default decision procedures go through the kernel and use ad-hoc
combinations of inference rules, including the simplifier. Those in
Decision_Procs use reflection and the code generator. The big advantage of
reflection is speed and the ability to prove both soundness and completeness of
your algorithm.
Tobias
On 09/04/2013 04:29 PM, Andreas Lochbihler wrote:
Hi Manuel,
Evaluation in the simplifier is a tricky beast to debug! Recently
(8e8941fea278), Florian added a tracing option code_simp_trace to see
what's happening. I expect that in your application, the abstract
datatypes cause the trouble. When you use polynomials of reals, you
have the following types stacked into one another:
- Numerals with constructors One, Bit0, Bit1
- int with constructors 0, Pos, Neg
- Rationals as abstract datatype with constructor Frct and destructor
quotient_of- Reals with constructor Ratreal
- Polynomials as abstract datatype with constructor Poly and
destructor coeffsEvaluation with the simplifier does not obey the call-by-value
strategy of ML. There are some congruence rules for some functions
like op & and op | that prevent execution of the second argument, but
nothing more. For normal code_datatypes like Numerals, int and Reals,
this is OK, because the simplifier works bottom-up, i.e., it will
first simplify the arguments of a constant (from left to right) and
only then try to rewrite with the constant's code equation. For
abstract datatypes, this breaks down as can be seen in your examples:"inverse 3 :: rat" is not evaluated because rat is an abstract type, a
quotient_of destructor would be necessary to trigger evaluation.
Instead, the simplifier continues the execution with the code
equations for outer constants. If these do not destruct "inverse 3",
this term will be passed around unevaluated. As may code equation
duplicate parameters, this can yield exponentially large terms. Even
worse, the duplicates are not shared (in terms of execution), i.e., if
"inverse 3" is destructed later, it will be destructed and evaluated
each time. In summary: evaluation in the simplifier currently does not
work well for abstract datatypes. Maybe Florian has some ideas to
mitigate the issue.Now to your next question with Poly: 'a poly is an abstract datatype
with constructor Poly and destructor quotient_of. The abstract means
that the constructor Poly must not occur in anything that you execute.
Otherwise, you will get an abstraction violation. For normal code
generation, this check is essential for soundness, because the code
generator transforms all the [code abstract] equations from destructor
style to constructor style.
For code_simp, however, this check is bogus because it does not do the
transformation and soundness is not endangered. Nevertheless, the
check currently is there. Maybe you can convince Florian to drop this
check for code_simp. But this will not stop the blow-up that I have
described above.Best,
Andreas
On 04/09/13 15:38, Manuel Eberl wrote:
Thanks for the explanations so far.
I use the development version because, if I remember correctly, it
contains some theorems that I need.The reason why I asked about "value [simp]" is that code_simp seems to
take a very, very long time, in fact, so long that I think it either
loops or builds up some enormously big term. Other expressions involving
polynomials also lead to unpleasant results, such as:value [simp] "gcd [:1, 2::real :] [:3:]"
Result: "smult (real_of_rat (inverse 3)) [:3:]" :: "real poly"If I try to use Poly instead of [: and :], I get the following error
message.value "Poly [0::real]"
*** Abstraction violation:
*** constant PolyAttempting to use any of the evaluation conversions on the ML level
results in the same error message, so apparently, switching from [: … :]
to Poly does not solve the problem either, it seems to make things even
worse.I can, of course, use evaluation instead of code_simp, but I do prefer
deduction within the logic over trusted prove such as the code
generator, and apart from that, I really would like to understand what
is going wrong here and why.Cheers,
Manuel
On 09/04/2013 03:28 PM, Andreas Lochbihler wrote:
Hi Manuel,
I tried to use Code_Simp now, but it does not terminate even after
quite
some time. I then tried "value [simp]" with some examples and found
the
following:value [simp] "[:1:] - [:1, 2::real :]"
Result: "[:1:] + - [:1, 2:]" :: "real poly"That is obviously not what I wanted. Does this mean that there is some
problem with the way the code equations in Polynomial.thy are set up?
What Isabelle version are you using? And what are your imports? In
Isabelle2013, I get the following results (imports Complex_Main and
Polynomial):value [code] => "[:0, -2:]"
value [nbe] => "[:0, -2:]"
value [simp] => "[: real_of_rat (1 - 1), real_of_rat (- 2) :]"With the development version f6629734dd2b, I get:
value [code] => "Poly [0, -2]"
value [nbe] => "Poly [0, -2]"
value [simp] => "[:1:] + - [:1, 2:]"Two months ago, Florian changed in 3cc46b8cca5e the code setup for
polynomials from explicit constructors 0 and pCons to an abstract type
with constructor Poly and destructor coeffs. This explains why the
syntax [: and :] is lost.Since poly is now an abstract datatype, the code generator transforms
the [code abstract] equations for code generation from "Rep (f x) =
..." to "f x = Abs (...)" where Rep is the destructor and Abs is the
constructor (following the usual typedef terminology). For code_simp,
however, no such preprocessing happens, i.e., the simplifier is fed
directly with "Rep (f x) = ...". Therefore, evaluation with [simp]
will be delayed until you destruct the values. This is only a problem
for value [simp], but not for proofs by code_simp, because code_simp
can only be called on terms of type bool, i.e., all polynomials in the
statement will be deconstructed if needed.Maybe Florian can say more how one could use change value [simp] to
address this issue, possibly before the next release makes all this
public.Best,
Andreas
Email Gateway (Aug 19 2022 at 11:55):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Why is it wrong? It seems a perfectly good description as I understand
the structure of the system.
Anyone who doesn't understand the reasons for what you say isn't likely
to see the expression "the ML level of Isabelle" as a "wrong idea", or
"Isabelle/ML" as the only correct term.
Cheers,
Jeremy
Makarius wrote:
Email Gateway (Aug 19 2022 at 11:55):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Manuel,
(first, thanks to Andreas for the thorough analysis).
the short answer is that code_simp indeed in its current state does not
perform well with abstract datatypes. To mitigate this, it would need
to be enriched with a non-trivial machinery to do bookkeeping on
invariants at runtime, to be able to reduce redexes rep (Abs x) = x when
needed. This is definitely nothing to be done in the short run.
To come to your particular issue. Usually when using the simplifier you
first determine an appropriate set of rewrite rules in order to solve
your problem by rewriting and then just do a specific simplifier setup
suited for your problem. Cf. the following minimalistic example
ML {*
val numeral_syms = @{thms numeral_1_eq_1 [symmetric] numeral_2_eq_2
[symmetric]};
fun subst_numerals ctxt =
simplify (ctxt |> put_simpset HOL_basic_ss |> fold
(Simplifier.add_simp o mk_meta_eq) numeral_syms) o Thm.transfer
(Proof_Context.theory_of ctxt)
*}
ML {* subst_numerals @{context} @{thm nat_mult_1} *}
Hope this helps,
Florian
signature.asc
Last updated: Apr 27 2024 at 01:05 UTC