coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: kirang <kirang AT comp.nus.edu.sg>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Interesting uses of Second order theorems in Coq proofs
- Date: Thu, 09 Jun 2022 05:14:08 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kirang AT comp.nus.edu.sg; spf=Pass smtp.mailfrom=kirang AT comp.nus.edu.sg; spf=None smtp.helo=postmaster AT mailgw0.comp.nus.edu.sg
- Ironport-data: A9a23:UJKVX6n/Jt9ziuY0ui9kEFno5gxXIERdPkR7XQ2eYbSJt1+Wr1Gzt xJJUWrXPKzZNmakeYh3O43g9EpU65DVz9VlTQZv/i0zFltH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvykTrSs1hlZHWeIcg944f5Ys7N/09cAbeSRWVvX4 4us+52HYzdJ5hYtWo4qw/LbwP9QlK+q0N8olgRWiSdj4TcyP1FMZH4uDfnZw0nQGuG4LcbmL wr394xVy0uCl/sb5nxJpZ6gGqECaua60QFjERO6UYD66vRJjnRaPqrWqJPwZG8P4whlkeydx /105cy8FQJ2MpHws8tGYxxjMjh6IfB/reqvzXiX6aR/zmXDenrozOo2SkoxOJVe/PtsR2xC6 LoDJ1jhbDja3L3wmenhDLkwwJ57RCXoFNt3VnVIzjDDBPApaZvERr2M48JDmjo8m4ZVEp4yY uJFMWM1NEuQPnWjPH85GrI1peSkg0LDTDR8hwilia86u2f6mVkZPL/FaouLJYPTHq25hH2wr WXfum/9HxsyL82a0TPD83S2h+aJkzmTZW4JPO3ks6QyxlaUw3RVDgANE1a3vL+ihSZSRu6zN WQtqnoi8a1t+HCXZfambxiDgWeAokMlDo84//IB1CmBza/d4gC8D2cCTyJcZNFOiCPQbWB1v rNut4+ybQGDoIF5WlrEre/F/FteLQBMdTRdO3RcJecQy4C7yLzfmC4jWf5YP8ZZZPXOGDf/y iiNtiVWa1471JRj6klW1QCbxmj04JPOSxZz4BjMGG+p80Via+ZJhrBEC3CGsJ6sz67AEDFtW UTofeDFvIji6rnWyESwrB0lRu3B2hp8GGS0baRTN5cg7S+x3HWoYJpd5jpzTG8wbJtYJmayO BKJ5FIPjHO2AJdMRfMnC25WI5h3pZUM6fy/PhwpRoQTP8MvHON51Hs0PSZ8IFwBYGB2wP9gZ s7AGSpdJXATFaVgyjOyD/ob0KEm3Ds/2XKbQp6z1BWh3rOGY2SYIYrpw3PSBt3VGJis+V2Pm /4GbpPi40wGAIXWP3mGmaZOfAtiBSVqWvje9ZcNHsbdeVUOJY3UI6KLqV/XU9Y7z/09eyah1 izVZ3K0P3Kk3CaYeFzUMCw/AF4tNL4mxU8G0eUXFQ7A8xAejUyHtc/zrrM7Iusq8vJN1/lxQ 6VXcsmMGK0SGD/A/ixba4Tm6oFuaVKwilvWbSaiZTE+eb9mRhDIqoO9IVO/pHFWA3rlr9Y6r p2hyhjfEMgKSAlVBcrLbO6ikgGqtn8HleMuB0bFe4EBeEjl/IVwBTb2i/s7f5MFJRnZn2bI3 AGTGVEeuPKLroMotsLG3PjWo4CsGup4P0xbA2iLse/pbXmKpjKumNYSXvyJcDbRUHLP1J+jP egFnevhNPAnnUpRt9suGrlm+qsy+t/zquII1Q9jBnjKMwymB748cHmL2c5D6v9EyrND41DkX 0uO/tZFYfOCP8b9VlgMP0woYvnFzv5Nwmve6vE8IUPb4i5r/erbCBoKb0nU0CENfqFoNI4Fw Ps6vJ9E4gOyvRMmL9Kag30G7G+LNHEBD/0qu81IGoPtkQZ3mFhObYaGU32mvNTVM5NHNUwyZ DmJn+zPi6ka3UWbKyg/En3E3Ox8g5USuUAWlQBadwTRwteV1OUq2BBx8CgsSlUHxxpK5Ot/J 2x3OhAnPq6J5Tpp2JBOUm3E99ut3/FFFpEdCmfllVE1i2GtX23JI3Jlf+2K+Vhf9X9HODVX4 feDxw4JlNoskN7ZhkMPtYxN8pQPjuCdMiXJn8W/WcKYBN83bSejmaDGia8gtU78Gc1o7KHYj bACwQuzAJEX8QYbpKgjTY+HzvIdRA3CP2MqrTSNOk8WNTm0RQxeEgRi56x8lg2h6hAKHYKF5 xRSG/9y
- Ironport-hdrordr: A9a23:Ob/1BaDZrZKT5HHlHemi55DYdb4zR+YMi2TDsHoBMCC9E/bo8f xG88576faZslYssRIb9+xoWpPwJE80nKQdieJ9UdiftWLdyQmVxe9ZnOjfKnHbakrDHr4079 YFT0GgMrfNMWQ=
- Ironport-phdr: A9a23:DGbGgxa7QFmgyCoDToiLGF3/LTEr2oqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gSPBN2LoK0Uw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PdbglSmTaxfbB/I Bq0oAjSq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ 7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4 qF2QxHqlSgHLSY0/27ZhMJwkqxVvRGvphNxzIHIb4+YL+Z+c6Hffd8GWWZMRNhdWipcCY28d YsPCO8BMP5br4n8vVsBtx2+BQaxD+7oyT9Ih2X20rc80+QuCgzJwAsgH9cWsHjOqtX1KbwSX fqrw6bV0DXPdehW2Tjk5YXObxsuru2CU6hqfsrN1UkgCRnFjlOIpIHmIz6b2esAvmqV4uZ8S +6ii2EppQ9srzWvx8ogl4fEip8ax17E6yh0xJg4KN2mREN4f9OpDZteuiWaOYZrRs4vRXxjt iUiyrAepJK2cioHxI46yxPRdfCLaYuF7x35WOqPPTt1gm9udqiliBao60egz/XxVsmq31ZOq SpIitzMuWoM1xzX5ciGROdx8l291jaI0gDT8vtIIUYplarAMZIu3KM/locJvUTYES/6gET2j KmIeUU44uWk9urqb7f8qpOBOYJ4lBvyP6chl8ClH+g0LhACX22B9uS90L3j81f5QLJPjvAuk anZsYraKt4dpq62GAJazoEj6xOnDzu81tQYgGIHIEhbdx2akojlIUrOIP/gAfe5mFujiC1ry OzePr39HpXNKWDOnKr5cbZn90Fc0BYzzcxY559MFr4BJ+vzVlbtu9zcEx82KBe5w/3nCdV4z oMRQ3iDAq6fMKPIsF+H/PgjI+eWZNxdhDGoIP88ovXqkHURmFkHfKDv04FERmq/G6FlIl+QZ 3Wk1tQAC24MsSI1S+nyzlufSnhea2v0RK1qtWJzM56vEYqWHtPlu7eGxiruRvW+B0hDA1GIS zLzcpmcHu0LY2SUK9NglToNUf6gTZUg3Fegrlyy0KJpe8zT/CBQrpf/zJ5t/eSGlhAo/Dp7J 8+a1nnLSXxv2G4EWnkt0/M3ulRzn2+KyrMwmPlEDZpW7vJNXB09MMvfzvZzDd/aUQXEZpGPV U3gT9m7Ryo+HZoq29FbRUF7Fp25iwzbmSqnB7hAj7uQGJk96b7RxVD0Lsd5xGmekqImikFgR NZUc2Cqm+hk+GA/HqbvlEOU3+avfKUYhmvW8XubiHCJtwdeWRJxVqPMWTYeYFHXpJL3/BGKS bjmErkhPgZbrKzKYqJXdt3ki0lHT/b/KZzfZWy2gWK5GRePwPuFcoPrf2wX2CiVBlIDlkgf+ nOPNA52ASnEwSqWDz10HFTgS0jr9PE4rm6gCEI40keRYAwp1ra4/AIUme3JU+kajddm8G8qr zR5Gkr43sqDUoHf4VM6JuMMPZVnuAQityqRrQF2M52+Iro3g1cfd14ypEbyz1BtDY4Gl8E2r XQsxQ40KKSC0VoHeSnLuPK4crDRNGT2+wiiLqDM3VSLmtWX4K4J59wzrFD7+ge0DQwv/2ghy NYfgB7+rt3aSREfV578SBN99BlgrrfVSiI64puS02B3d6S4r3nZ1Jh6YYltggbldNBZPqSeE Qb0GMBPHMmiJtshnF2xZw4FNuRfnEItF/uvbODOmKuiPeI62SmjkXwC+od2lESF6yt7TOfMm ZcD2fCRmAWdBX/wi1Kos8a/no4hB3laHWulwC7rLIVWY7U0e5sQT2qiPousyZ1yioXsVHhR6 FO4Twpdh4nwIkDUPwC7h1UY3F9fuXG9nCqk0zF49lNh5rGS2iDD2aWqdRYKPHJKWHg3iF7tJ YauiNVJFEOsbgUviF6k/ROjnPcd/f8laTmPBx0QLE2UZyl4X6C9t6SPeZtK4ZIs62BMVfikJ EqdQfj7qgcb1CXqGy1fwio6fnekoMac/VQyhWSDIXJ0tHecd9t3wEKV593GTPhe9jEBQTE+j yTMQFWwIp+y8p/H8vWL+vD7TG+nWpBJJGPozJmJsiST7mpvGVu5guv1l9H6VxM1m3yetZEiR WDDqxDyZZPu3qKxPLd8f0VmM1T77tJzBoB0loZjzIFVw3URgY+ZuGYWiWqme8sOwrrwNTBeI FxDi86Q+gXu31dva26E156sHGvI2dNvPpG/cisfkiMls5ITU/jStece23sp5APg9EWKO50f1 n8c0ad8sSVFxbhS4kx9kmPEWupVRhMQPDSwxU3TsJbn9/8RNT7pLeH3jxAb/5jpDane8FgHB zCgIc1kTXM2tJ04awiE0WWvuNi/J5+JNohV5kHSyU6H1LIwStp5n6ha2W8+YTu7tnog06g9k Aco0J2n+pOIY2w/rP78W0YCcDbyYttV/Cz2y6tSg4CN0OXNVt1oSC0MR4exC/mvFSpUs+n8c QuCDXsnpT+SS+qDWFXHrkxhqmqJFY2wcXybOT8CwrAADFGUdhwDxVpNGj49m4Z/EB2xgsHtb QFi6XgH71r84HOg08pOMB/yGifarQasMHIvTYSHaQBR5UdE7lvUNsqX6qRyGTtZ99uvtl7FL GvTfAlOAWwTPy7MT1n+Irmj48XB+OmEF6K/KfXJe7CHte1ZUb+B25uu1oJs+zvEON+IOzFuC Pgy20wLWn4ceYyRgzIUVykejD7AdeaerRa49TIv6Mu49eytXh/0o4aDFv1JPpQn+hy7h7uCK //FhCt9LmU9tNtEznvJxb4DmV8K3ng1KH/0Su5G5XKLFvqD/80fRwQWYC5yKsZSuqc13w0Xf NXelsuwzLlzyPg8F1ZCU1Xl3MCvf80DZW+nZzalTA6GMqqLITrTzoT5e6S5HPdTjf9dsRKYs jGeCwnlIy/FmjX0EQuge7Ip7mnTLFlFtYexfww4Q3DkV87jYwanPcVfiDQ3xbIr3jXBMmsEd z5haAVAoqDW9iwS0ZAdUyRRq3FiK+eDgSOQ6eLVf40XvfVcCSNxj+tG4X4+xtO9CQlPQ/lt3 i3PtZhjr0zgiebdklKPsTJLozdPi53T+05lPL2f8IRbH3vI4VQW4jfIY/zlj9BiD8Wpvb1Lj NXDieToJ2Ubm+8=
- Ironport-sdr: gvI35QiQbYIeecYZZKrBm0vLbV9rqv3MAFDh2AEzlkwa8zrKEIJ6joNt0k6RO0cUAPS5q69qTk osii0Cf4eecj+PR/+MdJTkCltJg+mK5je7LuJrWoHgsrAZDwSiwVpnSIFnPhj3m+7V2NEe8AiS L7BwrU43HmXBlRJOYrIxRVLvN8pEuj8rZrx8PyZWaCjhyTLFbgmUVQDKFUaQJFikxUBZODVIz6 JvWR2IXRfOfMc76x4np4ZqGNlEN0Tmv56ZXvJuVm8Vdoe9IAUcSdQctBPK0FBUIvF0ALWHddj4 0PIm+o/0cwJ+whmrjgLKuI23
Hi Coq Club,
For various reasons, I'm currently doing a light survey of examples of interesting uses of second order properties/lemmas in Coq proof scripts.
Currently, the main examples I've found in the wild have mostly been using various induction principles for custom datatypes and the such (found through searching Github/using Coq's search mechanism).
I've seemingly exhausted searching through Github for now and so I thought I might reach out to the magnanimous wisdom and experience of the Coq club community in this search.
Do you have any interesting examples of other classes of second order properties (i.e other than induction principles) you have seen/used in your own proofs?
Thanks,
Kiran.
- [Coq-Club] Interesting uses of Second order theorems in Coq proofs, kirang, 06/09/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, Qinshi Wang, 06/09/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, kirang, 06/10/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, roux cody, 06/09/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, Lawrence Dunn, 06/09/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, Castéran Pierre, 06/09/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, kirang, 06/10/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, Ralf Jung, 06/11/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, Qinshi Wang, 06/11/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, Ralf Jung, 06/11/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, kirang, 06/10/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, Castéran Pierre, 06/09/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, Lawrence Dunn, 06/09/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, kirang, 06/10/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, Steve Zdancewic, 06/10/2022
- Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs, Qinshi Wang, 06/09/2022
Archive powered by MHonArc 2.6.19+.