https://hal.inria.fr/hal-00819484Gregoire, BenjaminBenjaminGregoireLEMME - Software and mathematics - CRISAM - Inria Sophia Antipolis - Méditerranée - Inria - Institut National de Recherche en Informatique et en AutomatiqueMahboubi, AssiaAssiaMahboubiLEMME - Software and mathematics - CRISAM - Inria Sophia Antipolis - Méditerranée - Inria - Institut National de Recherche en Informatique et en AutomatiqueProving Equalities in a Commutative Ring Done Right in CoqHAL CCSD2005[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]Mahboubi, AssiaJoe Hurd and Tom Melham2013-05-01 15:59:202022-02-04 03:09:342013-05-01 15:59:20enConference papers10.1007/11541868_71We 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.