Practical and sound equality tests, automatically -- Deriving eqType instances for Jasmin's data types with Coq-Elpi

Benjamin Grégoire (1, 2) , Jean-Christophe Léchenet (1, 2) , Enrico Tassi (1, 2)

1 STAMP - Sûreté du logiciel et Preuves Mathématiques Formalisées
2 UniCA - Université Côte d'Azur

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 procedure scales to large inductive data types, as in hundreds of constructors, since the terms and proofs it synthesizes are linear in the size of the inductive type. Moreover it supports some forms of dependently typed arguments and sigma types pairing data with proofs of decidable properties. Finally feqb handles deeply nested containers without requiring any human intervention.

Domaines: Logiciel mathématique [cs.MS]; Logique en informatique [cs.LO]

Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi. Practical and sound equality tests, automatically -- Deriving eqType instances for Jasmin's data types with Coq-Elpi. CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2023, Boston MA USA, France. pp.167-181, ⟨10.1145/3573105.3575683⟩. ⟨hal-03800154⟩