Function termination proof in Isabelle

I have datatype stack_op which consists of several (~20) cases. I'm trying write function which skips some of that cases in list:

function (sequential) skip_expr :: "stack_op list ⇒ stack_op list" where
"skip_expr []  = []" 
| "skip_expr ((stack_op.Unary _)#other) = (skip_expr other)" 
| "skip_expr ((stack_op.Binary _)#other)  = skip_expr (skip_expr other)" 
| "skip_expr ((stack_op.Value _)#other) = other" 
| "skip_expr other = other"   
by pat_completeness auto termination by lexicographic_order

which seems to always terminate. But trying by lexicographic order generates such unresolved cases:

Calls:
  c) stack_op.Binary uv_ # other ~> skip_expr other
Measures:
  1) size_list size
  2) length
Result matrix:
    1  2 
c:  ?  ?

(size_change also desn't work)

I've read https://isabelle.in.tum.de/dist/Isabelle2021/doc/functions.pdf, but it couldn't help. (Maybe there are more complex examples of tremination use?)

I tried to rewrite function adding another param:

function (sequential) skip_expr :: "stack_op list ⇒ nat ⇒ stack_op list" where 
  "skip_expr l 0 = l"
| "skip_expr [] _ = []"
| "skip_expr ((stack_op.Unary _)#other) depth = (skip_expr other (depth - 1))"
| "skip_expr ((stack_op.Binary _)#other) depth = 
    (let buff1 = (skip_expr other (depth - 1))
      in (skip_expr buff1 (length buff1)))"
| "skip_expr ((stack_op.Value _)#other) _ = other"
| "skip_expr other _ = other"
 by pat_completeness auto
termination by (relation "measure (λ(_,dep). dep)") auto

which generates unresolved subgoal:

 1. ⋀other v. skip_expr_dom (other, v) ⟹ length (skip_expr other v) < Suc v

which I also don't how to proof.

Could anyone how such cases solved (As I can understand there is some problem with two-level recursive call on rigth side of stack_op.Binary case)? Or maybe there is another way to make such skip?

Thanks in advance

Solution

The lexicographic_order method simply tries to solve the arising goals with the simplifier, so if the simplifier gets stuck you end up with unresolved termination subgoals.

In this case, as you identified correctly, the problem is that you have a nested recursive call skip_expr (skip_expr other). This is always problematic because at this stage, the simplifier knows nothing about what skip_expr does to the input list. For all we know, it might just return the list unmodified, or even a longer list, and then it surely would not terminate.

Confronting the issue head on

The solution is to show something about length (skip_expr …) and make that information available to the simplifier. Because we have not yet shown termination of the function, we have to use the skip_expr.psimps rules and the partial induction rule skip_expr.pinduct, i.e. every statement we make about skip_expr xs always has as a precondition that skip_expr actually terminates on the input xs. For this, there is the predicate skip_expr_dom.

Putting it all together, it looks like this:

  lemma length_skip_expr [termination_simp]:
    "skip_expr_dom xs ⟹ length (skip_expr xs) ≤ length xs"
    by (induction xs rule: skip_expr.pinduct) (auto simp: skip_expr.psimps)

  termination skip_expr by lexicographic_order

Circumventing the issue

Sometimes it can also be easier to circumvent the issue entirely. In your case, you could e.g. define a more general function skip_exprs that skips not just one instruction but n instructions. This you can define without nested induction:

  fun skip_exprs :: "nat ⇒ stack_op list ⇒ stack_op list" where
    "skip_exprs 0 xs = xs"
  | "skip_exprs (Suc n) [] = []"
  | "skip_exprs (Suc n) (Unary _ # other) = skip_exprs (Suc n) other"
  | "skip_exprs (Suc n) (Binary _ # other) = skip_exprs (Suc (Suc n)) other"
  | "skip_exprs (Suc n) (Value _ # other) = skip_exprs n other"
  | "skip_exprs (Suc n) xs = xs"

Equivalence to your skip_expr is then straightforward to prove:

  lemma skip_exprs_conv_skip_expr: "skip_exprs n xs = (skip_expr ^^ n) xs"
  proof -
    have [simp]: "(skip_expr ^^ n) [] = []" for n
      by (induction n) auto
    have [simp]: "(skip_expr ^^ n) (Other # xs) = Other # xs" for xs n
      by (induction n) auto
    show ?thesis
      by (induction n xs rule: skip_exprs.induct)
         (auto simp del: funpow.simps simp: funpow_Suc_right)
  qed
  
  lemma skip_expr_Suc_0 [simp]: "skip_exprs (Suc 0) xs = skip_expr xs"
    by (simp add: skip_exprs_conv_skip_expr)

In your case, I don't think it actually makes sense to do this because figuring out the termination is fairly easy, but it may be good to keep in mind.