模块分析：lib

1. 角色定位

lib/ 提供通用数据结构、Coq/OCaml 互操作辅助与解析工具，是全仓库的基础依赖。

2. 关键组件

• 数学与整数：Integers.v, Zbits.v, IEEE754_extra.v
• 集合/映射：Maps.v, FSetAVLplus.v, Ordered.v, UnionFind.v
• 图与遍历：Postorder.v, Iteration.v, Wfsimpl.v
• 区间/格：Intv.v, IntvSets.v, Lattice.v
• Coq 兼容与抽取：Coqlib.v, Camlcoq.ml

3. OCaml 侧工具

• Commandline.ml: 命令行解析与选项定义（driver 等使用）
• Printlines.ml: 行号与输出格式
• Readconfig.mll, Tokenize.mll, Responsefile.mll: 基础解析/配置读取工具

4. 特点

• 多数为纯函数式结构，作为证明与抽取的基础
• OCaml 文件用于运行时解析、命令行和配置读取，不参与核心证明