coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] ring tatic on Z with positives
- Date: Fri, 8 Jan 2021 11:07:07 -0800
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f180.google.com
- Ironport-phdr: 9a23:z7YBghHcafMp7ZPXvPgXNJ1GYnF86YWxBRYc798ds5kLTJ7zrsuwAkXT6L1XgUPTWs2DsrQY0rWQ6fy9EjBdqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5wIRmsswncuckbjYRtJ6sx1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrx2hqRJxwIDafZ+bO+Zlc6zHYd8XX3BMUtpNWyFDBI63cosBD/AGPeZdt4Twu0ABrRu/BQm3BOPg1DxIjWLq0K08yeshFxzJ1xEnEt0Uq3vUrNT1NLwSUe+rz6nE1y/Mb/VM1jf79YfEaBEhofCQXbJ/asfRxkwvGBnEjlWUs4DqIzSV1uEUvmWd8uFvWv6hhXQ9pAFtvjig2N0sio/Ri48Lyl7J6zh0zYk6K9ClVkJ2b8CoHZhMuiyUN4V6XMwvTmVqtSonyLALpJ62cigIxZkkxRPTd+KLf5aL7x/gWuucJypzinxieLK6nRmy8E6gx/XgWcmzylZKqDRKkt3ItnwXyRPc99WHR/1g9UmiwTaCzx7f5v1ALEwulqfWK4QtzqMxm5cSq0jPAyz7lFnwgaSLbEsr4PKo5P7iYrj+pp+TKYt0igbmP6QrgMO/AOA4PhEPX2if5OiwzbPj8VD6TblWlPE2na7ZsJfVJcQfuKG1GRNa0oEm6xqnDjem1soXnWUfIV5bZB6Ki5LlNlLOLfziEPuyglWhnC12y/3FIrHtGpDNIWLCkLflc7Z98UlcyA8rwN9F/J1UCrABIOnzWkDvt9zUFAU2MwquzObhFdpxzIIeWWOTAq+WK67SvlqI6fguI+mIfoMapDH9K/096/70kXA5gUMdfbWu3ZYPdH+4Ge1mL1yFbnron9cOCnwHvhE+TezvkF2NSyRfZ3e0X6Im5zE0EpiqDYnZRtPlvLvU1yCiW5ZSe2oOXluLCDLjc5iOc/YKciObZMF7xG8qT7+kHqYr1RC1tAL5g5NhJ+zYsnkRv5Liz9h45Kvakxg0+Xp1DtiS+26IRmBw2GgPQmllj+hEvUVhxwLbguBDiPtCGIkLvq4bYkIBLZfZitdCJZXyVwbGJInbTV+nRpCnBWh0QIthm5kBZEFyH9jkhRfGjXLzUu0l0oeTDZlxyZrymn34JsJz0XHDjfBzgFwvQ88JPmqj1Pcmq1rjQrXRmkDcrJ6EMLwG1XeUpmiGxGuK+kpfVVwoXA==
It was a bit surprising that ring couldn't solve the lemma below:
Should it be extended to preprocess the goal as I do in the ringpp Ltac below?
It seems that would strictly increase the potence of ring.
Has someone written such more potent ring tactics and are willing to share?
Require Import ZArith.
Lemma ringz (numCpu: positive): (3 * 1 * Z.pos numCpu * Z.pos (1 * 16))%Z = (3 * 1 * Z.pos (1 * 16 * numCpu))%Z.
Proof.
Fail ring.
Ltac ringpp :=
repeat rewrite Pos2Z.inj_mul;
repeat rewrite Pos2Z.inj_add;
ring.
Lemma ringz (numCpu: positive): (3 * 1 * Z.pos numCpu * Z.pos (1 * 16))%Z = (3 * 1 * Z.pos (1 * 16 * numCpu))%Z.
Proof.
Fail ring.
Ltac ringpp :=
repeat rewrite Pos2Z.inj_mul;
repeat rewrite Pos2Z.inj_add;
ring.
ringpp.
-- Abhishek
http://www.cs.cornell.edu/~aa755/- [Coq-Club] ring tatic on Z with positives, Abhishek Anand, 01/08/2021
- Re: [Coq-Club] ring tatic on Z with positives, Frédéric Besson, 01/08/2021
Archive powered by MHonArc 2.6.19+.