关于Coq中Fix与Fix_sub等价性及Fix_eq用法的技术问询

两者的核心区别 #

从你给出的类型签名能直接看出：

• Fix的递归子接受分离的参数：对每个x，递归假设是forall y : A, R y x -> P y——处理满足R y x的y时，需要同时传入y和R y x的证明。
• Fix_sub的递归子把参数打包成sig类型：递归假设是forall y : {y : A | R y x}, P (proj1_sig y)——y和对应的R y x证明被封装在sig里，用proj1_sig提取y即可。

二者逻辑完全等价，只是参数传递的形式不同。

Fix_eq不兼容Fix的原因 #

Fix_eq是Coq标准库为Fix_sub设计的递归展开引理，它的前提和结论都是基于Fix_sub的递归子结构定义的。而Fix的递归子结构与Fix_sub不匹配，直接用Fix_eq处理Fix定义的函数，必然会出现类型错误。

直接使用Fix时的正确用法 #

如果你不想用Program或Function，可以通过两种方式解决展开问题：

1. 手动转换Fix和Fix_sub的递归子

先把Fix的递归子转成Fix_sub兼容的形式，再用Fix_eq展开：

(* 把Fix的递归子F转成Fix_sub需要的F_sub *)
Definition F_sub {A} {R : A -> A -> Prop} {P : A -> Type}
  (F : forall x : A, (forall y : A, R y x -> P y) -> P x)
  (x : A) (f : forall y : {y : A | R y x}, P (proj1_sig y)) : P x :=
  F x (fun y p => f (exist _ y p)).

(* 证明Fix定义的函数等价于对应的Fix_sub函数 *)
Lemma Fix_to_Fix_sub {A} (R : A -> A -> Prop) (wf : well_founded R) {P : A -> Type}
  (F : forall x, (forall y, R y x -> P y) -> P x) :
  Fix wf P F = Fix_sub wf P (F_sub F).
Proof. apply Fix_eq. reflexivity. Qed.

之后你就可以通过这个引理，把Fix定义的函数转换成Fix_sub形式，再用Fix_eq展开。

2. 手动证明Fix专属的展开引理

直接针对Fix的结构，证明和Fix_eq功能类似的展开引理：

Lemma Fix_unfold {A} (R : A -> A -> Prop) (wf : well_founded R) {P : A -> Type}
  (F : forall x, (forall y, R y x -> P y) -> P x) (x : A) :
  Fix wf P F x = F x (fun y p => Fix wf P F y).
Proof.
  apply well_founded_induction_type wf.
  intros x IH.
  unfold Fix.
  rewrite (Fix_sub_eq wf P (F_sub F) x).
  reflexivity.
Qed.

这个引理直接对应Fix的展开逻辑，使用起来和Fix_eq一样方便，且不需要依赖Fix_sub。

补充说明 #

Coq标准库没有提供现成的Fix/Fix_sub转换函数，是因为二者本质等价，用户可以根据需求手动定义上述转换逻辑和引理，完全满足直接使用Fix的需求。

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