coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Zify support for all instances of a type function

From: Kazuhiko Sakaguchi <pi8027 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Zify support for all instances of a type function
Date: Fri, 14 Oct 2022 09:01:27 +0900
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pi8027 AT gmail.com; spf=Pass smtp.mailfrom=pi8027 AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk1-f169.google.com
Ironport-data: A9a23:FldDOa/+1phqHJr9gk1lDrUDVnqTJUtcMsCJ2f8bNWPcYEJGY0x3n DMbXWGFP/yKMTCgcox+Oojj/E9X6JWGn4QyGlFl/ChEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPykYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f4nW8pWo4ow/jb8kk25K2p4GhwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEFL0OevHJSxjSCc53P/WXD23+Q2MGU/MNQo9MpqXEMfx 8VNfVjhbjjb7w636LeyS+0pmMd6aceyYtJZtXZnwjXUS/0hRPgvQY2QvY4ejGp23JoXW6+AN qL1ahI3BPjESwVOag9NV7oxme6pgj/0dDgwRFe9+/BmvDmDl1EZPL7FbouFR/epWONvr3mKj UDk3l/3BDQxHYnKodaC2iv02rWncTnAcIkVDfiz8uNgqEaCw3QaThwQT1qy5/ej4nNSQPpaI k0QvzQt9O08rRL6CNb6WBK8rTiPuRt0t8ds//MS1jinwbDI8l6lImEJFw5PRMF7lp4EfGl/v rOWpO/BCTtqubyTbHuS8LaIsD+/URT5y0dSOkfoqiNVvLHeTJEPYgHnFYk8Tfbk5jHhMXShn GDQ9XlWa6A71JZTj82GEUb7byVAT6UloyYw7wTTG3ymt0Z3PdD0IYOv7lff4LBLK4Pxori9U Josy5b2AAMmV8nleMmxrAMlQeDBCxGtbWy0vLKXN8N9nwlBAlb6FWyq3BlwJV1yLuEPciLzb UnYtGt5vcENYSX6MP8sON3tW6zGKJQM8/y1Bpg4ifIeMvBMmPOvoUmCmGbKjj+3yRd8+U3BE cnHL57E4Ykm5VRPlWLqHY/xIJckwScxwW67eHwI50XP7FZqX1bMEe1tGALWMIgRtfrYyC2Ir Ys3H5bVk313DreiCgGJqtV7BQ5RfRAG6WXe8ZM/mhireVo4RgnMypb5ndscRmCSt/8Pzr+Yo CznABEwJZiWrSSvFDhmo0tLMNvHNauTZ1phVcD1FQfzhyoQcsy04b0BdpA6W7Ai+aYxhbR3V vQJMYHISPhGVj2NqXxXYIjfvb5SUk2hpTuPGC65Pxk5XZprHDLS9vHeIwDAySgpDwiMj/UYn YGO7A3hfMc8d1xQN/qOMPOL5HGtjEcZg9N3DhfpIMEMWUDC87pKCi3Wj90xKf4iMR/omzmQj V6XJTw6puD9hZA/3/eUpKKDrqavS/BfGGgDFUblzL+GDwvo1Uv9/p1hCcGjYiL4eF7v3pmbd cF57q3ZIeIWulRnqK9+GOtb9r0/7N7RuLNq9ARoM3HVZVCNCLk7AH258eRQl69K1JlLkBCXX x+Rx9xkJrm5AsPpP1oPLg4DbO7Y9/U1mCHX3MslMnfB+y5707qWY3p8ZyDWpnRmE4J0F4c5z cMKms0csVW/gyV3FOe2tHlf8mDUI0EQV6kiiIohP7bqrQgVm3Viep3XDxHk7K6fM+tsNlYYG R7Kpa7gqYkF+G/8XSsSL1bv09BZp6wygzFR7VpbJ122itvP3fA2+xtK8AUIdAdezzQZ8ud/J llUM1ZRIIOQ9QxJn+lGZXinQCtaNS2a+2vw6loHr3LYRE+WTV7wLHUxFOKO3UIB+UdeQ2R/0 JSH7l36CBDGUdrU3CQgfWJE8dnYUs1X5AnOvOuFDva1NcA2ThS9i5D/eFdSjQXsBP0AoXHup M5o2b1VQrL6PytBmJ8LIdCW+ppIQS/VOVEYZ+9q+Z4IOmTueDuS/zyqAGLpc+NvI836y2OJO /ZMFOluCSvnjD2vqwoFD5EiO7V3xf4lxOQTc4PReFIpjeGtkSpLgrnxqA7O3HQmUvd/o/Ybc 4nxTQ+PIkaUpHlTmlLOkvV6B3qFUYEESjHRjOGR28cVJq0Hq9BpIB0T0KPrnnC7MzlH3hOzv SHfVpDS1MhS+55JpNLpN5lyWiGxJc35DuiTwjvusd4UNdLrGuXNvjMztVPIEVl3P7wQetIvj pWLkof9833ktYYMcVLyuse+BYxWw8StTcxrMs7TB1tLrxuoAcPDzUMKxDGlFMZvjthY2PiCe yK5T8mBLfguRNZXwSxuWRh0ShoyJfz+Ufb9mHmbsf+JNxk61D7HJvOB8VvCTzlSVg0MCq3EJ j7EgdSczfEGk90UHz4BPe9sPLFgKly6WacGScz4hQPFMkaW2GG9qpnQvjt+zwGSBne9RZOwp dqPQxXlbx29tZ3Z1NwT4cQ4ohQTC207muUqOF4U/9ltkT2hEWoaNqInPI4bDo1P2DnHvH0ii OohsEN5Yck8YdhFTfk4yNHqXwPaGO9Xf9mgeG1v8ESTZCO7QoiHBdONM8umD2heIlPeICOPc LnyOUEc+jC+x5hoQaAY4fnTbSJP2KbB3nxRkaziu5WaPvvdaInmEFRuGQNMUWrMFMSleIAn4 4QqbTgsfXxXgnId3Sqtl7C51f3ZUP7SI+0UUBqy
Ironport-hdrordr: A9a23:XKWgf6xFVeLsdvW6LxbGKrPwE71zdoMgy1knxilNoHtuA7Slfq GV7Y0mPHrP4gr5N0tQ/OxoVJPwI080sKQFgrX5Xo3CYOCFghrNEGgK1+KLqAEIWRefygc379 YGT0ERMqyXMbG4t6rHCcuDfurIDOPpzElgv4nj80s=
Ironport-phdr: A9a23:nIhXIREqAQRjCDE0H+pH351GfzVGhN3EVzX9CrIZgr5DOp6u447ld BSGo6k31xmSDdyQsa0MotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5ZPebx9GiTe+fL9+I wu6oAfMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2Q rxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+t6 LplSALziCcfKTE27H3XhMJ3jKJeuh2hphp/yJPQbIyaMPdye6XQds4YS2VcRMZcTyNOAo2+Y IUPAeQPPvtWoZfhqFUBtha+GRCsCfnzxjNUmnP736s32PkhHwHc2wwgGsoDvnHOo9T0KacSU eG1zKrPzT7ecv1ZwzT955LHchA8vf6MXbNwetfWxEk3FgPIjUmcpZLnMj6O2eQNtnKU7+tkV e61l2EnrARxryGpy8wxhYbHmpgbxUrY9SVl3ok1P9u4RVZ0bNOmEJZdtC6XOpZ3T84/Qmxlp Sg0x7MEtJKmfCYG1okqyhrCZ/GafYWF5hLtWeeMLTp5hn9oZb2yihmv/UWkzOD3S8e60FFPr iVfk9nMsGgA1xPS6sibSvt941yu1SyT2ADU7+FIOU80lavHK54h374/jYAfsUXEHiLwhU74j 7eWe1069uS07+nreLbrq5+GO4NqlA3yL74iltG+DOk8NAUFQnKV9v6m1LL5+E30WLVKgeMyk qneqJ3aIN4Upq+9AwNMzIYj6AuzAy6o0NgFnHQKKEhJeB2Aj4juNFHOJO73Ae2jjFSrlTdn3 /HGPrv/DZXRNnXPjqvtcLJn50NfyAc/185T64xJBr0bPf7+W0v8uMTdDhAjMgy0x+jnCM961 oMbQW+PGq6ZPaDOvVOW5O8iOOaMZIoPtzb8L/gp/eLhjXg8mVMFe6mmxoMYaGqkEfR+P0WZf X3sj88cHWsSpAoxUPTqiEGeUT5Uf3u9Q6U85igiBI26CYfDW5uijaea3Ca7G51WfnpJBkqNE XfubYWEWu0DZDicIs97wXQ4Uu2qTJZk3hWzvif7zaBmJ6za4H42r5Xmgft89fDTlBI1vQd9D M2SzmqNTikghmJYH2Vp9K96qE15jFyE1P4r0LRjCdVP6qYRAU8BPpnGwrkmWrgaOyrEd9aNE hO9R8m+RCs2RZQ3ysMPZEB0H5OjiArC1mykGexdjKSFUboz9K+UxH3tP4Bl0X+TzKhx1wN5a sRKPGyiwKV48lubHJbHxn2QjL3ibqEAxGjI/WaHw3CJuRRAUV4oC/rtUnUWZ0+QptP8tQvZV 7H7L7MhP0NazNKabKtHbtq8lVJdWPLqI8jTeUq0kma0QAiLn/aCNdS7PWoa2yrZBQ4PlAV7E W+uEw84C2/hpmvfCGYrDlfzewb29uI4rnqnT0gyxgXMbkt71rPz9ARHzfqbA+ge2L4JokJD4 319AUq90tTKCtGBuxspfaNSZsk46UtG0mSRvhJ0P5ipJaRvzlAEdAE/s0Tr3hRxQoJO9Kpi5 GsrnFIodoqX1VpAc3WT2pWxcrzbJ2/u/Qy+PrbM0wKW29KX96ETrfUg/g+77Uf5Swx4qSwhi ocEgB7+rt3QAQEfUIz8SBMy/hl+/fTBZzUlopnT3jtqOLW1tTnL35QoAvEkw1CuZYQ6UuvMG QnsHskdH8XrJvYtng3jdhNUZLoN3KExNsKiMfCB3eT4WYQo1CLjlmlB7I1nhwiU9nokELHg0 JMMwvXe1QyCHWS0nBKqtcb5nppBbDcZEz+kyCTqM4VWY7V7YYcBDWrGz9Sf/txlnNatXndZ8 ATmHFYawIqzfhHUaVXh3ApW3EBRoHq9mCL+wSYm2z0uq6Oe2mTJzYGAPFIfOz4THjZKglLlI IzyhNcfFESldAkmkhK56F2ynfAK4vQiaTOJGAERIXm+JnoqSqaqs7uef8NDjfFg+T5aVuixe xHSS7LwpQcbzzK2GmJfwD4hcDT58p79nhF8lCecNCMp9CufKZw2n02GooWCFK00vHJOXiRzh DjJC0LpOtCo+Y/RjJLfqqWkUGnnUJRPcC7txIfGtS2h5GQsDwfs+pL70tDhDwU+1jf2ktdwU iCd5g79MtGxiIy1NOtmeg9jA1q2uK8YUslu15A9gp0dwy1QnpTFpSBYuWj2ONRfn6n5aTBeD S5OyNnT7g//3URlJX/c3IP1WEKWxc55bsW7aGcbiUdfp4haTb2Z57tekW5ps0K1+EjPNONlk G5XmrM+rWQXiOYTtE8xwzWBV/oMSFJAM3WJ9VzA7sji/v4KIj/+Kf7qiBU4xZf7UPmDul0OB iq/IMx5W3YutoMndwudmHzrttO6Jp+JNYhV7lvM1E2Y6oodYJMpyqhU22w9ZTO77SVjk6lh1 VRvxc3o49LBcjkrpfPjREYfb229ZttPqG6xy/8Ew4DOmdjoR8sEeH1DXYO0H6vwQHRL6quhZ 0DWV2dl4naDReiGQlTZsRY66SqJS9fyaTmWPCVLl40zAknAYhUF0EZMG2xl+/xxXgGymJ67K Rk/u2BXvw+i7EMLk7MgNgGjAD2G+kHyMWZyE8LZdF0Pv0lU7kPRe6Ry98pVGCdVtt2kpQ2Jc CmAYhhQSHsOUQqCDkziOb+n4Z/B9fKZD6ywNamGZ7LGsuFYW/qSoPDnmoJ74zaBMNmONXh+H rU63ERER3VwB8XenX0GVSUWkyvHa8PTqg27/2V7qcW28fKjXwyKh8PHE7xJLdBm4Ay7m4+GP u+UwTh6cHNWj81dg3DPz7cb0RgZjCQvPzihHLIctDLcGaLdnqgEanxTIyh3NcZO8+c9xlwXY Z+d2o6zjOQhyKdrWgQgNxSpgMyiaM0ULnvoMVrGABzOL7GaPXjRxMqxZ6qgSLpWheESthuqu D/dHVWwW1bL3zTvSR2rNvlByS+BOxkL8pm8Ik43VkDsSdvnbluwN9o93lhUifUkw2jHM2IRK 202a0RWsriZ9j9VmN16Em1Fq2RmdKyKwnjIqebfLZkSvL1gBSE+xIc4qDwqjrBS6i9DXvl8n iDf+8Vvr1+Rme6K0jN7URBKp16jZaqOtERmfLvar9xOACiVuh0K6mqUBlIBoN43UrUHXohfz 9HOkOT4LzIQq7o8EuMTAsHVLISMN39zaHLU
Ironport-sdr: 6348a6e4_RcnEUr1I025zBS60h4aTjGB01L/XqJBGH99POxNQiUsA+Bv Ra2pUUVM4MT+od/8dweeSdITEn+SKc2VUGkHpxw==

