Decidable equality on multiply nested inductives

Using Coq
1

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?

2

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.

3

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

4

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.

5

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.