f (f bool) = bool 증명하기

Question

어떻게하면 co.kr에서 bool true|false을 받아들이고 bool true|false (아래 그림 참조)를 반환하는 함수 f가 하나의 bool에 두 번 적용될 때 true|false가 항상 같은 값을 반환하는지 증명할 수 있습니다.

(f:bool -> bool) 

예를 들어 함수 f은 4 가지만 수행 할 수 있습니다. b 함수의 입력을 호출 할 수 있습니다.

• 항상 반환 true
• 항상 반환 false
• 반환 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. 

Answer 4

감사합니다! 그런 멋진 정리!

이것은 Coq에 C-Zar 선언적 증명 스타일을 사용한 증명입니다. 긴급한 것보다 훨씬 길다. (나의 너무 낮은 기술 때문에 그럴 수도있다.)

 
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.