functional-programming - 用Agda编写证明

我想写证明“对于所有x都存在一个y，使得x 我以这种方式尝试过...

-- 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，记录{}。但这也不起作用。任何帮助将不胜感激。

最佳答案

您真正想要的是一次执行两个步骤。

这种定义的问题是所谓的“布尔盲”-通过将命题编码为布尔值，您将丢失它们包含的任何有用信息。结果是您必须依靠规范化（希望）完成其工作，您不能以任何其他方式帮助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

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

关于functional-programming - 用Agda编写证明，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/30071841/