Agda中如何避免违规证明？错误证明可编译问题咨询

问题的核心在于，你使用的≡⟨⟩本质是调用refl，而Agda的类型检查仅验证等式两端的命题相等（即最终范式相同），不会检查你写的步骤是否严格遵循Monus的定义规则。要强制每一步都正确应用规则，需要显式将Monus的每个定义条款封装为引理，证明时必须调用对应引理，而非依赖refl自动推导。

具体解决方法 #

1. 为Monus的每个定义条款定义显式引理 #

把Monus的三条规则分别命名为可调用的引理，让每一步的转换都必须对应明确的规则：

open import Relation.Binary.PropositionalEquality
open import Data.Nat

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

-- 显式定义对应每条规则的引理
monus-zero : ∀ m → m ∸ zero ≡ m
monus-zero m = refl

monus-suc-zero : ∀ m → zero ∸ suc m ≡ zero
monus-suc-zero m = refl

monus-suc-suc : ∀ n m → suc n ∸ suc m ≡ n ∸ m
monus-suc-suc n m = refl

2. 使用显式引理编写严格的证明 #

每一步必须调用对应规则的引理，若步骤不符合Monus规则，Agda会直接报错。比如你的错误步骤1 ∸ 3 ≡⟨⟩ 0 ∸ 3，在显式引理的约束下无法通过类型检查——因为suc 0 ∸ suc 2（即1 ∸ 3）对应的正确转换是0 ∸ 2，而非0 ∸ 3：

-- 正确的严格证明
_ : 3 ∸ 5 ≡ 0
_ =
  begin
      3 ∸ 5
    ≡⟨ monus-suc-suc 2 4 ⟩  -- 应用suc n ∸ suc m = n ∸ m规则
      2 ∸ 4
    ≡⟨ monus-suc-suc 1 3 ⟩  -- 再次应用第三条规则
      1 ∸ 3
    ≡⟨ monus-suc-suc 0 2 ⟩  -- 正确转换为0 ∸ 2
      0 ∸ 2
    ≡⟨ monus-suc-zero 1 ⟩   -- 应用zero ∸ suc m = zero规则
      0
    ∎

原理说明 #

显式引理将Monus的每条规则转化为类型化的约束：monus-suc-suc n m只能生成suc n ∸ suc m ≡ n ∸ m这一种等式，若你试图写出不符合规则的步骤（比如1 ∸3 ≡0∸3），Agda会检测到等式两端与引理的类型不匹配，直接拒绝编译，从而确保每一步都严格遵循定义规则。

内容的提问来源于stack exchange，提问作者Werner Germán Busch