证明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为真则返回true,反之亦然)
• 返回not b(即如果b为真,则返回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.