归纳关系：逆关系是refl的显式证明

Question

在 PLFA 中，他们定义了逆关系：

inv-z≤n :   ∀ {m : ℕ} 
            → m ≤ zero 
        ----------------------
            → m ≡ zero

然后断言：

inv-z≤n z≤n = refl

我的问题是，我怎样才能给出 m ≡ 0 的明确证明？我正在寻找看起来像这样的东西：

inv-z≤n {m} (z≤n) = 
    begin
        m
    ≡⟨⟩
        .....
    ≡⟨⟩
        zero
    ∎

但是用一些东西来完成中间步骤。当然只是简单地写

inv-z≤n {m} (z≤n) = 
    begin
        m
    ≡⟨⟩
        zero
    ∎

编译，但我觉得它不令人满意。我想知道为什么m ≡ 0，而不是仅仅写下refl是一个证明。

Answer 1

我认为为什么这是正确的方式如下：在关系

m ≤ zero

的定义中，

≤

形式的唯一不等式是

zero ≤ zero

，或等效于

z≤n {0}

。所以，如果我们假设

m ≤ zero

，我们“必须”有

m ≡ 0

。

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

如果你开始像这样写你的证明

inv-z≤n : {m : ℕ} → m ≤ zero → m ≡ zero
inv-z≤n = ?

然后

C-c C-l

将其转化为

inv-z≤n : {m : ℕ} → m ≤ zero → m ≡ zero
inv-z≤n = {!   !}

有目标

?0 : m ≤ zero → m ≡ zero

然后

C-c C-,

为您提供目标和背景：

m ≤ zero → m ≡ zero
m : ℕ   (not in scope)

所以这证实了你必须定义一个函数

m ≤ zero → m ≡ zero

。确实

C-c C-r

将会产生

inv-z≤n : {m : ℕ} → m ≤ zero → m ≡ zero
inv-z≤n = λ x → {!   !}

有目标和背景

m ≡ zero
x : m ≤ zero
m : ℕ   (not in scope)

在这个阶段，我能建议的最好是将你的定义更改为

inv-z≤n : {m : ℕ} → m ≤ zero → m ≡ zero
inv-z≤n x = ?

（事实上，这可能是比我最初建议的更自然的起点）并再次执行

C-c C-l

和

C-c C-,

。然后你得到：

inv-z≤n : {m : ℕ} → m ≤ zero → m ≡ zero
inv-z≤n x = {!   !}

有目标和背景

m ≡ zero
x : m ≤ zero
m : ℕ   (not in scope)

现在的技巧是记住

m ≤ zero

是归纳类型，因此您可以使用

C-c C-c

并在

x

上进行大小写拆分来区分可能的情况（当

x

只是局部变量时，这是无法完成的） ）。然后你只会得到一种可能的情况，即

z≤n

，原因在本文开头解释。现在你的定义看起来像这样：

inv-z≤n : {m : ℕ} → m ≤ zero → m ≡ zero
inv-z≤n z≤n = {!   !} 

有目标和背景（再次完成

C-c C-,

之后）

zero ≡ zero

然后很明显

refl

将关闭这个目标。事实上

C-c C-r

给你：

inv-z≤n : {m : ℕ} → m ≤ zero → m ≡ zero
inv-z≤n z≤n = refl 

有目标和背景

*All Done*