Types representing Even and Odd numbers

[Paul Cadman]

Hi,

I recently went to a talk by David Christiansen, he described constructing types representing Even and Odd numbers in his language PIE. I'm trying to write these types in Idris.

My definition of Even:

data Even : (num1 : Nat) -> Type where

  Twice : (num : Nat) -> Even (num + num)

Evidence that 2 is Even:

twoIsEven : Even 2

twoIsEven = Twice 1

I'd like to express the proposition that "3 is not Even" using this type so:

threeIsNotEven : (Even 3) -> Void

threeIsNotEven (Twice _) impossible

But the type checker rejects this as evidence with the error:

threeIsNotEven (Twice _) is a valid case

Is my definition not rich enough to express this? I also tried:

data Even : (num1 : Nat) -> Type where

  Twice : (num : Nat) -> ((num + num = num1)) -> Even num1

this, I think more closely matches what David had in his talk, but I ran into the same problems.

Can anyone see a way to define (Even n) that allows me to express that the type is uninhabited for odd n?

Thanks,

Paul

[Shu-Hung You]

Hi Paul,

threeIsNotEven (Twice n) is a valid case because, to the type checker,
it is not obvious that n + n = 3 is not ``satisfiable''. One way to
get around this is to expand the cases here, to help the type checker
evaluate '+' further to see that it is impossible:

threeIsNotEven : Even 3 -> Void
threeIsNotEven (Twice Z) impossible
threeIsNotEven (Twice (S Z)) impossible
threeIsNotEven (Twice (S (S Z))) impossible
threeIsNotEven (Twice (S (S (S Z)))) impossible
threeIsNotEven (Twice (S (S (S (S n))))) impossible

From cases Z to S (S (S Z)), the type checker can compute Z + Z, (S Z)
+ (S Z), ... to (S (S (S Z))) + (S (S (S Z))) and immediately see that
all the results are not 3.

For (S (S (S (S n)))), the type checker reasons by:

(S (S (S (S n)))) + (S (S (S (S n))))
= S ((S (S (S n))) + (S (S (S (S n)))))
= S (S ((S (S n)) + (S (S (S (S n))))))
= S (S (S ((S n) + (S (S (S (S n)))))))
= S (S (S (S (n + (S (S (S (S n))))))))

At this point, the type checker cannot simplify this term any further.
However, since 3 is S (S (S Z)), by comparison we see that the two
terms must be different

S (S (S (S (n + (S (S (S (S n))))))))
S (S (S Z))

because after the common prefix S (S (S ?)), one continues with S and
one ended with Z. So the type checker can decide that these two terms
are distinct, and thus this clause is also impossible.

Lastly, from the fact that all Nats must falls into one of the categories

Z
S Z
S (S Z)
S (S (S Z))
S (S (S (S n)))

the type checker concludes that threeIsNotEven is finished (total, proved!).

Best,
Shu-Hung

> --
> You received this message because you are subscribed to the Google Groups
> "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to idris-lang+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[David Thrane Christiansen]

Hello Paul,

> I recently went to a talk by David Christiansen, he described constructing
> types representing Even and Odd numbers in his language PIE. I'm trying to
> write these types in Idris.

Good exercise!

> My definition of Even:
>
> data Even : (num1 : Nat) -> Type where
> Twice : (num : Nat) -> Even (num + num)
>
> Evidence that 2 is Even:
>
> twoIsEven : Even 2
> twoIsEven = Twice 1

This certainly captures the idea, but it will be easier in the version
you have below with explicit equality proofs.

> I'd like to express the proposition that "3 is not Even" using this type so:
>
> threeIsNotEven : (Even 3) -> Void
> threeIsNotEven (Twice _) impossible
>
> But the type checker rejects this as evidence with the error:
>
> threeIsNotEven (Twice _) is a valid case
>
> Is my definition not rich enough to express this? I also tried:
>
> data Even : (num1 : Nat) -> Type where
> Twice : (num : Nat) -> ((num + num = num1)) -> Even num1
>
> this, I think more closely matches what David had in his talk, but I ran
> into the same problems.

A direct translation of the code in the talk is:

Even : Nat -> Type
Even = \ n => (half : Nat ** n = half + half)

but using a datatype is a good idea in a language with that feature :)

In any case, all three definitions of Even are equivalent.

> Can anyone see a way to define (Even n) that allows me to express that the
> type is uninhabited for odd n?

The issue here is not that your definition of evenness is off, it's that
you need to do more work to demonstrate to idris precisely _why_ 3 is
not even. There's nothing there that causes unrecoverable unification
failures, which is what's needed for the "impossible" keyword to work.

I'm a bit short on time at the moment, so I'm only going to post the
first thing that came to mind. There may well be easier ways than this!
But one technique to make it go through is to first prove that no number
is both even and odd, and then use 3's oddness to demonstrate that it
cannot be even.

The proof goes like this: to show that no number is both even and odd,
we start with 0 and 1 as base cases. 0 is not odd because there is no
proof that 0 = S (haf + haf). To show that 1 is not even, consider two
cases: either half of 1 is 0, or it is S k for some k. half cannot be 0,
because 0 + 0 does not equal 1. It cannot be 1, because (S k + S k) = S
(S (k + k)), and by the injectivity of S, 0 would need to equal S (k +
k) which is absurd.

