Recursive function leads to simplifier loop in Isabelle

Question

I have the following two Isabelle definitions:

fun remove_left :: "cmd ⇒ cmd × cmd option" where
"remove_left (Comp c d) = (case remove_left c of
  (head, Some c') ⇒ (head, Some (Comp c' d)) |
  (head, None) ⇒ (head, Some d)
)" |
"remove_left c = (c, None)"

function pop_flatten :: "cmd ⇒ cmd" where
"pop_flatten c = (case remove_left c of
  (h, Some c') ⇒ Comp h (pop_flatten c') |
  (h, None) ⇒ h
)"
by pat_completeness auto
termination by(relation "measure size"; simp; metis remove_left_decreases)

(As an exercise I am proving that various versions of program flattening routines are equal.)

The simplifier seems unable to handle this. For example, when I try the following obviously false lemma:

lemma "pop_flatten c = Skip"
  apply(simp)

The simplifier immediately goes into a loop. simp_trace shows it is continuously applying the definition of pop_flatten. My suspicion is that the case expression introduces the term c' which the simplifier considers to be completely new, so it unfolds the definition again. I am unsure how to work around this, I would like to not change my definition. I tried removing the simp rules for pop_flatten as follows:

declare pop_flatten.simps [simp del]

But now several proof steps which I would normally do by simp obviously don't work anymore. My definition of cmd is standard, just a skip, sequential composition, if and while. Is there indeed an edge case in the simplifier I am running into here, or is my definition just wrong in some way I am not seeing?

Answer 1

It's not particularly surprising that this leads to an infinite loop: The left-hand side of the pop_flatten.simps rules is immediately applicable to its right-hand side again, so you are almost guaranteed an infinite rewrite loop.

For that reason, if you do a recursive definitions with just a single equation that isn't guarded by a condition or a pattern match, it is best to immediately delete the .simps rule from the simp set (as you have done).

If you do want to apply it, you can either apply it once in a very targeted way using apply (subst pop_flatten.simps) or you can restrict it to the particular value you want to apply it to, e.g. apply (simp add: pop_flatten.simps[of c]).

Answer 2

For completeness, after Manuel's suggestion, what I wound up doing was rewriting pop_flatten to have a case split in the preconditions as follows:

function pop_flatten' :: "cmd ⇒ cmd" where
"snd (remove_left c) = None ⟹ pop_flatten' c = fst (remove_left c)" |
"snd (remove_left c) ≠ None ⟹ pop_flatten' c = Comp (fst (remove_left c)) (pop_flatten' (the (snd (remove_left c))))"
by simp auto
termination
  apply(relation "measure size")
   apply(simp)
  apply(simp add: remove_left_decreases)
  by (metis option.sel prod.collapse remove_left_decreases)

I don't know exactly, but my suspicion is that this is better for the simplifier because the unfolding is now guarded by a ⟹ condition. Apparently the simplifier is allowed to punch through the case of construct (?), which was thus my faulty assumption.

I then reproved my lemmas using this version, which all became massively simpler because I could use simp instead of having to custom design terms to be substituted, and in the end (after proving equality of pop_flatten and pop_flatten') substituted the simp-unfriendly version in there to get the final lemma. I guess this is not always an option but as my functions were pretty simple I did not have to change anything else.

(Thanks a bunch Manuel!)