false = 在 Coq 中求解引理时的真实问题

Question

我有定义：

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

还有引理...

Lemma l1: forall p : bool, f p false = true.

我尝试过的是这样的：

Lemma l1: forall p : bool, f p false = true.
Proof.
intros p.
destruct p.
simpl.
reflexivity.
simpl.

然后我得到 false=true。该怎么办？

Answer 1

你无法证明

l1

，因为

f false false = false

。