在 Agda 中证明类型为空

Question

我试图在 agda 中证明 2*3!=5。为此，我将定义一个签名为 2 * 3 ≡ 5 → ⊥ 的函数。

利用我对乘法的定义

data _*_≡_ : ℕ → ℕ → ℕ → Set where
  base : ∀ {n} → 0 * n ≡ 0
  succ : ∀ {n m k j} → m * n ≡ j → j + n ≡ k → suc m * n ≡ k

我已经证明了

1*3≡3 : 1 * 3 ≡ 3
1*3≡3 = (succ base) znn

和

3+3≡5 : 3 + 3 ≡ 5 → ⊥
3+3≡5 (sns (sns (sns ())))

但是当我试图证明时：

m235 : 2 * 3 ≡ 5 → ⊥
m235 ( ( succ  1*3≡3 ) ( x ) ) = ( 3+3≡5 x )

编译器吐出这个关于 x 的错误

.j != (suc 2) of type ℕ
when checking that the expression x has type 3 + 3 ≡ 5

对不起，如果这是一个愚蠢的问题。提前致谢。

Answer 1

首先，您忘记包含_+_≡_ 的定义。我假设如下：

data _+_≡_ : ℕ → ℕ → ℕ → Set where
  znn : ∀ {n} → 0 + n ≡ n
  sns : ∀ {n m k} → n + m ≡ k → suc n + m ≡ suc k

接下来，您的问题不在于找到正确的语法，而是您必须弄清楚如何从 2 * 3 ≡ 5 类型的值中得出结论。通过您完成的模式匹配，您可以询问 Agda 在上下文中可用的值，方法是将右侧替换为 ?，调用 Cc Cl 进行编译并使用 Cc C- 来询问上下文：

m235 : 2 * 3 ≡ 5 → ⊥
m235 ( ( succ  1*3≡3 ) ( x ) ) = ?

Agda 会说：

Goal : ⊥
-----------------------------
x     : .j + 3 ≡ 5
1*3≡3 : 1 * 3 ≡ .j
.j    : ℕ

也就是说：您正在寻求证明底部（即与假设不一致）并且您在上下文中有 3 个可用值。你有一个1 * 3 ≡ .j 类型的证明，一个未知数.j 以及一个.j + 3 ≡ 5 类型的证明。您似乎假设 Agda 可以自动注意到 j 必须为 3，但这对它来说太难了：它只会从统一中得出结论，而不是自己进行实际推理。因此解决方案是帮助 Agda 理解为什么 .j 必须为 3。您可以通过对 1 * 3 ≡ .j 类型的证明进行进一步的模式匹配来做到这一点：

m235 : 2 * 3 ≡ 5 → ⊥
m235 ((succ (succ base znn)) sum) = ?

现在上下文如下所示：

Goal: ⊥
————————————————————————————————————————————————————————————
x : 3 + 3 ≡ 5

您现在可以将3 + 3 ≡ 5 类型的证明x 与您之前证明不存在此类证明的证明结合起来：

m235 : 2 * 3 ≡ 5 → ⊥
m235 (succ (succ base znn) x) = 3+3≡5 x

---

更新：我在第一次阅读时错过了它，但是我错过了并且未能解释的问题中存在误解。错误在以下代码中：

m235 : 2 * 3 ≡ 5 → ⊥
m235 (succ  1*3≡3 x) = 3+3≡5 x

这里的误解是，这个子句左边的变量名1*3≡3，并不是指前面定义的同名值。相反，它引入了一个新的变量，Agda 知道该变量具有相同的类型，但它的值是未知的。

您所期望的可以通过使用 Agda 2.3.2 中引入的“模式同义词”功能来实现：参见the release notes：

pattern 1*3≡3 = (succ base) znn

m235 : 2 * 3 ≡ 5 → ⊥
m235 (succ  1*3≡3 x) = 3+3≡5 x

只有模式同义词在模式中扩展，其他值不会。