Agda：偶數產品甚至是

Question

我對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一些如何。但目標看起來並不那麼簡單。我對這個問題有困難嗎？還是我在正確的軌道上？有沒有更簡單的方法來做到這一點？我不想要這個解決方案。但正確的方向推動將不勝感激。我一直堅持這一段時間。

Answer 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₁))) 

Answer 2

如果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)) 

Answer 3

這可能不是預期的你爲這個作業，但一個乾淨的方式來處理這些引理沒有做太多的工作，如在通過@ 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與所有正確的進口和所有的證明。