如何延迟Lambda求值以替换Lambda？Coq中等价Lambda推导问题

嘿，这个场景我太熟悉了！Coq的自动β-归约确实会打断你的证明思路，直接把(fun s' : S => x = s') y归约成x = y，让你没法按预想的步骤保留Lambda结构。不过有几个实用的技巧能帮你绕开这个自动归约，一步步完成证明：

方法1：用f_equal构造应用后的等式 #

f_equal命令可以对等式两边应用同一个函数，这里我们选择应用“将函数作用到y”这个操作，这样就能得到两个Lambda应用后的等式，且不会触发自动归约：

Lemma lambda_eq_implies_eq (S : Type) (x y : S)
  (G : (fun s' : S => x = s') = (fun s' : S => y = s')) : x = y.
Proof.
  (* 对等式G两边应用"fun f => f y"，得到Lambda应用后的等式 *)
  apply f_equal with (f := fun f : S -> Prop => f y) in G.
  (* 现在G的内容是：(fun s' : S => x = s') y = (fun s' : S => y = s') y *)
  
  (* 手动触发β-归约，得到x = y = y = y *)
  simpl in G.
  
  (* 利用y=y的自反性，替换等式右边 *)
  rewrite <- eq_refl in G.
  
  (* 此时G就是我们要的x = y *)
  exact G.
Qed.

方法2：用set绑定Lambda为命名项 #

如果你想更清晰地保留Lambda的结构，可以用set命令把两个Lambda分别绑定成命名变量，这样后续操作时Coq不会自动归约它们：

Lemma lambda_eq_implies_eq' (S : Type) (x y : S)
  (G : (fun s' : S => x = s') = (fun s' : S => y = s')) : x = y.
Proof.
  (* 把两个Lambda分别绑定为f和g *)
  set (f := fun s' : S => x = s').
  set (g := fun s' : S => y = s').
  (* 此时G变成了f = g *)
  
  (* 构造f y = g y的等式 *)
  assert (f y = g y) by (rewrite G; reflexivity).
  
  (* 展开f和g的定义，触发归约 *)
  unfold f in H; unfold g in H.
  
  (* 现在H是x = y = y = y，直接用congruence完成证明 *)
  congruence.
Qed.

为什么直接构造会被归约？ #

Coq的默认解析器会自动执行β-归约（也就是把(fun x => t) a替换成t[x:=a]），所以你直接写(fun s' : S => x = s') y时，它会立刻变成x = y。而上面的两种方法通过延迟归约的方式，先构造好应用后的等式结构，再手动触发归约，完美契合你的证明思路。

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