Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Zify support for all instances of a type function
  • Date: Thu, 13 Oct 2022 21:45:37 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf1-f45.google.com
  • Ironport-data: A9a23:d/pBWqhsbaS/XfsjQBfuXjBTX161sxQKZh0ujC45NGQN5FlHY01je htvCDqHb6uDMzb3c9EiYImwo04AupHWyd4wTlE+/HtjF35jpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqicUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYpdDNJg06/gEk35q6r4GpD5gZWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVPKCSDXjCCd86HJW1bR8sozXBkbBKsJ3el9W2Nc3 s4aJQlYO3hvh8ruqF66Yuxlh8BmKMeyeY1D5zdvyjbWCftgSpfGK0nIzYUAjXFg24YXQ6mYO 5dxhTlHNHwsZzVKJ1QaE5IinfihnHi5cjxZtFe9qq8+4myVxwt0uFToGICEJITXHZ0I9qqej mft2338HQk9Dc2S2zqv7iOyqMOXuSyuDer+E5XhrqIw6LGJ/UQYDwRTXl+mq9Gim0umUpReL VYV82wgt8APGFeDS9D8W1i8rifBsEJBHdVXFOI+5UeGza+8Dxul6nYsYwNwV4F27OIPYy0N2 VXTncHCNz5iiejAIZ6CzYu8oTS3MCkTCGYNYy4YUAcIi+UPRqlj0Xojqf4zT8aIYs3J9SLYm G/V8XBv71kHpYtaiPXhpAGvbyeE/8CRFmYIChPrsnVJBz6Viaagbo2srFzVtLNOcNvfQV6Gs 3wJ3cOZ6Yji7K1hdgTSEI3h/5nzvJ5p1QEwZ3YxRPHNEBzzpxaekXh4um0WGauQGp9slcXVS EHSoxhNw5RYIWGna6R6C6roVZp3k/i9RY++CayEBjarXnSXXF/XlM2JTR7At10BbGBx+U3CE c3KLpz1UiZy5VpPkmboH4/xLoPHNghnnT+JLXwK5xug1rWaaRaopUQtYTOzghQCxPrc+m39q o4BX+PTkkk3eLCgP0H/rNFLRXhUdyRTLc6t8KR/KLXTSjeK7Ul7VJc9N5t6K9I790mU/8+Ul kyAtrhwkwan2yWadlzTMRiOqtrHBP5CkJ7yBgR0VX7A5pTpSd/HAH43JsBvL4o0vvdu1+B1R PQjcsCNSKYHADfe9jhXKdG3oIV+fV75zUiDLgi0UggZJpRAfg3u/sO7Xw3N8CJVMDG7m/Fjq JKd1yTaY6E5eSJcMOjsZsmC9WiB5UompLoqXm/jAMViR0H3wY07dw3zlqAWJu8PGzXixxyb9 QCcPjkAr8KQoYVvqNjtroKHprePDOFRMBd7HW7azLDuLgjc3DOp7rFhWdayXwL2dT3L6oT7Q s5K3dTQDeYhoG9al6ZdT5N60rMY5fb0gr1RkzRfA3TAamq0BoNaInWp2ddFsotPzOR7vTSad 12u+N5IH6egI+LgTUAsITQ6YtS51f07nifY6dI3Kh7Y4A515L+2blVADSKTiSByLKpHD619+ L0P4PUp0g2YjgYmFv2kjSoOrmSFESEmYpUd75ofBNfmtxovxlR8eqfjMy7R4q/eT/VXM0IvH C2Yu7qauZRY2Xj5UiQSEVrj4LNjoKog6T52yG0MHVCroub+p+QW2URR+AsnTw4OwRRg1flyC 1dRNEZ0BPuv+jt0tfdHRESpPR9LPzyC20nL01BSvnbof0qpcW3sLWMGJueG+n4CwV9cZjR2+ LK5yn7vdDTXIOXd+zQUYlE8jdDOVvlz+R/mtOH9Ov+aDr8oZTbBqY2/V1oi8hfIL5s4uxzam LNM4u11V5zeCQcRhK8eUKyxyrUaTUG/FlxoGP1O0vsAIjDBRWuUxzOLFkGWf/FNLdzs9WuTK ZRnBuBLZiSE+Be+lBIpLo9SHOYsh98s3sQIRZ3zL21fs7e/kCtggKiNygfA3l0UU/dcuudjD LOJbD+TMH2itV0NkU/3kcR0EG6ZY94FWQ7C4N6I4Ng5T5ItjMw8cGUZ8KeFgHGOAQ42ozOWp FziYoHV/cxDyKNtvZfdLaFYIzqkLPbIDeGu3D2ugY4fc+GVIcPqsiULoGLGJCVTB6MaAP5sp ISOsfn2/ULLh6k3WGbngKu8F7FFyMGxfehPOOflBSN+sQrbf+G0+DoF2WSzCaIRoeNn/sP9G jeJMpqhR+AaS/J25SNzaREHNz0/Fq6uTKPrhR3lnsS2EhJHjDD2doK2x0TIM1NeWDQDYaDlK wnOvP2r2NBUgaJMCDIABNBkG5VIG0Dia4R3a+zOsSSkMUfwjmOgorfCkT8S2QPPAFSAE+f45 svLeEGvPlD68qTF18pQvIFOrwUaRiQ1y/U5ekUGvcV6kXamBWoBNv4QKogCFooSqCHpyZXkf 3vYWQPO08kmsehsKn0QIegPXztzwsQLM9b9YzgnpgaaN3rwC4SHD79ssCxn5h+av9clIP6Pc bkjFr/YZ3BdAa2Fgc4c4/W6haFswfayKrcg5xXmi8Kra/oBKexi6ZGidTahkQTIFsjMkAPAI m1dqaWohq2kYRaZLPuMsEK51P3UUP0DAtnogeqyLA7jhrim
  • Ironport-hdrordr: A9a23:Ga6B+aPdX9GuKMBcTvijsMiBIKoaSvp037BL7TEJdfUxSKalfq +V7ZEmPHPP+VQssTQb6LO90cq7IE80l6QFhbX5VI3KNGLbUSmTTL2KhrGSpAEIdReOkNK1Fp 0NT0G9MrDN5JRB4voSKTPXL+od
  • Ironport-phdr: A9a23:OCIElRZ1psWwPg8Gz0rh+T3/LTFF2YqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gSPBtWDoKsZ0KL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNbQhEnjSwbLBuI Bm5sAnctscbipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3Q qBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4 qx2TxDmlToHNyUh8G7JlsNwkKxVoBWkpxNlwo7UZpyeOP5xc67ZeN8XQ3dKUMRMWCxbGo6zY IUPAOgBM+hWrIfzukUAogelCAa2GO/i0CVFimPq0aA41ekqDAHI3BYnH9ILqHnUqcj1NKQMX uCuzKnD0CnDb/JY2Djn8ojIcw0qrPaJXbJtcsre11IvFwPZjlWRp43qJSmV1uUXv2ia7upgV P6vi2s8pgF+pzig3MYsio3Tio0JzVDE8Dx0zYAoLtK3VEB1e8SrEIdMty6ELYt2RNsvT31mt Son1rELtpC2cSsXxJon2hLTdvyJfoeI7xztUOufLjR1iW5hdb6hmRu/8kiux/H8W8S03lhEr ipInNbDuH0Lyhfd5M+HSv5n8Ueg3zaCzw/T6uBYIUA0iKrUMIQtwr83lpYLvkTDHzP2mEXrj KCNbEkr5u+o6+Hhb777pZGcL5d5hh/iPqkqgMCyAuQ1PhITU2Wa++mwzrLu8E3/Tb5XlPM5i LPZv4rfJckDpq62HQtV0oE75ha6FTim0dAYkWADLFJLZR6LlobpNl7OLfziAve/hFOskDhvx //YJLHuHpLNLn3bnLfge7Zy9VJcxRItwdxD459YELIMLfLpVkPstdHVDAU1PgO0zur/DdVyz IIeWWaBAq+DN6PStEeF5ucyI+mPeoAVozb9K+Qk5//gl3A5g14dcbOo3ZsWaXC4AvFmLl6WY XrpmNgBEGMKshAiQ+ztjV2OSThTaG2qUKIm+j47EJ6mDZvERo21nbCNxD27EYFOZmBaFlCMF m/leJmDW/cVcS6dPsthkiEfWrW6UI8g1RSutBfgxLZ9L+rU/DcYtZP529Rv6e3Tj0J6yTshB MOElmqJUmtcn2USRjZw0rosj1Z6zwKGzKt1mPwQCd1M7ulIGlM/KJ3R1OxmCs/7QAOHf9aIV FOOTdCvADV3RdU0lYxdK31hEsmv20iQlxGhBKUYwuDabHRV2qfV3nyqYt14126Dz645yV8vX spIM2SiwK957QnaQYDTwA2Cj6j/U6Ma0WbW8Xubi3KUtRRdTQ19SqXZXG8WfEqQrNX4+kbqQ LqnCLBhOQxEmoaZMqUfUtTylh1dQev7ftHXYma/gWC1UBOVxb6XbJbrZGwH3WPcCUkYligc+ H+HMU41ASLy63nGAmlIElTiK1jp7fE4qH6/SRosyBqWakR6y7ev0hschPjZT/1Km7xY5WEur DJ7GFv71NXTYzaZjyxmeqgUIdY04VMckHncqxQ4JZu4aaZrml8ZdQ1z+ULozRR+TItaw4Asq zsxwQx+JLj9shsJfi6E3Z32JrzcK3XjtBGpZanM31jC0dGQsq4R4fU8ol/nsUmnDE0nu3lg1 tBU1TOb6PCoREIXTJH8SUYr9gdzvbCcYyg8+4b82nhlMK3yuTjHmpooCOYj1he8boJHKqrXc W26W8YeBsWoNKkrgw3zNkNCbL0UrfBreZ/7JJ7kkOaxMe1tnSyrlzFC6YF5iQeX8jZkD/XPx 9ADyu2Z2Q2OU3H9ik2gu4b5g9MhB3laE2yhxCzjHIMUaLd1eNNBDHqtLta32tRhjoTsHX9Z9 UKmL1wD0c6tPxGVahauuG8YnVRSunGhlSaimnZxjjIktaqD3TPH2eWkdRsGJmtjS2xrjFOqK o+xxYN/PgDgf00ikx2r4lz/zq5QqfFkLmXddkxPejD/M2BoVqbYWqOqW8dU89totCxWVL/5e lWGUvvmpANc1Sr/HmxYzTR9djewu5y/kQYowG6aKX9yqjLed6QSjV/a+d/RXv5N3yUPXig+i DjWGl2UMNyg/NHSnJDG+uyzTGOuUJRPfDKjl9vR8nvmozQ0Xlvjwri6gbiFWUAi3DX+1sV2W CmAtxv6boTxluy7Pe9hYkh0FQr54st+FJt5l9h4j5UR1H4Gw5SNqCBfwCGjbJMCh/24MCdeI FxDi8TY6wXkxkB5e3eAxoaiE26Y3tMkfN6iJGUfxiM66clOTqaS9r1N2yVv8T/a5UrcZ+Zwm jAFxL4g8nkf1qsMpQkg1SWBA68bB0gePC3tixGg4NW3raERb2GqO+vVtgI2jZW6AbeOrxsJE nPkeZo5HTNx8cxlMRTN0Xzv76nrfdDRaZQYsRjewHKix6BFbZk2kPQNny9uP2nw6GYkx+AMh htrxZimvYKDJjYl7OejDxVfLDGwe9IL92Snk/NFhsjPldPKfN0pCnARUZDvV/7tDD8CqaGtK VOVCDNl4naDReiEQEnGuR8g9S6QVcjsbS3fJWFFn4s+AkPGfwoG3lhSBHJjz/tbXkir3JCzL hk/v2hLoAa+8lwWkqppL0WtDDmZ/lv5LGdsDsDYdkIe7xketRiPd5XCqLsiRWcAucTxyW7FY m2DO1YXUSdQABHCXxa7eeDwrdjYr7rBXrr4dqSRJ+XI8asEDr+J3c79i9Q9uW/daoPXeCElV qNeuAILXGglSZ6BynNfFmpOzXKLN4nC+1+94nEl9Jnhtqm7Hlu+v83XTOIDedR3p0Ls2PnFb bXBwn0jb24fj8JppzeA3rEb2BR6ZzhGUT6rHPxAsCfMSPmVgapLF1sAbDs1MsJU7qU61w0LO MjBi9qz2KQqxvgyQ0xIU1DsgKTLLYQDPn29OVXbBU2KKKXOJDvFxNvyaL+9TrsYhftdthm5s zKWW0H5OTHLmz7sXhGpeeZC6UPTdARZo524ew1xBHLLSdvnbli/PoYyg2Frh7IzgXzOOCgXN j09O0JBo7uM7D9J1/VyH2sSixgtZeKAmiuf86zZMsNM6aotUnkyzrwFpihnmN43pGleSfd4m TXftItrqlCiyayUzyZ/FQFJsnBNjZ6KukNrPePY8INBUDDK5kFojy3YBhIUqt9iEtCqtbpXz 42Fkb/wJSxC79PL9NEdQcnVKd6CGHUkOBvtXjXTCUFWKFzjfXGanEFbnPyIozeNqYMmr5H3h JcUYrpSVVhwEv1DT0o5QZoNJ5B4Wj5imrmexp1thzL2vFzaQ8NUuYrCX/SZDKD0KTqXurJDY gMB3bLyKYl73mLT1Elra108l4PPSRO4tTFlpyRgakowrhwI/iQjCGI03E3hZ0Wm53pBTZZce zY5jwJ/ZaIm8zK+uz8K
  • Ironport-sdr: 634878fe_1WeMlLicex8JPOndqKZBorx9vfbujnxZL1870QkEwBfN5eX PJBdvcSpEwFnT877jlkQrsY7b1xx0YdacwKiKMg==

Hi Eddie,

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).

Best,
Mukesh 

[1] https://smtcoq.github.io/
[2] https://github.com/smtcoq/sniper

On Thu, 13 Oct 2022 at 20:29, Eddy Westbrook <westbrook AT galois.com> wrote:
Hello Coq club,

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.

Thanks,
-Eddy



Archive powered by MHonArc 2.6.19+.

Top of Page