在Coq中证明引理时遇到false=true矛盾问题

你的引理l1本身是不成立的。根据f的定义：

Definition f (b1 b2 : bool) :bool := match b1 with | true => true | false => b2 end.

当p = false时，f p false会直接返回第二个参数false，显然false = true不成立——这就是你遇到矛盾的核心原因。

可行的解决方向 #

你有两种选择：

• 修正引理为正确命题：
  示例1：限定p为true的情况

  Lemma l1_correct : forall p : bool, p = true -> f p false = true.
  Proof.
    intros p H. rewrite H. simpl. reflexivity.
  Qed.
  

  示例2：调整等式右侧，覆盖所有布尔值情况

  Lemma l1_correct : forall p : bool, f p false = p.
  Proof.
    intros p. destruct p.
    - simpl. reflexivity.
    - simpl. reflexivity.
  Qed.
  

• 放弃原引理：如果原引理是基于错误假设提出的，直接重新梳理你要证明的目标。

另外补充：你当前的证明流程中，destruct p后的第二个分支（p=false）执行simpl后得到false = true，这个分支本身无法证明，也直接印证了原引理的错误性。

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