proof - agda 的检查功能是如何工作的？

Question

我在上一个问题 Using the value of a computed function for a proof in agda 中看到了一个检查函数的例子。 ，但我仍然无法解决这个问题。

这是一个简单的例子:

给定函数 crazy ,

crazy : ℕ -> ℕ
crazy 0 = 10
crazy 1 = 0
crazy 2 = 0
crazy 3 = 1
crazy 4 = 0
crazy xxx = xxx

我想创建一个 safe函数使得 safe : {nn : ℕ} -> (id nn) ≢ 0 -> Fin (id nn) .换句话说，它会返回一个数字 mod 疯狂，如果你给它一个疯狂的证明是 0。(我知道这个例子有点做作，我可能最好在函数签名中使用 suc)

我的第一个解决方案是

safebad : {nn : ℕ} -> (crazy nn) ≢ 0 -> Fin (crazy nn)
safebad {1} hh with hh refl
... | ()
safebad {2} hh with hh refl
... | ()
safebad {4} hh with hh refl
... | ()
safebad {0} hh = # 0
safebad {3} hh = # 0
safebad {suc (suc (suc (suc (suc _))))} _ = # 0

但这是漫长而困惑的。所以我试图模仿 Using the value of a computed function for a proof in agda 中的例子但只能到此为止

safegood : (nn : ℕ) -> (crazy nn) ≢ 0 -> Fin (crazy nn)
safegood nn nez with crazy nn | inspect crazy nn
... | 0 | [ proof ] = ⊥-elim ???
... | _ | _ = # 0

我想，inspect 使用 Hidden 来隐藏类型签名中函数应用程序的记录。然后可以使用reveal检索。

这就是我认为我理解的:
Reveal_is_似乎持有隐藏的值(value) f , 和 x ;以及 x 的结果适用于 f . [_]将导致这种平等的证明。
⊥-elim取一个矛盾的证明并返回一个矛盾。

我该放什么 ???为了这个工作？

Answer 1

你让它变得不必要地复杂。 inspect仅当您需要使用模式匹配前的值等于模式匹配后的值的证明时才有用。请注意，您有 nez在使这变得微不足道的范围内。

我们真正想做的是减少假设crazy nn ≢ 0至 0 ≢ 0我们可以很容易地用它来构造一个矛盾。我们如何获得crazy nn减少到 0 ?您已经尝试过第一个选项 - 遍历所有可能的 crazy为那些确实减少的人争论和钓鱼 crazy nn至 0 .另一种选择是简单地抽象 crazy nn 的值。 .

首先，我们使用之前的目标类型with是 Fin (crazy nn)和 nez 的类型是 crazy nn ≢ 0 .现在，我们抽象了 crazy nn :

safegood nn nez with crazy nn
... | w = ?

注意我们的目标现在是 Fin w和 nez的类型是 w ≢ 0 ，更容易使用!最后，我们在 w 上进行模式匹配:

safegood nn nez with crazy nn
... | zero  = ?
... | suc w = ?

现在第一个目标是 Fin 0我们有一个 0 ≢ 0作为我们的假设之一。这显然是废话，结合 nez与 refl给了我们一个可以被 ⊥-elim 使用的矛盾:

safegood nn nez with crazy nn
... | zero  = ⊥-elim (nez refl)
... | suc w = ?

否 inspect就在眼前!事实上，使用 inspect这就像往返:你减少 crazy nn至 0在类型中，得到 crazy nn ≡ 0 的证明现在你需要“减少” 0返回 crazy nn以便您可以使用 nez proof .

为了完整起见:您可以避免在 crazy nn 上进行模式匹配保留证明类型 nez使用已弃用的 inspect 完好无损:

open Deprecated-inspect
  renaming (inspect to inspect′)

safegood₂ : (nn : ℕ) → crazy nn ≢ 0 → Fin (crazy nn)
safegood₂ nn nez with inspect′ (crazy nn)
... | zero  with-≡ eq = ⊥-elim (nez eq)
... | suc _ with-≡ eq = ?

由于我们抽象了 inspect′ (crazy nn) , 否 crazy nn子表达式将被替换并且 nez将保持其原始类型。

谈论疯狂的往返:你可以使用 proof重建 nez的原始类型；同样，这更像是“了解可能有用”而不是“在此处使用”:

safegood : (nn : ℕ) → crazy nn ≢ 0 → Fin (crazy nn)
safegood nn nez with crazy nn | inspect crazy nn
... | 0 | [ proof ] = ⊥-elim (subst (λ x → x ≢ 0) (sym proof) nez proof)
... | _ | _         = ?