Skip to Content.
Sympa Menu

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

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)


Chronological Thread 
    < Chronological >      < Thread >
  • From: "Weijer, W. de (Wessel)" <wessel.deweijer AT ru.nl>
  • To: "coq-club AT inria.fr" <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: Tue, 17 May 2022 11:46:10 +0000
  • Accept-language: en-US, nl-NL
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=softfail (sender ip is 131.174.52.101) smtp.rcpttodomain=inria.fr smtp.mailfrom=ru.nl; dmarc=fail (p=none sp=none pct=100) action=none header.from=ru.nl; dkim=none (message not signed); arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=Q3EXIqUu5OQPSpoCqTlyOiiaT1khgre36ni5q3rkQPc=; b=EcKJ3aVL10V7HwsXWDHhV48cCC1ZKW0A6v0yEfvQjTuGVtwJMhRRaaV0YuvX5k0seW6Kw9gEpAHuLoeJozZV/XNONrCqigqwjIVQNA7OXtuPhvz0ZP/zog44VMS05KTFdntnEgpKA6usUYlH77qC3oozLRkBsPLv2/0FBxtr3D1oNvQBVmGCxHYr3HBaHZ2vH04O+TrvBmumXzXASNrCa4P5mubmWR9Awhz+3GX2svrbRdTsQ1hFEHVcniyO5yGRy4um4nwhTAillVC2lzjsqzei1avLSq/3neI1A/5d7oRx+Div8neqnaG28SN7fFe4te7618+zLOG3qJcQydicpA==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=gsFyX8YB8qdroXVwgUzUHSg82ygpdZBaCAEMj7EPvOuzbTUDRaFGrBhm6mYbPUlJrrA+lmBSrYzaxIGzQ/n0wWoomLh7gLH7fd+NJgVEyEptISmtvT98dAu/NOErRCx0PkZ0uhkbsQ9w22WK8r0wZzMoH3K3Bf0aiQf5KevIocJCDBiCKb7rfnGz7hPSpF8ynkuu5VgjWmc9nNYMj/dnCdtZHUVhrtxaoyRERfMvvG+aVjbtSKc0BKT7N61GD9rROJSn112QOzrNSI+HV/33ep0/VRijo4v/PLOSroFMmd34IFfyAY8NEhYPlDV6ZUhFnrbXdpdbMA1WBdcrRSngcw==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=wessel.deweijer AT ru.nl; spf=Pass smtp.mailfrom=wessel.deweijer AT ru.nl; spf=None smtp.helo=postmaster AT mx08-005e0f01.pphosted.com
  • Ironport-data: A9a23:/5sXj69mg5ealLnB23yADrUDX3iTJUtcMsCJ2f8bNWPcYEJGY0x3m GtKDTyHbP3cMDTzct9zPt7k8khQusDRzYRiSldrr31EQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHvymYAL9EngZqTVMEU/Nsjo+3b9g6mJUqYLhWVnV5 Iqt+5S31GKNglaYDEpEs8pvlzs05JweiBtA1rDpTa0jUPf2zhH5PbpHTU2DByOQrrp8QoZWc 93+IISRpQs1yfuC5uSNyd4XemVSKlLb0JPnZnB+A8BOiTAazsA+PzpS2Pc0MS9qZzu1c99Z7 ed3t73vSzgTFe7rtNpGdglkAXBRBPgTkFPHCSDXXc27yl2eIz60m6hjVE9uZMsA4uZwGn1D+ boTLzVlghKr3rLrhuvrEa833oJ9fKEHP6tH0p1k5S7UFu0rRdbPTrrH5N1Vxh8qm4ZIGZ4yY uJCN2U2NEyfPnWjPH8cJ75uwdylvUP6WDkIiFWw+/dr5HPcmVkZPL/Fa4CJIIbSG625hH2wr WXfum/9HxsyL82a0TPD83S2h+aJkzmTZW4JPLiorq4v2AXOyzQdUERQTUO7puKlh0L4UNVaQ 6AJxsYwhY0Azk6KEdvCZTb7h1K65TsMZ8gBPNRvvWlh1ZHoywqeA2EFSBtIZ9onqNI6SFQWO rmhwIyB6dtH7+L9dJ6NyluHhWjtZnVNfAfucQdBHFRVuYCyyG0mpkuXFo4LLUKjsjHi9djNL 92iqThm1/BL1ZMGj6vjpBbfmzKrvYTEQkg+4QC/soOZAuFROtXNi2+AswKzARN8wGCxEgTpU J8sx5P20Qz2JcvR/BFhuc1UdF1T296LMSfHnXlkFIQ7+jKm9haLJN4Num4keRczbJteI1cFh XM/XysOu/e/21P1PcdKj36ZVqzGMIC6Soq5Bpg4kPIXOMMsJWdrAx2ClWbLhTy3yhBy+U3OE Y+BdsGiFXEbD7gjhDuwTKF17FPY7nBW+I8nfriil07P+ePGOha9EO5VWHPTMLxRxP7a8W39r oYOX+PXmk43eLCvMkH/r9VJRXhUdidTOHwDg5cKHgJ1ClE6Qz5J5j646e9JRrGJaIwPzbeVo iDkAxIHoLc97FWeQTi3hrlYQOuHdf5CQbgTZETA5H6khCouZ5iB9qAae8dldLUr7rEx1+MyS f1cI5eMBfFGSzLm/TUBbMim89E4Kkjz3Q/ebTC4ZDUffoJ7Q1Cb8NHTYQaypjIFCTC6tJVir uT4hB/bW5cKWy9rEN3SNKC011q0sHVEwLByUkLEL8N9YkLp9IQ2eSX9guVqcdsRbxPHn2PI2 wGTCBYehO/Mv45kq4aU3/7Y99+kSrIsEFBbEm/X6aeNGRPbpmfzk5VdVOuofCzGUD+m8quVe ugIner3N+cKnQgWvtMkQapr1683+/Dmu6ReklZ/BHzOYlmmVuFgL32B0ZUdv6FB3OUH6w6mA hLKooEHNO2HYJqjCEYRIxE5Y+jF3vYRw2GA4fMwKUT8xSl24LveCBUOZkDS1nMHIesnKp4hz McgpNUStF6yhx8sBdCM0XJZ+mGKGXofXvh1rZodGoLq1lEmxw0Qe5DaESOqspiDZ88WbBsvM mfEwfKa2rkEyBKbNWIrFX/WwedRw58JvUkSnlMFIl2InPvDh+M2hUQBrW1uEFoKlBgXgfhuP mVLNlFuIfrc8jptgv9FVT/+FgxEAiqf5UGsmUACk3fUThXzW2HARIHn1T1hIKzNH6NgkjlnE HWwzXa9AXOyJJz8hiVqAAh9s/zkVsB8+kvJn8XP8wFp2XUlSWKNv0NsTTNgR9jb7QcZnlCBo +0CECNYd/jgLSBJy0EkI9Dy6FnTISxo4ERYXLdn+Mvl2I0alC6agVCzFqx6Ri+ByzEmP6N15 wyC6/+jjyiD6Rs=
  • Ironport-hdrordr: A9a23:ShYwMK4cY11fIOJLTQPXwTSBI+orL9Y04lQ7vn2ZFiY6TiXIra +TdaoguSMc0AxhKU3I6urwSJVoIEmsgqKdhLN6XItKMzOWx1dAQLsSlbcKoAeQbREWlNQtq5 uIGpIWYLacbSkY/KKKh3jfYq8dLcG8gcWVbIzlvg1QpHRRGt1dBnBCe3um+yNNNXJ77K4CZd OhD4d81nqdUEVSSv7+KmgOXuDFqdGOvJX6YSQeDxpi0wWKhSPA0s+0L/DNtC1uMQ9n8PMHyy zoggb57qKsv7WQ0RnHzVLe6JxQhZ/I1sZDLNbksLlNFhzcziKTIKhxUbyLuz445Mu17kwxrd XKqxA8e+xu9nLqeH2vqxeF4Xin7N8X0Q679bakuwqmnSW5fkN+NyN5v/MaTvIN0TtmgDl+uJ g7k15x+aAnVi8o1x6NlOQgbCsa3XZckUBS2dL7x0YvI7f2V4Uh57D33HklXqvoTxiKqbzOLo FVfYzhDbBtABCnRkGch3JoxtO0WHQ1A1Opfmgu0/bliQR+rTRB1E0fy9UYnnAcsLQHa7cByd jlH81T5exzptl/V9MJOA4ue7rCNlDw
  • Ironport-phdr: A9a23:gGV1kRY+vig1MT/42DdKJPj/LTEN2oqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gSPANqQt6sMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5ZPebx9IiTe/br9/I wi6phjNu8cLhodvNrw/wQbTrHtSfORWy2JoJVaNkBv5+8y94p1t/TlOtvw478JPXrn0cKo+T bxDETQpKHs169HxtRnCVgSA+H0RWXgLnxVSAgjF6Bb6Xortsib/q+Fw1jWWMdHwQLspXzmp8 qVlRwLyiCofNzA37nzZitB+gqxYoRKuuxNwzpXOb42JLvdzZL/Rcc8HSWdHQ81fVzZBAoS5b 4YXAeYOPfhXr4j/p1QQtxuyHRSnC+P1xjRVm3D5w7Ax3+AhHg7YxwwgBMwBsHDRoNn7KawfV u60w7fTzTXYcfxW3S3x55XWfREvv/6MXLBwftTLyUQ0DQPFk0+cqYrhPz6M0OkGrmeU4fZ6W +21l24ntx9+oiKpxso0ioTHiJ8YxFDF+Ct33Is4JNO2RUB0b9OlEpZcqj+XOolqT80tQmxmt yc3xL0ItJOlYCUG1IoryRHBZvGbcoWE/xTuX/ufLzd/gXJqYrO/hxCq/Eivy+38Ssm00EtRo SZfjtbMsXUN2hrO4caEUvtw5lqt1DWP2gzJ9+1JIk45mbDVJpI92LI9l5kevVzeEiL5mEj6l rKaelgl9+Sy9ujqYLTrqoWBO4J3lw3yKrkil8KiDegiLwQDXWeW9f682bH950H1XalGguAun qXEvp3WON4XqrO7DgJayIou6wizAy273NgEg3UKKk9OdgidgIjzIV7OJej1DfehjFSolzdm3 /XGP7L9DpjON3TPjKvtcLZj5EJAxgo/0c1T64hMCrEZIPLzXVTxtMDGARAkKQC73+HnCNBl2 oMfX2KAHLOZPbvPvVKL5u8jOfSAaYwbtTrnJfUp++TigH46lFMFeKmmx5oXaHS2HvR8JEWZZ GLhg9kfHmcRpQoxUujqhEefXjFNaXe9QaM85jMlB4K8ForDXJ2tjKaH3Ce/BpFWYHtJBUiWE Xj0b4WER+sMaCWKL8N8ijAET6SuS5c91RGysw/306ZoLu3N+iEBqZ3j0MV16PbImBEp9T10C tyd3HuXQ2F1mGMIXT4207plrUxz0FfQmZR/1rZTEsUW7PdUWC87M4Tdxqp0EZq6DgnGZ5KCT EusatSgGzA4CNwrlYwgeUF4Tp+dgxHB0jDuS4BT37CGTNwL/7nH0nywbY4p1Hvdz6QlyVUrX cZON2C8rrRisQ7XUd2a236FnrqnIPxPlBXG832OmDLmVCBwVQdxVf+ARnUDfg7Mqt+/4EreT rioALBhMw1byMfEJLEZIsbxgwBgQ/HucM/bf3r3g325UAmF3aiBaMzmdnoQ3SfQEmAejkYV+ SXOLhAwUx+ouHmWFzlyDRTqakLo//N5rSakQ1QvwgXMY0B+2ru39wQ9n+HaTfdAlqkctnIHr DN5VE24w8qQC9eEoF95e75AZNom/Fpd/WfJ71w4ZsT9Ivhs3gdYaxx3uFjy2hkxAYJF+SQzh FUtygc6aaeR0VcbMiidwYi1ILrcbG/74BGobafSnFDYytefvKkVurw+rB34sQelG1BHkT0v2 sRJ03aa+pTBDRYDGZP3XEEt8hFmprbcKiAj7oLQ3HdoPOG6qDjHk94uAeIkzF6ncbI9eOubG RTpHslcC8WxJe0olkKBdA9COuQTvK84MsW6dueXjbaxNbUolzangGJbpYFlhxvcqmwlGrWOh M5DnaHLu2nPHy3xh1qgrM3tzIVNZDVIW3G61TChHolaIKt7YYcMD26qZcyx3NR3wZD3CBs6v BauAU0L3MixdF+cdVv4iEdP2F8MrHjhlSanwj12nisBtLfZ2iiEkIGAPFIXf3VGQmVvlwKmP oWvlN0eGkSlcAUolha/zVznga5f7vcaTSGbUQJDeC74KHtnW627u++ZYsJB35gvtD1eTOW2Z V3ypqfVmxIByGujGmJfwGp+bDS2otDjmBc8jmuBLXF1pX6feMdqxB6Z6saODfJW2zMHQmF/h 1y1ThCjMsKy8NHSm5rcv+G8WniJTIAVdy2jwY6btSS97HFnGlXmz631w428V1Nil3Grn9BxH T3FthP9fpXm28HYeap8c09kCUW9o8t2F4dik5ch0ZQZ2HwUnJKQrjIMlWb+N8ke2LqrNSpQA 2dbmJiOuE67iB4GTDrB3Y/yW3SDz9E0YtC7ZjlTwSch94VQD6zS6rVYnCxzq17+rATLYPE7k C1OrJlmoHMcnewNvxIgiyuHBbVHV1ZVJjfhk1KE4s+zradafk61bP620AAt+LLpRKHHuQxaV HvjL909EDRr48E5PF/T3Xzx55vMYsSWa9ZZ5Xj221/QyuNSLpw2jP8DgyFqbHn8sXMSwOk+l RVy3Ju+sdvPOyB38am+GBIdKiztapZZ5GT2lagH1JXzvcjnDtB7Fz4MRpetUf+4DGdYq6H8L wjXWDwk9iXCSeeZRFTFrh429DSWSsvjNmnLdiBJkJM7FELbfxQZ3lBeNNkjtrg+EA3ihMnoc UMjoysU+ka9sBxHjORhKxj4VG7b4gaucDY9DpaFflJQ6UlZ6kHZPNb7jKo7FjxE/pCnsA2GK 3CKLwVOA2YTX0WYBlfldrCw7NjE+uKcC6KwNfzLKbmJrOVfUb+Py/fNmsN++C2QM8yUInR4J /grghoGBSgkFpzXw2xJUzQXkDnRYsLdrxC5u2V2os257PX3SVfv6I+IWN4weZ1k/xG7h7vGN vbF3XYkb28IjdVXnTmWmOt6vhZakSxlejizHK5VsCfMSPiVgapLF1sBbCg1MsJU7qU61w0LO MjBi9qz2KQr65x9Q1pDS1HlndmkIMIQJGTofkzKH12GMPKKKCLGwsP6e4umVPtWiK8H0n/48 SbeCELlMjmZwnPxUAuzNOhXkCyBFBlO4NH4Kk4wBDDtFIugcgW7N8RrgDFwyroxzCCvVyZUI X13dEVDqaeV5CVTj6BkGmBP2XFiKPGNhyeT6+Swwnk+q+YtBCAmzoqyAVw/2+MFqXkcGfEtl nOL6MZ2o1a9juSDjDFgVUgWwt6urJiW+0Nma/2xyw==
  • Ironport-sdr: cLrNjTaTdU1CFXKMagcyMXrG5wU4Ylb+31fG6VlgnXoWS8mMV7FsYo54Lydr4Xskl/NU/b/JVV ooTffj1e2yGhAgL7xODpPdaTgIM16hv0Wj13IoJoCDbsaCcQbVhHgmHMSXNOe9wSr8ou/o04zi H+mFeBMpSEuuvYhQL4jYlj+sz1hT7WI9zFY7ZT7xcnGMHW6lWxWqVgKbnWJZCIHlCXh9wamLDE ef8os8Ykf7I4J5YLa2ivtFoWOvOYGAPIQrQFKfd1z8xqwb3M1Bq0SzsdX0KFbbSHbLkN4unoPz xRtk1/JO7SiCo/l7W5fLl4pa

