证明F（˚F布尔）=布尔

我在COQ如何，证明，接受一个布尔true|false并返回一个函数f一个bool true|false（如下所示）中，当在单个布尔施加两次true|false将始终返回相同值true|false：证明F（˚F布尔）=布尔

(f:bool -> bool)

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

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

因此，如果函数总是返回true返回false：

f (f bool) = f true = true

，如果函数总是返回false，我们将得到：

f (f bool) = f false = false

对于其他情况下让assum该函数返回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.

来源

2009-11-04 Marcus Whybrow

我已经意识到f（f b：bool）= b不能被证明，就好像f总是返回true f（f false）== f true == true！= false。 – 2009-11-04 15:20:04

然而，f（f（fb））= f（b）。也许这更接近你想要的问题？虽然我不知道如何在Coq中证明这一点！ – 2009-11-04 15:21:53

顺便说一句，你试图证明的财产有一个名字：幂等性。 https://en.wikipedia.org/wiki/Idempotence – krokodil 2017-11-14 19:49:15

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-26 04:45:59 mattiast

写什么语言？数学？ – 2010-01-05 23:05:52

它是Coq。我想，这不太可读。 – mattiast 2010-01-07 20:54:19

一点点缩短证明：

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-02 14:04:19 akoprowski

基于相同想法的略短的证明：'intros f []; case_eq（f true）; case_eq（f false）;一致性“。 – 2018-01-18 18:34:26

在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-13 10:43:54 huitseeker

更简洁的证明：'by move => f []; case et：（f true）;例如：（f false）;重写？et？ef.' – 2018-01-18 18:33:57

感谢精彩的任务！这样一个可爱的定理！

这是使用C-ZAR声明证明样式Coq的证明。它比命令式的要长得多（因为我的技能太低，可能会这样）。

 
Theorem bool_cases : forall a, a = true \/ a = false. 
proof. 
    let a:bool. 
    per cases on a. 
    suppose it is false. 
     thus thesis. 
    suppose it is true. 
     thus thesis. 
    end cases. 
end proof. Qed. 

Goal forall (b:bool), f (f (f b)) = f b. 
proof. 
    let b:bool. 
    per cases on b. 

    suppose it is false. 
     per cases of (f false = false \/ f false = true) by bool_cases. 
     suppose (f false = false). 
      hence (f (f (f false)) = f false). 
     suppose H:(f false = true). 
      per cases of (f true = false \/ f true = true) by bool_cases. 
      suppose (f true = false). 
       hence (f (f (f false)) = f false) by H. 
      suppose (f true = true). 
       hence (f (f (f false)) = f false) by H. 
      end cases. 
     end cases. 

    suppose it is true. 
     per cases of (f true = false \/ f true = true) by bool_cases. 
     suppose H:(f true = false). 
      per cases of (f false = false \/ f false = true) by bool_cases. 
      suppose (f false = false). 
       hence (f (f (f true)) = f true) by H. 
      suppose (f false = true). 
       hence (f (f (f true)) = f true) by H. 
      end cases. 
     suppose (f true = true). 
      hence (f (f (f true)) = f true). 
     end cases. 

end cases. 
end proof. Qed.

来源

2011-04-15 13:54:59 Vag

证明F（˚F布尔）=布尔

回答

相关问题