Evenness in Agda

Even.agda

module Even where

open import Data.Bool
open import Data.Nat
open import Function

open import Relation.Binary.PropositionalEquality

even : ℕ → Bool
even 0             = true
even 1             = false
even (suc (suc x)) = even x

data isEven : ℕ → Set where
  ZisEven  : isEven 0
  SSisEven : {n : ℕ} → isEven n → isEven (2 + n)

even-sound : (n : ℕ) → T (even n) → isEven n
even-sound zero          prf = ZisEven
even-sound (suc zero)    ()
even-sound (suc (suc n)) prf = SSisEven (even-sound n prf)

even-complete : (n : ℕ) → isEven n → T (even n)
even-complete 0             ZisEven        = _
even-complete (suc (suc n)) (SSisEven prf) = even-complete n prf

x : even 12 ≡ true
x = refl

y : isEven 12
y = even-sound 12 _

mutual

  data isOdd′ : ℕ → Set where
    OisOdd′    : isOdd′ 1
    SEvenIsOdd : {n : ℕ} → isEven′ n → isOdd′ (suc n)

  data isEven′ : ℕ → Set where
    ZisEven′   : isEven′ 0
    SOddIsEven : {n : ℕ} → isOdd′ n → isEven′ (suc n)

isEvenisEven′ : (n : ℕ) → isEven n → isEven′ n
isEvenisEven′ .0            ZisEven        = ZisEven′
isEvenisEven′ (suc (suc n)) (SSisEven prf) = SOddIsEven (SEvenIsOdd (isEvenisEven′ n prf))

isEven′isEven : (n : ℕ) → isEven′ n → isEven n
isEven′isEven .0 ZisEven′                      = ZisEven
isEven′isEven .2 (SOddIsEven OisOdd′)          = SSisEven ZisEven
isEven′isEven ._ (SOddIsEven (SEvenIsOdd prf)) = SSisEven (isEven′isEven _ prf)

open import Data.Nat.Divisibility

isEven′′ : (n : ℕ) → Set
isEven′′ n = 2 ∣ n

isEvenisEven′′ : (n : ℕ) → isEven n → isEven′′ n
isEvenisEven′′ .0            ZisEven        = divides zero refl
isEvenisEven′′ (suc (suc n)) (SSisEven prf) with isEvenisEven′′ n prf
... | divides q eq = divides (suc q) (cong (suc ∘ suc) eq)

isEven′′-inv : (n : ℕ) → isEven′′ (2 + n) → isEven′′ n
isEven′′-inv n (divides zero ())
isEven′′-inv n (divides (suc q) eq) = divides q (cong (pred ∘ pred) eq)

isEven′′isEven : (n : ℕ) → isEven′′ n → isEven n
isEven′′isEven zero          prf = ZisEven
isEven′′isEven (suc (suc n)) prf = SSisEven (isEven′′isEven n (isEven′′-inv n prf))
isEven′′isEven (suc zero) (divides zero ())
isEven′′isEven (suc zero) (divides (suc q) ())