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