Matt Griffin (May 25 2023 at 22:12): Matt Griffin (May 25 2023 at 22:12):Is there a way to limit the simplifier to a single simproc, in my case fun_upd2? I understand that I can specify a list of theorems and omit all others with only but this doesn't seem to extend to simproc(s). IE: `simp only: fun_upd2' fails with "Undefined fact".
Mathias Fleury (May 26 2023 at 04:51):It is hard to recommend. The ML version:
apply (tactic ‹ALLGOALS (Simplifier.simp_tac (empty_simpset @{context} addsimprocs [\<^simproc>‹fun_upd2›]))›)
Better is probably the "one simproc is going rogue, let's deactivate it":
using [[simproc del: fun_upd2]]
Mathias Fleury said:
It is hard to recommend. The ML version:
apply (tactic ‹ALLGOALS (Simplifier.simp_tac (empty_simpset @{context} addsimprocs [\<^simproc>‹fun_upd2›]))›)Better is probably the "one simproc is going rogue, let's deactivate it":
using [[simproc del: fun_upd2]]
Thanks for this. For context, I needed to run fun_upd2 to simplify a very large map structure with repeating keys and the simp method took too long (mainly due to arith_simps/rel_simps which would persist even with "del:"). Unfortunately, the ML version you suggested doesn't solve the speed issue but I think I understand why. Looking at the definition of fun_upd2 it invokes the simplifier in the last step of "Goal.prove".
Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
(fn _ =>
resolve_tac ctxt [eq_reflection] 1 THEN
resolve_tac ctxt @{thms ext} 1 THEN
simp_tac (put_simpset ss ctxt) 1)
Is there any way I can limit the simpset in this call, or alternately pass the goal back to the caller to solve?
Mathias Fleury (May 26 2023 at 15:29):I think that this is only doing the rewriting and should not be the cause of your problem
Mathias Fleury (May 26 2023 at 15:30):can you try
supply[[simp_trace, simp_debug]]
to see if there is something weird?
Matt Griffin (May 26 2023 at 18:13):I had to extend the simp_trace_depth_limit to get meaningful results
using [[simp_trace, simp_debug, simp_trace_depth_limit=40]] apply (tactic ‹ALLGOALS (Simplifier.simp_tac (empty_simpset @{context} addsimprocs [\<^simproc>‹fun_upd2›]))›)[1]
Seems to produce output as I would expect. I guess rewriting for such a large map takes time. I am able to prove the goal much faster than the rewriting rule using a custom proof method (my use case can make a number of assumptions fun_upd2 cannot) so I've added my own simproc goal. Thank you for the help.
Last updated: Apr 28 2024 at 16:17 UTC