coq - Coq - 我必须定义一个只有当 x 和 y 不同时才为真的函数，我还必须证明这个定义

Question

这是我定义 diffb 的尝试。diffb xy 如果 x <> y 返回 true，否则返回 false。

Definition diffb (b c : bool) : bool :=
match b, c with
| true, false => true
| false, true => true
| false, false => false
| true, true => false
end.

我已经尝试在上面定义 diffb，但我不确定它是否正确:(，我还需要证明 diffb：

Theorem diffb_correct : forall a b : bool, 
  a <> b <-> diffb a b = true.

虽然我不确定当 diffb 出现在我的子目标中时该怎么办。

谢谢

卢西奥

编辑。解决了:)

这里是

Definition diffb (b c : bool) : bool :=
match b, c with
| true, false => true
| false, true => true
| false, false => false
| true, true => false
end.

(* 现在证明你的函数满足规范。*)

Theorem diffb_correct : forall a b : bool, 
  a <> b <-> diffb a b = true.
intro a.
destruct a.
intro b.
destruct b.
split.
intro c.
destruct c.
reflexivity.
intro d.
discriminate.
split.
intro e.
reflexivity.
intro f.
discriminate.
intro g.
destruct g.
split.
intro h.
reflexivity.
discriminate.
split.
intro i.
destruct i.
reflexivity.
discriminate.
Qed.

Answer 1

你的diffb功能似乎完全没问题。由于它是通过对其论点的案例分析来定义的，因此您的证明必须遵循相同的路径。我会给你两个建议，而不是一个完整的脚本：

• 您可能想了解策略case并destruct执行案例分析。
• 并查看unfold或simpl替换diffb其定义并在分析后对其进行简化。

干杯，V。