首页 文章

通过长度感应,然后通过归纳规则进行上下文无关语法(例如来自prog-prove)

提问于
浏览
2

我是Isabelle / HOL的新手(虽然不是HOL),所以我决定开始学习优秀的"prog-prove" tutorial中的例子 .

我一直坚持上下文无关语法问题(第43页的练习3.5) . 在这个问题中,您将获得两个无上下文语法:

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

并要求你证明他们描述的是同一种语言 . 证明T中的元素位于S描述的语言中很容易,但我正在与另一个方向斗争 . 特别是,我想表明T描述的语言是在连接下关闭的 .

这是一个非正式的证明:假设 uv 在语言中 . 然后我们要证明 uv 在于语言 . 继续归纳 v 的长度 . 如果 length v = 0 那么 v 是空字符串而 uv = u 就完成了 . 否则,请查看T的 生产环境 规则 . 显然 v 不是空字符串,因此对于语言中的某些 w, x ,它必须是 waxb 形式 . 由于 wv 短,(强)归纳显示 uw 必须在语言中 . 现在使用第二个 生产环境 规则 .

这个证据看起来很复杂,所以我怀疑它不是prog-prove的作者想到的那个 . 所以我有两个问题:

  • 什么(非正式或正式)证明该练习的作者希望您使用?

  • (更多技术问题)我如何在Isabelle / HOL中表达我的非正式证据?

到目前为止,我的尝试/诽谤从以下开始:

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

并且第二次归纳申请失败,但我认为这是因为我要求Isabelle做错事......

1 回答

  • 2

    我可以't say what the authors expected, but let me comment anyway ;) First, what'你的 TS 的定义?我将假设以下内容:

    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 的结构进行案例分析(根据语法的情况;相应的事实是 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
    

    Update: 实际上,对 x 结构的案例分析证明是多余的 . 非正式地,我认为如下 . 假设 T xT y 成立 . 现在根据 T 的形成规则对 y 的结构进行归纳 .

    • y = [] . 然后我们就完成了 T (x @ y) = T (x @ []) = T x ,这是其中一个假设 .

    • y = u @ a # v @ [b] . 通过归纳假设(IH),我们得到 T uT vT (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持有 .

相关问题