Coq中如何表示归纳关系的某一元素无法从另一元素推导获得

你需要的是区分「蕴含成立」和「基于给定前提的语法推导路径存在」，这在Coq里是可以实现的，核心思路是把推导路径本身形式化为归纳对象，再证明你要的路径不存在。

实现逻辑 #

1. 首先明确你给出的R的核心不变量：对任意成立的R n m，m - n的值只能是1或者2，且归纳构造子Ind不会改变这个差值。
2. 你提到的蕴含式(R 2 3) -> (R 3 5)之所以可证，是因为它的证明完全没有用到前提R 2 3，而是直接通过Base2构造出R 0 2再应用三次Ind得到R 3 5，前提属于冗余项，和你要刻画的「从前提出发的连续推导路径」完全是两个概念。
3. 要形式化推导路径，可以先定义单步构造子应用关系，再取其传递闭包表示多步推导：

(* 对R的证明项打包，方便统一表示推导节点 *)
Definition R_obj := exists n m, R n m.

(* 单步推导：每一步都是Ind构造子的直接应用 *)
Inductive R_step : R_obj -> R_obj -> Prop :=
| step_apply_ind : forall n m (H : R n m),
  R_step (ex_intro _ n (ex_intro _ m H)) 
         (ex_intro _ (n+1) (ex_intro _ (m+1) (Ind n m H))).

(* 多步推导：即你说的构造子连续应用序列 *)
Inductive derives : R_obj -> R_obj -> Prop :=
| derives_refl : forall A, derives A A
| derives_trans : forall A B C, R_step A B -> derives B C -> derives A C.

4. 你要表述的命题可以直接写为：

Theorem no_derivation_path : 
  forall (pf23 : R 2 3) (pf35 : R 3 5),
  ~ derives (ex_intro _ 2 (ex_intro _ 3 pf23)) 
            (ex_intro _ 3 (ex_intro _ 5 pf35)).

证明过程非常简单：先归纳证明所有derives A B都满足「A对应的m-n差值等于B对应的m-n差值」，而R 2 3的差值是1，R 3 5的差值是2，二者矛盾即可得证。

如果不需要保留推导路径的具体结构，也可以直接给R的证明项定义高度参数、或用反演策略推导不变量，都能得到同样的结论。

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