未能解决约束：(k ≤ 5) x (k * 2 ≡ 5)。我怎样才能做到这一点？

Question

我是 agda 的新手，正在尝试证明 5 是素数:)。

我现在试图否认 2 是 5 的约数。我有：

p1 : k * 2 ≡ 5
p2 : k ≤ 5

我现在希望模式匹配如下：

case (p2 ,′ p1 ) of λ where ()

将进行类型检查，因为有 6 个术语满足

p2

，但没有一个满足

p1

。看起来计算预算不应该这么快就超出，不是吗？

有办法让它发挥作用吗？我还能如何继续

p1

和

p2

以及一般情况下：如何证明 5 是素数或 2 不能整除它？

Answer 1

让我们尝试定义以下内容：

goal : ∀ k → (k ≤ 5) × (k * 2 ≡ 5) → ⊥

如果我们简单地绑定所有变量，我们有

Goal: ⊥
y : k * 2 ≡ 5
x : k ≤ 5
k : ℕ

虽然我们可以看到这是荒谬的，但 Agda 不能：每个前提都是孤立可能的，并且 Agda 不会尝试检查

k

的每个可能值，因为它不知道何时停止。因此，我们必须通过自己进行适当的案例分割来引导它。让我们看看如果我们在

k

上分裂一次会发生什么：

goal (suc k) (x , y) = {!   !}

现在 Agda 能够将

zero

的情况视为荒谬而丢弃，因为在这种情况下我们有

y : zero ≡ suc (suc (suc (suc (suc zero))))

，这是不可能的。我们留下了

suc k

的案例，这仍然不是立即荒谬的。让我们再分开两次

k

：

goal (suc (suc zero)) (x , y) = {!   !}
goal (suc (suc (suc k))) (x , y) = {!   !}

现在 Agda 可以看出这两种情况都是荒谬的，因为在第一种情况下我们有

y : 4 ≡ 5

，而在第二种情况下我们有

y : 6 + k * 2 ≡ 5

，后者减少为

suc (k * 2) ≡ zero

。但我们不能仅仅丢弃这两种情况，因为 Agda 需要知道它应该进行这些拆分。因此，最简单的定义是

goal : ∀ k → (k ≤ 5) × (k * 2 ≡ 5) → ⊥
goal 2 ()

Agda 将创建一个包含

2

的案例树，并发现每个案例都是荒谬的（这也适用于更高的数字）。请注意，我们没有使用

k ≤ 5

参数。