These refinement type vectors that others have noted are implemented in math-comp in the file tuple.v [1] and they work quite well. They are defined as a record instead of a sigma and they can be easily constructed using canonical structures, for example
    Check [tuple of rev (map S (iota 0 3))] : 3.-tuple nat.

> I also suspect that the vec1 definition above would
> give a clumsy access to components when using Fin.t as
> indices, by converting Fin.t to nat and then using List.nth ...
> Also the proofs in between would certainly block computations
> with vec1.

Tuples in math-comp are normally indexed using what they call an ordinal [2]
    Inductive ordinal := Ordinal m (H : m < n).
It seems like Vector.t is to tuple what Fin.t is to ordinal but I'm not sure what the exact relation would be.

For good reasons (which I don't understand), math-comp is very Opaque and computations larger than the usual small-scale don't go through. Instead, CoqEAL [3] should be used for such computations. CoqEAL defines refinements between opaque, proof oriented, datastructures (like nat) and transparent, computationally oriented, datastructures (like the binary natural numbers N) and they create a lot of infrastructure to automatically move between them. Although they don't explicitely have refinements between Vector.t and tuples (or rather seqs/lists) yet, this should be very possible.

I am currently writing my MSc thesis for which I really should be using CoqEAL but since I don't feel comfortable enough with math-comp and with the infrastructure in CoqEAL I'm currently defining tuples and ordinals myself (but it's still to incomplete to show to the world :)

[1] https://github.com/math-comp/math-comp/blob/1f0daa44f834a040367f5fcb44451571fc9b646b/mathcomp/ssreflect/tuple.v
[2] https://github.com/math-comp/math-comp/blob/1f0daa44f834a040367f5fcb44451571fc9b646b/mathcomp/ssreflect/fintype.v#L1763
[3] https://github.com/coq-community/coqeal


Archive powered by MHonArc 2.6.19+.

Top of Page