Email Gateway (Jul 25 2022 at 14:30): Email Gateway (Jul 25 2022 at 14:30):From: Thomas Sewell <tals4@cam.ac.uk>
I've come across a really annoying situation in which the simplifier went into a loop.
After a lot of fiddling, I can exhibit a minimised example:
lemma
"P (f x) ==> f x = f y ==> y = x ==> Q"
apply simp
This seems to put the simplifier into a cycle, rewriting "f x -> f y" and then "y -> x" back again. Curiously, of the six possible orders of the three assumptions in this goal, this is the only one that results in this cycle.
Of course, this actual goal isn't very interesting. Also, it can be normalised into a safe form by calling clarify or hypsubst or similar before calling the simplifier.
In the actual problem I have, the problematic pattern above is exposed by doing some simplification, starting from a case that looks a bit more like this:
lemma
" nodes (next_C prev_old) = Some nd'd ==>
nodes (next_C nd'd) = Some nd' ==>
nodes (prev_C nd'd) = Some nd'a ==>
nodes (prev_C nd'a) = Some nd'e ==>
next_C nd'e = prev_C nd'd ==>
nodes (prev_C nd'd) = Some nd_old ==>
nodes (prev_C nd_old) = Some prev_old ==>
prev_C nd_old = prev_C nd' ==>
prev_C nd' = next_C ==>
Q"
apply simp
As might be obvious, this is about some kind of doubly-linked list implementation. The proof requires a case division based on whether some of the pointers might alias. It happens that this kind of list permits small cycles, so those cases cannot be ruled out by separation arguments or similar. This creates a lot of trivial special cases, and one of those cases happens to include the a version of this simplifier-looping behaviour. This can be solved, eventually, by doing some steps by hand, but both the final proof and the process of producing it are unpleasant.
I'm raising this to ask if anyone has any idea what might be possible in this kind of situation? I'm hoping for some kind of tweak to the automation that gets rid of this pattern or lets the simplifier cope with it. Obviously the simplifier is a bit unsafe to use blindly in a general setting, since there may be assumptions in the goal which lead to loops when they're used as rewrites. I've made some progress in the past by using variants like (simp(no_asm_simp)) and (simp(no_asm_use)), or controlling what the simplifier can do with (simp only: ...). None of that seems to be much help here, as different simp configurations will either fail to make any useful progress or expose the problematic case. Maybe metis or meson could solve the whole problem if supplied with enough rules about the relevant datatypes, but I haven't managed to get that to work. In general, it seems to be a problem that, once the simplifier is misbehaving, it's a lot of work to replace it with any other automation.
Any thoughts?
Update: I've found one solution to my own problem, using repeat_new from one of the Eisbach libraries to repeat (safe | simp(no_asm_use) | simp only:). I wonder if anyone can think of something better.
Best regards to all,
Thomas.
Email Gateway (Jul 25 2022 at 14:46):From: Thomas Sewell <tals4@cam.ac.uk>
My apologies, there was a typo in the larger of those two pasted goal statements.
The second one should read:
lemma
" nodes (next_C prev_old) = Some nd'd ==>
nodes (next_C nd'd) = Some nd' ==>
nodes (prev_C nd'd) = Some nd'a ==>
nodes (prev_C nd'a) = Some nd'e ==>
next_C nd'e = prev_C nd'd ==>
nodes (prev_C nd'd) = Some nd_old ==>
nodes (prev_C nd_old) = Some prev_old ==>
prev_C nd_old = prev_C nd' ==>
prev_C nd' = next_C prev_old ==>
Q"
apply simp
Also, I should mention that I've tested that this behaviour in a recent Isabelle repository version and also in the 2020 release. I'm guessing that the relevant parts of the simplifier have been stable for quite a while.
Best regards again,
Thomas.
Last updated: Apr 25 2024 at 20:15 UTC