# Decidable equality on multiply nested inductives

Hello,

I came across another problem with a similar expression type, as in my last question. I would like to prove decidable equality for this expression type.

``````Inductive Expression : Type :=
| EEmptyList
| ETuple (l : list Expression)
| EMap   (l : list (Expression * Expression)).

Theorem expr_eq_dec : forall e e' : Expression, {e = e'} + {e <> e'}.
``````

At first, the `EMap` constructor had two lists instead of the product, and I managed to prove the property in question with `Fixpoint` (like in this question), however, when using product inside the list, I get ill-formed recursion errors. I also tried to use the mentioned code about trees and json in the above mentioned thread, but I wasn’t able to formalise it in the case of `EMap`-s (in this case both elements of the product are recursive, unlike in json code).

Is there an easy approach to generate or prove decidable equality for multiply nested inductive types or can I use somehow `Program Fixpoint` here? Also is there a way to generate correct induction principles for types like this?

Using stdpp’s solve_decision, here’s an example

This sort of code should work just fine even with a product of two expressions being involved; if it doesn’t, please post your best attempt. That file also includes induction principles (in both Type and Prop), but the code there (and the Ltac!) is likely overkill for you, since you have so few constructors.

Thank you! I’ll write as soon as I figure it out.

Well, we found another working solution. Initially, a manually written `prod_eq_dec` was used, and not the build-in `prod_eqdec` in `Coq.Classes.EquivDec` while proving the `expr_eq_dec` as `Fixpoint`. This change immediately solved the ill-formed recursion problem. However, we will investigate the induction principles further.

Did your `prod_eq_dec` end in `Qed`? That’d explain it — Coq’s termination checking must likely inline `prod_eq_dec` so that it can check to what argument `expr_eq_dec` is applied.
Also, you want decidable equality proofs to end in Defined anyway, in case you want to run them :-).

BTW, reminder to posting actual code and errors — after enough years with Coq, some problems become easy to spot from errors; I think my diagnosis would be easy to check.