0

给定以下对 和 的否定定义以及三个参数，我可以轻松地证明不同的情况，但我想以某种方式使用 Coq 将这个证明写在一个 forall 语句中。Forall b1 b2 b3 : bool 其中一个为假返回真，三个为真返回假。我如何在 Coq 中编写这个前提，以便我可以使用拆分之类的策略来分解连词等？

Definition negb (b:bool) : bool :=
match b with
| true => false
| false  => true
end.

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

Definition nandb3 (b1:bool)(b2:bool)(b3:bool):bool :=
 negb (andb3 b1 b2 b3).


Example nandb1: (nandb3 true false true) = true.
Proof. reflexivity. Qed.

Example nandb2: (nandb3 false true true) = true.
Proof. reflexivity. Qed.
4

2 回答 2

1

您可以使用“当且仅当”公式，如下所示。如果您向后阅读该语句，它会说：如果nandb3给您错误，那么唯一可能的情况是所有输入都为真。而直读完全是微不足道的。

Lemma nandb3_property : forall b1 b2 b3,
  b1 = true /\ b2 = true /\ b3 = true <->
  nandb3 b1 b2 b3 = false.
Proof.
  intros b1 b2 b3.
  destruct b1; destruct b2; destruct b3; intuition.
Qed.

然后我们只是在破坏方面提供一点帮助，剩下的工作就是直觉策略。

于 2016-04-11T18:21:00.493 回答
0

math-comp 中提供了一个解决方案，基本上您定义自己的归纳And3并证明 Anton 概述的等价性。然后，您可以使用 case 和构造函数来处理这 3 个目标。看：

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrbool.v#L757

于 2016-04-12T03:01:39.830 回答