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)
For example the function f can only do 4 things, lets call the input of the function b:
- 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)
So if the function always returns true:
f (f bool) = f true = true
and if the function always return false we would get:
f (f bool) = f false = false
For the other cases lets assum the function returns not b
f (f true) = f false = true
f (f false) = f true = false
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.
So how would you prove this in coq?
Goal forall (f:bool -> bool) (b:bool), f (f b) = f b.
mattiast :
Goal forall (f:bool -> bool) (b:bool), f (f (f b)) = f b.\nProof.\nintros.\nremember (f true) as ft.\nremember (f false) as ff.\ndestruct ff ; destruct ft ; destruct b ; \n try rewrite <- Heqft ; try rewrite <- Heqff ; \n try rewrite <- Heqft ; try rewrite <- Heqff ; auto.\nQed.\n",
2009-11-26T04:45:59
akoprowski :
A tad shorter proof:\n\nRequire Import Sumbool.\n\nGoal forall (f : bool -> bool) (b:bool), f (f (f b)) = f b.\nProof.\n destruct b; (* case analysis on [b] *)\n destruct (sumbool_of_bool (f true)); (* case analysis on [f true] *)\n destruct (sumbool_of_bool (f false)); (* case analysis on [f false] *)\n congruence. (* equational reasoning *)\nQed.\n",
2010-03-02T14:04:19
Francois G :
In SSReflect:\n\nRequire Import ssreflect.\n\nGoal forall (f:bool -> bool) (b:bool), f (f (f b)) = f b.\nProof.\nmove=> f.\nby case et:(f true); case ef:(f false); case; rewrite ?et ?ef // !et ?ef.\nQed.\n",
2010-03-13T10:43:54