Proving Equalities in a Commutative Ring Done Right in Coq

Assia Mahboubi 1, * Benjamin Gregoire 1
* Auteur correspondant
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.
Type de document :
Communication dans un congrès
Joe Hurd and Tom Melham. TPHOLs 2005, Aug 2005, Oxford, United Kingdom. Springer, 3603, pp.98-113, 2005, Lecture Notes in Computer Science. 〈10.1007/11541868_7〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00819484
Contributeur : Assia Mahboubi <>
Soumis le : mercredi 1 mai 2013 - 15:59:20
Dernière modification le : samedi 27 janvier 2018 - 01:30:50

Lien texte intégral

Identifiants

Collections

Citation

Assia Mahboubi, Benjamin Gregoire. Proving Equalities in a Commutative Ring Done Right in Coq. Joe Hurd and Tom Melham. TPHOLs 2005, Aug 2005, Oxford, United Kingdom. Springer, 3603, pp.98-113, 2005, Lecture Notes in Computer Science. 〈10.1007/11541868_7〉. 〈hal-00819484〉

Partager

Métriques

Consultations de la notice

161