1

我试图在 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

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

4

1 回答 1

4

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

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

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

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

阿格达会说：

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。您可以通过对 type 的证明进行进一步的模式匹配来做到这一点1 * 3 ≡ .j：

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

现在上下文如下所示：

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

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

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 中引入的“模式同义词”功能可以实现您的期望：请参阅发行说明：

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

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

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

于 2013-08-09T06:09:42.267 回答