Agda 允许错误证明吗？

Question

我在 PLFA 之后在 Agda 中尝试了一下证明，特别是 monus 运算符。

-- Monus
_∸_ : ℕ → ℕ → ℕ
m ∸ zero = m
zero ∸ suc (m) = zero
suc (n) ∸ suc(m) = n ∸ m

我发现的问题是我可以做出不正确的编译“证明”：

_ : 3 ∸ 5 ≡ 0
_ =
  begin
      3 ∸ 5
    ≡⟨⟩
      2 ∸ 4
    ≡⟨⟩
      1 ∸ 3
    ≡⟨⟩
      0 ∸ 3
    ≡⟨⟩
      0
    ∎

虽然 3 ∸ 5 ≡ 0 确实如此，但在 monus 的规则中，没有规则表明 1 ∸ 3 ≡⟨⟩ 0 ∸ 3。正确应用规则 3 将产生 1 ∸ 3 ≡⟨⟩ 0 ∸ 2。我怎样才能确保我在证明的每一步中只应用正确的规则，并拒绝这种证明？谢谢你。

Answer 1

@Naïm Favier 在评论中所说的是正确的。

您要求逐步镜像特定的计算，而 Agda 不会这样做，它会一直计算。所以它一直看到

0

。

如果你想推理推导，那么你应该创建具有两个规则的单体relation；从该关系中，您可以“提取”函数，因为它是函数关系。但现在你有了证明相关的关系，推导是有形的，你将无法写下错误的推导。