按长度归纳，然后按上下文无关语法的归纳规则（来自 prog-prove 的示例）

Question

我是 Isabelle/HOL 的新手（虽然不是 HOL），所以我决定通过出色的 "prog-prove" tutorial 中的示例开始学习。

我遇到了一个与上下文无关的语法问题（第 43 页的练习 3.5）。在这个问题中，你会得到两个上下文无关的语法：

S → ε | aSb | SS
T → ε | TaTb

你被要求证明他们描述的是同一种语言。证明 T 中的元素位于 S 所描述的语言中很容易，但我正在努力寻找另一个方向。特别是，我想证明 T 描述的语言在连接下是封闭的。

这是一个非正式的证明：假设 u 和 v 位于语言中。然后我们要证明uv 存在于语言中。继续对v 的长度进行归纳。如果length v = 0 那么v 是空字符串，uv = u 就完成了。否则，请查看 T 的产生式规则。显然v 不是空字符串，因此对于语言中的某些w, x，它必须是waxb 的形式。由于w 比v 短，（强）归纳表明uw 必须位于语言中。现在使用第二个生产规则。

这个证明似乎很复杂，所以我怀疑它不是 prog-prove 的作者所想的。所以我有两个问题：

1. 练习的作者希望您使用什么（非正式或正式）证明？

2. （技术性更强）我如何在 Isabelle/HOL 中表达我上面的非正式证明？

到目前为止，我的尝试/摇摆是从以下开始的：

lemma T_mult: "cfT u ==> cfT v ==> cfT (u @ v)"
  apply (induction "length v")
  apply (auto)
  apply (induction v rule: cfT.induct)

第二次感应申请失败，但我认为这是因为我要求伊莎贝尔做错事......

Answer 1

我不能说出作者的期望，但无论如何让我评论一下；） 首先，您对T 和S 的定义是什么？我将假设以下内容：

datatype alphabet = a | b

inductive S
where
  empty [simp]: "S []" |
  betw: "S x ⟹ S (a # x @ [b])" |
  conc: "S x ⟹ S y ⟹ S (x @ y)"

inductive T
where
  empty [simp]: "T []" |
  conc_betw: "T x ⟹ T y ⟹ T (x @ a # y @ [b])"

你说得对，T x ==> T y ==> T (x @ y) 是关键引理。至于证明这个引理，因为我们有经验（和启发式）的归纳定义，它们各自的归纳规则最有可能用于通过归纳证明关于它们的事实。我觉得其他归纳方案，例如您使用 length v 对自然数进行归纳，会使事情变得不必要地复杂化。

非正式地证明

lemma
  assumes "T x" and "T y"
  shows "T (x @ y)"

我会先对T x的结构做一个case分析（根据语法的case；对应的事实是T.cases），然后对T y进行归纳（使用规则T.induct），但可能还有其他方法可以做到这一点。一般结构是

using assms
proof (cases rule: T.cases)
  case empty
  ...
next
  case (conc_betw u v)
  with `T y` show ?thesis
    apply (induct rule: T.induct)
    ...
qed

更新：实际上，对x 结构的案例分析证明是多余的。非正式地，我将论证如下。假设T x 和T y 成立。现在根据T的形成规则对y的结构进行归纳。

• y = []。然后我们从T (x @ y) = T (x @ []) = T x 开始就完成了，这是假设之一。

• y = u @ a # v @ [b]。通过归纳假设 (IH)，我们有 T u、T v、T (x @ u) 和 T (x @ v)。现在实例化T的第二个形成规则我们有

  T (x @ u) ==> T v ==> T ((x @ u) @ a # v @ [b])
  

  它简化为T (x @ u) ==> T v ==> T (x @ u @ a # v @ [b])（通过@的关联性），从而使我们能够将我们的主要目标（恰好是T (x @ u @ a # v @ [b])）简化为两个子目标T (x @ u)和T v，这反过来又成立由 IH 提供。