Abstract:

I will present a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language, which features dedicated proof commands to automate the synthesis, and the verification, of the technical parts often eluded in the literature. We aim to build a tool which can be used for a wide variety of formalization projects and which is easy to use (with, e.g., an interactive interface, some automations, and the formalization of some useful helping lemmas, one of them having, up to now and to our knowledge, no formal proof in the litterature). Joint work with Benoît Guillement, Ambroise Lafont and Assia Mahboubi.