Proving even-ness in Agda

I've been just getting started with Agda. I tried to prove, as exercise, evenness.

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

x : even 12 ≡ true
x = refl

But asserting truth using _≡_ seems like a really bad way. What would be the best way of doing the same thing?

One thing you can do is define an inductive predicate describing what it means for a number to be even. You could for instance write:

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

You can then prove that your even function is sound: whenever it returns true (which is what Data.Bool's T means) then the input was indeed an even number.

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)

Now, you can write the following test rather than your previous equality: even-sound generates the proof that isEven 12.

y : isEven 12
y = even-sound 12 _

If you want to be even more precise in the way you specify even, you can also prove that it is complete: whenever an input is even, it indeed returns true.

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

Now, the specification of Even-ness I have chosen is a bit arbitrary, you may want to prove that it is equivalent to other formulations.

First, we can describe evenness in terms of oddness and reciprocally using mutually defined predicates:

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)

Or we can use divisibility by 2 as the fundamental notion:

open import Data.Nat.Divisibility
isEven′′ : (n : ℕ) → Set
isEven′′ n = 2 ∣ n

Edit: I have included the proofs that these definitions are equivalent in a gist in case you want to peek.

StackExchange Code Review Q#113557, answer score: 3