Agda：如何获得依赖类型的值？

Question

我最近问了这个问题： An agda proposition used in the type -- what does it mean? 并收到了关于如何使类型隐式并获得真正的编译时错误的深思熟虑的答案。

但是，我仍然不清楚如何创建具有依赖类型的值。

考虑：

div : (n : N) -> even n -> N
div zero p = zero
div (succ (succ n)) p= succ (div n p)
div (succ zero) ()

其中N是自然数，偶数是下面的命题。

even : N -> Set
even zero = \top
even (succ zero) = \bot
even (succ (succ n)) = even n
data \bot : Set where
record \top : Set where

假设我想写一个函数如下：

f : N -> N
f n = if even n then div n else div (succ n)

我不知道如何以我想要的方式做这样的事情......在我看来，最好的办法是证明 (not (even n)) \to even (succ n)。我真的不知道如何在 agda 中表达这一点。我会写

g : (n:N) -> (even n) -> (even (succ n)) -> N
g n p q = if evenB n then (div n p) else (div (succ n) q)

由此，我可以做以下事情：

g 5 _ _ 

并评估为正常形式...以获得答案。如果我想写f，我可以这样做

f n = g n ? ?

我得到 f n = g n { }1 { }2 其中 ?1 = 偶数 n，而 ?2 = 偶数 (succ n)。然后我可以做 f 5 之类的事情并评估为正常形式。我真的不明白为什么这是有效的......有没有办法告诉agda更多关于f以这种方式定义的信息。我可以确定如果 ?1 失败 ?2 会成功，然后告诉 agda 评估 f 总是有意义的吗？

我将 g 解释为一个函数，它接受一个数字 n，一个 n 是偶数的证明，一个 (succ n) 是偶数的证明，并返回一个数字。 （这是阅读本文的正确方法吗？或者有人可以提出更好的阅读方法吗？）我真的很想准确（或更准确地）理解上述类型的检查方式。它是否使用感应 - 它是否将 (evenB n) 与 p 连接：甚至 n？等等。我现在很困惑，因为它知道

if evenB n then (div n q) else (whatever)
if evenB n then div (succ n) q else div n p

不正确。首先我明白为什么 - q 代表 succ n，所以它不匹配。但第二次失败了，而且原因更神秘，而且似乎 Agda 比我想象的更强大......

如果我能弄清楚该怎么做（如果有意义的话），这是我非常喜欢的第一步。

g : (n : N) -> (even n) -> N
g n p = if evenB n then (div n p) else (div (succ n) (odd p))

其中奇数 p 证明如果偶数 n 是荒谬的，那么 succ n 是偶数。我想，这需要我能够处理依赖类型的值。

最终，我希望能够写出这样的东西：

g : N -> N
g n = 
  let p = proofthat n is even
  in
      if evenB n then div n p else (div (succ n) (odd p))

或者类似的东西。甚至

g : N -> N
g n = if evenB n then let p = proofThatEven n in div n p else let q = proofThatEven succ n in div n q

我真的很想知道如何制作一个与依赖类型相对应的证明，以便我可以在程序中使用它。有什么建议吗？

Answer 1

功能与命题

将内容编码为命题和函数之间存在至关重要的区别。让我们看看_+_ 实现为数字关系和函数。

功能当然是微不足道的：

_+_ : (m n : ℕ) → ℕ
zero  + n = n
suc m + n = suc (m + n)

_+_ 作为命题是数字的三元关系。对于数字m、n 和o，它应该恰好在m + n = o 时保持：

data _+_≡_ : ℕ → ℕ → ℕ → Set where
  zero : ∀ {  n  }             → zero  + n ≡ n
  suc  : ∀ {m n o} → m + n ≡ o → suc m + n ≡ suc o

例如，我们可以证明2 + 3 ≡ 5：

proof : 2 + 3 ≡ 5
proof = suc (suc zero)

现在，函数对允许的内容更加严格：它必须通过终止检查器，必须有唯一的结果，必须涵盖所有情况等等；作为回报，它们给了我们可计算性。命题允许冗余、不一致、部分覆盖等，但要真正表明2 + 3 = 5，必须涉及程序员。

这当然是你的if 的一个噱头：你需要能够计算它的第一个参数！

是吗？

但是有希望：我们可以证明您的even 命题实际上对于每个自然数都是可计算的（我应该说是可判定的）。我们如何证明这一点？通过写一个函数来决定。

我们需要对命题进行否定：

data ⊥ : Set where

¬_ : Set → Set
¬ A = A → ⊥

接下来，我们将写下一个数据类型来告诉我们这个命题是否成立：

data Dec (P : Set) : Set where
  yes :   P → Dec P
  no  : ¬ P → Dec P

最后，我们将定义 even 可判定的含义：

EvenDecidable : Set
EvenDecidable = ∀ n → Dec (even n)

这读作：even 是可判定的，如果对于任何自然数n，我们可以证明even n 或¬ (even n)。让我们证明这确实是真的：

isEven : EvenDecidable
isEven zero          = yes _
isEven (suc zero)    = no λ ()
isEven (suc (suc n)) = isEven n

