f Demostrando (f bool) = bool

Question

¿Cómo puedo en Coq, demostrar que una función f que acepta un bool true|false y devuelve un bool true|false (mostrado a continuación), cuando se aplica dos veces a un solo bool true|false siempre volvería ese mismo valor true|false:

(f:bool -> bool) 

Por ejemplo la función f sólo se puede hacer 4 cosas, permite llamar a la entrada de la función b:

• siempre volver true
• Siempre volver false
• Return b (es decir, devuelve verdadero si b es cierto viceversa)
• Return not b (es decir, devuelve FALSE si b es verdadero y vice vera)

lo tanto, si la función siempre devuelve verdadero:

f (f bool) = f true = true 

y si el función siempre devuelve falso que se pueden conseguir:

f (f bool) = f false = false 

Para los otros casos permite assum la función devuelve not b

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

En ambos casos de entrada posibles, siempre terminamos con la entrada original. Lo mismo vale si asumimos que la función devuelve b.

Entonces, ¿cómo demostrarías esto en coq? prueba

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

Un poco más corto:

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

En 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

Gracias por asignación maravilloso! ¡Un teorema tan encantador!

Esta es la prueba usando el estilo de prueba declarativa C-zar para Coq. Es mucho más largo que imperativo (aunque podría serlo debido a mi habilidad demasiado baja).

 
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.