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: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is there a micromega or omega tactic for axiomatic Z?
Date: Fri, 25 May 2018 11:01:17 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f43.google.com
Ironport-phdr: 9a23:jiuN1B1Tra1Hg1FpsmDT+DRfVm0co7zxezQtwd8Zse0TIvad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLnhykHODw5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo6ycYsPCPAGPelArIb9pl4OrR6gCgm2AePg0DlIhnnr1qA9z+QhER/J3As6E9MPsXTUqdD1NKYJXOC6yanH1zTDb/dM1Tjh74jIdwksrPeRVrx+dsrRzFMgFwLDjliIpozlODSV1usJs2eF9eZvSeWvi2s/pwFwpDiv2tkjio3Tio0I1F/J8zhyzoUtJdCgVkJ3fdqpHIFTuiyaLYd6XN4uTm9ytCs1xLALv4OwcjIQx5Q93RHfbuSKc4iW7RLnU+acOTJ4i2hkeLK7nhqy70ugxvHlWsm631tHoDBJktbLtnAK2BzT7taIRuFh8Uem3DaDzwHT6udaLkAojafXNYItz7oqmpcQsUnPBDH6lFj4gaOMeUgp9PCk6+H9bbXnop+cOZV0igb7Mqk2hsy/Afo3Mg8UU2ma+OS80bjj/UziTbVFi/05iKjZsJTAKcsHoa65BhdZ0pw/5BanEzemzNMYkGEbI1JCYRKLlpTmO1XTIP/jFvq/mFStkDJzx//cJLHhA5PNLmLCkLj7Z7p95VRcm0IPyoVU4IsRAbUcKtryXFXwvZrWFEwXKQuxltrnidJK5IIbXG+VB6afNuuGrV+F4aQ9IuyJZacavT/8L74u4Pu43ixxokMUYaT8hchfU3u/BPkzexzIM0qpuc8IFCIxhiR7SeXrjFOYVjsKPiS9Wqs94ncwD4f0VN6fFLDou6SI2WKAJrMTfnpPUwneHnLhdoHCUPAJOnrLf51R1wccXL3kcLcPkBGjsAigluhiJ+vQvzMb7dftiIMz6OrUmhU/szdzCpbF3g==

Dear Michael,

The transfer library won't require Leibniz equality at any point. It works just as well with another equivalence relation.

Cheers,

Théo

Le ven. 25 mai 2018 à 10:00, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

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