Stream: General

Topic: simp looping on trivial goal

Leander Behr (Nov 06 2022 at 18:27):

lemma Dummy: True ..
lemma X using Dummy apply simp+

In the above simp+ loops infinitely. It appears to be related to pulling the True premise from wherever using puts them into the regular premises of the goal beacause apply - apply simp+ works as expected. The problem appears to depend on how exactly the Dummy lemma looks. There is no problem in the following

definition "A ≡ True"
lemma Dummy: A unfolding A_def ..
lemma X using Dummy apply simp+

I am on Isabelle 2021. Is this a known issue? Anyone have an idea how to work around this in an eisbach method? I don't want to have to type apply - but method s = -, simp does not fix the problem. Is this maybe fixed in Isabelle 2022?

Leander Behr (Nov 06 2022 at 18:29):

Also, what's the proper place to look for known bugs/problems in Isabelle and report them if they are unknown? I didn't find any kind of issue tracker.

Mathias Fleury (Nov 07 2022 at 04:52):

supply [[simp_trace]] using Dummy apply simp+

Mathias Fleury (Nov 07 2022 at 04:52):

+ works by repeating a tactic until it fails

Mathias Fleury (Nov 07 2022 at 04:53):

So when does simp fail? when it has nothing to do.

Mathias Fleury (Nov 07 2022 at 04:54):

Except that simplifying Dummy counts as something

Mathias Fleury (Nov 07 2022 at 04:55):

so simp is repeatedly simplifying the Dummy assumption. Then + asks simp to do the same thing again.

Mathias Fleury (Nov 07 2022 at 04:56):

This is why apply - works: it adds Dummy to the assumption, so simp can simplify only once and fails in the next iteration of +

Mathias Fleury (Nov 07 2022 at 04:57):

So: this is exactly the expected behavior of + and of simp

Mathias Fleury (Nov 07 2022 at 04:59):

I don't know what are trying to achieve, but: apply (simp; fail)+ or apply (solves simp)+ repeats simp as long as the goal is solved, not as long as simp can do something. This is also usually more robust than simp+

Leander Behr (Nov 07 2022 at 18:49):

I use simp to do some normalizations and it's used in a loop like (simp add: norm_simps | ... | ... )+ which forms a simple solver. Now this solver loops in the described case. I don't think I can apply your solution here because I don't expect simp to solve any goals usually.

Leander Behr (Nov 07 2022 at 18:51):

curiously apply (-, simp+), which was my first idea for a fix, also loops

Leander Behr (Nov 07 2022 at 19:00):

so, simp (no_asm) fixes this, which would work for me, except I'm actually using

method_setup normalize_with_impl =
  ‹Attrib.thms >>
  (fn thms => fn ctxt =>
    SIMPLE_METHOD'
      (simp_tac (
        ((empty_simpset ctxt) addsimps thms)
      )
  ))›

because I want simp to use absolutely nothing except for my normalization rules

Mathias Fleury (Nov 07 2022 at 19:02):

simp only: norm_simps

Mathias Fleury (Nov 07 2022 at 19:02):

will use only the rule you are specifying

Mathias Fleury (Nov 07 2022 at 19:03):

Leander Behr said:

curiously apply (-, simp+), which was my first idea for a fix, also loops

you can check with supply [[simp_trace]] what is looping

Leander Behr (Nov 07 2022 at 19:24):

apply (-, simp+) loops for the same reason as simp+ apparently. The True premise is there in every invokation. simp only: norm_simps still solves some trivial subgoals which I don't want

Mathias Fleury (Nov 08 2022 at 07:15):

apply (-; simp)

Mathias Fleury (Nov 08 2022 at 07:17):

will apply simp on all goals exactly once

Christoph Madlener (Nov 08 2022 at 08:56):

Not sure if I'm missing something here, but why wouldn't you just use simp_all at that point?

Last updated: Dec 21 2024 at 12:33 UTC