如何在 Isabelle 中创建适当的引理来证明这个引理？

Posted 2023-03-28

【中文标题】如何在 Isabelle 中创建适当的引理来证明这个引理？

【英文标题】：How to create appropriate lemmas to prove this lemma in Isabelle?

【发布时间】：2020-05-17 13:12:52

【问题描述】：

fun intersperse :: " 'a list ⇒ 'a ⇒ 'a list" where
  "intersperse (x#y#xs) a = x#(a#(intersperse (y#xs) a))"|
  "intersperse xs _ = xs"

lemma target:"map f (intersperse xs a) = intersperse (map f xs) (f a)"

引理似乎很直观，但我无法让 Isabelle 证明这个引理。我尝试对xs 进行归纳，但大锤仍然找不到证据。然后我尝试添加辅助引理，它们都很容易证明，但对证明 target 没有多大帮助。不过，我将在下面列出我的尝试：

lemma intersp_1: "interspserse (xs@[y,x]) a = (intersperse (xs@[y]) a) @ [a,x]"
...done

lemma intersp_2:"map f (intersperse (xs@[b,x]) a) = (map f (intersperse (xs@[b]) a)) @ [(f a),(f x)]"
...done

lemma intersp_3: "map f (intersperse (x#y#xs) a) = (f x)#(f a)#(map f (intersperse (y#xs) a))"
...done

作为 Isabelle 的新学习者，我有点卡在这里。我目前能想到的唯一解决方案是提出一个适当的引理，为求解器提供足够的提示。但是我不知道如何“适当地”将target 的归纳步骤（在 xs 上应用归纳之后）划分为补充引理。归纳步骤是

goal (1 subgoal):
 1. ⋀aa xs.
       map f (intersperse xs a) = intersperse (map f xs) (f a) ⟹
       map f (intersperse (aa # xs) a) = intersperse (map f (aa # xs)) (f a)

感谢任何帮助！

【参考方案1】：

这是一个证明：

lemma target: "map f (intersperse xs a) = intersperse (map f xs) (f a)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  consider "xs = []" | "∃y ys. xs = y # ys" by (meson list.exhaust)
  then show ?case using Cons by (cases; auto)
qed

这里的关键是intersperse (x # []) a和intersperse (x # y # ys) a匹配不同的模式，所以通过单独考虑每个案例，大锤可以很容易地找到一个证明。

【讨论】：

除了手动区分大小写，您还可以使用 `by (cases xs) auto`。

【参考方案2】：

这是另一种选择：对intersperse 使用专门的归纳规则：

lemma target:"map f (intersperse xs a) = intersperse (map f xs) (f a)"
  by (induct "(map f xs)" "f a" arbitrary: xs rule: intersperse.induct) auto

规则intersperse.induct包含三种情况：

x#y#xs [] [v]

这些可以通过自动解决，因为它们符合函数可用的简化规则。

由于引理中intersperse的参数不是变量，所以需要明确地将它们赋予induct方法，并使用arbitrary来说明变量部分是什么。