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