[Agda] equality reasoning and contradictory type indices

[Chris Casinghino]

Hi Agda hackers,

I'm trying to prove an equality goal which looks like:

      foo1 ≡ (foo2 | compare (m + k) m)

foo1 and foo2 are complicated expressions.  Agda is indicating that
foo2 could be evaluated more, if only I knew the value of (compare (m
+ k) m).  "compare" is the standard library function for comparing
nats (definition copied below).  Its result can be "less", "equal" or
"greater".  Of course, here, the "less" case can't occur.

My instinct was to write a "with" clause to look at the cases and rule
out "less" by finding a contradiction.  This won't work, though -
agda gives this error message if you ask it to case split on the
result of the comparison:

  Cannot pattern match on constructor less, since the inferred indices
  [m2, suc (m2 + k2)] cannot be unified with the expected indices [m1
  + k1, m1] for some <...> when checking that the expression ? has
  type foo1 ≡ (foo2 | pat)

This makes sense - the desired type indices in the "less" case are
themselves contradictory, so the pattern match can't type check (I
think).  (Here "pat" is what I called the application of compare and
the <...> is a list of everything in my context).

So, how can I work with this goal?  I could try proving a lemma
showing that (compare (m + k) m) must be "equal" or "greater".  Even
stating this is tricky (I found I had to use "subst" twice to make the
type indices work out).  And I'm not sure how I would apply it to
refine the original goal.

Any advice?  Thanks for your help... it seems I'm still getting the hang
of equality reasoning in Agda.

--Chris Casinghino


The definition of compare:

data Ordering : Rel ℕ zero where
  less    : ∀ m k → Ordering m (suc (m + k))
  equal   : ∀ m   → Ordering m m
  greater : ∀ m k → Ordering (suc (m + k)) m

compare : ∀ m n → Ordering m n
compare : ∀ m n → Ordering m n
compare zero    zero    = equal   zero
compare (suc m) zero    = greater zero m
compare zero    (suc n) = less    zero n
compare (suc m) (suc n) with compare m n
compare (suc .m)           (suc .(suc m + k)) | less    m k = less    (suc m) k
compare (suc .m)           (suc .m)           | equal   m   = equal   (suc m)
compare (suc .(suc m + k)) (suc .m)           | greater m k = greater (suc m) k