Как я могу в coq доказать, что функцияf который принимает булtrue|false и возвращает булtrue|false (показано ниже), когда применяется дважды к одному booltrue|false всегда будет возвращать это же значение:true|false

(f:bool -> bool)

Например, функцияf можно сделать только 4 вещи, давайте вызовем ввод функции:b

Всегда возвращайсяtrueВсегда возвращайсяfalseВернутьb (т.е. возвращает истину, если b истинно, и наоборот)Вернутьnot b (т.е. возвращает false, если b истинно и наоборот)

Так что, если функция всегда возвращает true:

f (f bool) = f true = true

и если функция всегда возвращает false, мы получим:

f (f bool) = f false = false

Для других случаев давайте предположим, что функция возвращаетnot b

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

В обоих возможных случаях ввода мы всегда получаем исходный ввод. То же самое верно, если мы предположим, что функция возвращает.b

Так как бы вы доказать это в coq?

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