Rodin工具Prover传递性证明问题求助：默认自动Prover无法完成基础不等式传递性推导

我刚上手Event-B和Rodin的时候也踩过类似的小坑，来帮你一步步理清：

为什么自动Prover没搞定这个证明？ #

Rodin的默认自动 prover（比如内置的Atelier B prover）有时候不会自动触发所有基础算术规则，尤其是当变量的类型声明不够明确的时候：

• 首先确认v和n的类型是不是都声明为ℕ（自然数）或者ℤ（整数）——如果类型模糊，prover没法识别不等式的传递性语义。
• 其次，默认的自动策略可能没有把传递性规则设为高优先级触发，这时候需要手动干预或者调整prover配置。

手动完成证明的步骤（超简单！） #

Event-B的证明基于 sequent 演算，针对这个问题直接用不等式传递性规则就能搞定：

1. 在证明视角里，你当前的 sequent 是：H1: 1 ≤ v, H2: v ≤ n ⊢ 1 ≤ n
2. 在Rodin的证明规则面板里，搜索trans_le（或者类似名称的传递性规则，不同版本可能叫le_trans）
3. 选中这个规则，依次选择假设H1和H2并点击应用——瞬间就能得到目标结论1 ≤ n，完成证明。

如果找不到直接的传递性规则，也可以用自然数的定义推导：

• 从H1得v = 1 + k（其中k ∈ ℕ）
• 从H2得n = v + m（其中m ∈ ℕ）
• 代入后n = 1 + k + m，因为k + m ≥ 0，所以1 ≤ n——不过这个步骤比直接用传递性规则繁琐多了。

调整自动Prover的配置 #

如果想让自动prover能处理这类问题，可以试试这些操作：

• 切换到SMT类的prover（比如Z3，需要提前在Rodin里安装对应的插件），这类 prover对算术规则的支持更全面，通常能自动识别传递性。
• 在Rodin的Prover Preferences里，调整自动策略的规则集，把传递性、算术相关的规则加入到默认触发列表里。

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