从Dec 到Bool

现在，我们有：

data Bool : Set where
  true false : Bool

if_then_else_ : {A : Set} → Bool → A → A → A
if true  then t else _ = t
if false then _ else f = f

还有一个函数isEven，它返回Dec，而不是Bool。我们可以通过简单地忘记里面的证明从Dec转到Bool（⌊可以通过\clL输入，⌋通过\clR输入）：

⌊_⌋ : {P : Set} → Dec P → Bool
⌊ yes _ ⌋ = true
⌊ no  _ ⌋ = false

最后，我们可以在if 中使用isEven：

if ⌊ isEven n ⌋ then ? else ?

导出矛盾

接下来，您的g 函数：您需要even n 和even (suc n) 的证明。这是行不通的，因为没有人可以同时提供这两者。事实上，我们甚至可以使用这些来推导出一个矛盾：

bad : ∀ n → even n → even (suc n) → ⊥
bad zero          p q = q
bad (suc zero)    p q = p
bad (suc (suc n)) p q = bad n p q

但是，两者都

bad₂ : ∀ n → even n → even (suc n) → ℕ
bad₂ n p q = div (suc n) q

bad₃ : ∀ n → even n → even (suc n) → ℕ
bad₃ n p q = div n p

typecheck 很好，所以我不完全确定你为什么对第二个if 有问题。

把它们放在一起

现在，我们进入主要部分，odd 函数。如果我们知道这个数字不是even，我们应该能够证明后继者是even。我们将重用之前的否定。 agda-mode 可以只用 C-c C-a 填充右侧：

odd : ∀ n → ¬ even n → even (suc n)
odd zero          p = p _
odd (suc zero)    p = _
odd (suc (suc n)) p = odd n p

现在我们已经准备好编写您的g 函数了：

g : ℕ → ℕ
g n = ?

我们会使用isEven函数询问号码是否为even：

g : ℕ → ℕ
g n with isEven n
... | isItEven = ?

现在，我们将在 isItEven 上进行模式匹配以找出结果：

g : ℕ → ℕ
g n with isEven n
... | yes e = ?
... | no  o = ?

e 证明该数字是even，o 证明它不是even（它有一个类型¬ even n）。 e可以直接和div一起使用，对于o我们需要使用之前定义的odd函数：

g : ℕ → ℕ
g n with isEven n
... | yes e = div n e
... | no  o = div (suc n) (odd n o)

if 为Dec

但是，您不能仅使用 if 实现上述版本。 Booleans 不携带任何附加信息；他们肯定没有我们需要的证据。我们可以编写if 的变体，它与Dec 一起工作，而不是Bool。这使我们能够将相关证明分发到 then 和 else 分支。

if-dec_then_else_ : {P A : Set} → Dec P → (P → A) → (¬ P → A) → A
if-dec yes p then t else _ = t  p
if-dec no ¬p then _ else f = f ¬p

请注意，这两个分支实际上都是将证明作为其第一个参数的函数。

g : ℕ → ℕ
g n = if-dec isEven n
  then (λ e → div n e)
  else (λ o → div (suc n) (odd n o))

我们甚至可以为这个if 创建一个很好的语法规则；不过，在这种情况下，它几乎是无用的：

if-syntax = if-dec_then_else_

syntax if-syntax dec (λ yup → yupCase) (λ nope → nopeCase)
  = if-dec dec then[ yup ] yupCase else[ nope ] nopeCase

g : ℕ → ℕ
g n = if-dec isEven n
  then[ e ] div n e
  else[ o ] div (suc n) (odd n o)

with 是什么？

现在，我注意到 with 构造在您在上一个问题中链接的介绍的后面部分中提到。以下是它的工作原理：

有时您需要对中间表达式进行模式匹配，例如上面代码中的isEven。要在没有with 的情况下做到这一点，您实际上需要编写两个函数：

h₁ : (n : ℕ) → Dec (even n) → ℕ
h₁ n (yes e) = div n e
h₁ n (no  o) = div (suc n) (odd n o)

h₂ : ℕ → ℕ
h₂ n = h₁ n (isEven n)

h₂ 设置我们想要进行模式匹配的表达式，h₁ 进行实际的模式匹配。现在，像这样的中间表达式的模式匹配相当频繁，因此 Agda 为我们提供了更紧凑的符号。

h : ℕ → ℕ
h n with isEven n
h n | yes e = div n e
h n | no  o = div (suc n) (odd n o)

所以，with 的行为就好像它添加了一个额外的参数，我们可以对其进行模式匹配。您甚至可以同时在多个表达式上使用with：

i : ℕ → ℕ
i n with isCool n | isBig n
i n | cool | big = ?

然后我们可以在 cool 和 big 上进行模式匹配，就好像函数有 3 个参数一样。现在，大部分时间原始左侧保持不变，正如前面的函数所示（在某些情况下它实际上可能不同，但我们现在不需要处理）。对于这些情况，我们有一个方便的快捷方式（尤其是当左侧很长时）：

i : ℕ → ℕ
i n with isCool n | isBig n
... | cool | big = ?