Having taken care of the base cases, we have the step. Assuming k is not
both even and odd, we need to show that (S (S k)) is not even and odd.
In other words, assume (a) that a contradiction comes from k's
simultaneous evenness and oddness, and (b) that (S (S k)) is both even
and odd. We derive from (b) the input to (a) by showing that if (S (S
k)) is even, then k is even, and that if (S (S k)) is odd, then k is
odd. Those follow from the injectivity of S and the aforementioned fact
that (n + S j = S (n + j)).

In retrospect, it was enough to show that 1 is not even, and then the
"go back two" step, which is what the more general version is doing, but
this way is a bit more fun :-)

/David

Here's the code in full:

-- A version of the code from the talk, translated to Idris

data Even : Nat -> Type where
MkEven : (half : Nat) -> (k = half + half) -> Even k

zeroEven : Even 0
zeroEven = MkEven 0 Refl

data Odd : Nat -> Type where
MkOdd : (haf : Nat) -> (k = S (haf + haf)) -> Odd k

evenSOdd : Even k -> Odd (S k)
evenSOdd (MkEven half prf) = MkOdd half (cong prf)

oddSEven : Odd k -> Even (S k)
oddSEven (MkOdd haf prf) = MkEven (S haf) (cong (trans prf $
plusSuccRightSucc haf haf))

allEvenOrOdd : (k : Nat) -> Either (Even k) (Odd k)
allEvenOrOdd Z = Left zeroEven
allEvenOrOdd (S k) = case allEvenOrOdd k of
Left l => Right $ evenSOdd l
Right r => Left $ oddSEven r

-------------------------------------------------------------------------
-- Alternative characterizations of evenness, all equivalent

data Even' : Nat -> Type where
Twice : (half : Nat) -> Even' (half + half)

evenOk1 : Even k -> Even' k
evenOk1 (MkEven half prf) = replace {P=Even'} (sym prf) (Twice half)

evenOk2 : Even' k -> Even k
evenOk2 (Twice half) = MkEven half Refl

Even'' : Nat -> Type
Even'' = \ k => (half ** k = plus half half)

evenOk3 : Even k -> Even'' k
evenOk3 (MkEven half prf) = (half ** prf)

evenOk4 : Even'' k -> Even k
evenOk4 (half ** prf) = MkEven half prf

-------------------------------------------------------------------------
-- Now let's prove that 3 is not even.

succInj : S k = S j -> k = j
succInj Refl = Refl

zeroNotOdd : Odd 0 -> Void
zeroNotOdd (MkOdd haf prf) = absurd prf

oneNotEven : Even 1 -> Void
oneNotEven (MkEven Z prf) = absurd $ sym prf
oneNotEven (MkEven (S k) prf) =
absurd $ succInj (trans prf (sym (plusSuccRightSucc (S k) k)))

twoBackEven : Even (S (S k)) -> Even k
twoBackEven (MkEven Z Refl) impossible
twoBackEven (MkEven (S j) prf) =
MkEven j $ succInj $ succInj $ trans prf (sym (plusSuccRightSucc (S
j) j))

twoBackOdd : Odd (S (S k)) -> Odd k
twoBackOdd (MkOdd Z Refl) impossible
twoBackOdd (MkOdd (S j) prf) =
MkOdd j $ succInj $ succInj $ trans prf (sym (plusSuccRightSucc (S
(S j)) j))

oddNotEven : (k : Nat) -> Even k -> Odd k -> Void
oddNotEven Z e o = zeroNotOdd o
oddNotEven (S Z) e o = oneNotEven e
oddNotEven (S (S k)) e o = oddNotEven k (twoBackEven e) (twoBackOdd o)

threeNotEven : Even 3 -> Void
threeNotEven e3 = oddNotEven 3 e3 (MkOdd 1 Refl)

-- The simple case, without using the general tool
threeNotEven' : Even 3 -> Void
threeNotEven' x = oneNotEven $ twoBackEven x

[David Thrane Christiansen]

> threeIsNotEven : Even 3 -> Void
> threeIsNotEven (Twice Z) impossible
> threeIsNotEven (Twice (S Z)) impossible
> threeIsNotEven (Twice (S (S Z))) impossible
> threeIsNotEven (Twice (S (S (S Z)))) impossible
> threeIsNotEven (Twice (S (S (S (S n))))) impossible

Yep, this is way easier than what I wrote :-)

/David

[Conor McBride]

It's still too much like hard work.

I'd be inclined to define

parity : Bool -> Nat -> Bool
parity b Z = b
parity b (S n) = parity (not b) n

Parity : Bool -> Nat -> Type
Parity True = Even
Parity False = Odd

and prove some stuff like

introParity : (b : Bool)(n : Nat) -> So (parity b n) -> Parity b n
elimParity : (b : Bool)(n : Nat) -> Parity b n -> So (parity b n)

I'd also reconsider defining Even to bless (n * 2), not (n + n), the
better to keep the Ss at the front. Likewise, Odd could bless
(S (n * 2)).

As my old man used to say, "Never solve one problem.".

Cheers

Conor


>
> /David

[Paul Cadman]

Thanks all for your enlightening replies.

I hadn't come across the replace function before. It seem like there's plenty of Idris I've still got to explore.

Paul