证明n次偶数在Agda中产生偶数

Question

我试图在Agda 中定义1..n∈ℕ的和为n *（n + 1）/ 2，并且需要证明n * （n + 1）就是这样。 证明非常简单，但似乎有一个概念我不明白，因为我是Agda的新手（虽然对数学和哈斯克尔都不熟悉），并从http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf 中得知它（指向更高级的教程比欢迎！ ）。

open import Data.Nat 
open import Relation.Binary.PropositionalEquality 
open import Data.Sum 

-- A natural number is even, if there is a k ∈ ℕ with k * 2 = n. 
data IsEven : ℕ → Set where 
    even : (k : ℕ) → IsEven (k * 2) 

-- A product is even, if one of the factors is even. 
even-product : {n m : ℕ} → IsEven n ⊎ IsEven m → IsEven (m * n) 
even-product {n} {m} (inj₁ (even k)) = even (m * k) 
even-product {n} {m} (inj₂ (even k)) = even (n * k) 

代码返回

m != 2 of type ℕ 
when checking that the expression even (k * m) has type 
IsEven (k * 2 * m) 

我已经带有图案的使用，以说服编译器K * 2实际上Ñ试过，但没有成功。将m * k切换到k * m给出

k * m != m of type ℕ 
when checking that the expression even (k * m) has type 
IsEven (m * (k * 2)) 

Answer 1

您可以将{！ ！}标记，并使用C-c C-.快捷方式。

even-product : {n m : ℕ} → IsEven n ⊎ IsEven m → IsEven (m * n) 
even-product {n} {m} (inj₁ (even k)) = {!even (m * k)!} 
even-product {n} {m} (inj₂ (even k)) = {!even (n * k)!} 

重新加载该文件，然后在第一孔光标按C-c C-.给出了如下回应：

Goal: IsEven (m * (k * 2)) 
Have: IsEven (m * k * 2) 
———————————————————————————————————————————————————————————— 
n : ℕ 
m : ℕ 
k : ℕ 

现在的问题是明确的：我们的目标是要证明(m * (k * 2))均匀，但你有一个证明(m * k * 2)是偶数。

要解决此问题，您必须使用*是关联的事实。我会以示例的方式假设它，但显然你会想稍后给它一个实际的证明。

postulate 
    *-assoc : (k l m : ℕ) → k * (l * m) ≡ (k * l) * m 

现在我们可以使用rewrite关键字与*-assoc解决第一种情况：

even-product : {n m : ℕ} → IsEven n ⊎ IsEven m → IsEven (m * n) 
even-product {n} {m} (inj₁ (even k)) rewrite *-assoc m k 2 = even (m * k) 
even-product {n} {m} (inj₂ (even k)) = {!even (n * k)!} 

在第二种情况下，C-c C-.给出了如下回应：所以现在

Goal: IsEven (k * 2 * n) 
Have: IsEven (n * k * 2) 
———————————————————————————————————————————————————————————— 
m : ℕ 
n : ℕ 
k : ℕ 

你需要使用*的交换性以及关联性。我将把完整的解决方案作为练习留给读者。

Answer 2

证明2 * sum（1..n）= n *（n + 1）是否更容易？这说明n *（n + 1）是偶数？