functional-programming - 在 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

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

这种定义的问题是所谓的“ bool 盲目性”——通过将你的命题编码为 bool 值，你会丢失它们包含的任何类型的有用信息。结果是你必须依靠规范化来(希望)做它的事情，你不能以任何其他方式帮助 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' !记住给定 x' , thm0返回一些 y'连同证明 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

但是，话虽如此，我建议不要这样做。不要将你的命题编码为 bool 值，然后通过 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 可以在没有我帮助的情况下编写代码。