使用反证法证明

Question

我有以下目标：

  f : bool -> bool
  b : bool
  H1 : f true = true
  H2 : f true = false
  H3 : f false = false
  ============================
   false = true

现在用H1和H2，我想用反证法证明目标。我知道 inversion 策略，但我不认为我可以在这里应用它。知道如何从这里开始吗？

这是完全可重现的代码，您可以在其中实现上述目标：

Theorem bool_fn_applied_thrice :
  forall (f : bool -> bool) (b : bool),
  f (f (f b)) = f b.
Proof.
  intros f b.
  destruct (f b) eqn:H1.
  - destruct (f true) eqn:H2.
    + rewrite -> H2.
      reflexivity.
    + destruct (f false) eqn:H3.
      * reflexivity.
      * destruct b in H1.
        {

        }

也有兴趣知道是否有比上述方法更简单的解决上述定理的方法（只是提示。另一种方法是最初在 b 上使用 destruct，这实际上证明了使用 5 次 destructs 后的定理）。

Answer 1

有很多方法可以继续，由于这是一个来自软件基础的练习，可以作为家庭作业，我不会给出完整的答案。

确实H1和H2相互矛盾

我希望您此时了解的方式是使用重写。例如，rewrite H1 in H2. 将在 H2 中用 true 替换 f true，生成 H2 : true = false。然后您可以执行 inversion H2 或 discriminate.

我不确定是否有最好的证明方法，基本上有 8 种情况需要考虑，而且只有很小的空间可以简化这些。

使用反证法证明

Proving using contradiction technique

coq