Agda：偶数的乘积是偶数答案

【问题标题】：Agda: Product of even numbers is evenAgda：偶数的乘积是偶数
【发布时间】：2017-07-10 12:00:25
【问题描述】：

我对 Agda 很陌生。我正在处理作业中的一个问题。我已经完成了大部分任务，但我一直坚持一个目标。

data Arith : Set where
 Num : ℕ → Arith
 Plus : Arith → Arith → Arith
 Times : Arith → Arith → Arith

eval : Arith → ℕ
eval (Num x) = x
eval (Plus e1 e2) = eval e1 + eval e2 
eval (Times e1 e2) = eval e1 * eval e2

data Even : ℕ → Set where
 zEven : Even 0
 ssEven : {n : ℕ} → Even n → Even (suc (suc n))

-- [PROBLEM 1]

plusEven : ∀ n m → Even n → Even m → Even (n + m)
plusEven zero m x x₁ = x₁
plusEven (suc zero) m () x₁
plusEven (suc (suc .0)) m (ssEven zEven) x₁ = ssEven x₁
plusEven (suc (suc ._)) m (ssEven (ssEven x)) x₁ = ssEven (ssEven (plusEven _ m  x  x₁ ))

-- [PROBLEM 2]

timesEven : ∀ n m → Even n → Even m → Even (n * m)
timesEven zero m x x₁ = zEven
timesEven (suc ._) zero (ssEven x) x₁ =  (timesEven _ zero x x₁)
timesEven (suc ._) (suc ._) (ssEven x) (ssEven x₁) = ssEven ((λ h → {!!}) (timesEven _ _ x x₁))

我要证明的目标是

Goal: Even (.n₁ + suc (suc (.n₁ + .n * suc (suc .n₁))))

我觉得我必须使用plusEven some how。但目标看起来并不那么简单。我让问题变得困难了吗？还是我在正确的轨道上？有没有更简单的方法来做到这一点？我不想解决这个问题。但是，我们将不胜感激朝着正确的方向前进。我已经坚持了一段时间了。

【问题讨论】：

标签： functional-programming agda

【解决方案1】：

我真的很喜欢这里发布的答案，它们对我帮助很大。但我无法更改作业中给出的问题。我使用发布的答案来解决问题。我花了一段时间，它看起来有点乱，但它的工作原理。我也想把它贴在这里。

timesEven : ∀ n m → Even n → Even m → Even (n * m)
timesEven zero m x x₁ = zEven
timesEven (suc zero) m () x₁
timesEven (suc (suc n)) zero (ssEven x) x₁ = timesEven n zero x x₁
timesEven (suc (suc n)) (suc zero) x ()
timesEven (suc (suc n)) (suc (suc m)) (ssEven x) (ssEven x₁) = ssEven ((λ h → plusEven m (suc (suc (m + n * suc (suc m)))) x₁  (ssEven (plusEven m (n * suc (suc m)) x₁ h))) (timesEven n (suc (suc m)) x (ssEven x₁)))

【讨论】：

【解决方案2】：

这可能不是您对本作业的期望，但正如@user3237465 所暗示的，在不做太多工作的情况下处理这些引理的干净方法是重用自然数的众所周知的属性。

从这些众所周知的属性中获得更多信息的一种方法是引入Even 的替代定义，您可以证明它等同于归纳定义：

data Even : ℕ → Set where
 zEven  : Even 0
 ssEven : {n : ℕ} → Even n → Even (suc (suc n))

record Even′ (n : ℕ) : Set where
  constructor mkEven′
  field factor    : ℕ
        .equality : n ≡ factor * 2
open Even′

Even⇒Even′ : {n : ℕ} → Even n → Even′ n
(...)
Even′⇒Even : {n : ℕ} → Even′ n → Even n
(...)

然后，您可以通过使用等式推理，重用标准库中的引理来证明 plusEven 和 timesEven(Right/Left)。比如plusEven的证明变成：

plusEven′ : ∀ n m → Even′ n → Even′ m → Even′ (n + m)
plusEven′ n m (mkEven′ p Hp) (mkEven′ q Hq) = mkEven′ (p + q) eq where

  .eq : n + m ≡ (p + q) * 2
  eq = begin
         n + m          ≡⟨ cong₂ _+_ Hp Hq ⟩
         p * 2 + q * 2  ≡⟨ sym (distribʳ-*-+ 2 p q) ⟩
         (p + q) * 2
       ∎

plusEven : ∀ n m → Even n → Even m → Even (n + m)
plusEven n m en em = Even′⇒Even (plusEven′ n m (Even⇒Even′ en) (Even⇒Even′ em))

Here is a gist 包含所有正确的导入和所有证明。

【讨论】：

【解决方案3】：

如果n 是偶数，那么n * m 也是偶数，因此m 是否偶数无关紧要，因此您应该丢弃这个约束。所以实际的定理是（我隐含了n和m，因为这样很方便）

timesEvenLeft  : ∀ {n m} → Even n → Even (n * m)
timesEvenRight : ∀ {n m} → Even m → Even (n * m)

您可以证明n * m ≡ m * n 并从前者推导出后者定理。因此只需要证明第一个即可。在递归情况下，您需要证明Even (suc (suc n) * m)（简化为Even (m + (m + n * m)）在范围内具有Even (n * m)（归纳假设）。为此，您还需要另一个引理：

plusDoubleEven : ∀ {n} m → Even n → Even (m + (m + n))

【讨论】：