Alternative definition of Even

Even.agda

module Even where

open import Data.Nat
open import Data.Nat.Properties.Simple
open import Function
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning

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′ zEven      = mkEven′ zero refl
Even⇒Even′ (ssEven p) =
  let (mkEven′ p eq) = Even⇒Even′ p
  in mkEven′ (suc p) (cong (suc ∘ suc) eq)

suc≠zero : {n : ℕ} {A : Set} → .(suc n ≡ zero) → A
suc≠zero ()

Even′⇒Even : {n : ℕ} → Even′ n → Even n
Even′⇒Even {zero} p = zEven
Even′⇒Even {suc (suc n)} (mkEven′ (suc p) eq) =
  ssEven (Even′⇒Even (mkEven′ p (cong (pred ∘ pred) eq)))

Even′⇒Even {suc zero} (mkEven′ zero eq)    = suc≠zero eq
Even′⇒Even {suc zero} (mkEven′ (suc p) eq) = suc≠zero (sym (cong pred eq))
Even′⇒Even {suc (suc n)} (mkEven′ zero eq) = suc≠zero eq


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

timesEven′Right : ∀ n m → Even′ m → Even′ (n * m)
timesEven′Right n m (mkEven′ p Hp) = mkEven′ (n * p) eq where

  .eq : n * m ≡ (n * p) * 2
  eq = begin
         n * m        ≡⟨ cong (n *_) Hp ⟩
         n * (p * 2)  ≡⟨ sym (*-assoc n p 2) ⟩
         (n * p) * 2
       ∎

timesEvenRight : ∀ n m → Even m → Even (n * m)
timesEvenRight n m em = Even′⇒Even (timesEven′Right n m (Even⇒Even′ em))

timesEvenLeft : ∀ n m → Even n → Even (n * m)
timesEvenLeft n m rewrite *-comm n m = timesEvenRight m n