is there a way to rewrite and simplify `decEq x x`?

Question

In the following code (which is an attempt to solve an exercise from 'Software Foundations' [chapter on Lists]), Idris reports a very complex type for countSingleton_rhs. The type includes a complex expression having the following at its core: case decEq x x of ....

module CountSingleton

data NatList : Type where
  Nil : NatList
  (::) : Nat -> NatList -> NatList

-- count occurrences of a value in a list
count : (v : Nat) -> (s : NatList) -> Nat
count _ [] = Z
count Z (Z :: ns) = S (count Z ns)
count Z (_ :: ns) = count Z ns
count j@(S _) (Z :: ns) = count j ns
count (S j) ((S k) :: ns) =
  case decEq j k of
    Yes Refl => S (count (S j) ns)
    No _ => count (S j) ns

-- to prove
countSingleton : (v : Nat) -> (count v [v]) = S Z
countSingleton Z = Refl
countSingleton (S k) = ?countSingleton_rhs

Why isn't Idris simplifying decEq x x to Yes Refl? Is there a better way to implement count which avoids this behaviour? What can I do to simplify/rewrite the types in order to make progress?

Answer 1

Your count function is more splitted than it needs to. If you check for decEq x y anyway, you can unify all cases except count _ [] = Z:

count : (v : Nat) -> (s : NatList) -> Nat
count _ [] = Z
count x (y :: ns) = case decEq x y of
    Yes Refl => S (count x ns)
    No _ => count x ns

The straight-forward way to prove countSingleton is to follow the flow. Your countSingleton_rhs has a complex type, because the type is a case switch, depending on the result of decEq v v. Using with Idris can apply the result of the branch to the resulting type.

countSingleton : (v : Nat) -> (count v [v]) = S Z
countSingleton v with (decEq v v)
    | Yes prf = Refl
    | No contra = absurd $ contra Refl

---

As you have noted, this seems a bit redundant, as decEq x x is clearly Yes Refl. Luckily it is already proven in the library: decEqSelfIsYes : DecEq a => decEq x x = Yes Refl, which we can use to rewrite the resulting type:

countSingleton : (v : Nat) -> (count v [v]) = S Z
countSingleton v = rewrite decEqSelfIsYes {x=v} in Refl

Unfortunately because of an open issue, rewriting case types doesn't always work. But you can just rewrite count with with to circumvent this issue:

count : (v : Nat) -> (s : NatList) -> Nat
count _ [] = Z
count x (y :: ns) with (decEq x y)
    | Yes _ = S (count x ns)
    | No _ = count x ns