Udowodnienie F (f BOOL) = bool

Question

Jak można w coq udowodnić, że funkcja f przyjmująca bool true|false i zwraca bool true|false (pokazane poniżej), w którym stosuje się dwa do jednego bool true|false zawsze powrócić tego samego wartość true|false:

(f:bool -> bool) 

na przykład funkcja f może zrobić tylko 4 rzeczy, pozwala wywołać wejście funkcji b:

• Zawsze powrócić true
• Zawsze wracam false
• Powrót b (tj. zwraca true jeśli b jest prawdziwe odwrotnie)
• Powrót not b (tj zwraca false, jeśli b jest prawdziwe i vice vera)

Więc jeśli funkcja zawsze zwraca true:

f (f bool) = f true = true 

i jeżeli funkcja zawsze return false chcielibyśmy dostać:

f (f bool) = f false = false 

Dla pozostałych przypadkach pozwala assum funkcja zwraca not b

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

W obu możliwych przypadkach wejściowych zawsze otrzymujemy oryginalne wejście. To samo dotyczy, jeśli założymy, że funkcja zwraca b.

Jak to udowodnić w 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

Odrobinę krótszy dowód:

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

W 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

Dzięki za wspaniały przypisania! Takie cudowne twierdzenie!

To jest dowód przy użyciu deklaratywnego stylu dowodzenia C-i dla Coq. Jest to o wiele dłuższy czas niż imperatyw (może to być spowodowane zbyt niskimi umiejętnościami).

 
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.