4
\$\begingroup\$

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?

\$\endgroup\$
3
\$\begingroup\$

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.

\$\endgroup\$
  • \$\begingroup\$ Thank you so much for the helpful answer! A quick question I have: what is insufficient about using the isEven type as my proposition? It is inhabited only if its argument is an even number so why do I have to prove that it's sound? My understanding is that's to make sure that it is consistent with my definition of even-ness as I've expressed in even : ℕ → Bool, is that correct? \$\endgroup\$ – cauliflower Dec 12 '15 at 4:35
  • 1
    \$\begingroup\$ I was trying to prove that the function even is sound and complete in terms of the specification isEven. The specification is indeed the thing you would take as being an obviously valid definition of evenness. \$\endgroup\$ – gallais Dec 12 '15 at 14:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.