Como posso no coq, provar que uma funçãof que aceita um booltrue|false e retorna um booltrue|false (mostrado abaixo), quando aplicado duas vezes a um único booltrue|false sempre retornaria esse mesmo valortrue|false:

(f:bool -> bool)

Por exemplo, a funçãof só pode fazer 4 coisas, vamos chamar a entrada da funçãob:

Volte sempretrueVolte semprefalseRetornab (ou seja, retorna verdadeiro se b é verdadeiro e vice-versa)Retornanot b (ou seja, retorna falso se b é verdadeiro e vice-versa)

Então, se a função sempre retorna true:

f (f bool) = f true = true

e se a função sempre retornar false, teríamos:

f (f bool) = f false = false

Para os outros casos, vamos supor que a função retornanot b

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

Em ambos os possíveis casos de entrada, nós sempre acabamos com a entrada original. O mesmo vale se assumirmos que a função retornab.

Então, como você prova isso no coq?

Goal forall (f:bool -> bool) (b:bool), f (f b) = f b.