递归原理中能否证明等价子情形具有等价归纳假设？

问题说明 #

在递归过程中，我们有合理依据假设：若两个子情形f b1与f b2等价，它们应产生等价结果IH b1 = IH b2——毕竟我们本就打算用IH = rec ∘ f调用归纳步骤。现在需要证明如下扩展递归原理rec2，允许使用UIP/公理K，但不假设函数外延性。

相关定义与待证定理 #

Axiom UIP : forall X (x1 x2 : X) (e1 : x1 = x2) (e2 : x1 = x2), e1 = e2.

Variables (A : Type) (B : A -> Type).

Inductive W : Type := suc : forall a, (B a -> W) -> W.

Variables (P : W -> Type).
Fixpoint rec (H : forall a f, (forall b, P (f b)) -> P (suc a f)) (x : W) : P x
  := match x with suc a f => H a f (fun b => rec H (f b)) end.

(* 我们期望 rec2 H (suc a f) =
     H a f (fun b => rec H f b)
       (fun b1 b2 => f_equal (fun x => existT P _ (rec x))) *)
Theorem rec2
  (H : forall a f (IH : forall b, P (f b)),
       (forall b1 b2, f b1 = f b2 -> existT P _ (IH b1) = existT P _ (IH b2))
       -> P (suc a f))
  (x : W) : P x.

证明实现 #

通过对W类型做结构归纳，结合UIP公理构造证明项：

Proof.
  induction x as [a f IHrec].
  (* 构造兼容性证明：当f b1 = f b2时，对应existT项相等 *)
  assert (compat : forall b1 b2, f b1 = f b2 -> existT P (f b1) (IHrec b1) = existT P (f b2) (IHrec b2)).
  {
    intros b1 b2 e.
    rewrite e.
    f_equal.
    (* 利用UIP保证等式的唯一性，完成类型转换后的相等性证明 *)
    apply UIP.
  }
  (* 调用H，传入归纳假设和兼容性证明 *)
  apply H with (IH := IHrec).
  apply compat.
Qed.

证明解释 #

1. 结构归纳：针对W的构造子suc a f执行归纳，得到归纳假设IHrec : forall b, P (f b)，这正是rec2所需的IH参数。
2. 兼容性证明：定义compat函数，处理子情形相等时的结果等价性。通过重写等式e将目标统一到同一类型下，再用f_equal将问题转化为证明归纳假设的结果相等，最后借助UIP公理保证等式的唯一性，完成证明。
3. 最终调用：将归纳假设和兼容性证明传入H，完成rec2的构造。

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