Hi Eddy,

According to Frédéric Besson (the author of zify), "zify is about some
fragment of first-order logic" and thus it does not support
polymorphic or dependently-typed data types and functions.
https://github.com/coq/coq/pull/11906#issuecomment-630682539

Best,
Kazuhiko

2022年10月14日(金) 8:46 Eddy Westbrook <westbrook AT galois.com>:
>
> Mukesh and Pierre,
>
> It’s ironic that you would say that, because we actually go the other
> direction, and only translate to Coq when we can’t just solve something
> with SMT. Unfortunately, while SMT is good at proving properties of
> concrete sizes of bitvectors, it is not good at proving properties for all
> sizes of bitvector.
>
> Back to my original question: is it maybe the case that Add Zify is just a
> thin wrapper around adding some hints to a particular database? If so,
> could I add them in a way that generalizes over the width value?
>
> -Eddy
>
> On Oct 13, 2022, at 2:07 PM, Pierre Vial <pvial2401 AT gmail.com> wrote:
>
>
>
> Le jeu. 13 oct. 2022 à 22:46, mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
> a écrit :
>>
>> This is not an answer to your question, but have you seen SMTCoq [1, 2].
>> I haven’t used it in my projects but SMT solvers are good with length
>> indexed vectors so most of your problems can be solved (but I could be
>> wrong).
>>
>> [1] https://smtcoq.github.io/
>> [2] https://github.com/smtcoq/sniper
>>>
>>>
>>> I have a type function bitvector : nat -> Set that constructs the type of
>>> bitvectors (binary numbers) of a given bit width. Is it possible to get
>>> the zify tactic to support the class of types bitvector w for all w? The
>>> existing Add Zify commands seem to only work for a specific type.
>>>
>
> Mukesh is right, Sniper not only features SMTsolving, but also Trakt which
> allows you to quickly implement an equivalent of zify w.r.t any integer
> type you want.
> You will find examples on the sniper repository but also there (
> https://github.com/ecranceMERCE/trakt ) and I think Enzo Crance will be
> happy to answer any question you have on Zulip.
>
> --
> Pierre
>
>

[Coq-Club] Zify support for all instances of a type function, Eddy Westbrook, 10/13/2022
- Re: [Coq-Club] Zify support for all instances of a type function, mukesh tiwari, 10/13/2022
  - Re: [Coq-Club] Zify support for all instances of a type function, Pierre Vial, 10/13/2022
    - Re: [Coq-Club] Zify support for all instances of a type function, Eddy Westbrook, 10/14/2022
      - Re: [Coq-Club] Zify support for all instances of a type function, Kazuhiko Sakaguchi, 10/14/2022
      - Re: [Coq-Club] Zify support for all instances of a type function, Chantal Keller, 10/14/2022
- Re: [Coq-Club] Zify support for all instances of a type function, Samuel Gruetter, 10/14/2022