Доказательство f (f bool) = bool

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

(f:bool -> bool)

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

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

Итак, если функция всегда возвращает 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.

Ответ 1

Goal forall (f:bool -> bool) (b:bool), f (f (f b)) = f b.
Proof.
intros.
remember (f true) as ft.
remember (f false) as ff.
destruct ff ; destruct ft ; destruct b ; 
    try rewrite <- Heqft ; try rewrite <- Heqff ; 
    try rewrite <- Heqft ; try rewrite <- Heqff ; auto.
Qed.

Ответ 2

Более короткое доказательство:

Require Import Sumbool.

Goal forall (f : bool -> bool) (b:bool), f (f (f b)) = f b.
Proof.
  destruct b;                             (* case analysis on [b] *)
    destruct (sumbool_of_bool (f true));  (* case analysis on [f true] *)
    destruct (sumbool_of_bool (f false)); (* case analysis on [f false] *)
    congruence.                           (* equational reasoning *)
Qed.

Ответ 3

В SSRизменить:

Require Import ssreflect.

Goal forall (f:bool -> bool) (b:bool), f (f (f b)) = f b.
Proof.
move=> f.
by case et:(f true); case ef:(f false); case; rewrite ?et ?ef // !et ?ef.
Qed.

Ответ 4

Спасибо за замечательное задание! Такая прекрасная теорема!

Это доказательство с использованием C-zar декларативного стиля доказательства для Coq. Это намного дольше, чем императивные (это может быть так из-за моего слишком низкого навыка).

Theorem bool_cases : forall a, a = true \/ a = false.
proof.
    let a:bool.
    per cases on a.
    suppose it is false.
        thus thesis.
    suppose it is true.
        thus thesis.
    end cases.
end proof. Qed.

Goal forall (b:bool), f (f (f b)) = f b.
proof.
    let b:bool.
    per cases on b.

    suppose it is false.
        per cases of (f false = false \/ f false = true) by bool_cases.
        suppose (f false = false).
            hence (f (f (f false)) = f false).
        suppose H:(f false = true).
            per cases of (f true = false \/ f true = true) by bool_cases.
            suppose (f true = false).
                hence (f (f (f false)) = f false) by H.
            suppose (f true = true).
                hence (f (f (f false)) = f false) by H.
            end cases.
        end cases.

    suppose it is true.
        per cases of (f true = false \/ f true = true) by bool_cases.
        suppose H:(f true = false).
            per cases of (f false = false \/ f false = true) by bool_cases.
            suppose (f false = false).
                hence (f (f (f true)) = f true) by H.
            suppose (f false = true).
                hence (f (f (f true)) = f true) by H.
            end cases.
        suppose (f true = true).
            hence (f (f (f true)) = f true).
        end cases.

end cases.
end proof. Qed.