伊德里斯：证明一些矛盾的案例

Question

总的来说，我是 Idris 和 Proofs 的新手，但我正在通过移植到 Idris 的软件基础取得进展。我正在做一个练习

namespace Booleans

  data Bool = True | False

  andb : Booleans.Bool -> Booleans.Bool  -> Booleans.Bool
  andb True b = b
  andb False _ = False

  orb : Booleans.Bool -> Booleans.Bool -> Booleans.Bool
  orb True _ = True
  orb False b = b

  (&&) : Booleans.Bool -> Booleans.Bool  -> Booleans.Bool
  (&&) = andb

  (||) : Booleans.Bool -> Booleans.Bool  -> Booleans.Bool
  (||) = orb

  andb_eq_orb : (b, c : Booleans.Bool) -> (b && c = b || c) -> b = c

显然有四种情况，两种情况适用于自反性。

  andb_eq_orb True True _ = Refl
  andb_eq_orb True False prf = ?rhs1
  andb_eq_orb False True prf = ?rhs2
  andb_eq_orb False False _ = Refl

检查漏洞

Main.Booleans.rhs1
    prf : True && False = True || False
---------------------------------
Main.Booleans.rhs1 : True = False

Main.Booleans.rhs2
    prf : False && True = False || True
---------------------------------
Main.Booleans.rhs2 : False = True

我不明白，虽然这些断言显然不合逻辑，但我需要为这两个步骤证明这一点。我没有看到我可以做的任何重写步骤。更多但抽象地，我不理解在语言中逻辑或明确地解决这个问题的方法或模式（伊德里斯）。

---

我可以通过为类型签名实现 Uninhabbited 接口来使这两种方法都起作用：

Uninhabited (Booleans.True && Booleans.False = Booleans.True || Booleans.False) where
    uninhabited Refl impossible

Answer 1

我不确定你是如何定义 && 和 || 的，以及为什么它们不适合你，所以让我展示一下这对 stdlib Bool 是如何工作的：

如果你写如下：

andb_eq_orb : (b, c : Bool) -> (b && c = b || c) -> b = c
andb_eq_orb True  True  _   = Refl
andb_eq_orb True  False prf = ?rhs1
andb_eq_orb False True  prf = ?rhs2
andb_eq_orb False False _   = Refl

然后

> :t rhs1
prf : False = True
--------------------------------------
rhs1 : True = False
Holes: Booleans.rhs2, Booleans.rhs1

 > :t rhs2
prf : False = True
--------------------------------------
rhs2 : False = True

你可以通过这些简化的证明，在必要时交换边来填充它：

andb_eq_orb : (b, c : Bool) -> (b && c = b || c) -> b = c
andb_eq_orb True  True  _   = Refl
andb_eq_orb True  False prf = sym prf
andb_eq_orb False True  prf = prf
andb_eq_orb False False _   = Refl

另一种正确的方法是使用the Uninhabited interface，它给你一个Void的证明，前提是矛盾的。然后，您可以使用void : Void -> a 函数（又名the principle of explosion）或方便的同义词absurd = void . uninhabited：

andb_eq_orb : (b, c : Bool) -> (b && c = b || c) -> b = c
andb_eq_orb True  True  _   = Refl
andb_eq_orb True  False prf = absurd prf
andb_eq_orb False True  prf = absurd prf
andb_eq_orb False False _   = Refl