伊莎贝尔的终止证明答案

【问题标题】：Termination proof in Isabelle伊莎贝尔的终止证明
【发布时间】：2021-07-18 18:30:53
【问题描述】：

我正在尝试为此功能提供自动终止证明：

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

与 isEmpty 存在

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

我对此完全陌生，所以我不知道终止证明是如何工作的，或者 pat_completeness 是如何工作的。

任何人都可以提供参考以了解更多信息和/或帮助我完成这个特定示例吗？

提前致谢。

【问题讨论】：

注意：如果你的递归是明确的结构，我相信证明会完全自动完成："aux p [] = []" | "aux p (x#xs) = (if p x then x # aux p xs else [])"
还要注意写isEmpty []的惯用方式就是xs ≠ []。用最惯用的方式写东西往往会让你的生活更轻松，例如因为自动化效果更好。

标签： isabelle termination hol

【解决方案1】：

文档位于https://isabelle.in.tum.de/dist/Isabelle2021/doc/functions.pdf，第 4 节。

这个想法是提供一个有充分根据的关系，并且递归调用的参数正在减少。在您的情况下，第二个参数的长度正在减少，所以：

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

【讨论】：