In this paper we describe the design and implementation of \feqb{}, a tool that synthesizes sound equality tests for inductive data types in the dependent type theory of the Coq system.

Our tool aims at lowering the manual labor today required in order to use the Mathematical Components library in the development of the Jasmin certified compiler. That library requires a sound equality test for each and every data type, a requirement today often satisfied manually.

The \feqb{} tool is able to handle inductive data types which:

• feature a large number of constructors, as for describing the instruction set of a mainstream CPU. \feqb{} automatically synthesizes terms and proofs which are linear in the size of the inductive data type

• use the dependent function space to mix data and proof, as the sigma type of bounded integers, i.e machine word. \feqb{} synthesizes equality tests which discard proof arguments when the property is decidable and proves their soundness by appealing to the uniqueness of identity proofs

• use containers, such a list, option, pair, \ldots, in the type of constructor arguments. \feqb{} requires no human intervention even in this case and builds the tests and the proofs by composing the existing tests and proofs for the containers

To the best of our knowledge no existing tool has all the features above, which are used in real Coq developments such as the Jasmin compiler. In the paper we describe the procedure and we benchmark it, showing that thanks to its better complexity it outperforms all alternatives, in spite of being implemented in Coq-Elpi, which is an interpreted, high level, programming language.