0

次の 3 つの引数を持つ and の否定の定義が与えられれば、さまざまなケースを簡単に証明できますが、この証明を 1 つの forall ステートメントで何とか Coq を使用して書きたいと思います。Forall b1 b2 b3 : bool そのうちの 1 つが false の場合は true が返され、3 つすべてが true の場合は false が返されます。この前提を 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.
4

2 に答える 2

1

以下のように、「if and only if」定式化を使用できます。ステートメントを逆に読むと、次のように書かれています: ifnandb3が false の場合、考えられる唯一のケースは、すべての入力が true の場合です。そして、直読は完全に自明です。

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 に答える