coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Experience with formalising projects with length indexed vector (Vector.t) and finite type (Fin.t)

From: "D. Ben Knoble" <ben.knoble AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Experience with formalising projects with length indexed vector (Vector.t) and finite type (Fin.t)
Date: Mon, 16 May 2022 11:08:04 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ben.knoble AT gmail.com; spf=Pass smtp.mailfrom=ben.knoble AT gmail.com; spf=None smtp.helo=postmaster AT mail-lj1-f178.google.com
Ironport-data: A9a23:sHwaKKPsabi9BCnvrR2akcFynXyQoLVcMsEvi/4bfWQNrUoq1GQEy WRKDGqCPf+MYmTyKo8kPI2zoUwOu5CDydMyGnM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8kk/vgqoPUUIYoAAgoLeNfYHpn2EsLd9IR2NYy24DkWl3V4 LsenuWGULOb824sWo4rw/nbwP9flKyaVOQw4zTSzdgS1LPvvyF94KA3fcldHFOkKmVgJdNWc s6YpF2PEsw1yD92Yj+tuu6TnkTn2dc+NyDW4pZdc/DKbhSvOkXe345jXMfwZ3u7hB2PkoF2l +h1uaecWAopEIHypMMQVAtxRnQW0a1uoNcrIFC6uM2XiknEKj7imqo+Sk4xOoIc96B8BmQmG f4wcmhcKEDewbjukPTiFbkEascLdKEHOKsVt3cmzjfeB/IraZ/GSqTOo9Rf2V/cg+gVQ6uFP pNENVKDajzBXxJQO1o2NqgkwsqlxULiS2xBinms8P9fD2/7lVQtitABKuH9cduTAM5Rg0ywv XPD522/AxcANdXZxyDtz563rurGnCe+XIBLUbPhqa4sj1qUyWgeThYRUDNXvMVVlGa4VoNYd HEs9hECvKUy2mCVcv7wWA+R9SvsUgEnZ/JcFOgz6Qeow6XS4hqECmVsctKnQIx23CPRbWx6v mJlj+8FFhQ07+LIESP1GqO86GLtaXJMfAfucAddFVNdi+QPtr3fmf4mczqOOKu8j9mwHTOph j7T83h4iLIUgsoGka68+DgrYg5ARLCZH2bZBS2NBgpJCz+Vgqb7POREDnCFsZ59wH6xFAXpg ZT9s5H2ABoyJZ+MjjeRZ+4GAauk4f2IWBWF3wM1QcJwq2/3pSD/FWy13N2YDBc5WirjUW+5C HI/RSsMjHOuFCD3MfEuONrZ5zoClPG4SI2Nug/ogipmO8AtLmdrDQlhYkmf222FraTfufBXB HtvSu71VSxyIf0/klKeHr5BuZd2mH1W7T6MHfjTkkX/uZLDNSX9YepUYDOmMLplhIva+1692 4gEZ6O3J+B3CrKWjt//qt5Nczjn7BETWfjLliCgXrTYclc6STh4VqC5LHFIU9UNopm5X9zgp hmVMnK0AnKl7ZEeAQnVOH1ldp31WpNz8SAyMSA2bASn3nEiZcCk66JGL8k7erwu9epCy/9oT qldK5/QXKgXEjmXqS4AaZTdrZB5cEv5iA+LOR2jamdtcpNlQTvP5dK5LBDk8zMDD3bsuMZn+ ++g2wrXTIAtXQNnCMqKOvujw0ng73cYkeN2GUDPJ4ALKknr9YFrLQ33j+M2c5lcc0WdmmPC2 l/PUxkCpOTLr4sky/XzhPiJ/9WzDu9zPktGBG2Ev7u7MC/t+GD8k4JNVeC/ey+ECDH59aCkU uViz//mNcoBklsX4ZF3FKxmzP5n6tbi++1awwBjECmZZlinEOk8cHyP3M0Ksq8Ug7EA5lvwV UWI9d1Xf76OPZq9QlIWIQMkaMWF1O0VymaOt6VreB2i6X8l5qeDXGVTIwKI1H5XIoxzPd532 uwmosMXt1Gyh0Z4KNqAlSwIpW2AImZaD/civ5AeRYvp008lkw4SJ5PbDSDy7deEbNAVahsmJ TqdhazjgbVAxxqdLyBiSyCVhecN144TvB1qzUMZIwjbkNTygPJqjgZa9i46T1gIwxhKuw6p1 rOH66GoyWSyEzZUaAxrWmmtH0RFBkTc9BWumx0Gk2rWS0TuXWvIRIH41SBh42hBm1+wvBACl F1b9IoheTnvdcD1mCA1XCaJbtT9GMdp+FSqdN+PRqy48lpTXdYhqqCrbGsM7RDgBKvdQaEBS fZCpI5NVEEwCcLcT2DXxWVXOXT8hS1o/FB/fMw=
Ironport-hdrordr: A9a23:s7coEqNHKlXdz8BcTvijsMiBIKoaSvp037BL7TEJdfUxSKalfq +V7ZEmPHPP+VQssTQb6LO90cq7IE80l6QFhbX5VI3KNGLbUSmTTL2KhrGSpAEIdReOkNK1Fp 0NT0G9MrDN5JRB4voSKTPXL+od
Ironport-phdr: A9a23:w8oJWxdjgPF1/eqCQZvS4vZUlGM+c9TLVj580XLHo4xHfqnrxZn+J kuXvawr0AWSG9iGoKIew8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PdbglShDewYbx+I RaooQ7MqsQYnIxuJ7orxBDUuHVIYeNWxW1pJVKXgRnx49q78YBg/SpNpf8v7tZMXqrmcas2S 7xYFykmPHsu5ML3rxnDTBCA6WUaX24LjxdHGQnF7BX9Xpfsriv3s/d21SeGMcHqS70/RDKv5 LppRhD1kicKLzE28G/VhcJwgqxVow+vqQJjzIPPfIGZKOBzcr/Bcd8GR2dMWNtaWSxbAoO7a osCF+QNM+hCo4LgulYBsx2+DhSpCuPpzT9HnXv20rM03+88FgzJxxIvH9QUvHTXqtX1M7wdU eSrw6TTwjXDaulZ2Tb56ITSbh8hpvSMUKt2fMHMxkYhCxnLgU+MqYz5ITyVzOINvnCF4+dkV eyiiGApphx+rDah2MshiIrEi5wJx13F8Sh3zpo5KN+6RUN5fdOpEIZduz+HO4Z4Tc4vQmFmt DgkxrACv5OwYSYEyJMixxHFavyHdZCF4h3iVOaNITd4mWlqdKijiBa19Eis0vb8VtWu31lWr SpFlcfMuW4X1xzd7siHTfV88l291jaI0gDf8uBEIUYularaMZEt2LAwloAVvE/eHSH2gF37g LGKekgg4OSl6OTqbq/4qpOANIJ4kBzyP6Ytl8G5HO82KBIBX3KB9uS5zLDj/VP2QLFNjvAul 6nWqpHaJcACqq69AQ9Zz58v6xiiAzqk09kUh3YHLFVCeBKIi4jmJUvCL+z/Dfe6m1iskTFry O7aPrD5HJnBMnzOnK3icLt98UJQ1hY/wNNF655JCLwMI+r/Wkrru9zZCh85PRa0w+HiCNhlz YwRR2SPDrWaMKPUtl+H/eYvLPeXaY8avTbyMfkl5/r0gXAlnl8deLGl3Z0MZ3+gBPRpP12ZY WbwgtcGCWoGoxIyTPb2h12aTT5Te3GyUrog6TE8EYKqFJvMRoSwgLOaxyq7BZ1XZmVeCl+WC 3vodoOEW+0NaC2IOMNhnCYEBvCdTNoq0gjrvwvnwZJmKPDV82sWr8HNzt9wsqf/01kY+Do8L MKa2WWABSkglG4OATww26p7rGRyz16C1e5zhPkORo8b3O9ATgpvbc2U9Od9Ed2nAmopH/+MQ VeiGJC9BC0pC8g2yJkIalp8HNOrilbC2TCrCvkbje/DH4Q6p4Tb2XW5PMNh0zDezqB0hVQgB MhJMmeii4Zw8gHSA8jClEDK372ye/Ek1TXWvHyG0XLIuUhZVABqVqCQV30ZIEjQqt7962vNS ravDfIsNQ4SgdWaJP5sbdvkxU5DWO+lONnaZDepnHysAB+T2r6WRI/jemFY2CeETUZdzFBV8 nGBOgwzQCympgoyFRRIElTiKwPp+Oh68jagS1MsihuNZAtn3qa0/RgcgbqdTekS1/QKonVpr TI8B1u709/MbrjI7wN8YKVRZ88861ZbxCrYsQJ6JJmpM6FlgBYXbQ12u0rk0xg/BJ9HlIAmq 3YjzQw6Lqz9shsJfT6em5P2PbfTJ0H9+Rmub+jd3VSfmNea96ET6egp/k35tVLhHU4j/nN7l thNhiHEt9OaUUxICcK3CxlnpH0Y7/nAbyIw5p3ZzyhpOKiw6HrZ3s4xQfEiwVCmdsteN6WNE EnzFdcbDo6gMr9P+RDhYxQaMeRV7KNxMdmhcq7M0qOteuVmmziigExI5Yl81gSH8C82GYuql 94VhuqV2AeKTWK2hlqn9MPxnopAaBkdG2O+zW7vA4sbNcgQNc4bTGypJcOw3NB3gZXgDmVZ+ FCUDFQDwMa1eBCWYjQRxCVo3F8M6TyikCq8lXlvli0x67CY12rIyvjjcxwOPihKQnNjhBHiO 9r8g9cfVUmuJw8n8XntrUz3we5YoqN1K2T7TkJBfiywJGZnGqe9rbuNZcdT5Yhg630GFrThJ wrCGvik/EtS2jirB2ZEwTEnazym3/ex1wd3jm6QNjc7rXbUf91x2QaK4dXdQfBL2T9VDCJ8i DTRGh29J4zzpYTSx8qF6LjuETv+Bs42E2Gj146LuSql6Hc/BBS+m6r2gdj7CU0g1iS90dB2V CLOpRK6Y4/x1q38P/g0GysgTFL69cd+HZlz14Uqg5RFk3IXgNOW+30NlWrbPtBS2Ka4Z30ID 21uoZad8E3+1UtvI2jcjYj0UDOexMxrY9SSbWYf2yZ75MdPQvTxjvQMjW5+pVy2qhjUaP52k 2IGyPcg33UdhvkApAsnyijOSqBXB0RTOjbg0giZ993r5rsCf36hKPLjsSg21cDkFryJpRtQH Wr0aot3VzEl9d1xaRrNyCGhsdyiIYiIK4hP6VvM1E2cx+lNdMBvyrxQ3nEhYDyl+yVikr9e7 1Qm3Inm7tbZbTw1puThREYfbGW9ZttPqG+zy/wCz4DGh8b3Wc85UjQTAMm3F7TxTHRL5K6hb 0HXQFhe4j+aAeaNQlPZsR076SqJS9fyaTmWPCVLlI0yAkDCewoPxlhTBmxyn4ZlRFn1n4q4I Rs/vnZJoQemz3kEguNwa0ulCjaZ9FruM21kDsDYdUUe7xketR2Mb4rDvqQqTnseptr4/USMM jDJPV0WSztSCwrfXRa7eeD/gLuIu/6RAu70RxfXSZOJr+EWF/KBxJb1l5Bj4y7JLMKEeH9rE /w83ENHG3F/AcXQ3TsVGWQRkGrWYsiXqQ3ZmGU/p92j8PntRAPk5JeeQ7pUP9J1/hmqgKCFf +eOjSd9IDxc29sC33jNgLQY2VcTjWlpeVzPWfwYsjXRSavLhqJNJxsSaic2MMkRqqxlgVkLN snchdf4kLV/i799CltIU0DghtD8ZcEOJDLYVhuPD0KKObKaYDzTlpuvMOXsFPsK1LUS7kLg6 lP5Wwf5Mz+OlifkTUWqOOBI1mSAOQBG/Zu6eVBrAHTiS9Tvblu6NsV2hHs42+5R5DuCOGgCP Dx7a04IoKeX6HYSiPh5XW9H6XBhIMGLni+Y66/TLZNc4p4JSmxk0vlX5ng30e4f9CZfWPl8g zfftPZrqlCi1+2Nk39pCUUe7DlMg42PsANpPqCTpfwiET7UuRkK62uXEREDodBoX8but65nw d/KjKvvKT1G/ro8HOMZDsnQbcaFaT8vaEW5XjHTCwQBQHigMmSN3yS1ddmd83SUqt4xrZ2+w PLmpZdUUVU0ErURDUE3RbQ/
Ironport-sdr: DveVzMcLgAQe7hqWeKwR+bUzCGg5kTlmuRcQlfrE5DDsL2ovPAyBb0Lo5OtVocgVwLmphIJ6lx JHD4NhKhCjgdW8QNH6K4JgBskyryLd6Q3yejsfO2QKyVdfIgptz2RJxZWiQMYKNzyd0Q3oxV2z lZ/B1qvQ9yAOzMDRjX+2zVuEcIqmOk9+0DzlehJk4+ELcgEjdkiAShXhSI5m+/Uo3qyuUzgKG1 +FvW/ge3HBvsLYBcj6W/AdndJfgPVp4Jq6FleY2ey7Iw1XlmR6N+ZvSgBqL5ZJjC6nFDbTvW3n 35iYsIZ/ZBf+lBGJEGYdImmw

