Agda (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)

我不知道如何以自己想要的方式做这样的事情。。。在我看来，最好的办法是证明(不是(偶数n))\到(偶数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都是荒谬的，而成功cc是偶数。我猜想，这将要求我能够使用依赖类型的值。

最终，我希望能够编写如下内容:

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

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

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

我们将使用 even函数询问数字是否为 isEven:

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来实现上述版本。 Bool eans不携带任何其他信息。他们肯定没有提供我们需要的证据。我们可以编写 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 = ?