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: Fri, 25 May 2018 07:59:43 +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 mga04.intel.com
Ironport-phdr: 9a23:uA2jdBXWkyk9YXYRPQDZa3AHrYLV8LGtZVwlr6E/grcLSJyIuqrYbBCBt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlMJ+kb5brhyiqRxxwYHUYZ2aO/Vlc6zHYd8XQXBMUtpNWyFDBI63cosBD/AGPeZdt4TxqUYArRygCgmjGOPv0DhIhmfu0aYn1OohEB3J3Aw6EN0QtHTYosj+OaAXUeC00KbIzS/MYO1S2Tvn84jIdQ4uof6QXbJqdsrR0VIiFwLDjlWMt4PlOymZ2fgKs2ie9udtU/+khWAgqwF0uDevx8Esh5HIhoIT1lDL6yF5zJwoKtKmTkNwfN2qEINIui2HM4Z6XNkuTmFotSogyrAKp4S3cDUUxJg73xLTdv2KfoaS7h/tWuudOyl0iXxhdb6lmhq/8lSsxvXhWsS11FtGtDRJn9nDu3wX2RHf8NWLR/l580qnxD2BzRrc6vteLkAxjafbK4Auwro3lpcLtETDETX5lFn5gaOMd0Uk/PSo5PrjYrn8upCcMIp0hhn/MqQohMO/Hfw1PhUKUmSF4+ix1L3u8Vf5TblUlPE6j7fVvIzCKcQevKG5AgtV0og56xa4CjeryNEYnXgbI1JFYh2IkYzpN0vVIPD/E/i/jEiskC1sx/DeJbDhA5PNLmTdn7flZ7py90lcyA8rwdBF+51UEq0BIO70WkLpqNPYCQY5PxWozObjFdVyzZgTWXmPA6+cKKPdq0WE5uMpI+mWZY8aoizxK/Y/562msXhs01QaZOyi2YYdQHG+BPVvZUuDKzK4idAYVGwOowAWTerwiVTEXyQFNFioWKdprAo8BY26F4DbAsiIgbeB1Sq/VNUCY2FNClmBFTHzcIiLR+0LcAqTJNNslnoPUr33GNxp7g2nqAKvk+kvFeHT4CBN7cuyhugw3PXakFQJzRIxCs2c12+XSGQtxzEJQSM72OZ0pkkvkw7fg5g9uORREJlo390MSh0zbMeOzupmBtS0UQXELI/QFQSWB+6+CDR0deofht8DZ0EkRIengRmbg2yrBaMYk/qAA5lmqq8=

Dear Nicolas, Théo,

I could make good use of some advice from you. I try to apply your technique to just a ZAxiomsSig module. One of the nastier things is that ZAxiomsSig does not offer Leibnitz equality but just an equivalence. This makes some of the proofs a bit harder and of cause also requires to change the type classes using eq on the target type to use ZAxiomsSig.eq, e.g. what is Instance Biunique_R in iso_ssrint.v.

My question: do you think it is the right path to continue without Leibnitz equality? Asked in a different way: will the transfer mechanism at some point require Leibnitz equality anyway so that attempts to live without it will be fruitless, or do you think trying to live without it is the right path?

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