coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?
Date: Fri, 18 May 2018 16:34:34 +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 mga14.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.200.100
Ironport-phdr: 9a23:fQVpEhZ1PV0/jSiu0ZKDL2X/LSx+4OfEezUN459isYplN5qZr8i4bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57m/Zl9BwgqxYrhKguxNwzJXZb5uJOPd6ZK7RYc8WSXRHU81MVyJBGIS8b44XAuYPIOhYqJfyp1QSrRukAgmsHPvjwSJPiH/3waI60/4uHh/C3AAuAtkDt3HUrNTpO6cSS++60q3IwS/Yb/NRxzj955TIcgomofGURr9wcMzRyVUxGAPBlFmftYvlPzaM2+kLrmOV4e1gVee1hG4mrQF8ujmvxsEwiobXgoIZ0E3L+jt/zY0oJtO4UFZ2bcOgHZdOrS2XN4t7TtkiTm12oio216AKtJ6jcCQXyZkqyQTTZvKJfoSS/B7uWuKcLS1liH9mZr6znwu+/Emkx+HmSMW50FlHojBbntXWqHwA2Bje586aQfVn5EihwyyA1wXL5+FEP080ka3bJoYkwr4/jJUfrEvOEjX3mEXwkK+ZaEEk9vK05OTgZ7Xqvp6cN4lqhQHiKqkih8iyDfoiPgUOX2WX4+Sx2KP58UHkXblHjuU6kqzDv5DbIcQbqLS5AwhQ0os77ha/Diup0NQCknYZKFJJYgmHj4/3NFHBPPD4F/C/g0y3nTdqwfDGIqPuApHXInffl7fheK5x61RAxwor0dBf+5VUB6kdL/L0Q0/9rcDXDhskMwOv2OvnE9V81oYGWW2VGKOZMaXSsUWJ5u01OeWMapUV637BLK1v7Pn3yHQ9hFU1fK+z3JJRZmryVqBtJFzcan7xiP8AF30Lt0wwVrq5pkeFVGsZXHG/UL4m4Sl/QKenBofKS4TnyOiE3Sy7F5BSIHtBB1+QC3DwX4SCR/oILimVJ5kywXQ/SbG9Rtp5hlmVvwjgxu8/d7uGymgjrZvmkeNNyajWnBA2+yZzCp3EgWCLU2xw2GgPQm1vhfwtkQlG0l6GlJNArblAD9UKvqFIVBs3MdjXyOkoU4mvCDKERc+ATROdevvjATw1SYtukdoBah8hXdSkkh3HmSGtBu1Nmg==

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