Isabelle inductive_set能否表达谓词不成立场景及LTS证明问题

原有形式化定义 #

已编写的标记迁移系统（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" for Δ and Δ' where
  LTS_Empty[intro!]: "LTS_is_reachable Δ Δ' q [] q" |
  LTS_Step1: "LTS_is_reachable Δ Δ' q l q'" if "(q, q'') ∈ Δ'" and "LTS_is_reachable Δ Δ' q'' l q'" |
  LTS_Step2[intro!]: "LTS_is_reachable Δ Δ' q (a # w) q'" if "a ∈ σ" and "(q, σ, q'') ∈ Δ" and "LTS_is_reachable Δ Δ' q'' w q'"

其中Δ为带动作集合约束的标记迁移，Δ'为不消耗输入动作的无条件沉默迁移。

待证明的初始引理如下：

lemma "¬ LTS_is_reachable Δ Δ' q x ε  ⟹ ¬ LTS_is_reachable Δ ({(p,q)} ∪ Δ') p x ε"

核心问题说明 #

这个引理无法证明，和Isabelle归纳定义的表达能力没有关系，本质原因是引理本身不成立，可以直接举出反例：

• 最直观的反例：如果在原有迁移关系下，p本身就可以沿路径x到达ε，那无论q是否能沿x到达ε，向Δ'加入(p,q)之后，p依然保留原有的可达路径，结论直接不成立。
• 边界反例：取空路径x = []，根据LTS_Empty规则，空路径下节点只能到达自身。如果p = ε且q ≠ ε，此时前提¬ LTS_is_reachable Δ Δ' q [] ε成立，但加边后LTS_is_reachable Δ ({(p,q)} ∪ Δ') p [] ε显然成立，结论不成立。

针对你提到的归纳定义能力疑问：Isabelle的inductive/inductive_set确实是通过正向规则构造满足规则的最小谓词/集合，但这完全不代表它无法刻画否定性质。归纳定义会自动生成对应的消去规则（cases规则与归纳规则）：一个命题满足归纳谓词，当且仅当它可以通过有限次规则应用构造得到；反过来，如果所有可能推导出该命题的规则分支都无法成立，就可以证明命题不成立。实际证明中，大量关于不可达、不变量的否定性质，都是基于归纳谓词的消去规则完成的，不存在只能描述正向成立场景的限制。

修正方向 #

要让结论成立，需要补充缺失的前提约束：

• 补充前提：原有迁移关系下，p本身无法沿路径x到达ε；
• 补充边界前提：当路径x为空时，p ≠ ε；
• 注意你定义的Δ'迁移是不消耗输入的沉默迁移，加入(p,q)后，p可以先通过该沉默迁移到达q，再沿完整路径x继续推导，现有前提仅约束了q的不可达性，没有约束p原有的可达性，这是引理失效的核心原因。

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