13

coqでf、boolを受け入れてbooltrue|falseを返す関数true|false（以下に表示）を1つのboolに2回適用すると、true|false常に同じ値が返されることを証明するにはどうすればよいですかtrue|false。

(f:bool -> bool)

たとえば、関数fは4つのことしか実行できません。関数の入力を呼び出しましょうb：

  • 常に戻るtrue
  • 常に戻るfalse
  • Return b（つまり、bがtrueの場合はtrueを返し、その逆の場合）
  • Return not b（つまり、bがtrueの場合はfalseを返し、その逆の場合はfalseを返します）

したがって、関数が常にtrueを返す場合：

f (f bool) = f true = true

関数が常にfalseを返す場合、次のようになります。

f (f bool) = f false = false

その他の場合は、関数がnot b

f (f true) = f false = true
f (f false) = f true = false

両方の可能な入力の場合、私たちは常に元の入力で終わります。関数がを返すと仮定した場合も同じことが言えますb。

では、これをcoqでどのように証明しますか？

Goal forall (f:bool -> bool) (b:bool), f (f b) = f b.
4

4 に答える 4

11 
Goal forall (f:bool -> bool) (b:bool), f (f (f b)) = f b.
Proof.
intros.
remember (f true) as ft.
remember (f false) as ff.
destruct ff ; destruct ft ; destruct b ; 
    try rewrite <- Heqft ; try rewrite <- Heqff ; 
    try rewrite <- Heqft ; try rewrite <- Heqff ; auto.
Qed.
于 2009-11-26T04:45:59.793 に答える
4

少し短い証拠：

Require Import Sumbool.

Goal forall (f : bool -> bool) (b:bool), f (f (f b)) = f b.
Proof.
  destruct b;                             (* case analysis on [b] *)
    destruct (sumbool_of_bool (f true));  (* case analysis on [f true] *)
    destruct (sumbool_of_bool (f false)); (* case analysis on [f false] *)
    congruence.                           (* equational reasoning *)
Qed.
于 2010-03-02T14:04:19.050 に答える
4

SSReflectで：

Require Import ssreflect.

Goal forall (f:bool -> bool) (b:bool), f (f (f b)) = f b.
Proof.
move=> f.
by case et:(f true); case ef:(f false); case; rewrite ?et ?ef // !et ?ef.
Qed.
于 2010-03-13T10:43:54.693 に答える
2

素晴らしい割り当てをありがとう！そのような素敵な定理！

これは、CoqのC-zar宣言型証明スタイルを使用した証明です。それは命令型のものよりもはるかに長いです（私のスキルが低すぎるためにそうかもしれませんが）。

定理bool_cases：forall a、a = true \ / a=false。
証拠。
    a：boolをしましょう。
    の場合ごとに。
    それが間違っているとしましょう。
        したがって、論文。
    それが本当だとしましょう。
        したがって、論文。
    エンドケース。
エンドプルーフ。Qed。

ゴールforall（b：bool）、f（f（fb））=fb。
証拠。
    b：boolとします。
    bのケースごと。

    それが間違っているとしましょう。
        bool_casesによる（f false = false \ / f false = true）のケースごと。
        仮定します（f false = false）。
            したがって、（f（f（f false））= f false）。
        H：（f false = true）と仮定します。
            bool_casesによる（f true = false \ / f true = true）のケースごと。
            仮定します（f true = false）。
                したがって、Hによる（f（f（f false））= f false）。
            （f true = true）と仮定します。
                したがって、Hによる（f（f（f false））= f false）。
            エンドケース。
        エンドケース。

    それが本当だとしましょう。
        bool_casesによる（f true = false \ / f true = true）のケースごと。
        H：（f true = false）と仮定します。
            bool_casesによる（f false = false \ / f false = true）のケースごと。
            仮定します（f false = false）。
                したがって、（f（f（f true））= f true）byH。
            仮定します（f false = true）。
                したがって、（f（f（f true））= f true）byH。
            エンドケース。
        （f true = true）と仮定します。
            したがって、（f（f（f true））= f true）。
        エンドケース。

エンドケース。
エンドプルーフ。Qed。
于 2011-04-15T13:54:59.233 に答える