Coq中复杂实例应用简单引理报错，如何实现目标转换？

错误原因 #

你的引理eq1本身是正确的，但调用时参数传递错误：

• eq1的类型是(A <-> B) -> ~A -> ~B，第一个参数需要的是A和B之间的等价关系（类型为Prop <-> Prop）
• 你传入的ATK (S t_N)是单个Prop类型的表达式，不符合参数要求，因此报错。

正确的使用方式 #

假设在你的证明环境中，已经有一个等价关系假设，比如H_iff : ATK (S t_N) <-> B（这里的B是你目标中的对应命题），那么正确调用应该是：

pose proof (Test.eq1 H_iff _).

或者用更简洁的apply命令：

apply (Test.eq1 H_iff).

这会把目标从~B转化为~ATK (S t_N)，刚好匹配你当前的目标结构(A <-> B) -> ~A——你可以先引入等价关系假设H_iff : A <-> B，目标变为~A，再通过eq1 H_iff将目标转为~B。

更直接的证明方法 #

其实不需要单独定义引理，直接在证明中推导即可：
假设当前目标是(A <-> B) -> ~A，可以这样操作：

intros H_iff. (* 引入等价关系假设，目标变为~A *)
unfold not; intros H_B. (* 展开否定，假设B成立 *)
rewrite H_iff in H_B. (* 用等价关系将B替换为A *)
contradiction. (* A与~A矛盾，完成证明 *)

或者更简洁的版本：

intros H_iff not_A B_true.
rewrite <- H_iff in B_true.
contradiction.

补充：优化你的引理证明 #

你的eq1证明可以简化，无需额外assert步骤：

Section Test.
Variables A B : Prop.

Lemma eq1 : (A <-> B) -> ~A -> ~B.
Proof.
  intros H_iff not_A B_true.
  rewrite H_iff in B_true. (* 利用等价关系将B转化为A *)
  contradiction. (* 此时A和~A矛盾 *)
Qed.

End Test.

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