证明f（f bool）= bool [英] Proving f (f bool) = bool

问题描述

我怎样才能证明自己的函数 f 接受布尔 true | false 并返回一个bool true | false （如下所示），当两次应用于单个bool true | false 时，总是返回相同的结果值 true | false ：

How can I in coq, prove that a function f that accepts a bool true|false and returns a bool true|false (shown below), when applied twice to a single bool true|false would always return that same value true|false:

(f:bool -> bool)

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

For example the function f can only do 4 things, lets call the input of the function b:

• 总是返回 true


• 总是返回 false


• 返回 b （即，如果b为真，则返回true，反之亦然）


• 返回不是b （即，如果b为true则返回false，反之亦然）

• Always return true
• Always return false
• Return b (i.e. returns true if b is true vice versa)
• Return not b (i.e. returns false if b is true and vice vera)

因此，如果函数始终返回true：

So if the function always returns true:

f (f bool) = f true = true

，如果函数始终返回false，我们将得到：

and if the function always return false we would get:

f (f bool) = f false = false

在其他情况下，假设函数返回不是b

For the other cases lets assum the function returns not b

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

在两种可能的输入情况下，我们总是以原始的输入。如果我们假设函数返回 b ，同样如此。

In both possible input cases, we we always end up with with the original input. The same holds if we assume the function returns b.

那么您如何在coq中证明这一点？ p>

So how would you prove this in coq?

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

推荐答案

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.

这篇关于证明f（f bool）= bool的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！