coq - 证明 f (f bool) = bool

Question

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

(f:bool -> bool)

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

永远返回 true

永远返回 false

返回 b (即如果 b 为真则返回真，反之亦然)

返回 not b (即，如果 b 为真则返回假，反之亦然)

所以如果函数总是返回真:

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.