Stream: Beginner Questions

Topic: Focusing the simplifier

Hanno Becker (Apr 23 2023 at 05:50):

Hi! Is there a way to focus the simplifier on part of the current subgoal's conclusion? Say my goal has the shape a0 OP a1 with a1 being a very complex term which however doesn't matter yet at the stage of the proof. How could I tell the simplifier to only simplify a0, _but_ take into account the subgoals premises as usual? And, as a variant, how could I tell the simplifier to ignore _some_ assumptions? The current simp (no_asm_use) only switches between using all and ignoring all.

Lukas Stevens (Apr 23 2023 at 10:36):

Currently, this is unfortunately not possible. You could use Rewrite in HOL-Library, but that tatctic only applies a single equation.

Lukas Stevens (Apr 23 2023 at 10:48):

It shouldn't be too hard to modify the rewrite tactic to use the simplifier, though.

Hanno Becker (Apr 23 2023 at 18:02):

Thank you Lukas, I'll have a look.

Hanno Becker (Apr 23 2023 at 18:09):

Can one perhaps abstract the conclusion to a generic function application with the single argument being the sub-term to be simplified, then simplify this abstracted goal, and finally transform back into the original goal by instantiating the function accordingly?

Mathias Fleury (Apr 24 2023 at 05:00):

The SMT method is doing things like that internally a lot for speed. For example, the following from ~~src/HOL/Tools/SMT/z3_replay_methods.ML) ignores everything that is not an arithmetic term:

fun arith_th_lemma ctxt thms t =
  SMT_Replay_Methods.prove_abstract ctxt thms t arith_th_lemma_tac (
    fold_map (SMT_Replay_Methods.abstract_arith ctxt o dest_thm) thms ##>>
    SMT_Replay_Methods.abstract_arith ctxt (dest_prop t))

but I don't know how useful this would be for you.

Hanno Becker (Apr 24 2023 at 05:10):

Interesting, thanks Mathias! I will have a look and see if/how it could be adapted

Hanno Becker (Apr 24 2023 at 05:12):

What about ignoring some assumptions? In some situations close to finishing a goal, I can just filter out irrelevant premises, but generally, I'd like to tell the simplifier to ignore some assumptions, but not remove them

Mathias Fleury (Apr 24 2023 at 05:16):

you could abstract them away too

Mathias Fleury (Apr 24 2023 at 05:18):

or Subgoal.FOCUS after abstracting

Hanno Becker (Apr 24 2023 at 05:50):

Do you mind explaining a bit more how prove_abstract is to be used (and how it works)? I see you're one of the authors of z3_replay_methods.ML

Mathias Fleury (Apr 24 2023 at 06:13):

Here is a small example where I embedded it into a tactic:

(*declare [[simp_trace]]*)
lemma "(if xy then a else b) + 2= (if xy then a else b) + 2"
  apply (raw_tactic ‹HEADGOAL ((Subgoal.FOCUS (fn  {context, prems, concl, ...} =>
     let val thm = @{print} (SMT_Replay_Methods.arith_th_lemma_wo_shallow context prems (Thm.term_of concl))
     val _ = @{print} ("concl = ", concl)
     in HEADGOAL (resolve_tac context [thm]) THEN print_tac context "stuff" end) @{context}))›)
  done

Mathias Fleury (Apr 24 2023 at 06:14):

prove_abstract takes several arguments, the important ones are the conclusion (as a term), the premises (as premises), and a function to abstract

Mathias Fleury (Apr 24 2023 at 06:14):

The function to abstract iterates over the term and decides to abstract a term or to continue going into the term itself

Mathias Fleury (Apr 24 2023 at 06:16):

For example, abstract_arith_shallow (used in the example above) goes into disjunction, but does not go into if-then-else (put the simp_trace back in to see what the simplifier is handling: it does not see the if-then-else and instead has a term t1 that abstracts away)

Mathias Fleury (Apr 24 2023 at 06:34):

For now, prove_abstract supports only a syntactic criterion, but generalization should be easy… (although you need to copy-paste the code)

Kevin Kappelmann (Apr 24 2023 at 07:11):

Is your goal always of the shape OP x y where OP is a constant? Because then you may simply use an appropriate congruence rule and pass it to the simplifier.

Hanno Becker (Apr 25 2023 at 19:44):

@Kevin Kappelmann Not always, but in some meaningful cases, yes. Can you elaborate how I'd instruct the simplifier to ignore y in this case and only simplify x?

Kevin Kappelmann (Apr 28 2023 at 14:09):

@Hanno Becker sorry for the late reply. Here's an example:

definition "SIMPS_TO s t ≡ s = t"

lemma SIMPS_TO_iff: "SIMPS_TO s t ⟷ s = t" unfolding SIMPS_TO_def by simp

text ‹Prevent simplification of second argument›
lemma SIMPS_TO_cong [cong]: "s = s' ⟹ SIMPS_TO s t = SIMPS_TO s' t" by simp

lemma SIMPS_TOI: "SIMPS_TO s s" unfolding SIMPS_TO_iff by simp

lemma "SIMPS_TO (0 + 0 :: nat) (0 + 0)"
  apply (simp) (*simplifies only the first argument*)
  oops

(*you can use it to find the normal form of a term in a given context like this:*)
schematic_goal "x = 0 ⟹ SIMPS_TO (0 + 0 + x :: nat) ?X"
  apply (simp)
  apply (rule SIMPS_TOI)
  done

Kevin Kappelmann (Apr 28 2023 at 14:10):

I actually wrote some library functionality for this purpose a couple of days ago. If you are happy to wait another few days, I can share the code with you next week.

Hanno Becker (May 01 2023 at 13:37):

Thank you Kevin, that's great and already helps me. I'll likely have further questions on how to best controlled-restrict the simplifier, but I'll read a bit more first.

Last updated: Apr 28 2024 at 12:28 UTC