证明f (f bool) = bool

Question

如何在coq中证明接受bool f并返回bool true|false的函数(如下图所示)，当对单个bool true|false应用两次时，总是会返回相同的值true|false。

(f:bool -> bool)

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

• 总是返回true
• 总是返回false
• 返回b (即如果b为true，则返回true，反之亦然)
• 返回not b (如果b为true，则返回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.

Answer 1

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.

Answer 2

稍短一点的证据：

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.

Answer 3

在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.