0

これが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.
4

1 に答える 1

0

あなたのdiffb機能は完全に問題ないようです。引数のケース分析によって定義されるため、証明は同じパスをたどる必要があります。完全なスクリプトの代わりに、2 つのアドバイスをします。

  • 戦術について学び、ケース分析を実行するcaseことをお勧めします。destruct
  • そして、その定義を見て、unfoldまたはその定義simplに置き換えdiffbて、分析後に単純化してください。

乾杯、V.

于 2013-11-07T13:14:27.673 に答える