coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?

From: Nicolas Magaud <magaud AT unistra.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?
Date: Sat, 19 May 2018 22:13:18 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=magaud AT unistra.fr; spf=Pass smtp.mailfrom=magaud AT unistra.fr; spf=None smtp.helo=postmaster AT mailhost.u-strasbg.fr
Ironport-phdr: 9a23:vW9dkhGhBGKsgIcM+0cF551GYnF86YWxBRYc798ds5kLTJ78rs6wAkXT6L1XgUPTWs2DsrQY07GQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDSwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOCI2/2/KisJ/jqxVrh2iqRxx3YDaZ5qYNOZnfqPYYd8aRXZNU8RXWidcAo28dYwPD+8ZMOhAronyu1wOrR+kCgm3GejhzSVHhnDs0q0nzusqDAbL3Ak6ENIBqnvUscj6ObwPUeCzzanI1inDb+lM1jvn5ojIaAksrPeRVrx+dsrRzFMgFwLDjliIs4PlJS+a1uQMs2iF8eVgTvuji2k6qwFvvDev3NsshZfSho4PxFDE7z11wIczJd2kVkF7ZcSoH4ZOuCycKoB4QdsiTnl1tCs01rEKo5y2cSwQxJg52RLTdeaLf5aV7h/hTOqcIil0iGh7dL+xmhq+60mtx+/mWsWpzFpHryxImcTWuH8XzRzc8M2HR+N9/ki/3TaP0Bje6uReLkA1karbK5khwqUslpYJrETPBzT2mFnsjKCMbUUr4eeo5/7pYrX8vpOcNol0hR/iMqk2h8CyD/g0PhIMUmWf4+iwyqPv8VPjTLlUk/E7kLHVsJXAKsQaoq65DRVV0oEm6xunCjepytsYkmMaLF1YYx+Hko7pO1DVIPDkF/ewmU6gkDlxx/zeJL3uHo3NLmTfkLfmZbty90lcyBMqwd9D45JUF6oOLenoWk7xsdzYFgU2Pxa1w+bhEtV915kRVXiBAq+DY+vutgqD4ftqKO2RbqcUviz8Ir4r/a3Al3g8zHkcdq6t1IBfTXm3F+lqaxGcaHXln9spDGELpRYkRarkkgvRAnZoe3+uUvdktXkAA4W8ANKbH9H/sPm6xC6+W6ZuSCVDA1GIH23vctzeCeoKaTmOOMYnnCZWDOH9Gb9k7gmnsUrB85QiNvDdo3dKqJTiz8Rv7qvdj0NqrGEmP4Gmy2iIClpMsCYISjsxhvstpEV8zleEyrQ+nrlDCcZa/PlGFAkgZ8bR

Dear Michael,

I think there is no such tool at the moment. However you may be interested in
reading this workshop paper:
"Transferring Arithmetic Decision Procedures (on Z) to Alternative
Representations” (https://hal.archives-ouvertes.fr/hal-01518660) which
explains how to get back to Z and omega when dealing with an alternative
representation of integers (we mainly studied how to make omega usable for
ssrint, but it shall work as well for axiomatic integers).

Best regards,

Nicolas Magaud

> On 18 May 2018, at 18:34, Soegtrop, Michael
> <michael.soegtrop AT intel.com>
> wrote:
>
> Dear Coq Users/Team,
>
> I wonder if there is an omega or micromega tactic for axiomatic integers
> (based on ZAxiomsSig). I guess this exists only for the concrete integers Z?
>
> In case there isn’t: is there some documentation on how to extend micromega?
>
> 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] Is there a micromega or omega tactic for axiomatic Z?, Soegtrop, Michael, 05/18/2018
- Re: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Nicolas Magaud, 05/19/2018
  - RE: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Soegtrop, Michael, 05/21/2018
    - Re: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Théo Zimmermann, 05/22/2018
      - RE: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Soegtrop, Michael, 05/22/2018
        
        Re: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Théo Zimmermann, 05/22/2018
        
        RE: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Soegtrop, Michael, 05/25/2018
        
        Re: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Théo Zimmermann, 05/25/2018
        RE: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?, Soegtrop, Michael, 05/25/2018