Agda: Продукт четных чисел даже

Question

Я довольно новичок в Агда. Я работаю над вопросом из задания. У меня есть большая часть, но есть одна цель, на которой я застрял.

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 со всеми правильными импорта и всех доказательств.