Rocq中索引相等但类型检查失败问题求助

问题背景 #

定义了两个离散系统B1、B2，以及精化函数f : B2 → B1，在证明精化引理RefineIncrEven和RefineIncrOdd时，出现类型检查错误。以RefineIncrEven为例，报错信息：

ev : Nat.Even n
The term "stutter1 (f b2)" has type "B1 (h n)"
while it is expected to have type "B1 (h (n + 1))".

尽管已通过h_even引理证明当n为偶数时h(n) = h(n+1)，但Rocq的类型系统无法自动将该命题等式应用于类型匹配。

问题本质 #

Rocq的依赖类型系统要求项的类型必须严格语法匹配，即使两个类型在命题上等价（如h n和h(n+1)），它们在类型层面仍被视为不同实体。必须显式使用命题等式，将一个类型的项转换为另一个等价类型的项。

解决方案 #

修正RefineIncrEven引理 #

通过展开f的定义，利用h_even引理重写目标，使两边类型统一后完成证明：

Lemma RefineIncrEven : ∀ (n : nat) (b2 : B2 n) (ev : Nat.Even n),
  f (incr2_even ev b2) = stutter1 (f b2).
Proof.
  intros n b2 ev.
  unfold f. (* 展开f的定义，暴露内部的类型转换逻辑 *)
  rewrite (h_even ev). (* 用h_even引理将h(n+1)替换为h(n)，统一两边类型 *)
  reflexivity.
Qed.

修正RefineIncrOdd引理 #

同理，利用h_odd引理完成类型统一：

Lemma RefineIncrOdd : ∀ (n : nat) (b2 : B2 n) (odd : Nat.Odd n),
  f (incr2_odd odd b2) = incr1 (f b2).
Proof.
  intros n b2 odd.
  unfold f.
  rewrite (h_odd odd).
  reflexivity.
Qed.

优化f的定义（可选） #

如果希望f的定义更显式，可直接在定义中使用eq_rect（依赖类型转换的核心函数）处理类型匹配，避免依赖rewrite的隐式转换：

Fixpoint f (n : nat) (b2 : B2 n) : B1 (h n).
Proof.
  induction b2.
  - exact init1.
  - (* 处理incr2_even分支：用eq_rect将B1(h n)转换为B1(h(n+1)) *)
    exact (eq_rect (h n) B1 (stutter1 (f b2)) (h (n+1)) (eq_sym (h_even ev))).
  - (* 处理incr2_odd分支：用eq_rect将B1(h n + 2)转换为B1(h(n+1)) *)
    exact (eq_rect (h n + 2) B1 (incr1 (f b2)) (h (n+1)) (h_odd odd)).
  - exact (stutter1 (f b2)).
Defined.

优化后，两个精化引理可直接用reflexivity完成证明。

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