2

我在上一个问题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 crazy，如果你给它一个疯狂的证明是 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

但这是漫长而混乱的。因此，我尝试在将计算函数的值用于 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_似乎持有隐藏的价值f，并且x；以及x应用于的结果f。 [_]将导致该相等性的证明。

⊥-elim接受矛盾证明并返回矛盾。

我要投入什么才能让它???发挥作用？

4

1 回答 1

3

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

我们真正想做的是减少我们可以很容易地用来构建矛盾的crazy nn ≢ 0假设0 ≢ 0。我们如何crazy nn减少到0? 您已经尝试过第一个选项 - 遍历所有可能的crazy参数并找出那些确实减少crazy nn到0. 另一种选择是简单地对 的值进行抽象crazy nn。

首先，我们使用之前的目标类型withisFin (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假设。这显然是胡说八道，结合nezwithrefl给了我们一个可以被 使用的矛盾⊥-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.

为了完整起见：您可以通过使用 deprecated来避免模式匹配crazy nn以保持证明的类型完整：nezinspect

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 = ?

由于我们对 over 进行抽象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)
... | _ | _         = ?
于 2013-09-02T02:41:04.583 回答