Isabelle/HOL中余类型推理及图路径定义与引理证明需求

我最近在Isabelle/HOL里折腾用隐式关系定义的图——就是那种用'a => 'a => bool类型的谓词表示边的图，graph u v就代表从u到v有一条有向边。核心需求是要描述图里的无限路径，普通的列表肯定搞不定这个，翻了Isabelle自带的《Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL》（就是datatypes.pdf那篇），用里面的'a llist惰性列表余类型来实现，目前跑起来没问题，但还有些想深挖和优化的点，跟大家分享下我的思路：

首先得导入惰性列表的理论库，然后明确图的边关系定义：

theory Graph_Paths
  imports Main "~~/src/HOL/Library/Lazy_List"
begin

(* 图的边关系：graph u v 表示u到v有一条有向边 *)
type_synonym 'a graph = "'a => 'a => bool"

llist的好处就是能同时表示有限和无限序列，完美适配图里的两种路径：

• 有限路径：以LNil结尾的惰性列表，比如LCons u (LCons v LNil)就是u→v的短路径
• 无限路径：没有LNil结尾的无限惰性列表，比如从某个节点出发绕环的无限序列

我用共递归定义了路径的合法性谓词is_path：

(* 惰性列表的共递归定义（其实Lazy_List库已经自带了，这里写出来方便理解） *)
codatatype 'a llist = LNil | LCons 'a "'a llist"

(* 判断一个惰性列表是否是图g的合法路径 *)
primcorec is_path :: "'a graph => 'a llist => bool" where
  "is_path g LNil = True"  (* 空路径默认合法，可根据需求改成False *)
| "is_path g (LCons x xs) = (case xs of
    LNil => True  (* 单节点路径合法 *)
  | LCons y ys => g x y ∧ is_path g xs)"

这里空路径和单节点路径的合法性可以根据自己的需求调整——如果只关心非空的多节点路径，直接把对应分支改成False就行。

因为涉及到余类型和无限结构，证明的时候要用到共归纳，Isabelle里的coinduction方法会帮我们处理大部分细节。举两个我已经证出来的引理：

引理1：非空路径的后继合法性 #

如果一个路径是LCons x xs，那么要么xs是空路径，要么xs的第一个节点和x有边，且xs本身也是合法路径：

lemma path_cons_validity:
  assumes "is_path g (LCons x xs)"
  shows "(xs = LNil) ∨ (∃ y ys. xs = LCons y ys ∧ g x y ∧ is_path g xs)"
proof -
  from assms show ?thesis
    by (cases xs) auto  (* 分情况讨论xs是空还是非空，自动推理就能搞定 *)
qed

引理2：无限路径的每一对相邻节点都有边 #

对于无限路径，任意位置i的节点和i+1的节点之间一定有边：

lemma infinite_path_all_edges:
  assumes "is_path g p" "llength p = ∞"
  shows "∀ i. g (lnth p i) (lnth p (i+1))"
proof (coinduction arbitrary: p)
  case (is_path g p)
  then show ?case
    by (cases p) (auto simp add: lnth_LCons llength_LCons)
    (* 共归纳的核心是拆解惰性列表的构造，结合长度无限的条件推导 *)
qed

目前的基础框架能用，但还有几个点想优化：

• 更方便的无限路径构造：想定义infinite_paths_from g u表示从u出发的所有无限路径的集合，然后证明这个集合非空的充要条件是u在一个有环的强连通分量里。
• 统一处理路径的前缀/后缀：利用llist自带的ltake（取前n个元素）、ldrop（丢弃前n个元素）操作，证明路径的前缀也是路径、无限路径的后缀还是无限路径这类性质。
• 路径的等价关系：想定义“最终等价”的关系——两个路径p和q最终等价，当且仅当存在某个n，使得ldrop n p = ldrop n q，然后证明这个关系是等价关系，以及相关的替换性质。

内容的提问来源于stack exchange，提问作者Rupert Swarbrick