Isabelle中LTS空Delta引理emptyDelta1证明问题

我定义了如下所示的归纳谓词，现需要证明空转移集合下可达路径必为空的引理，当前证明过程存在卡点。

基础定义 #

首先定义了标号迁移系统（LTS）的类型同义词，以及支持空转移、普通转移的可达性归纳谓词：

type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set"

inductive LTS_is_reachable :: "('q, 'a) LTS ⇒  ('q * 'q) set ⇒ 'q ⇒ 'a list ⇒ 'q ⇒ bool" where
   LTS_Empty[intro!]:"LTS_is_reachable Δ Δ' q [] q"|
   LTS_Step1:"(q, q'') ∈ Δ' ∧ LTS_is_reachable Δ Δ' q'' l q' ⟹ LTS_is_reachable Δ Δ' q l q'" |
   LTS_Step2[intro!]:"a  ∈ σ ∧ (q, σ, q'') ∈ Δ ∧ LTS_is_reachable Δ Δ' q'' w q' ⟹ LTS_is_reachable Δ Δ' q (a # w) q'"

三个构造子的含义：

• LTS_Empty：任意节点到自身存在空列表长度的可达路径
• LTS_Step1：先走Δ'集合中的空转移（不消耗输入字符），再走后续路径可达，则整体可达
• LTS_Step2：当前字符a属于转移标号集合σ，且存在Δ中对应的普通转移，后续路径可达，则a拼接后续路径的整体可达

待证引理与现有证明脚本 #

待证明的引理核心结论：当普通转移集合Δ为空时，任意可达路径对应的字符列表必然是空列表。
当前未完成的证明脚本如下，卡在LTS_Step1分支无法证明：

lemma "LTS_is_reachable {} Δ' p x q ⟹ x = []"
proof(induction rule:LTS_is_reachable.cases)
case (LTS_Empty Δ Δ' q)
then show ?case by auto
next
  case (LTS_Step1 q q'' Δ' Δ l q')
then show ?case apply simp sorry
next
case (LTS_Step2 a σ q q'' Δ Δ' w q')
then show ?case by auto
qed

卡点原因与正确证明 #

卡点原因 #

当前证明错误使用了LTS_is_reachable.cases规则做结构化证明：cases规则仅做分情况拆分，不会给出子证明中的归纳假设，因此LTS_Step1分支中无法直接得到子路径l为空的结论。LTS_Step2分支能直接通过auto证明，是因为Δ为空时(q, σ, q'') ∈ Δ直接矛盾，不需要归纳假设即可消去目标。

正确证明方法 #

将归纳规则替换为LTS_is_reachable.induct，即可在LTS_Step1分支拿到归纳假设，直接推出路径为空：

lemma emptyDelta1: "LTS_is_reachable {} Δ' p x q ⟹ x = []"
proof(induction rule:LTS_is_reachable.induct)
  case (LTS_Empty q)
  then show ?case by simp
next
  case (LTS_Step1 q q'' l q')
  then show ?case by simp
next
  case (LTS_Step2 a σ q q'' w q')
  then show ?case by simp
qed

更简洁的写法不需要手动分情况，直接用自动证明工具即可一次性证完：

lemma emptyDelta1_simp: "LTS_is_reachable {} Δ' p x q ⟹ x = []"
  by (induction rule: LTS_is_reachable.induct) auto

内容的提问来源于stack exchange，提问作者Hongjian Jiang