Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] morphism option of ring tactic

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] morphism option of ring tactic


Chronological Thread 
  • From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: RE: [Coq-Club] morphism option of ring tactic
  • Date: Tue, 7 Aug 2018 08:56:50 +0000
  • Accept-language: de-DE, en-US
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga14.intel.com
  • Ironport-phdr: 9a23:QvntbBPiVuvqOUl8dn8l6mtUPXoX/o7sNwtQ0KIMzox0IvjzrarrMEGX3/hxlliBBdydt6oazbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlJiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkHKTA37X3XhMJzgqJVoh2hpgBwzIHbboyOKPpxZafQcc8GSWZdXMtcUTFKDIOmb4sICuoMJehUoZT6p1QQohu+GROsBOT3yjNQm3T42qw63PghEQ7cwgMgG9wCu2nTodXwNacdTeC1w7PWwjXHdf9WwjD955bHchA9u/GMWqpwfNHQyUkpCwPKkFGQpZb5MDOS0+QAqm6W5PduW+Kojm4osQBxoj63y8ctjInJmpwaylTe+Spk3ok4I8CzRk1jYdO8DZddsz+WO5F2T84iWW1luDg2xqcbtZKmfCUG0Ikryh/RZvCdfYWF7AjvWPifLDp8nn5pZbGyiwqq/US9y+DxUtO43EhKoydKiNXAqGoB2wHO5sSbTPZ2412v1iyV1w/J7+FJOUA0mrTfK54m2rMwk5UTvl7eEiL5gkn2jamWdlk69eis8ejofrLmppqEO491jAHxLLgul9SiDek8LAQCRWiW9OSm2LDj40H1WqhGguA2n6XBtZDVP8Ubpqq3Aw9P1YYj7g6yDzKn0NsEnXkINkxKeBadg4jyPFHBPv/4Deulg1SriDdm3PHGPrv9AprTKnjPiqvufbF460JE0go80chf545ICrEGOP/8RkjxtMXBAhAlNwy03v3oBc5m1oIeXGKPGrWWPLnTsV+O/OIvIvODaJUbuDbneLAZ4Kukhngg3FQZYKOB3J0NaXn+EO4saxGSZmOpidMcG08LuBA/RarkkgvRfyRUYiP4ZKUx6S0hD5riRaLCTYCkjbjLlHO+H5ZWb21CTEuLHHj0bYKcc/YKdC+WZMRml2pXBvCaV4Y92ET250fBwL19I7+Mo3xKhdfYzNFwotbru1Q3/D1wAd6a1jjUHWBygm4MATQx2fIm+BAv+hK4yaF9xsdgO5lL/foQC1U7M4LRy6pxDNWgAlucLOfMc06vR5CdOR90Tt81xIZRMUNyEoz+yBHFwyeuRbQSku7TCQ==

Dear Samuel,

in general the purpose of ring is to solve goals by using the associativity
and commutativity laws of one ring. The ring is selected by the type
parameter of the equality. In your case you need additional lemmas to solve
the goal, which have nothing to do with associativity or commutativity.

The Coq manual states, that the purpose of providing a ring morphism is to
extend a generally non computational ring with a computational constant type,
so that constant folding can be done. I would think this only works when the
provided morphism is computational and not an axiom. It might also be that
the ring tactic only tries to use the morphism if the respective terms are
free of variables, which is not the case in your example. Add Ring has a
"cnstants" option to provide a tactic to judge what a constant is, but I
don't see how this would help you. So your usage of morphism seems to be a
stretch.

But there is a way to do it: use the "preprocess" option to Add Ring to apply
rewrites to convert all Z operators to mword operators like this:

Add Ring mword_ring :
(@regRing mword MW) (
morphism (@ZToReg_morphism mword MW),
preprocess [repeat (rewrite ZToReg_morphism.(morph_add) || rewrite
ZToReg_morphism.(morph_sub) || rewrite ZToReg_morphism.(morph_mul))]
).

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928



Archive powered by MHonArc 2.6.18.

Top of Page