Question

我怎么能用共同q来证明,在一次单一篮子(<条形码>>>>上采用双环形形形形形形形形形形色色色/代码(以下文目)时,采用双倍于单项 b(<条形码>>>复式>。始终如一地退还<代码>trufal>:

(f:bool -> bool)

例如,职能<代码>f 只能做4件事,请打电话给<条码>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)

因此,如果职能始终如一地恢复:

f (f bool) = f true = true

如果这种职能总是退回错误,我们就会:

f (f bool) = f false = false

在其他情况下,请将职能回报列为“条码”

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

在这两种可能的投入案件中,我们总是以原始投入为最终。如果我们承担职能回报,则同样如此。

因此,你会如何证明这一点。

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

Answer 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.

Answer 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.

Answer 3

http://ssr.msr-inria.inria.fr“rel=“nofollow noreferer”

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.

Answer 4

感谢出色的任务! 这种热爱的 the!

这是使用C-zar申报证明风格为Cq提供的证据。这比必须的要长得多(因为我的技能太低,可能会如此困难)。

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.

友情链接