Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?


Chronological Thread 
  • From: Kazuhiko Sakaguchi <pi8027 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?
  • Date: Tue, 30 Jan 2024 14:35:35 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pi8027 AT gmail.com; spf=Pass smtp.mailfrom=pi8027 AT gmail.com; spf=None smtp.helo=postmaster AT mail-lj1-f171.google.com
  • Ironport-data: A9a23:BBECdqIwdYGE9FwPFE+RGZAlxSXFcZb7ZxGr2PjKsXjdYENSg2YDy GcdCG/XPP/fNGfxKtEjaY+zp0gPu8KAmIUyT1Yd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6j+fSLlbFILasEjhrQgN5QzsWhxtmmuoo6qZlmtHR7zml4 LsemOWBfgf4s9JIGjhMsf7b8Uk+5K6aVA4w5zTSW9gb5DcyqFFOVPrzFYnpR1PkT49dGPKNR uqr5NlVKUuEl/uFIorNfofTKiXmcJaKVeS9oiY+t5yZv/R3jndaPpDXmxYrQRw/Zz2hx7idw TjW3HC6YV9B0qbkwIzxX/TEes3X0GIvFLLveBCCXcKvI0LuTEPN0a1vJ0gMY9cW6+1XWFlfr 9w5J2VYBvyDr7reLLOTT+BtgoEnLpCuMtpA4zdvyjbWCftgSpfGK0nIzYUAjXFg24YURaaYP pVAAdZsREyojxlnIlZHUMhhtOitj3j7NTZfrTp5oIJuvzmInV0sgeWF3Nz9fPW3FOx/nxuhu 3/G8lnUAgAFCu29xm/Qmp6rrqqV9c/hY6oZE6T9/fp3inWI12kLAVsXU0G6qL+3kCaDt8l3L kUV/m8qr/F3+hX0F5/yWBq3pHPCtRkZMzZNL9AHBMi24vK8y26k6qIsFFatsfR/7JRuFw85n ESEhc3oDjFJubiYAyDVvLSNoD/4fWBfIWYebGVWBUEI8vvykrEV1xjvd9dEFLLqr9vXHTqr/ SuGghJjjJoujOkK9Z6Bw3b5vxyWqKPkcCsJ9yTMf2f87gpGdI+vPIOpzl7A7Md/FoWST3jfn X1dm8Gh8/wEIpadsBO8UMMfMaybvaebAmfMhXpqOYcrzBW22nuZZYsLyipPFERoFccleDHSf 07Yvz1K1qJTJHeHaaxWYZq7LtYDlYzMNI3CeKjPT9xsZpNRSle2zBt2bxTN41G3wVker64vH Ly6L+CuNC8+IoZ6xmOUQ+w97+ca9homzzmOeaGhngWV6pvAVnu7UrxfDUCvaNo+56a6oAn41 dZTGs+J6hdHWt3FfSjl3t8PHG8OMEQEK8j6m+5Pes6HBzhWKmUrJvvS4LEmIqhOvaBekMXW9 XCcBG5c7nfChkP8FAbbUUA7NYvTXqt+o0krYg0qH1KjgEY4baiVsawwSpoQfJscztJF88Jad fc+Vv+7Mqx9cQifozU5RrvhnbNmbyWu1F6vPTL6QT0RfKxAZg3u+/3idDTB7CMlUyi975M/h 5aC1QrrZ4UJaCo/LcTRadOpl0iQu1pEks1MfkL4GPthU2Syz5pLcgvake0SD/wXDyn61h+29 lqzEAgJg+vguKo3+4T5vr+FpIKXDOdOJEpWMG3F57KQNyOB3G6c7aJfceSPbxbPfXjV/fi8W OBr0P3MCv0Ls1JUuY5aEbww76Yf5cPqloBK3DZfA3THQFS6OIxOekDc85F0iZRM4btFtS+de EGFoIBaMIrUHvLVKgcaIQ59Y9mT0f0RpCLp0s00B0fH/w5ywquMVBRDHhuLiREFFoBPDqEe/ b4DtvIVuiuFsTh7FvadjytRyXaAEWxYbYUjqaMhIdHKjigF9wh8RKLyWwHK5KOBUdFuCnURA yS1gfPCjotMx0CZfHsUE2PM7NVnhp8PmU5ryVMeFmuNgf7AoOE95zxK0DENVg8O5A524+FyH WlKNkNOOqSF+QlztvVDR2yBHwJgBgWT307Ml38lsXL/dFbxcEDgN0g/NvSp0GFD1llDbx5J+ L2840T0YwbAJc3e8HM7Zh94lqbFU9d0yDznpOmmOMagRLwRfjvvh/6VV1oi8hfIL5s4uxzam LNM4u11VKzcMBwQqY0dD62x9+wZaDKAFVx4bcBRxoE7NkCCR2jqwhmLEV67Re1VLf+T8UOYN d1nFvgSazuAjhSxvhIpLo9SBYRrncwZxssIIZLqAm8kj4GxjBRUtLDoyyyvo1NzHvtPl58xJ LqEInjGWiaViGBPkmDAkNhcNyDqKZMYbQn7x6au/P9PC5sHt/p2fFov1qev+U+YKxZj4wneq Tari3U6FAC+4d8Ec0rQ/qR/68GcLNryUKGM8ln2vY0RNJXANsDBsw5ToV7iV+iT0X39RPwv/ YlhcvautK8GgFrye2/ckpiFUaJO4K1emcJJZ9nvIiAycTSqAafRDthqx4x8AZNMmdJZoMKgQ mNUrSd2mcE9A79g+ZGeV8SS/9vxxUg6gmcMaB5Rd8ixNyU=
  • Ironport-hdrordr: A9a23:u65EdKlsJWdgpZ4mem4Qvr7/Lf7pDfIT3DAbv31ZSRFFG/Fw8P re5MjztCWE8Qr5PUtLpTnuAtjkfZqxz+8W3WBVB8bAYOCEggqVxeNZnO/fKlTbckWUygce78 ddmsNFebrN5DZB/KDHCcqDf+rIAuPrzEllv4jjJr5WIz1XVw==
  • Ironport-phdr: A9a23:ahgfkRcDQxPaj/4idxif8lsBlGM+udTLVj580XLHo4xHfqnrxZn+J kuXvawr0AWZG96DtbkZ0aL/iOPJZy8p2dW7jDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgH c5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTajYr5+N hu7oRnQu8UZgYZuNLs6xwfUrHdPZ+lZymRkKE6JkRr7+sm+4oNo/T5Ku/Im+c5AUKH6cLo9Q LdFEjkoMH076dPyuxXbQgSB+nUTUmMNkhpVGAfF9w31Xo3wsiThqOVw3jSRMNDsQrA1XTSi6 LprSAPthSwaOTM17H3bh8pth69dvRmvpQFww5TMbY6aOvpxfKPTc90ZS2RcQMheSyNPD5igb 4sWFecNIfpUo5X/qlYIsBCwBROsBOTqyjJQg3H5x6w70/khEQHH3wwgGM8FvmnOo9X2LqgSX v21w7XIzTXCcvhb3i/96InLfxw9v/2BX6l9ccXUyUY1FgPFik+cppDiPzOQz+kAtXWQ4OV8W +y1kWEntx1xrSa1xscqkoTFmJ4Zx1LE+Chn3oo4ONO1RU54bNCkHpZcqi6UO5Z2TM8+XW1lu To2xLMEtJO5cyUHx4grywLfZvGHfIaF5hHuWeCMKjl2g3Jlfaiwhxe08UW4xe38V9W00FZXr iVeiNXDqncN1xnV58OaSfV95l+s1SiT2w3X8O1JIkA5mbDFJ5I9wbM8jIcfvEbeEiLwhU77k quWdlg/+ui09evneKjopp6dNoBqkgzyLqIjkdGlD+siKAgBRW2b9Py81LL9+U35R61Hjvgsn anYtJDWPMAbpqykDwNM3IYv9hSyAyq83NQXmnkHK11FeBaZgITzJ17OJ/X4Ae++g1Sqjjhr2 +jLMqP9DpjJNHTOk7fscaxj50JAywc/181T6pBJBr0ZJfL8QE7xtNjWDh8jNAy0xv7qCM181 o4dRW6DHK2UPbjdsV+N/O0vIu2MaJUJtzb6Lvgp//jugmQhll8HYaapxYcXaGy/Hvl+PkmVe WDsjcsZEWcWogo+S/Tnh0GFUT5Kfnq9Q6Y85iwgB4+9FofCRoWtgKSb0yuhH51WYHpGClGWH nvyeYWEQaREVCXHKch41zcASLKJSok71BjouhWp5aBgK7/38z8FtZPg05BO7u7amgw59T08W 9ycgznXEEl7m2oJQ3k926Up8h818UuKzaUt268QLtdU/f4cCm/SVLbZxu1+UZXpXx7ZO82OQ xCgS8mnBjc4SpQwxcUPagBzAYbqlQjNigytBbJdjLmXHNos6KuJx3mhf5wi43nD3aglyVIhR 5gHLnWo05Z27BObHIvViwOcnqeue74b2XvV9TfblzWms0RRUQo2WqLADjgEfkWDi9P/6wvZS qO2T7QqNgwU0cmZNq5DccHkl31DTfbnfdDcOie/wjjpQxmPwbyIYczhfGB1MDz1Lk8CnkhT+ H+HMVJ7HSK9uyfECzcoE1vzYkTq+O04qXWhT0ZywRvYJ0tmn6G4/BIYn5n+A7saw64EtSE9q j51AEf13tTYDMCFrhZge6MUaM004VNO32bU/wJnOZnoI6dnj18YOwN52iGmnw12Wt0azuAlq XoryEx5LqfZmFJNejWE3Izhb6XNIzq69xSuZqjKn1DGhYzOq+FftbJi8wWl5V7wRS9Auz193 tJY0mWR/MDPBQsWC9fqV1ovsgJ9rPfcazU84IXd0TttN7O1u3nMwYFMZqNtxxC+ctNYKK7BG hX1FphQH8n+cLZ1s1esZxMAeutV8eRnWqHuP+vDw6OtMOt6yXi+jDQfut9V3UeF9i46QenNl cVN07ST2Q2JUC35hVGqv5XsmIxKUjoVG3K21SnuAIM5irRaRY8QEi/uJsS2wo87nJvxQztC8 1XlAVoa2civcB7Ublrn3AQW215F6XCgnCK5yXRznVRL5uKH3XyWmbvKex8OO2oNT25nxVvhO om7idkGUVPgNVB40kv4oxyil+4C+/03JnKbWUpSeinqM2xuN8n4/qGPZcJC8tJgsClaVvi9f UHPT7f8pxUA1CawV2BaxT09a3SrosCjx0082D/bdi4j6iOGIJIVp1+X/tHXSP9P0yBTQSB5j WOSHV2gJ5yz+t7SkZ7fs+e4XmbnV5tJcCCtw5nT0UnzrWBsHxC7mOi+39P9Fg1vmzf6h4EwC g3HqR/9Zs/g0KHwYocFNgF4QUTx7cZ3ANQ0iopg3MtP8Xcfj5SRu3EAlC2gecUe0qX4Yn0XQ DcNyNOA+wnp1npoKXeRzp74XHGQka4DL5GqJ3kb0SUn44VWGb+ZufZayDBtrAPy/krBJOJwl TAHxb4y5W4G1qsX7RE1wHz4YPhaHFEEb3ex0U3Zt5bk8PoRPCH1LfCxzBYsw4znVurZ5FgCA DChPc5zVS5ospchbhSViCe1sse8P4OICLBb/hyMz0We0a4PdMN3xqJM3W09YSr8pSF3lLR91 EAohMDg+tDAcjUl/brlUEEEcGSvOoVLvGmq1Pg7/I7e3pjzTMw5SnNSA8SuHbTwV2hL/fX/a 1TXT2Z68ybHX+KZRUjGtg9nty6dScj6cSHKYiBDnZM6A0DCQS4XyAEMAGdgx8B/S1DsnZ27N h8+v2FZ50ak+EEVlKQybEi5CT2Z/EDxO38iQZybZnK69ylk4EHYeYyb5+N3RWRD+4G56RaKI SqdbhhJCmcAXgqFAUriN/+g/4uI9e/QHee4I/bUBNfG4eVDS/eFw46u2Yp67n6NMMuIJHxrE /w83AJKQ3l4H83TnzhHRTYQkmrBaMuSpRH0/SMSzIj36PPwRAfm/peCEZNXONRrvhS02OKNb rHJwil+Ljlc29UHwnqJgLkT0VgOij1/IjmgFbNT0EyFBKnUm6JRE1sac3YpbJoOv/96hFEdf 5eE04CQtPYwlPM+BlZbWEa0n8ioYZZPOGShLBbdA03NMr2aJDrNysWxYKWmSLQWgv8H0n/48 TudDULnOSyO0jfzUBX6e/lN3HnBYzRRvYi8dlBmDm2pH7eEIlWrdcR6izE72+h+nnTRKWsVK iRxaWtIp7yUqCda27BxQjMYqHViKuaAlmCS6OySefN0+bN7Ry9zkexd+nEzzbBYuTpFSPJCk yzXttdyoluin4FnLxJoVRNPrnBAg4fZ5S2K2I3c/5hEHHLGpVcDtDrJTRsNoNRhB5vkvKUCk rAne4r8LT5D95Tf+s5OXqDp
  • Ironport-sdr: 65b8fb3d_XafTWnUpTrAjzjIKKwHL4LXv78pJN8xnSteY3IYhiD1r/7t np0WaaEUrjoMAlSiObj93EmyJx7ahOziNTf8ftw==

Hi Suneel,

If you don't mind using the Mathematical Components library (which
provides other definitions of sortedness and mergesort), these are the
lemmas you are looking for:
https://github.com/math-comp/math-comp/blob/8b28eb944e9140d4749870ab2d86f83d6635ab04/mathcomp/ssreflect/path.v#L942
https://github.com/math-comp/math-comp/blob/8b28eb944e9140d4749870ab2d86f83d6635ab04/mathcomp/ssreflect/path.v#L1019

Best,
Kazuhiko

2024年1月30日(火) 14:09 Suneel Sarswat <suneel.sarswat AT gmail.com>:
>
> Dear Members,
>
> I have list L of unique records type.
> I have defined ordertype "dec" on these records. I am using MergeSort
> module from standard library. Now I need to prove a basic result on this
> list. Any help would be appreciated.
>
> Lemma sort_sorted L:
> Sorted dec L -> L = sort dec L.
>
> Thanks,
> Suneel
>



Archive powered by MHonArc 2.6.19+.

Top of Page