Email Gateway (Aug 19 2022 at 17:34): Email Gateway (Aug 19 2022 at 17:34):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I have statements like this:
0 ≤ (7 / 10 * 21 + 6 :: real)
More formally: equations and inequalities on real numerals with the
operations uminus, +, -, *, /, inverse.
I want to write a tactic that solves goals like this. The simplifier
with its ‘default’ simpset in HOL-Main can solve these automatically,
but how can I do that robustly? What is some minimal simpset that solves
these problems? Or should I perhaps use linarith?
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 17:34):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Manual,
if you are willing to import some AFP-entry then it becomes trivial:
theory Test
imports "$AFP/thys/Real_Impl/Real_Impl"
begin
lemma "0 ≤ (7 / 10 * 21 + 6 :: real)" by eval (* via oracle *)
lemma "0 ≤ (7 / 10 * 21 + 6 :: real)" by code_simp (* without oracle *)
end
Cheers,
René
Email Gateway (Aug 19 2022 at 17:34):From: Wenda Li <wl302@cam.ac.uk>
Dear Rene and Manuel,
I think we can use eval and code_simp without importing Real_Impl. Also,
I was wondering if tagging eval with "via oracle" is a little bit
misleading, as I think "via oracle" usually indicate to fully trust the
result of an external program while the method eval merely extends our
trust base with the current code generation setup.
Besides, I am a little unclear about the word "robust". By robust, do
you mean you only want to do rewritings within the kernel and avoid code
generation? If yes, simp should be robust enough as I think it only
involves rewritings through the kernel.
Cheers,
Wenda
Email Gateway (Aug 19 2022 at 17:34):From: Manuel Eberl <eberlm@in.tum.de>
Yes, I want to use only the kernel. simp would be my first choice, but I
don't know what simpset to use it with.
Email Gateway (Aug 19 2022 at 17:34):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Yes, I want to use only the kernel. simp would be my first choice, but I
don't know what simpset to use it with.
This you can perhaps figure out via code_simp: here is a potential solution,
though it might not be the cleanest one:
theory Test
imports
"$AFP/thys/Real_Impl/Real_Impl"
begin
(* a definition which uses all constants for reals that should be supperted:
numerals, +, unary -, -, /, *, <, =, ≤ *)
definition "use_all (x :: real) = (if (-x) + 3 / x * 5 - 1 ≤ x then x < 3 else x = 2)"
ML {*
val real_tac = Code_Simp.static_tac {consts = [@{const_name use_all}],
ctxt = @{context}, simpset = NONE}
*}
lemma "0 ≤ (7 / 10 * 21 + 6 :: real)"
by (tactic {* real_tac @{context} 1 *})
(* doing some nasty changes has no effect *)
declare ma_code_eqns[code del]
declare real_standard_impls[code del]
lemma [code, simp]: "x + y = x + y" by simp
lemma "0 ≤ (7 / 10 * 21 + 6 :: real)"
by (tactic {* real_tac @{context} 1 *})
end
Hope this helps,
René
Email Gateway (Aug 22 2022 at 08:58):From: Wenda Li <wl302@cam.ac.uk>
How about this one?
ML {*
fun foo1_tac (ctxt : Proof.context) i =
let
val simpset =
fold Simplifier.add_simp @{thms arith_simps times_divide_eq_left
divide_simps
rel_simps HOL.if_False HOL.if_True } (empty_simpset ctxt
|> Simplifier.set_subgoaler asm_full_simp_tac
|> Simplifier.set_mksimps (mksimps []))
in
CHANGED (asm_full_simp_tac simpset i)
end
*}
lemma "0 ≤ (7 / 10 * 21 + 6 :: real)"
apply (tactic {* foo1_tac @{context} 1 *})
We start with an empty simpset and add some basic simplification rules.
Wenda
Last updated: Apr 25 2024 at 01:08 UTC