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 11:56:50 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.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 mga05.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 10.0.102.7
Ironport-phdr: 9a23:Lic6nRNcxoJQduuV1r0l6mtUPXoX/o7sNwtQ0KIMzox0Ivj/rarrMEGX3/hxlliBBdydsKMbzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFKiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkHKTA37X3XhMJzgqJVoh2hpgBwzIHbboyOKPpxZafQcc8GSWZdXMtcUTFKDIOmb4sICuoMJehUoZT6p1QQohu+GROsBOT3yjNQm3T42qw63PghEQ7cwgMgG9wCu2nTodXwNacdTeC1w7PWwjXHdf9WwjD955bHchA9u/GMWqpwfNHQyUkpCwPKkFGQpZb5MDOS0+QAqm6W5PduW+Kojm4osQBxoj63y8ctjInJmpwaylTe+Spk3ok4I8CzRk1jYdO8DZddsz+WO5F2T84iWW1luDg2xqcJtJO1ZCQG1ZUqyhDFZ/GJfYWE+AzvWeiVLDtimX5oe6yziw6v/UWhzuDwTNe43VZFoyZfjNXArG4B2wHO5sWBV/Bz5F2u2SyV2ADW8uxEIV47la7cK5M5x74wmYAcvVjDEyPsmUX2irOWeVsg+uSy9+vnZbDmqoedN49ylA7+LrwjltG7DOgmKAQDX2iW9f682bH950H0T7tHguUzkqbDsZDaIcobprS+Aw9Qyosj7he/ACum0NsCg3YHKEhJeAmAj4f3NFHOPOr4DfCng1m3kTdrwezGMaPlApnXMnfDl7Lhca5n60FA0Aoz0cxf55VMB74dJ/LzQ1b9u8DcDh8kKAO52P3nCdV41oMGQ22DGK6ZMKXIsV+J/O0jOeeMZJVG8Ar6frIu4Oerhnskk3cce7Oo1N0ZcjrwSv9hOgCSZWfmqtYHC2YD+AQkGr/EklqHBHRoYHu9Q7g7/nVzLYOtDY7OQsrl1LmA1yeyE5kQfWdLBUyWFm/AdoOYVvNKYyWXdJwy2gcYXKSsHtdynSqlsxX3nuJq

Dear Gaetan,

> You can also use a type alias.

thanks, an interesting hint!

> This works because ring uses the relation to figure out which structure
> should be
> used.

This I don't get. In my situation all relations are different (including eq)
and all relations in the term I present to ring are either from on or the
other ring structure, only the type is the same. Still the ring tactic
selects the wrong ring structure. So my impression is that ring only looks at
the type. If this doesn't match your expectation, I can prepare a sample. It
is also possible that I did a mistake here.

Which relation do you think ring looks at? The equality relation? How about
ring_simplify then?

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