coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Calvin Beck <hobbes AT seas.upenn.edu>
- To: Patricia Peratto <psperatto AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Rocq
- Date: Mon, 05 May 2025 10:44:44 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=hobbes AT seas.upenn.edu; spf=Pass smtp.mailfrom=hobbes AT seas.upenn.edu; spf=None smtp.helo=postmaster AT mail-qk1-f180.google.com
- Ironport-data: A9a23:kGbslKvSzYr8c81wl/4SlzY+VufnVPFaMUV32f8akzHdYApBsoF/q tZmKTuOa/mOY2Lze40gb423/RlQ6MTUm4RmSQY4qC81RHkWgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTrSCYEidfCc8IA85kxVvhuUltYBhhNm9Emult Mj7yyHlEAbNNwVcbCRNtspvlDs15K6v4G5A4wRnDRx2lAa2e0c9XMp3yZ6ZdCOQrrl8RoaSW +vFxbelyWLVlz9F5gSNz94X2mVTKlLjFVDmZkh+A8BOsTAezsAG6ZvXAdJHAathZ5plqPgqo DlFncTYpQ7EpcQgksxFO/VTO3kW0aGrZNYriJVw2CCe5xSuTpfi/xlhJGJrJYI9//QtOlAQx /s1NjEMaRa/i9vjldpXSsE07igiBMziPYdao3I5iD+AXa5gTpfETKHHo9Rf2V/chOgURaeYN 5dfM2A1Kk2QO3WjOX9PYH46tOevjHPyaBVDpVuO47cv7m7VigF9zdABNfKMI4HaG5kFwhjwS mTu9U3EDjQcbMel7Sfe7U3vgtHqggfGV9dHfFG/3qU32QXMlzJ75ActfVC8uLyyjlO0c8lOL lQdvCsot6k7skKxJuQRRDW9qX+A+wcfAp9eSr1irg6KzaXQ7kCSAW1soiN9hMIOl5IuShkvx AWyro3bAhFxsbyST06Rz+LBxd+tAhQ9IWgHbC4CaAIK5dj/vY0+5i4jqP4zT8ZZafWlSVnNL yC2kcQou1kEYSc2O0iT+FnGh3e1pcGMQFdlvkPYWWWq6g4/b4mgD2BJ1bQ5xaYfRGp6ZgDe1 JThpyR4xL5WZX1qvHLVKNjh5Jnzu5643MT02DaD5aUJ+TW34GKEdotN+jx4L0oBGp9bJWGyM BSP6VIPu8870J6WgUlfM93Z5yMCnfiIKDgZfqqFBjazSsEhLVbYpXs2DaJu9zu9zBZ1yMnTx qt3ge73UC9CVvU5pNZHb+ga1rAvy2g/w2iVLa0XPDz2uYdykEW9EO9fWHPXNr5RxPrd/G39r YwDX+PUkE43eLOlMkHqHXs7dwxiwY4TX82u85Q/my/qClYOJVzN/NeKmuJwJNQ/w/4J/goKl 1nkMnJlJJPErSWvAW23hrpLM9sDhL4m9Stnbx8/d02lwWYiaouJ5aISPcl/N7o++eApibY+Q /AZco/SSr5CWxbWyQQ7NJPdlY1FcAj0pASsOyH+XiMzUaQ9TCP0+/jlXDDVyg8wMgSNu/ED/ oKQjjHgfcJbRiBJLtrnV/a0/lbg4VkfgL1TWmXLEPlyeWLt0ppYFALjqvkJPPMzdAjnwwWZ2 z23GjYdn/HG+KUuwenKhIeFjoanKPR/FUxkBFvm7a66GC3Z32i7y6pSeb+sUQGGcVjr6YOeZ elx5NPtAs0txVplndJ1LOd28PgY+dDqmY5/8i1lO3f6N3KQFbJqJyi97/ll76Fi6OdQhlqrZ xip5NJfBLSuPfHlGn43IC4OTLyK9dMQqwnowcUFGmfIzw4pw+PfSmRXBQeGtwJFJrgsMI8F/ /YoiPRL1yOB0CgVIvS0pQEK0V+TL04wcbQt7bAbJ47JtjAF6H9/Zb7kNyunx63XNvttNBExL y62lZjyoe1W5nD/fkoZEVnP2utghqoyhi1a8W9aJ3m0novqu/xm+jxQ7jU9cSpNxDplze9YG zZmJm91F4q07hZqg8lIBV6sEBAcXRa2xFH7ygYNpk3kTm2DdG/EHEsiM8mjoWEb9GN9eGBA3 be6kWzKbxfjTPvT7AATB3F3juPFdsMr0B/vg+WlIpi1JIY7aj/bnaOeX2oEhB/5C8cXhkech +1V0MtvSK/8bwg8nrYaDtSE6LEuVxy0HmxObvV/9qcvH2uHWjWT2yCLGn+haPF2OP3G3k+pO fNAfvsVeUyF6x+PiTQHCYonAbx+xqcp7eVfXILbHzcNtr/Howd5tJ7VyDPFu1YqZNdTiuc4F JLacmOTM26XhEYMoVT3kut/BjOab+UHNSrG58Lk1MUSFpkGjvNgTlFq7JuwoEeuEVVG+zC6g Vr9QpH4ns1Y9JRUvorzE698KR2+BvHtWc+prg2ikdR8QuneEMXJtgkqhEHtFF1GNKk8R+Z1u Oiom4Px1hmUurwZbn3owcidNqhW5PedWPhcHdL3IUJ7wwqDep7IyDkS91+oLadmlItm2fCmY A+jeu6cRMUzWdxN4FF0Mg9wSw08DYbzZYfe/RKNleyGUEUh4FaWPeGZ+m/MRkAFUC0xYrnVK BL+4tSq7fBm9LV8PgcOXaxaMsUpMW3YePUUcvPqvmOlFUiuuFSJv4XimTcG6T3mDnqlEt7w0 anaRyrRJQiDh6XV8O5364BCnAUbLHJYs9kCekgw/91XiTfjKEUkKe8bE4sNC7AKsyjU+az7W grwbzoZOX2gZQhHTBTy3o2yFEPXTOkDIczwKTEV7luZIXX+Tp+JBLx6sDxs+TFqcz/k1/uqM swa5ma2BBWq35V1XqwG05RXWwu8Ki/ynRrkOHwRkvAexz4bCLQOkWViRU9DDHyfVc7Kk0rPK C4+QmUsrIRXj6LuOZ4IRpKXMEhxUPDTI/EAdiqG25DCo4idyqtNxOCX1yTbzOgYdMpTTFIRb SqfeoZOilx6HlQItKIy/c8xjKlyT/+HA6BW6UMlqRI6x8mN14jsAy/Ocefjgi3vFM6z3m4xT gWR3kU=
- Ironport-hdrordr: A9a23:MswrpqMVOPzk2MBcThGjsMiBIKoaSvp037Dk7TEUdfU1SL3mqy nKpp4mPHDP+UwssR0b6LK90ey7MBXhHP1OkPUs1NWZLXTbUbuTXfhfBOLZqlWKak7DH6xmpN 9dmsBFaOEYZmIK6voSjjPIdurIjOP3i5yAtKPxyzNCQ2hRBJ2ILD0UNu9YKCBLrcV9a6bR3a D82vZ6
- Ironport-phdr: A9a23:JBIpzxxDviQEHcbXCzI+wFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z xaZva0m1g+QBtuTwskHotSVmpijY1BI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDebRtEiCChbb9uI xm6swbcutQYjIZjN6081gbHrnxUdutZwm9lOUidkxHg6Mmu4ZVt6T5Qu/Uv985BVaX1YaE1R qFGATolLm44+tTluQHMQgWT6HQcVH4WkgdTDAje8B76RJbxvTDkued7xSKXINf5TbEwWTSl8 qdrVBrlgzoJOjIl7G3ajNF7gblFqxy9uRNw34/UYJmUNPVgeKPdYcgaTndFUspISiBNHp+wY 44JAuEcP+hXspP9qkMOoxWgGwSiGeHgyjhGhnD406M00OsuHh3d0Qw8A94DqmjYoMnvOasOV +2+0anGzS/Eb/NTwTrw9pLHchQ/ofGNW7J7bNfcxlczGAPGk16drozlPzSO2esWrWeb9PFtV fmxhGE9sAF9uCWvxt8yhYnPgIIZ0E7L+jhkwIssI9CzVUF0b8K+HpRKqyGaK5V5QtkkQ2xwt ys0xL0LtIC4cSQUzJkqxRHRZv+HfYSV/x/uW+mcLDR4inxqd7+ymRm//FauxODySMW500pGo CpZntTOuH0ByRre4dWJRPt6+0euwzeP1wbL5+FeJkA7ibPbJ4c5wr4qkZoTr1rMHjXslEXxl q+WeUMp8fWr5eT/erjquIOQOotuhgz9MqkigNKzDfomPgQUQmSW+viw2KX98UD4XLlGkvg7n 6bFvJ3VOcgWo6y0DBVR34o97huwEzmm3MgEkXQCI19FdgyLg5bsNl7UJP31DPOyjlGxnzhww /3LO7PsD5TTInTdlrrqYKhw60pByAoo0dBQ+YhUBKwAIPPyRED8rMDUAxkkOAKu2ennEs9y1 oYGVGKPHKCZNKTSvEeN5u01IumMYJYZuC/+K/Q4/vLug2I1lFwBcaWz0psXb3e4HvtiI0qHe 3bjntABEWISsgo/SuzllkGCXCZNa3quW68w/DI2BYK8AYvdWIyhnqaN0Dq4E5FKfmxGD0qDE Xbsd4WKQfcMbyeSL9dhkjwDTreuUJEu1Qq1uQ/h1bVoNPHU9jcFtZL7ytd14evTmQss+jNpE sSRy2eNQHpskWMSWzA2xLx/oVB6ylqbzKR0m+ZYGsBL5/NVTgc6MobRwPB9C9DrQw7OYtOJS Eu9Tdi9GjEwTtcxw8cUbEpnGtWiiArD3yuwDLMPmbyLHs98zqWJ53HtPcd2yn+O7KQ7hkU6R YMbLXa+i7R26xTUL4HMmkSd0a2tcPJP8jTK8TKoxG6QvUcQegN7Uu2RXXcVbEbNhc/071iEU qejD7JhPwdcn53RYpBWY8Hk2A0VDMzoP87TNifowz/Y7Xegw7qNaNGvYGABxGDGD1BClQkP/ HGAPAx4ByG7omuYAiY9XUn3bRbK9u9z4Gi+Uldy1xuDOk1m3bC44TYOiPWHDe4L07QC/iott mY8B06ziurfEMHIvA99ZONZaNI57k1A0DfZsAZ3M4eINK1rnRgDawlxuQXj2wgkQp5Yn50Mq 3UnhBF3Nbre0F5FcGaA2ovsP7TMNmTo1BWmaqqTw1KHldjPqv9J5/M/pFHu+gquEyLO6l1B1 N9YmzuZ75TOV08JVI7pF10w7158rq3bZS8048XV02dtOO+6qG2K3dVhH+Yjxhu6GrUXeKqZC A//FdEbDMmyOaQrnVaudBcNIOFV8uY9Icqnc/KM3KPjMvxnmXqqimFO4YY11UzplWI0SunC1 Zse6+qV1xDBSi/xilHnv8zq2MhFaTwUAmuj2H38HocCA886NY0PCGqoP4i23oAk38+rCyMer gT5QQpWgJzMG1LadVH20AxO2F5CpHWmnXD91Dloi3QyqbLZ2iXSwuPkfR5BO2hRRWAkg02/R Or8x90cQkWsaBAk0RW/4kOvjahcrq5yNEHITE5TOTXuImdkFKa8q/DRBqwHoINtqihRXOmmN BqaTbT3rgAyyC7qBC1D3D09cXentoizzHkYwCqNaX10qnTeY8R5wxzSscfdSfBm1T0DXCBki DPTCzBQJvGR9M6P39fGu+G6DCe6U4FLNDLs1cWGvTe64mtjBVu+meqyk5vpC1py3Sj+3thsH SLGyXS0Kons3a63Ksp8c0BzQkLk5sx8XIxyj8M8iYoR1n4TmpiOtSBfwCGjbJMBg/i4NSpVD TcQi8bY+g3kxFFuIhfrj8riW3ORz9EgL9i2b2UK2z4susVDCaOa9rtBzmN+plu1qx6UYOAox G9Mj6tzriRA2adQ6FJ+q0fVSqofFkRZIyH2whGB7tTl6b5SeH7qar+okkx3gdGmCriG5ABaQ nfwPJk4TkoSpo1yNkzB1Hrr58TqYt7VOJgTsReengzolOVcM9QsjvcMg2xqNX+37hhHg6Yry Adj2523pt3NK2Jn9q+iKgVVPyazetse/DergKpD1JXzvcjnDtBqHTMFW4HtRPSjHWcJtPjpA A2JFSU1tnaRHbeMVR/a8kptqGjDVoy6L3zCbmdM1s1sHVPOQS4XyBBRRjgxmYQ1Uxyn1NC0O lks/Sgfvxb5skcekLo5cUmiFD2F/kHxOm98DZGbKFA+AhhqwUDTPITe6+tyG3od5Zi9tEmWL XTdYQ1UDGYPU0jCBlb5P7Do68OSu+6fTvGzKffDe9Ds4aRXSuuIyJSz04Bn4yfEN8OBOWNnB uE63UwLVG5wGsDQkTECAyINkCeFY8merRa6sip5y6L3uOzsQx7q7JCTBqF6NNxu/1Wvgv7GO bfA3GB2LjFX0p5KznjNifAe0FMUlyByZmytHLAH5kuvBOrbnq5aCQJeajsmbpMZqfJhmFMXY 4iC2oums9wwxuQ4AFpES1H7z8SgZMhRZnq4KEuCH0GTcrKPOTzMxcjzJ6K6U7xZyutO5HjS8 X6WFVHuOjObmnznTReqZKtMiyuRMQd2o4y0aVBwEWXlSpTrZgDxY7oVxXUmhKY5gH/HLztWK T9nb0ZEtaGd9wtdi/R7XnVCtz9rdLnc3Sme6ObcJ9Adtv4hUUEW36pKpX89zbVS9iRNQvd4z TDTotBZqFajiuCTyzBjXXKmTx5QiYuQ+1h6NKPfsJRMRCSclPrsxWCZChBPvtg8T9O26/gWx d/Im6b+bjxF9oCMlSPzL9PZIdnBLWIsNxyvFTLJXlJtcA==
- Ironport-sdr: 6818cee0_AfpUFG1cWE2rMrjy1FpGCuR6NTQfja17j8nEr6SSE+TYFdz Bu6C452/B7KXLBFgUf22BvB+Ka8aqVYIYRLyDEA==
- Organization: University of Pennsylvania
> The proofs done in Coq can be used in Rocq ?
Typically yes, but there are a few changes. I believe there are
deprecated / renamed lemmas from the standard library, imports should
change because of the new Stdlib split, and Rocq itself has some
improvements that might make things like rewrites succeed when they
previously failed, command line tool names are also changing.
https://rocq-prover.org/doc/v9.0/refman/changes.html#porting-to-the-rocq-prover
https://rocq-prover.org/doc/v9.0/refman-stdlib/changes.html#changed
Generally the changes to proofs themselves are relatively minor. It's
not too different from a typical version bump in Coq. There's mostly
just a bit more renaming of imports and stuff this time around.
--
Calvin Beck
- [Coq-Club] Rocq, Patricia Peratto, 05/05/2025
- Re: [Coq-Club] Rocq, Calvin Beck, 05/05/2025
- Re: [Coq-Club] Rocq, Ralf Jung, 05/09/2025
- Re: [Coq-Club] Rocq, Ralf Jung, 05/09/2025
- Re: [Coq-Club] Rocq, Calvin Beck, 05/05/2025
Archive powered by MHonArc 2.6.19+.