coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] More than one ring structure (e.g. modulo ring) for one type

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type
Date: Fri, 14 Jul 2017 12:34:14 +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 mga01.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 10.0.102.7
Ironport-phdr: 9a23:Ee4gWBxyAcChZLXXCy+O+j09IxM/srCxBDY+r6Qd2+keIJqq85mqBkHD//Il1AaPBtSEraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze6/9pnRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKiI5/m/UhMxxkK1UrwmsqAZjz4PQeoyZKOZycr3bcNgHRWRBRMFRVylZD4+ycoUPCPQOPelEr4nnoFsOtQOyDhSrCuPu1jBIhmX50rM+0+gvDArL2wkgH9MSv3TUttr6KqMSXfquzKnP0zrDYO9W2S366IjQaR0hoPeMXa5ufsrV00UgCwTFjlCJpIHjIjib2OMNs22B4OphU+Kik28nqwdtojexwscgkJTGiZwTx1vZ9it52J44KcC8RUJle9KpEJtduzuaOodoWM8vQGJltD4nxrAHt5O3ZiYHxZo9yxLBZfGKd5KE7g/gWeqMOTt0mXNodbalixqs8UWtxffwWteu3FpUsyZJj9/BvW0X2RPJ8MiIUP5981+h2TmR0wDT7flJIUU7laXBN5It36Q8lpsVsUTfACD2nF/6g7ORdkUh4uSo6uLnbav6ppKEKoN5jh/yPr4ul8G/G+g1MhYCU3KY9Om/zLHj+Ff2QLROjv04iKnZt5XaKNwepq64HwBV0pws5Ai7Dzu8y9QYmmcILF1ZeBKdiIjpI0rDIPH+DfejnVuslC1nyOzBPr3kGpnNNGTMkK/9fbZh7E5R0BY8zddG555NFr4BJO/zVVTqudzDDh45NhS0zPz9BNV80IMeQ2OPDbWDPKPcq1/brt4odqOHY5ZQszLgIdAk4eTvhDk3gxVVKaKuxN4cbG2yNvVgOUSQJ3T21IQvC2AP60AFS+HllEeFSXobQne5X6sx4ntzXIenBofKS4Trm7uM0zuhGYV+Z2ZaB1TKGnDtIdbXE8wQYT6fd5cy2gcPUqKsHtcs

Dear Coq Users/Team,

I sometimes want to have two ring structures defined for one type using different operators. An example is the usual ring for Z and a modulo ring for Z. The ring tactic seems to select the ring structure to use based on the type of coefficients and variables, not on the operators used in the term. Also the ring tactic does not allow to specify a ring explicitly. So I wonder how I can use several ring structure for the same type in one proof.

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] More than one ring structure (e.g. modulo ring) for one type, Soegtrop, Michael, 07/14/2017
- Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Emilio Jesús Gallego Arias, 07/15/2017
  - RE: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Soegtrop, Michael, 07/17/2017
    - Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Emilio Jesús Gallego Arias, 07/17/2017
      - Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Gaetan Gilbert, 07/17/2017
        
        RE: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Soegtrop, Michael, 07/17/2017
        
        Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Gaetan Gilbert, 07/17/2017
        
        RE: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Soegtrop, Michael, 07/17/2017
        Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Gaetan Gilbert, 07/17/2017
        
        Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Emilio Jesús Gallego Arias, 07/17/2017