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: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?
Date: Mon, 21 May 2018 13:19:49 +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 mga02.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.200.100
Ironport-phdr: 9a23:b6X4IhISkvMWTZMAwtmcpTZWNBhigK39O0sv0rFitYgeL/7xwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhicZOTAk7GHZhM9+jKxZrxKguxNwzIHabZqJNPVleq7RYc8WSXZDU8tXSidPApm8b4wKD+cZM+pWso79qEUBrRuiHwmsA/vvxidVjXHx3K01z+QhHhvY0wwkEd4FrXPZrND0NKgOUeC61rfHzTHZY/NN3jfy9ofIcgw7ofGLRbJ9asvRyU8zFwzbilWcs5DqPzSQ1ukUtWWQ8uRuVeWqi2E9qgFxpCCixsYqionVmI0VzkrI+jhnz4szONa2S1Z7bMa5HJZeuCyWLZZ6T80tTm1ypSo3xLwLtYSlcCQW0Jgr2h/SZvKdf4WG7B/vTvidLDl8iX5/Zb6yhAi+/VC9xuD9UsS4ykhGoypKn9XWqHwBzQLf58eDR/Z740yvwyyA1xrJ5eFBOU00lbTUK5omwrMok5oTvl7MEjPolEnsja+WcFkk9fas6+j9frrmoZqcO5d1igH4LKsuhtSyDfk2PwUBRWSX5Oqx2bL58UHkTrhHj+c6nrfFvJzCIMQUvK+5Awtb0oY57Ba/Ci+r0NEZnXYbLFJKYgyIj4zzN1HVJ/D3E/i/g0i2kDds3/DLJbzhApPRLnfdlLftZ6py60lZyAYr19BQ+4pUCq0dIPL0QkL+qNvYDgYgPwOox+bnFc5y25gFWWOPB6+ZKLndvUWJ5uIpOemMZZUatCzzK/g/tLbSiipzklgEOKKtwJE/aXaiH/0gLV/TKS7nhc5EGmMXtCI/SvbrgRuMS2gASWy1Wvd23TY2B568Cp+HDqWsi7yI0SPxVslTZ2tGA12IV2zveoqYQfAUQCOUPsJl1DcDUO7yGMcayRiyuVqimPJcJe3O93hA7MOx5J1O/+TW0CoK23lxBsWZ3XuKSjgtzGIOWzIymqt4pB4kkwvR4e1Dm/VdUOdrybZRSA5jbMzdyfB3D5b5XQeTJo7UGmbjec2vBHQKdvx0w9IKZB8iSdCth0iZmSusH7IR0beMAc5s/w==

Dear Nicholas,

thanks for the pointer, very interesting!

Just I am not sure if it would be possible to write a gallina function
mapping axiomatic Z to concrete Z. In axiomatic Z, the number 2 would be
succ(succ(zero)), where succ is a function from ZAxioms.t to ZAxioms.t, not a
constructor. What I could do is:

1.) write an Ltac function
2.) define an inductive prop, which relates axiomatic and concrete Z
3.) write such a function assuming a more Church numeral like definition of
the axiomatic Z

But as far as I can see none of this would help me to use the techniques you
describe with the axiomatic Z from the standard library.

Any suggestions welcome!

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