@inproceedings{b6e001403a4240aabe3217fe1a8848a7,
title = "Proving equalities in a commutative ring done right in Coq",
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. {\textcopyright} Springer-Verlag Berlin Heidelberg 2005.",
author = "Benjamin Gr{\'e}goire and Assia Mahboubi",
year = "2005",
doi = "10.1007/11541868_7",
language = "English",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "98--113",
booktitle = "Theorem Proving in Higher Order Logics: 18th International Conference, TPHOLs 2005. Proceedings",
note = "18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005 ; Conference date: 22-08-2005 Through 25-08-2005",
}