coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Suneel Sarswat <suneel.sarswat AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?
- Date: Tue, 30 Jan 2024 19:23:57 +0530
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=suneel.sarswat AT gmail.com; spf=Pass smtp.mailfrom=suneel.sarswat AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f52.google.com
- Ironport-data: A9a23:ZNzv4KAKtFxDShVW/7Pnw5YqxClBgxIJ4kV8jS/XYbTApGkjhDVWm 2FLW2DUM6zfN2ejcox2PIu38x4FvZbWm4BqOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6j8lkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/YuHZTdJ5xYuajhIs/vZ+Us11BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc51GddGHF5NBJNVkVNq9J4NpQKkoXz NVNfVjhbjjb7w636LeyS+0pi8h6ace2ZsUQvXZvyTyfBvEjKXzBa/+StJkIgXFq3pAIQKy2i 8kxMVKDaDzbfhtCN1NRE5skh/ihmlHwdjRZrBSeoq9fD237k1wrium3boO9ltqiSJ1Ptx6Tm Xr90XnIRSwWF9CW5jG8/Sf57gPItXimAdpNRePQGuRRqFaU3ykYDAAcfUCqpOGwzE+4QdNWb UIOkhfCtoA3/U2vC9TxBli2/STCsRkbVN5dVeY97Wlh15Y4/S6FXW8eZxlkT+U+l8QUFCYW8 XSixurAUGkHXKKudVqR8bKdrDWXMCcTLHMfaSJscefjy4mzyG3UpkKQJuuPAJKIYsvJ9SYcK g1mQQA7jrQXyMMHjuC1oAqBjDWrqZzECAUy4207v15JDCsoOeZJhKTxtjA3CMqsyq7HEjFtW 1BawKCjABgmV83lqcB0aLxl8EuVz/iEKibAplVkAoMs8T+gk1b6ItgNvmkkehgybZpUEdMMX KM1kVMBjHO0FCv1BZKbn6roVKzGMIC5SYq8CKiKMrKinLAqK1HepUmCmnJ8L0i2zRF0zvBhU XtqWcmrCnkeBOxmyjHwL9rxIpd6rh3SMVj7HMihpzz+ieT2TCfMFd8tbgHSBshnt/jsiFuOr L5i2z6ikEk3vBvWOXSPreb+7DkicRAGOHwBg5UNLr7eclc4Rz9J5j246epJRrGJVp99zo/gl kxRkGcDoLYmrSSfc1vYWWMpc771Q5d0oFQyOCFmbx7i2GEubczrpO0Tfoc+N+tvvuFy7+9Gf 99cceW5A9NLVmvm/RYZZsLDt4BMTkmgqj+PGCuHWwIBWaBcaTbHwfLeRTu3xhIyVnK2keAcv 4yf0hjqRMtfZgZ6U+fTRvGd73Kwmnk/nuhNcVPCCYRRch+08axBCS/4vtkoKe4idDTBwTq70 V6NIBE6/OPina48wOPrt4ul8bi7MrJZNVVIOkXm9pCKDDn+0kv/5J5fQcCKUCv4VmipyJ69Z O5Q8e7wAMcHkHlOrYB4NbRhloA62PfCuJ5YyRZCDlzQTlH2FI5lHGaK7fNPuoJJ2LVdnwm8A WCL29tCPIS2KNHXK0EQKCUlf9a8+6ktwBeK1ssMIWL++CNT15iEWx8LPxCz1QpsHIEsO4Yhm eocqMoa7jKksSUTM/GEszt18lqdJXlRQoQlsZAnWLXQsDQJ8W0bQ5LgCX7R2qqtOvFsKUghJ wGGiJXS34p8wlXwSFttNHzv89cEu7EwlkFk8FswKW6NuOL5vd4s/RgI8T0IXgVflRpG9ORoO 1lUDU5+JITQ3jJkmPl8W3uIHidfDia44W308UMCz0fCfnmrV0vMDWwzAvmM90Yn6FBhfiBX0 bWb6WT9WxPoQZ3V8g4tf3V68trPYMdU9ALQvOyGReG+AIgccz7ppoSMdFg4gULrLu1pjXKWu NQw2vh7bJPKEBI5ooo5LtK//qsRQhXVH15ya6ht041RFF6NZQzo/yaFLn2wXcZ/J/bq10ucI O42L+JtUyWO7gq/ngo5N4UtfYAtxOUI4eAccIzFPWQF6ruTjgR4uaLqqxTRujUZfMVMo+0cd KXqaDOwIk6BjyB1mkjMjvV+FEiWXN0mXDD4jceJqLgnNpRbq+x9U1AA4p3ttVWvDQZX1Ra1v gTCWqzo89Jf2blcx4vCLogTBiGfC8/Ca+CTwQXi7/VMdYzuNOnNhSM0q37mHRhnAr8Kf+tJl pG26dvR4GLYjuxnTVKDi52lEo9X7/6TR8tSCNr8d1NBrBuBWejtwhoNwH+5Ipp3i+Fg5tGra g+7Scmof/sHco156FwMTAYGCDcbKaD8Tpm4lBOHt/7WVyQsi13WHu2o5VrCTD99dBZRH7bcF wWtmfKlxu4AnbR2HBVeWs1XWc5pEmTCB5kjWcb67wSDL2+ShViHhLvuuDwg5RzPCViGCMzK2 o3EdDevaCWNvLz08/8Bv7xQphE3CFNPsds0dG8Z+P90jGmeJ0wCJuI/L54HK891lgrf6ZLGX wzOPVASUXjFYTd5cBvCuYWpGk/VA+EVId72KwA4507eOW/8GIqEB6An7St6pWt/fjz41uy8N NUC4TvKMwOsxo1yD/MmjhBhbTyLGtuBrp7Jxaz8ryA2KxMXALFP2XA4WQQQD2rIFMbCkEiNL m8wLYyBrIdXVmapefuMuVYMcP3agN8r5zotZCaLht3Yvu13CcVenebnNbibPqIrNaw3yX1ne Z8zb2SI6mGSnHcUvMPFfj7vbbBcUZq2IyRxEEMvqcD+UU19BqTL8v7uRRYycfw=
- Ironport-hdrordr: A9a23:01bdUqPb/MotFMBcTvijsMiBIKoaSvp037BL7TEJdfUxSKalfq +V7ZEmPHPP+VQssTQb6LO90cq7IE80l6QFhbX5VI3KNGLbUSmTTL2KhrGSpAEIdReOkNK1Fp 0NT0G9MrDN5JRB4voSKTPXL+od
- Ironport-phdr: A9a23:nPmU2RxFHalIusDXCzJtwFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z hyZvq0zxwKXFazgqNt6yMPu8JrcEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PQbglSijexfbJ/I Bq2oAjQq8IbnZZsJqEtxxTGpXdFZ/5YyWR0K1yNgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7U LJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5 LplRRP0lCsKMSMy/WfKgcJyka1bugqsqBNxw4HWYI+bOvlwcL7Dc9wGXmdORNpdWjZbD4+gc 4cCDewMNvtYoYnnoFsOqAOzCxSxBOPp1DBHmHv21rAn3es7CwHGxwIhEMgSsH/Jq9j1L7oSU earw6bWyTXPdehW1i3n6IjTfBEuu+2MUKl/ccrU00YvFgfFgk+MpoziOjOYz+IAuHWU4OR8T +ygkXInqx1vrTi1wMchkobHi4IVx13Z+ih3wIY7KN2kREJnb9CpFIVduz+VOodqXM8uXm9lt iY0xLAGt5C2YDUGxpslyhPRdfCKbZaE7g7lWe2MLzl4g3dld6i+hxa06UWgxez8VtW00FZXt SVJiMXDtncI1xHV98OJSeN981+/1TqT0w3f8OJJLEAumabFN5IswaQ8m5oNvUnFAyT7hkH2j LKNdkU45Oeo8fnpYrTnp5CCL4J4lgfzObk0lMOlG+Q3KA0OUnCb+eui0L3j+lX0QLBQgf03l qnVqY7VKtkGqqKgDQ9Y0pgv5wywDzeh19QYkn0HI0xfdB2biIjpPknCIPH+Dfihn1ShiClny +zCM7H7AZjALmLPnKn9cbt+8UJRyBQ/wcha551OC7EBJPzzWlX2tNzdFhI5KBG0w+D5B9pj0 oMSQ3mPDbWDMKPJv16H/P4vLvKDZI8Qojn9Kvwl6+Tygn8+nF8RZa+p0oAPZ3CiAvtmO1mZY WbrgtoZDGsGphA+Q/DyiF2eTT5TYG6/UL475jEiEY6pEYPDRp22j7Gaxye6HphWZnhcBVyWE HfocZ+EW/YWZy6ILM9hiG9Mab/0QIg4kBqqqQWyn7FgN6/f/jASnZPlztl8oePJw0Ic7ztxW v+A1WyASylPl3kTWDYqlPRkvEpwx1PFyqFimONRCfRc4vpIVkExMpuKnL8yMMz7Rg+UJoTBc 12hWNjzWVnZL/o0yt4KOANmHsm6ywvEx2ysCqMUkLqCANo19Ljd1j7/PZU10G7IgY8miVRuW c5TLSu+nKcq7BXVCoPN1V6Qjb21fLg00yvE9WPFxm2L7wlDSAAlaazeRjgEY1fO69Hw50fMV birXK86NAZMzYiZI7FRddT1pVpDTfbnft/ZZjH5gH++UDCPwL7Ed4/2YyMd0SHaXVADiBwW9 G2aOBIWAy6gpyfTAGUrGw+1JUzr9uZ6pTWwSUpcIxiiSUpn2vL1/xcUgafZUPYPxvcfvz9nr TxoHVG71taQCtyapgMncr8OKdU6qExK027UrWkfdtSpMrxii1gCcg92o1Km1hN5DZ9FmNQrq 3VixRR7KKaR2ldMPz2C2pW4NrrSI2j0tBehDsyekkrD1tub/uEU4e4jtFz/lA6sH0smtX5g1 pgd0neR4InLEBtHSYj4ASNVv1Bxo7DXZDV45puBjyU9d/np9GWai5R0XrhAqF7oZdpUPaKaG RWnFsQbA5PrM+k2gx2yaQpCOulO9akyNsfgdv2c2aftMvwz+VDuxWlB/o151VqBsiRmTeudl Y0YxfyV2k2cXi3nk169ms/ykIFAIzoVGyDsrEqsTJ4UfaB0cYsRXC21Psu6y9E4nJf3QGFR6 HasAloH3Imifh/YPDmflUVAkE8Qp3Kggy6xyTd5xioooqSo1yvL2+3+dRADNwanXUFahEz3a cixhtEeBw2zahQx0QCi/QD8zrRao6J2Ky/SR11Jdm74NTMqXqy1v7uEK8lBjfFg+T5KVumxZ RaBQ6TmvBIG+yzmFmpagjs8cnmmt474kBpzlG+GZCwr/TyJJIcqnUeZuYaUTOU0vHJOXCRij DjLGlWwd8Kk+9mZjdaLs+yzUX6gSowGdCDqyY2asy7orWZuABC5g7Wygoi9SVl8gXK9jYE6E 3iS/3OeKsHx2q+3MPxqZBxtDV74sI9hH51m15A3nNcW0GQbgZOc+TwGl33yOJNVw/GbDjJFS DgVztrS+AWg1ldkKyfD3J//W3iZhNBofcKla38+1Sc07sQMA6CRpu8h/2M9sh+joATdbOIo1 CwAz/Yj7DgBivsSpwMx5iqYC7EWW0JfOGa/8nbAp8D7p6JRamG1dLG230crhtGtAoaJpQREU Wr4cJMvTmdgq99yO1XW3Djv+5npLZPOOMkLuETewHKix6BFbYg8nf0QiW97NHLh6Dc7nvUjg 0Um3Inm7tPabTw8pOTjXkEebnqvO4sS4m2/0/oYxJ3NmdnxRtM5XWxaOfmgBfOwTGBM67K+b 1zISHtk7S3DUbvHQV3BtgE88yOJQ8jtbzbNfDEY1YkwG0PbfRAZ2VFOGm19x85cdEjixdS9I hgloGlLuxig7EMLk7wgNgGjAD6H9EHxNWhyGN7Ha0APpgBauxWMbpfYt7MvWXkeptr48mnvY iSaf1gaVzlYHBzZQQm5bv/2ooCfu+mAWrjkdqWIPOXI8L0EEa/PnMPn05M6rWzVaIPVZSgkV Kd9gg0aDBUbU4zPkjELAUT7jgrraMiW7Fe58yxz9YWk9ejzHRno/c2JAqdTNtNm/1a3h72CP qiennQxLzEQzZ4KyXLSrdpXlFcPlyFjcSWsGrUcpGbMSqzXgKpeEx8cbWt6KsJJ66s22gQFN 9Tcj5v50btxj/h9DFkgNxSpgsayeckDOH2wLnvCDUePcbmKfHjFnpuxbqS7Rrldyu5Tslz4u DqWFVPiIiXWlzTtUEPKU6kEhyWaMRpC/YClJ0w1WC6zEZS8Mk39bYUk6F9+iac5jX7LK2MGZ D11ckcW66aV8TsdmfJnXWpI8ntiK+CA3Sef9ejRbJgM4p4JSmx5kfxX5HMixv5b9iZBEbZuh S3fo9oouFi8ifaG1hJoVRNPrnBAg4fB7iAAce3Js4JNX3rJ5kdH9WKLFxEDvMdoEPXqsqFUj 9XDzef9dW0E/NXT8s8RQcPTLYjUVRhpeQqsEznSAgwfSDetPmyKnE1RnsaZ8XiNp4Q7oJzh8 HLrYrBeXV0xUPgdDxY9dDTjCJJ+XzdhnLLCycBVvzyxqx7eQMgctZfCBKr66RrHJzOQjL0Cb BwNk+qQEA==
- Ironport-sdr: 65b8ff82_pTGlxcm1gQ+jiOKShBTT+qKY5Fuvac1hl+V3Sz+vDAvNNTH 6G74Wziu3Yv9MHVbQphLgRdi1Cxlw1efnugBeUw==
Dear Kazuhiko,
Thanks for the quick reply. I will look into it. I have defined and proved lemmas using Sorted and now need to connect these lemmas to a function that uses MergeSort library. So will prefer a solution of MergeSort if someone help.
Also, my work uses mostly standard library so I am avoiding it presently as mathcomp needs to be installed separately.
Thanks again for your help. Looking for a response from someone who knows how to do it using MergeSort library function.
Thanks,
Suneel
On Tue, 30 Jan 2024, 19:06 Kazuhiko Sakaguchi, <pi8027 AT gmail.com> wrote:
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
>
- [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Suneel Sarswat, 01/30/2024
- Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Kazuhiko Sakaguchi, 01/30/2024
- Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Suneel Sarswat, 01/30/2024
- Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Dominique Larchey-Wendling, 01/30/2024
- Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Xavier Leroy, 01/30/2024
- Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Dominique Larchey-Wendling, 01/30/2024
- Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Xavier Leroy, 01/30/2024
- Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Dominique Larchey-Wendling, 01/30/2024
- Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Suneel Sarswat, 01/30/2024
- Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Dominique Larchey-Wendling, 01/30/2024
- Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Xavier Leroy, 01/30/2024
- Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Kazuhiko Sakaguchi, 01/30/2024
Archive powered by MHonArc 2.6.19+.