13

我如何在 coq 中证明一个f接受 booltrue|false并返回 bool的函数true|false（如下所示），当两次应用于单个 bool 时，true|false将始终返回相同的值true|false：

(f:bool -> bool)

例如函数f只能做 4 件事，让我们调用函数的输入b：

  • 总是返回true
  • 总是返回false
  • 返回b（即如果 b 为真，则返回真，反之亦然）
  • 返回not b（即如果 b 为真则返回假，反之亦然）

因此，如果函数始终返回 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 ：对于所有 a, a = true \/ a = false。
证明。
    让：布尔。
    每一个案例。
    假设它是错误的。
        因此论文。
    假设这是真的。
        因此论文。
    结束案例。
结束证明。Qed。

目标 forall (b:bool), f (f (fb)) = f b。
证明。
    让 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真=假）。
                因此 (f (f (f false)) = f false) 由 H.
            假设（f真=真）。
                因此 (f (f (f false)) = f false) 由 H.
            结束案例。
        结束案例。

    假设这是真的。
        根据 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) 由 H.
            假设（f false = true）。
                因此 (f (f (f true)) = f true) 由 H.
            结束案例。
        假设（f真=真）。
            因此 (f (f (f true)) = f true)。
        结束案例。

结束案例。
结束证明。Qed。
于 2011-04-15T13:54:59.233 回答