Email Gateway (Aug 22 2022 at 19:15): Email Gateway (Aug 22 2022 at 19:15):From: Viorel Preoteasa <viorel.preoteasa@gmail.com>
Hello,
I have a lemma of the following form: "g (S f) = f" and I would like to
use it evaluate for example "g (S Suc) 3" using
value "g (S Suc) 3"
Is it possible to achieve this behavior? Simplification works OK, but I
need also a quick way to calculate this kind of expressions.
Next is the complete example
definition "S f x = f x"
lemma S_simp: "S f = f"
by (simp add: S_def fun_eq_iff)
definition "g A = (SOME f . A = S f)"
lemma g_S_simp[code,simp]: "g (S f) = f"
by (simp add: g_def S_simp)
lemma "g (S Suc) 3 = 4"
by (simp) (this works OK)
value "g (S Suc) 3" (this gives Wellsortedness error)
Best regards,
Viorel Preoteasa
Email Gateway (Aug 22 2022 at 19:16):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Manuel,
Thanks for the suggestion. I briefly had thought about this, but then dismissed it because
Viorel wrote that a "quick way" to evaluate such expressions, and code-unfold is not quick
as it is done by the simplifier.
Andreas
Email Gateway (Aug 22 2022 at 19:16):From: Manuel Eberl <eberlm@in.tum.de>
I don't see what "code_unfold" has to do with performance. Are you
perhaps confusing it with code_simp/"value [simp]"?
As far as I know, "code_unfold" is just a code generator preprocessing
option that allows you to tweak the input before the code generator is
invoked. Viorel seems to want to use something as a "code equation" that
does not fulfil the syntactic prerequisites to be a code equation, and
code_unfold works pretty well for that. I don't see why it should be slow.
Manuel
Email Gateway (Aug 22 2022 at 19:16):From: viorel.preoteasa@gmail.com
Hi,
Thank you for your messages. code_unfold is exactly what I was looking for. Probably my message was a bit confusing.
By "a quick way" I did not mean necessarily efficient, but easy way to evaluate that kind of expressions.
Before I would define a function F = g (S f), then introduce a lemma [code]: "F = f", but to introduce this lemma, I would need
to obtain f first which could be a very long expression.
Viorel
Email Gateway (Aug 22 2022 at 19:16):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Viorel,
Thanks for clarifying the requirements w.r.t. efficiency. I indeed misread your "quick" as
efficient instead of "easy to do".
Andreas
Email Gateway (Aug 22 2022 at 19:21):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Viorel,
value "..." tries to generate SML code for the given expression and evaluate it in the
run-time system. In your example, the lemma g_S_simp is not a code equation, because in a
code equation, you can only pattern match on constructors. This is also what the warning
tells you. Accordingly, the code generator ignores this equation and tries to generate
code for g using its definition. This definition contains SOME and that's where the
well-sortedness error comes from.
So there's no way to get to this behaviour for any of the evaluator. The reason is that
the code generator simply does not allow such non-constructor pattern, although the
symbolic evaluators code_simp and normalization could deal with such equations.
Andreas
Email Gateway (Aug 22 2022 at 19:22):From: Manuel Eberl <eberlm@in.tum.de>
Hello,
there is one possible solution that Andreas may have missed. Whether
this works for you depends a bit on your application, but at least in
the case you presented, you can simply use "g_S_simp" as a "code_unfold"
rule instead of a "code" rule, and then "value" works on your example:
lemma g_S_simp[code_unfold, simp]: "g (S f) = f"
You can read up on what "code_unfold" does in the code generator manual;
very briefly, if I recall correctly, it just rewrites the input
expression with the unfold rules before attempting to generate code for
it. I often use it to generate code for "non-executable" constructs that
can be rewritten into a more palatable form, or to introduce optimisations.
Manuel
Last updated: May 06 2024 at 08:19 UTC