Coq中destruct报错无法实例化元变量P，如何证明compose_trivial引理？

先定义一个通用的函数组合fun_comp，允许通过等式关联定义域与陪域：

Definition fun_comp {X Y Z W}
  (f : X -> Y) (g : Z -> W) (H : Y = Z) : X -> W.
destruct H. refine (fun x => g (f x)). Defined.

接下来尝试证明一个看似平凡的引理：

Lemma compose_trivial {X Y Z} (f : X -> Y) (g : Y -> Z) (H : Y = Y)
  : forall x, fun_comp f g H x = g (f x).
Proof.
  intros x. revert f g. destruct H.

但执行destruct H.时触发错误：

Cannot instantiate metavariable P of type
"forall a : Type, Y = a -> Prop" with abstraction
"fun (Y : Type) (H : Y = Y) =>
forall (f : X -> Y) (g : Y -> Z), fun_comp f g H x = g (f x)"
of incompatible type
"forall Y : Type, Y = Y -> Prop".

若尝试独立泛化H右侧的Y，destruct策略可生效，但会与目标右侧的g (f x)产生类型矛盾。请问该compose_trivial引理能否证明？若可以，该如何操作？

解决方案 #

可以证明，核心是避免泛化时破坏上下文的类型关联，让Coq正确识别等式两边的一致性，以下是两种可行方法：

方法1：使用subst替代destruct

subst策略会直接将等式H: Y=Y代入上下文，不会引入多余的类型泛化，可直接简化目标：

Lemma compose_trivial {X Y Z} (f : X -> Y) (g : Y -> Z) (H : Y = Y)
  : forall x, fun_comp f g H x = g (f x).
Proof.
  intros x. subst H. reflexivity.
Qed.

方法2：先展开fun_comp定义再处理

先展开fun_comp的内部实现，让Coq识别其基于destruct的构造逻辑，再用reflexivity完成证明：

Lemma compose_trivial {X Y Z} (f : X -> Y) (g : Y -> Z) (H : Y = Y)
  : forall x, fun_comp f g H x = g (f x).
Proof.
  intros x. unfold fun_comp. destruct H. reflexivity.
Qed.

原方法失败的原因

你之前执行的revert f g操作，让H的类型Y=Y中的Y绑定到上下文的全局Y，而destruct需要将等式右侧泛化为任意类型a，但目标中的g: Y->Z依赖于全局Y，无法随泛化后的a变化，因此出现类型不匹配。而subst或先展开定义的方式，不会改变上下文的类型绑定，直接利用Y=Y的自反性完成证明。

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