基于归纳的可判定相等类型UIP特定证明有效性探究

在Coq默认的逻辑体系中，若类型T具备可判定相等性，那么对任意x:T，所有x=x的证明都与eq_refl等价——这就是恒等证明唯一性（UIP）。针对任意满足条件的T，存在通用的标准证明；而像nat这类特定归纳类型，往往能找到更直接的替代证明。

核心问题探讨 #

1. 归纳法证明X_fwd_refl'的可行性

   • 在Coq默认的外延Martin-Löf类型论中，对满足可判定相等性的类型，尤其是nat、bool这类简单归纳类型，用归纳法证明X_fwd_refl'是完全可行的。这类类型的归纳原理可以覆盖所有元素的相等证明场景，结合可判定相等性的前提，能将任意x=x的证明归约到eq_refl。
   • 本质上，因为默认逻辑中UIP是可证的，所以基于归纳法的证明路径自然成立，可以认为在该体系下“始终可行”。

2. HoTT模型中的反例

   • 在同伦类型论（HoTT）的模型里，存在不满足UIP的类型，最典型的是圆类型（Circle）。圆类型的基点存在非平凡的自同构路径：对应不同绕圈次数的路径都是x=x的合法证明，且这些证明无法归约到eq_refl。
   • 这类场景下，给定X_eq_refl和X_eq_fwd，用归纳法无法完成X_fwd_refl'的证明——归纳原理无法覆盖圆类型的非平凡自同构路径，这就构成了明确的反例。

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