如何显式证明PLFA中inv-z≤n的m≡zero？

要搞清楚m ≡ zero的推导逻辑，得先回到PLFA里自然数小于等于关系_≤_的定义：

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n : ℕ} → zero ≤ n
  s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n

显式分情况证明 #

我们可以通过模式匹配分情况写出完整的推导步骤，把“为什么m必须是zero”的逻辑展现出来：

open import Relation.Binary.PropositionalEquality using (_≡_; refl; begin_; _≡⟨⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _≤_)

inv-z≤n : ∀ {m : ℕ} → m ≤ zero → m ≡ zero
-- 情况1：m是zero时，前提是zero ≤ zero，直接用refl证明相等
inv-z≤n {zero} z≤n =
  begin
    zero
  ≡⟨ refl ⟩
    zero
  ∎
-- 情况2：m是suc k时，不存在suc k ≤ zero的构造子，用空模式消去不可能的情况
inv-z≤n {suc k} ()

推导逻辑说明 #

给定前提m ≤ zero，只有两种可能的m：

• 当m = zero：此时前提就是zero ≤ zero，正好匹配z≤n构造子，zero ≡ zero的证明就是refl，这是最直接的等式；
• 当m = suc k：根据_≤_的构造规则，只有s≤s能构造出以suc开头的左边，但s≤s要求右边也是suc n，而zero不是任何suc n，所以这种情况不存在对应的前提构造子，用空模式()直接消去即可，不需要额外证明。

如果非要用你期望的单分支等式推理形式，也可以利用模式匹配后m被约束为zero的上下文信息，显式写出：

inv-z≤n {m} z≤n =
  begin
    m
  ≡⟨ refl ⟩ -- 此时上下文里m已经被推断为zero，refl即证明m≡zero
    zero
  ∎

这里的关键是：当你匹配到z≤n时，Agda的类型检查器已经能推断出m必须是zero，所以refl本质上就是在说zero ≡ zero。

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