Proving Equalities in a Commutative Ring Done Right in Coq

Assia Mahboubi 1, * Benjamin Gregoire 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

https://hal.inria.fr/hal-00819484
Contributor : Assia Mahboubi <>
Submitted on : Wednesday, May 1, 2013 - 3:59:20 PM
Last modification on : Saturday, January 27, 2018 - 1:30:50 AM

Links full text

Identifiers

Collections

Citation

Assia Mahboubi, Benjamin Gregoire. 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⟩

Share

Metrics

Record views

275