coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] ring_theory instance for Z mod d setoid
- Date: Thu, 23 Jun 2022 23:14:04 +0200 (CEST)
- Authentication-results: mail2-relais-roc.national.inria.fr; dkim=none (message not signed) header.i=none; spf=SoftFail smtp.mailfrom=dominique.larchey-wendling AT loria.fr; spf=None smtp.helo=postmaster AT zcs-store7.inria.fr
Sure, there is one such library in the Coq Library of Undecidability proofs, mostly/solely used to establish
Matiyasevich theorem (ie the exponential function is Diophantine).
You can start here:
Best,
Dominique
De: "Abhishek Anand" <aa755 AT pm.me>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Jeudi 23 Juin 2022 21:21:43
Objet: [Coq-Club] ring_theory instance for Z mod d setoid
Has someone written a ring_theory instance for the Z mod d setoid (a and b are equal iff a mod = b mod d)? Along with the equation d \equiv 0, ring_simplify could deep inside mod terms, e.g. (a+d)(a+d) \equiv a*a.--Abhishek Anand
- [Coq-Club] ring_theory instance for Z mod d setoid, Abhishek Anand, 06/23/2022
- Re: [Coq-Club] ring_theory instance for Z mod d setoid, Dominique Larchey-Wendling, 06/23/2022
Archive powered by MHonArc 2.6.19+.