Coq记录类型合一失败：改写引理时为何无法自动转换类型？

问题复现代码 #

Record ord : Type := mk_ord
{ tord: Type;
  ole: tord -> tord -> Prop;
}.

Definition onat := mk_ord nat le.

Definition singl (O : ord) (e : tord O) : list (tord O) :=
  cons e nil.

Lemma singl_len :
  forall (O : ord) (e : tord O), length (singl O e) = 1.
Proof.
  trivial.
Qed.

Example unif : length (singl onat 2) = 1.
Proof.
  Set Printing All.
  simpl (tord _). (* [tord nat] 变为 [nat] *)
  Fail rewrite singl_len.
Abort.

问题原因 #

你猜的方向没错，核心是Coq的依赖类型统一算法仅做语法匹配，不会自动展开定义判断语义相等：

• 引理singl_len的结论里，singl O e的类型是list (tord O)
• 执行simpl (tord _)后，目标里的singl onat 2类型变成list nat，和list (tord O)在语法结构上不一致
• 虽然tord onat定义等价于nat，但rewrite的默认统一过程不会主动展开ord的投影tord来完成匹配，因此无法将?O绑定为onat

解决办法 #

1. 移除提前的simpl操作 #

直接去掉simpl (tord _)步骤，此时目标里的singl onat 2类型保持为list (tord onat)，和引理的list (tord O)语法完全匹配，rewrite会自动绑定?O := onat：

Example unif : length (singl onat 2) = 1.
Proof.
  rewrite singl_len.
Qed.

2. 显式指定引理的实例 #

如果已经执行了simpl，可以直接把O和e的具体实例传给引理，跳过统一过程：

Example unif : length (singl onat 2) = 1.
Proof.
  Set Printing All.
  simpl (tord _).
  rewrite (singl_len onat 2).
Qed.

3. 使用setoid_rewrite替代rewrite #

setoid_rewrite会考虑定义相等这类等价关系，能自动展开投影完成匹配，即使做了simpl也能成功：

Example unif : length (singl onat 2) = 1.
Proof.
  Set Printing All.
  simpl (tord _).
  setoid_rewrite singl_len.
Qed.

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