Decidable equality in Agda with less than n^2 cases?

Question

I've got a datatype for the AST of a programming langauge that I'd like to reason about, but there are about 10 different constructors for the AST.

data Term : Set where
  UnitTerm : Term
  VarTerm : Var -> Term
  ...
  SeqTerm : Term -> Term -> Term

I'm trying to write a function that has decidable equality for syntax trees of this language. In theory this is straightforward: there's nothing too complicated, it's just simple data being stored in the AST.

The problem is that writing such a function seems to require about 100 cases: for each constructor, there's 10 cases.

  eqDecide : (x : Term) -> (y : Term) -> Dec (x ≡ y)
  eqDecide UnitTerm UnitTerm = yes refl
  eqDecide UnitTerm (VarTerm x) = Generic.no (λ ())
  ...
  eqDecide UnitTerm (SeqTerm t1 t2) = Generic.no (λ ())
  EqDecide (VarTerm x) UnitTerm = Generic.no (λ ())
  ...

The problem is, there are a bunch of redundant cases. After the first pattern match where the constructors match, ideally I could match with underscore, since no possible other constructor could unify, but it doesn't appear that I can do that.

I've tried and failed to use this library to derive the equality: I'm running into problems with strict positivity, as well as getting some general errors that I'm are pretty hard to debug. The Agda Prelude also has some facility for this, but looks pretty immature, and is lacking some things that I need from the standard library.

How do people do decidable equality in practice? Do they suck it up and just write all 100 cases, or is there a trick I'm missing? Is this just a place where the newness of the language is showing through?

Your Term type looks very vanilla, I'm surprised the Generic package didn't work with it. Can you post more detail about how it failed? — Cactus
@Cactus, I guess the problems are the ones described in this issue. jmite, if there are other problems, then please open more issues, I'd be glad to try to help you. Could you also clarify why Ulf's Prelude is not appropriate for you? Also, you might try to request adding missing functionality to Prelude, it's likely can be added by just copypasting from the standard library. As to your issue itself, yes, people just tend to manually write all the boilerplate or generate it using external tools. — user3237465
@user3237465: the linked issue is about datatypes where some constructors have parameters that are 'indirectly inductive', right? So if he had SeqTerm : List Term -> Term then that issue could apply; but the example in the question is directly inductive in SeqTerm : Term -> Term -> Term. — Cactus
@Cactus, yes, but I assume the mention of problems with strict positivity implies there are indeed some non-trivial constructors like your SeqTerm. For Term provided as is there should be no problems. — user3237465

Jesper Jesper · Accepted Answer · 2017-07-26T09:06:08

If you want to avoid using reflection and still prove decidable equality in a linear number of cases, you could try the following approach:

Define a function embed : Term → Nat (or to some other type for which decidable equality is easier to prove such as labelled trees).
Prove that your function is indeed injective.
Make use of the fact that your function is injective together with decidable equality on the result type to conclude decidable equality on Terms (see for example via-injection in the module Relation.Nullary.Decidable in the standard library).

Decidable equality in Agda with less than n^2 cases?

1 Answers