Termination proof in Isabelle

Question

I'm trying to provide an automatic termination proof for this function:

function aux :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list" where
  "aux p xs = (if ¬isEmpty xs ∧ p (hd xs) then hd xs#aux p (drop 1 xs) else [])"
  by pat_completeness auto

with isEmpty being

fun isEmpty :: "'a list ⇒ bool" where
  "isEmpty [] = True"
| "isEmpty (_#_) = False"

I'm totally new at this, so I don't know how termination proofs work, or how pat_completeness works, for that matter.

Could anyone provide a reference to learn more about this and/or help me with this particular example?

Thanks in advance.

Note: I believe the proof would go through fully automatically if your recursion was explicitly structural: `"aux p [] = []" | "aux p (x#xs) = (if p x then x # aux p xs else [])"` — Maya, Apr 25 '21 at 12:58
Also note that the idiomatic way to write `isEmpty []` is just `xs ≠ []`. Writing things in the most idiomatic way tends to make your life easier, e.g. because the automation works better. — Manuel Eberl, Apr 25 '21 at 15:57

score 3 · Accepted Answer · edited Jul 01 '23 at 20:11

The documentation is available at https://isabelle.in.tum.de/dist/Isabelle2022/doc/functions.pdf, Section 4. (original link modified from 2021 version).

The idea is to provide a relation that is well-founded and such that the arguments of the recursive calls are decreasing. In your case, the length of the second argument is decreasing, so:

function aux :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list" where
  "aux p xs = (if xs≠ [] ∧ p (hd xs) then hd xs#aux p (drop 1 xs) else [])"
   by pat_completeness auto
termination
  by (relation ‹measure (λ(_, xs). length xs)›)
    auto

Termination proof in Isabelle

1 Answers1