时间戳

首页 > 解决方案 > 如何在 Isabelle 中创建适当的引理来证明这个引理？

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

问题描述

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

作为伊莎贝尔的新学习者，我有点卡在这里。我目前能想到的唯一解决方案是提出一个适当的引理，为求解器提供足够的提示。但是，我不知道如何“适当地”将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)

任何帮助表示赞赏！

标签： isabelle

解决方案

这是一个证明：

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匹配不同的模式，所以通过单独考虑每个案例，大锤可以很容易地找到一个证明。

推荐阅读