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: Emilio Jesús Gallego Arias <e AT x80.org>
Cc: "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 10:24:35 +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
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 10.0.102.7
Ironport-phdr: 9a23:En9yQRQvJ12HY6MXYdqBrRaLL9psv+yvbD5Q0YIujvd0So/mwa6yYBON2/xhgRfzUJnB7Loc0qyN4v+mATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbF/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpxJ9zI7VfI6aO/Vwc7jBfdMDQWdNQtpdWzBcDo66coABD/ABPeFdr4TlqVcAsBy+ChejBOPz0D9IgWf20bUn2OomEAHJwAwgEMgQv3TQotn+KaAfUeW0zKbUzTXMde1Z2TPn5IjTdRAuv/6MXa5qccrW0UkiDALFjlOMqYP7OzOZzPgCs2+e7+d5U++klmApqwZ0oje1x8csjJHEhoMTylDY6yp5xJw5KsCmR0N9fNWqE4NQujmHO4ZyXM8uWWFltSYgxrAGp5K3ZjUGxIknyhLHdvCKcoaF7gjtWeufOzt0mnxodbalixqv8kWs1PXwWtS13VtOtCZJjNnBu38X2xDN8MSLVOZx8lqn1D2SzQ7c8PtELloxlafDK54u3Lowlp0LvETGES/5glj6gaCMekUl/Oio9/roYrH8qpCAMI90jxnyMqUomsOhHeQ1KhUCUmyF9eim1LDu/Vf1TbVUgvEsj6XVrZDXKdwepqGjAg9V1ogj6wy4DzejyNkYmHgHI05FeB2dkYfpP0vCIOv/DfihjFSsjC1rx/fePrD6A5XNKGTDn6nlfbpn90Fczw8zwchF551IErEBPO7zWkjpudPECR85KhW4zPrjCNVgzYwTQnmPA6+cMKPKq1CE/OMvI++WZI8UojnxMfYl5+S9xUM+zHIYfK2o2qw1ZWsqBcNJKkGdbHXrtf4bEG4R9l4zZPy60BuFSzEFNFioWKdprAo8BY26F4DbAsiIgbeB1Sq/VNUCY2FNClmBFTHzcIiLR+0LcAqTJNNslnoPUr33GNxp7g2nqAKvk+kvFeHT4CBN7Z8=

Dear Emilio,

I wanted to use the ring tactic in proofs of pretty much what you describe
(various variants of standard library CycliyType), so to use it in this way I
would have to define an intermediate type just for the proofs, which is not
so convenient.

So I either have to redefine the ring tactic from time to time or extend it
to take an options ring structure name.

Best regards,

Michael

Michael Soegtrop
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