I had a small attempt at using them for a class project (my partner
and I were barely a semester into Coq and related techniques). I'll
link the two commits, but we eventually switched to a less dependent
representation (the project was never finished, however). The
dependent representation also generated the type of SO questions you
might expect from folks new to dependently-typed vectors.

https://github.com/benknoble/zelda-mosaic-proof/commit/6b5cc1c784db24c4bd8510f55719b662407b3c4b
https://github.com/benknoble/zelda-mosaic-proof/commit/8ae89c9d2991261e380aa830d523c8724a1e37b1
https://stackoverflow.com/q/66863226/4400820
https://stackoverflow.com/q/67008122/4400820

D. Ben Knoble

On Sun, May 15, 2022 at 2:41 PM mukesh tiwari
<mukeshtiwari.iiitm AT gmail.com> wrote:
>
> Hi everyone,
>
> Have you formalised some non-trivial project using vectors, and
> finite type [1]? If yes, then what was your experience? What did you
> like and what did you not like about it? Also, could you point me
> towards your project?
>
> Best,
> Mukesh
>
> [1] https://coq.inria.fr/library/Coq.Vectors.VectorDef.html

[Coq-Club] Experience with formalising projects with length indexed vector (Vector.t) and finite type (Fin.t), mukesh tiwari, 05/15/2022
- Re: [Coq-Club] Experience with formalising projects with length indexed vector (Vector.t) and finite type (Fin.t), Dominique Larchey-Wendling, 05/16/2022
- Re: [Coq-Club] Experience with formalising projects with length indexed vector (Vector.t) and finite type (Fin.t), jtm, 05/16/2022
  - Re: [Coq-Club] Experience with formalising projects with length indexed vector (Vector.t) and finite type (Fin.t), Qinshi Wang, 05/17/2022
    - Re: [Coq-Club] Experience with formalising projects with length indexed vector (Vector.t) and finite type (Fin.t), Talia Ringer, 05/17/2022
  - Re: [Coq-Club] Experience with formalising projects with length indexed vector (Vector.t) and finite type (Fin.t), Dominique Larchey-Wendling, 05/17/2022
    - Re: [Coq-Club] Experience with formalising projects with length indexed vector (Vector.t) and finite type (Fin.t), Adam Chlipala, 05/17/2022
- Re: [Coq-Club] Experience with formalising projects with length indexed vector (Vector.t) and finite type (Fin.t), D. Ben Knoble, 05/16/2022
- <Possible follow-up(s)>
- Re: [Coq-Club] Experience with formalising projects with length indexed vector (Vector.t) and finite type (Fin.t), Weijer, W. de (Wessel), 05/17/2022