Coq中互归纳“外延性”是否可靠？能否泛化至任意互归纳类型？

这是个非常关键的问题，触及了互归纳类型相等性推理的核心。我从你提到的两个角度展开解答：

一、互归纳外延性原则的普遍可靠性 #

你定义的path_eq本质上是互模拟关系的一个实例——它逐构造子地要求两个path的结构完全一致：每一步的迁移关系R相同，后续的子路径也满足path_eq。而path_extensionality公理断言这种互模拟关系蕴含命题等式p = q。

从主流的构造性数学和Coq的语义模型（比如集合论模型、域论模型，或者基于归纳构造演算的标准语义）来看，这类外延性原则是可靠的：

• 互归纳类型的元素可以被理解为"无限展开的树"，两个元素相等当且仅当它们的无限展开完全重合。path_eq正好刻画了这种逐节点的一致性，因此它和命题等式的等价性符合我们对无限结构相等性的直观理解。
• 类似的例子在Coq中很常见：比如无限流（stream）的外延性公理（两个流相等当且仅当所有位置的元素相等），本质上和你的path_extensionality是同一类原则，已经被广泛接受并用于依赖互归纳类型的证明中。

当然，在一些更严格的预设主义逻辑框架下，这类涉及无限的外延性可能会有争议，但在Coq的常规使用场景中，它是完全安全且符合直觉的。

二、为任意互归纳类型引入外延性的通用方法 #

确实不需要为每个互归纳类型手动添加专属公理，我们可以基于**互模拟（bisimulation）**这个通用概念来统一处理：

1. 互模拟的通用定义：对于任意互归纳类型，都可以自动生成对应的互模拟关系——它的规则会逐构造子要求：两个元素的构造子参数相等，且所有递归位置的子元素也满足互模拟。比如你的path_eq就是path类型的互模拟关系。
2. 通用外延性公理：对于任意互归纳类型T，假设bisim_T是它的互模拟关系，那么通用的外延性原则可以写成：

   Axiom bisim_ext_T : forall (x y : T), bisim_T x y -> x = y.
   

3. 自动化实现：在Coq中，你可以通过以下方式简化这个过程：
   • 使用**模板多态（Template Polymorphism）**编写一个通用的脚本，自动为任意互归纳类型生成互模拟关系和对应的外延性公理。
   • 借助Equations插件：它支持为互归纳类型定义等式，并自动生成基于互模拟的相等性推理规则，无需手动编写公理。
   • 一些高阶扩展（如Coq的HoTT库）中，互归纳类型的外延性甚至可以被推导出来，而不是作为公理引入，但这需要依赖同伦类型论的语义。

你的path类型的代码示例可以整理为：

Section Paths.
Context {state : Type}.
Variable R : relation state.

CoInductive path (s: state) : Type := 
| step : forall s', R s s' -> path s' -> path s.

CoInductive path_eq : forall {s}, path s -> path s -> Prop := 
| path_eq_intro : forall x y r p p', path_eq p p' -> path_eq (step x y r p) (step x y r p').

Axiom path_extensionality : forall s (p q: path s), path_eq p q -> p = q.
End Paths.

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