Skip to Main content Skip to Navigation
Conference papers

Proving Equalities in a Commutative Ring Done Right in Coq

Benjamin Gregoire 1 Assia Mahboubi 1, *
* Corresponding author
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We present a new implementation of a reflexive tactic which solves equalities in a ring structure inside the Coq system. The efficiency is improved to a point that we can now prove equalities that were previously beyond reach. A special care has been taken to implement efficient algorithms while keeping the complexity of the correctness proofs low. This leads to a single tool, with a single implementation, which can be addressed for a ring or for a semi-ring, abstract or not, using the Leibniz equality or a setoid equality. This example shows that such reflective methods can be effectively used in symbolic computation.
Document type :
Conference papers
Complete list of metadatas
Contributor : Assia Mahboubi <>
Submitted on : Wednesday, May 1, 2013 - 3:59:20 PM
Last modification on : Monday, December 16, 2019 - 2:46:09 PM

Links full text




Benjamin Gregoire, Assia Mahboubi. Proving Equalities in a Commutative Ring Done Right in Coq. TPHOLs 2005, Aug 2005, Oxford, United Kingdom. pp.98-113, ⟨10.1007/11541868_7⟩. ⟨hal-00819484⟩



Record views