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.