coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [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: RE: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type
Date: Mon, 17 Jul 2017 16:39:04 +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 mga06.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 10.0.102.7
Ironport-phdr: 9a23:U2mGXhayUfU7wd+bxGo4CkD/LSx+4OfEezUN459isYplN5qZr8m6bnLW6fgltlLVR4KTs6sC0LuJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT6/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57m/Zl9BwgqxYrhKvpRN/wpLbb46OOfp7Yq/QeckXSXZdUstTUSFKH4Oyb5EID+oEJetUoZTzp1wQohuxGQmsHuTvyidQinTr2qM60vguEQHc0wM+G9ICvmnfodLwNKcTTe+1zLPHwivHb/9Mwjf975bHch89ofGWWrJwadHcyUgpFwPZkFqQrZbpMC+S1uQIqmWW6fdrW+yoi24isQ5xoz6vy98tionPmoIa1FTE+T9kz4krI9CzVU11Yca8HZdNuSyXOJF6Tt4sTmxnoio217MLtJ+hcCUE1Zgr3wPTZv2JfoSS7B/uWvydLSl2iX9hYr6zmhW//Va4xuHhV8S51ExGojRFn9TDrHwByQbf5taaRvdg+EqqxCyB2BrJ6u5eJEA5jarbJIAlwr43jpcTtEvDETXqlEj3lqOWd0Mk+vS25OTjeLnpupicN4pshgH/NKQhhNC/DPwlPgUAUGWX4/mw2bPs8EHjXblHgPw7nrPXvZzHPcgbo7S2Aw5R0oYt8Ra/CDKm3cwdnXkGMF1FeAiIgJbtO13UO/D4Cumwg1uwkDdxwPDGJqbsApTLLnjfjrjheaxx5FJbyAo21dxf/Y5bCqkdIPLvXU/8rMDXDhggMwCt3+nnDMh92ZgFVGKUAq6ZNbvSvkWS6uIuJemMfo4VtyznJ/gr/f69xUM+zBUWerDs1p8KYli5GO5nKgOXezCk1twGCCIBuhc0ZO3sklyLFzBJMSWcRaU5s3sAD4+pEZ3EXsTlpb2K3C62GtceMmVHAVCFHHOubIKJVOsWbzq6I8l9nzhCXr+kHdxynSqyvRP3nuI0ZtHf/TcV4Mru

Dear Gaetan,

>>If this doesn't match your expectation, I can prepare a sample.

>Please do.

attached please find a Z modulo ring example which shows two unexpected
behaviors of the ring tactic:

1.) it looks like the ring operators applied to literal coefficients need to
compute with simpl, which is a serious restriction since simpl does not
behave in a very consistent way. It is not sufficient that operators applied
on literal coefficients compute with cbv.

2.) addition of ring structures for the same type hides previously defined
ring structures, even if all relations are different.

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

Attachment: ModuloRingMinimal.v
Description: ModuloRingMinimal.v

[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