Decidable Equality in Linear Lines

Suppose you're defining a data type for days of the week (or really, any enum type):

data Day
  = Monday
  | Tuesday
  | Wednesday
  | Thursday
  | Friday
  | Saturday
  | Sunday

Besides being an actually useful ADT for "real-life" work, it has only 7 constructors which makes pattern-matching on it manually a tractable problem. You can hand-write an instance for Eq Day in a few lines:

Eq Day where
  Monday == Monday = True
  Tuesday == Tuesday = True
  Wednesday == Wednesday = True
  Thursday == Thursday = True
  Friday == Friday = True
  Saturday == Saturday = True
  Sunday == Sunday = True
  _ == _ = False

Now suppose you want to provide an instance for DecEq, which is an interface for what Idris calls "decidable equality" : a way to tell whether two values are equal in such a way that there's a proof that they're equal or a proof that they're not (similar to the concept of decidability in recursion theory, versus the weaker property of recursive enumerability). Running :doc DecEq gives output similar to the following:

interface Decidable.Equality.DecEq : Type -> Type
  -- Decision procedures for propositional equality
  Parameters: t
  Methods:
    decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
      -- Decide whether two elements of `t` are propositionally equal

And the same command on Dec:

data Prelude.Dec : Type -> Type
  -- Decidability. A decidable property either holds or is a contradiction.
  Totality: total
  Visibility: public export
  Constructors:
    Yes : prop -> Dec prop
      -- The case where the property holds.
      -- @ prf the proof
    No : Not prop -> Dec prop
      -- The case where the property holding would be a contradiction.
      -- @ contra a demonstration that prop would be a contradiction

The obvious approach

The first, obvious solution is to follow the implementation for Eq:

DecEq Day where
  decEq Monday Monday = Yes Refl
  decEq Tuesday Tuesday = Yes Refl
  decEq Wednesday Wednesday = Yes Refl
  decEq Thursday Thursday = Yes Refl
  decEq Friday Friday = Yes Refl
  decEq Saturday Saturday = Yes Refl
  decEq Sunday Sunday = Yes Refl
  decEq d1 d2 = No ?hmm

If you ask Idris for the type of the hole ?hmm, it'll tell you

  d1 : Day
  d2 : Day
---------------------
hmm : d1 = d2 -> Void

Now we've hit a snag: the days d1 and d2 are arbitrary Days. In other words, with what we've written, Idris doesn't know that if it gets to this line, d1 and d2 won't be the same. If we want to convince it, we'll have to do it the hard way -- and that means adding a whole bunch of new lines.

  decEq Monday Tuesday = ?hmm_8
  decEq Monday Wednesday = ?hmm_9
  decEq Monday Thursday = ?hmm_10
  decEq Monday Friday = ?hmm_11
  decEq Monday Saturday = ?hmm_12
  decEq Monday Sunday = ?hmm_13
  decEq Tuesday Monday = ?hmm_14
  decEq Tuesday Wednesday = ?hmm_15
  decEq Tuesday Thursday = ?hmm_16
  decEq Tuesday Friday = ?hmm_17
  decEq Tuesday Saturday = ?hmm_18
  decEq Tuesday Sunday = ?hmm_19
  -- I give up ...

This will need O(n^2) lines, where n is the number of constructors -- so nearly 50 lines!

A better way

There's a better way to write this instance that's shorter and more elegant. The idea is to write a provably-injective function to another type that already has an instance of DecEq. That's it.

Just as the Eq instance takes SLOCs that are linear in the number of constructors, so does this method. I think the most popular choice is Nat, though you could use other types (even String, which could be useful in the case you have an already-defined Show instance for your type, as long as you can prove injectivity):

dayToNat : Day -> Nat
dayToNat Monday = 0
dayToNat Tuesday = 1
dayToNat Wednesday = 2
dayToNat Thursday = 3
dayToNat Friday = 4
dayToNat Saturday = 5
dayToNat Sunday = 6

Injectivity is the property that every element in the codomain is targeted by a unique element in the domain. In other words, we say f is injective if and only if \forall x, y : f(x) = f(y) \implies x = y. However, before we do that, let us in true mathematical fashion convince ourselves that injectivity is enough for the DecEq instance before we actually prove it's injective:

-- notice how similar the type looks like to the definition of injectivity above
dayToNatInj : (d1, d2 : Day) -> dayToNat d1 = dayToNat d2 -> d1 = d2

DecEq Day where
    decEq d1 d2 = ?hmm

Since the idea is to inject d1, d2 into Nat, let's do that:

dayToNatInj : (d1, d2 : Day) -> dayToNat d1 = dayToNat d2 -> d1 = d2

DecEq Day where
    decEq d1 d2 = case decEq (dayToNat d1) (dayToNat d2) of
        Yes prf => Yes ?hmm
        No contra => No ?nothmm

Inspecting the type of ?hmm, we can see there's enough information in the context to use our lemma directly:

dayToNatInj : (d1, d2 : Day) -> dayToNat d1 = dayToNat d2 -> d1 = d2

DecEq Day where
    decEq d1 d2 = case decEq (dayToNat d1) (dayToNat d2) of
        Yes prf => Yes (dayToNatInj d1 d2 prf)
        No contra => No ?nothmm

Now, inspecting the type of ?nothmm we see it's a function, so we can introduce it as a lambda and get access to its argument, which is itself a proof:

dayToNatInj : (d1, d2 : Day) -> dayToNat d1 = dayToNat d2 -> d1 = d2

DecEq Day where
    decEq d1 d2 = case decEq (dayToNat d1) (dayToNat d2) of
        Yes prf => Yes (dayToNatInj d1 d2 prf)
        No contra => No \d1eqd2 => ?hmm

We see that d1eqd2 : d1 = d2 and contra : dayToNat d1 = dayToNat d2 -> Void. We can use cong from the Prelude to modus-ponens our way to the goal:

dayToNatInj : (d1, d2 : Day) -> dayToNat d1 = dayToNat d2 -> d1 = d2

DecEq Day where
    decEq d1 d2 = case decEq (dayToNat d1) (dayToNat d2) of
        Yes prf => Yes (dayToNatInj d1 d2 prf)
        No contra => No \d1eqd2 => contra (cong dayToNat d1eqd2)
    -- alternatively No (contra . cong dayToNat)

Now let's move on to the heart of the proof: filling in the definition for dayToNatInj. Since Idris has knowledge of the implementation of dayToNat, we can merely pattern match on each argument:

dayToNatInj Monday Monday Refl = Refl
dayToNatInj Tuesday Tuesday Refl = Refl
dayToNatInj Wednesday Wednesday Refl = Refl
dayToNatInj Thursday Thursday Refl = Refl
dayToNatInj Friday Friday Refl = Refl
dayToNatInj Saturday Saturday Refl = Refl
dayToNatInj Sunday Sunday Refl = Refl

Idris will accept this as a total function (you can add total above its type yourself if you'd like to be convinced. Or perhaps fiddle with the definition of dayToNat so it isn't injective and see what the resulting type errors are). Thus in the end, we used 14 = 2*7 = 2*n = O(2n) = O(n) pattern-matching lines which did the bulk of the work, a much better solution!