定理的 Coq 语法涵盖了三个 args 的否定情况答案

【问题标题】：Coq syntax for theorem covering cases of negation of and with three args定理的 Coq 语法涵盖了三个 args 的否定情况
【发布时间】：2016-04-11 16:05:53
【问题描述】：

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

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.

【问题讨论】：

标签： coq coq-tactic

【解决方案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.

然后我们只是在破坏方面提供一点帮助，其余的工作执行intuition 策略。

【讨论】：

【解决方案2】：

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

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

【讨论】：