为什么Coq的强制类型转换无法在pair（对偶）结构中生效？

Coq 的强制转换系统默认仅支持顶层直接类型转换，不会递归深入类型构造子的参数自动应用已有的转换规则，这是问题的根本原因。

你的场景中，已声明的fromFoo仅覆盖了Foo到Bar的直接转换逻辑：

• 当你定义单个Bar类型变量时，Coq 直接匹配到顶层的Foo转Bar规则，转换正常生效
• 当你写(foo, foo)时，Coq 首先推导出该对偶的原生类型为Foo * Foo（即prod Foo Foo），你指定的目标类型是Bar * Bar，二者是乘积类型prod的不同实例，没有直接的转换规则匹配，因此类型检查失败。

Coq 不默认自动逐元素转换乘积类型成员，主要出于两点设计考量：

• 控制类型检查开销：如果默认对所有类型构造子递归应用强制转换，多层类型嵌套场景下的类型推导复杂度会大幅上升，拖慢开发效率
• 避免转换歧义：当存在多条可选转换路径时，自动递归转换很可能选择不符合用户预期的路径，引入隐性的逻辑错误

你可以通过显式声明乘积类型的提升强制转换解决该问题，针对你的场景专用的实现如下：

Inductive Foo := foo.
Inductive Bar := fromFoo of Foo.

Coercion fromFoo : Foo >-> Bar.

(* 新增 Foo*Foo 到 Bar*Bar 的强制转换规则 *)
Coercion prod_Foo_to_Bar (p : Foo * Foo) : Bar * Bar :=
  (fromFoo (fst p), fromFoo (snd p)).

(* 现在可以正常通过类型检查 *)
Definition bars : (Bar * Bar) := (foo, foo).

如果需要适配任意可转换类型的乘积转换需求，可以声明多态的通用提升规则：

Definition prod_coerce {A B C D} (c1 : A -> B) (c2 : C -> D) (p : A * C) : B * D :=
  (c1 (fst p), c2 (snd p)).

(* 声明当存在A到B、C到D的强制转换时，A*C可自动转换为B*D *)
Coercion prod_coerce : forall {A B C D}, (A -> B) -> (C -> D) -> (A * C) -> (B * D).

内容的提问来源于stack exchange，提问作者Proof-By-Sledgehammer