coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

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 09:02:20 +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 mga17.intel.com
Ironport-phdr: 9a23:cOZvpRx67/bWuMHXCy+O+j09IxM/srCxBDY+r6Qd2+4eIJqq85mqBkHD//Il1AaPAd2Fraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HSbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKiI5/m/UhMx+jq1boQ6uqBNwzYPPfIGaL/5zcr/Bcd8GR2dMWNtaWSxbAoO7aosCF+QNM/tfr4bjqFsOsQG+BQ60BO/31zRGgX720rE60+s7Dw7G2AIsFM8JvXTRrdX6KKcSXvqrw6nM1znDdPRW1iny6IjUaBAhpumMUKlxccrX1UkgCQfFgk+MpoziOjOYz+IAuHWV4epnUOKgkW8nqwdprziuwMcslpfGhoYPxl/Z6yp0xps+K96gSENjfNKpFIVcuzuaOoZ2WM8vQ39ktDwnxrAGpJK3ZDUGxZUpyhLFZfGKfZKE7gztWeuVOzt0mXFodK6nixqv8EWtzvfwWte03VtFtCZJjMPAum0Q2xDP7MWMV+Fz8V272TmV0gDe8uFELl4wlarcM5Mhx7EwmYAOvUnBBCP2mUP2jLOIeUUg4OSn9+PnYrD+qp+dMY97lB3+P7wzlsG7H+g0KAgDUmiB9em8yrHv51D1TbVXgvEul6nWqpHaJcAVpq6jBA9V154u6xO+Dzi60NQXh2cILFZfdBKciIjmJV7OIOziDfe4m1ShizZrx/baPrL/BpXBNGTMkLDkfbpl8U5T1BIzzcxD55JTErwOPPXzWlbouNPECh85Lhe7zv38CNR904MeQXiADrWYMKPUq1+I5/ggL/OCZI8P637BLK1v7Pn3yHQ9hFU1fK+z3JJRZmryVqBtJFzcan7xiP8AF30Lt0wwVrq5pkeFVGsZXHG/UL4m4Sl/QKenBofKS4TnyOiE3Sy7F5BSIHtBB1+QC3DwX4SCR/oILimVJ5kywXQ/SbG9Rtp5hlmVvwjgxu8/d7uGymgjrZvmkeNNyajWnBA2+yZzCp3EgWCLU2xw2GgPQm1vhfwtkQlG0l6GlJNArblAD9UKvqFIVBs3MdjXyOkoU4mvCDKERc+ATROdevvjATw1SYtukdoBah8iXdSkkh3HmSGtBu1Nmg==

P.S.: of cause you can remove the morphism from Add Ring, since it doesn't
serve any purpose:

Add Ring mword_ring :
(@regRing 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

[Coq-Club] morphism option of ring tactic, Samuel Gruetter, 08/06/2018
- RE: [Coq-Club] morphism option of ring tactic, Soegtrop, Michael, 08/07/2018
  - RE: [Coq-Club] morphism option of ring tactic, Soegtrop, Michael, 08/07/2018
    - Re: [Coq-Club] morphism option of ring tactic, Samuel Gruetter, 08/08/2018
      - RE: [Coq-Club] morphism option of ring tactic, Soegtrop, Michael, 08/08/2018
        
        Re: [Coq-Club] morphism option of ring tactic, Samuel Gruetter, 08/10/2018