在 Agda 中编写证明

Question

我想写出“对于所有 x 都存在 y 使得 x < y 且 y 是偶数”这一陈述的证明。我是这样试的...

-- ll means less function i.e ' < '

_ll_ : ? ? ? ? Bool
0 ll 0 = false
0 ll _ = true
a ll 0 = false
(suc a) ll (suc b) = a ll b 

even : ? ? Bool
even 0 = true
even 1 = false
even (suc (suc n)) = even n

Teven : Bool ? Set
Teven true = ?
Teven false = ?


thm0 : (x : ?) ?  ?[ y ? ? ]  (Teven ( and (x ll y) (even y))) 
thm0 0 = suc (suc zero) , record {}
thm0 (suc a) = ?

对于最后一行，即对于 'suc a'，agda 无法找到解决方案。我曾经尝试过写 2 * suc a ，记录 {}。但这也行不通。任何帮助将不胜感激。

Answer 1

你真正想要的是一次做两个步骤。

这种定义的问题是所谓的“布尔盲目性”——通过将你的命题编码为布尔值，你会丢失它们包含的任何类型的有用信息。结果是你必须依靠规范化来（希望）做它的事情，你不能以任何其他方式帮助 Agda（比如通过证明条款的模式匹配）。

但是，在您的情况下，您可以thm0稍微更改 的定义以帮助 Agda 进行规范化。even提出了两个suc在每个递归步骤步骤-你可以thm0做两步为好。

让我们来看看：

thm0 : ? x ? ? ? y ? Teven ((x ll y) ? (even y))
thm0 zero = suc (suc zero) , tt

两个新案例适用于suc zero（也称为1）：

thm0 (suc zero) = suc (suc zero) , tt

而对于suc (suc x')：

thm0 (suc (suc x') = ?

现在，如果我们知道y（你存在量化的那个）是suc (suc y')用于其他的y'，Agda 可以标准化even y为even y'（这只是遵循定义）。同样处理“小于”证明 - 一旦你知道了x = suc (suc x')，y = suc (suc y')对于一些y'（x'我们已经知道），你可以减少x ll y到x' ll y'.

所以选择y很简单……但是我们如何获得y'（当然还有证据）？我们可以用归纳法（递归），并应用thm0到x'！请记住， given x',thm0返回 somey'以及证明even y'和x' ll y'- 这正是我们所需要的。

thm0 (suc (suc a)) with thm0 a
... | y' , p = ?

然后我们简单地插入y = suc (suc y')和p（如上所述，(x ll y) ? even y减少到(x' ll y') ? even y'，即p）。

最终代码：

thm0 : ? x ? ? ? y ? Teven ((x ll y) ? (even y))
thm0 zero = suc (suc zero) , tt
thm0 (suc zero) = suc (suc zero) , tt
thm0 (suc (suc x')) with thm0 x'
... | y' , p = suc (suc y') , p

但是，话虽如此，我建议不要这样做。不要将你的命题编码为布尔值，然后通过Teven. 这实际上只适用于简单的事情，不能扩展到更复杂的命题。相反，尝试明确的证明条款：

data _less-than_ : ? ? ? ? Set where
  suc : ? {x y} ? x less-than y ? x less-than suc y
  ref : ? {x}                   ? x less-than suc x

data Even : ? ? Set where
  zero    :                  Even 0
  suc-suc : ? {x} ? Even x ? Even (2 + x)

thm0 然后可以使用一个简单的引理来编写：

something-even : ? n ? Even n ? Even (suc n)
something-even zero = inj? zero
something-even (suc n) with something-even n
... | inj? x = inj? (suc-suc x)
... | inj? y = inj? y

（这表明要么n是偶数要么其后继者是偶数）。其实thm0不用递归就可以实现！

thm0 : ? x ? ? ? y ? Even y × x less-than y
thm0 n with something-even n
... | inj? x = suc (suc n) , suc-suc x , suc ref
... | inj? y = suc n , y , ref

有趣的是，当我写这个定义时，我只是模式匹配something-even (suc n)并使用C-a（自动完成）填充右侧！如果有足够的提示，Agda 可以在没有我帮助的情况下编写代码。