coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
- To: Rajeev Gore <rajeev.gore AT iinet.com.au>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Proof about permutation
- Date: Fri, 23 Dec 2022 17:00:51 +1100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf1-f52.google.com
- Ironport-data: A9a23:x7FYkKM8ye8jYJPvrR17k8FynXyQoLVcMsEvi/4bfWQNrUoggWRTy GBNXGqPO/uLa2PweIx+aIqw90kPvJLWndFqTnM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/jgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5CZaQHNNwJcaDpOsfvZ8kg35ZwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGXhWGLC29pjL3g/ONIRpuh2LEJIy v0xfWVlghCr34pawZq+Q+how8AtdYzlYdlZtXZnwjXUS/0hRPgvQY2QvY4ejGp2354RW6uED yYaQWIHgBDoZgBMN0wXFJMhlf2pwHj+ciFdgF2QrKszpWPUyWSd1ZCxa4aNJIzWGq25mG7Bu 2v55UvwBi1Fau6Y9GfU90u1gOjQyHaTtIU6TeXkrJaGmma7zWsKTRYSSFGTuui8kkf4WtRFK kVS9DBGkEQp3EmiT924WxPh5XDZ5FgTXN1fF+B84waIokbJ3+qHLk8vVxBZR9EFjcYzGjV22 F6kvNXWBBU65dV5Vkmh3ruTqDqzPw0cImkDeTIIQGM5Dz/L8NFbYvXnHoYLLUKlsjHmMWqvn G3S/UDSk51W3JFbjfzqlbzSq2v0/sChc+Ij2unAsouYAu5RYYekY8ms5wGe46saaomeSVaFs T4PnM32AAEy4XOlxHLlrAYlRurBCxO53Nv03wIH834JqWjFxpJbVdoMiAyS3W8wWir+RRfnY VXIpSRa74JJMX2hYMdfOtzuUptxlvi6To61CJg4i+aihLAhJGdrGwk+NSatM5zFzSDAbIlla MnFKZ3wZZrkIfU9lmLeqxghPU8Dn3hinws/tLj0yBOo1bf2WZJmYeZtDbd6VchgtPnsiFyNr b53bpLWoz0CDrCWSnSIqeY7cwpWRVBlXsueg5IMJoa+zv9OQj5J5wn5muN/JeSIXs19yo/1w 51KchQHlwam3SWbdV3ih7IKQOqHYKuTZEkTZUQEVWtEEVB5CWp2xPZEL8kEbvM8+fZ9zPV5a fAAdo/SSr5MUznLsXBVJ5X0sIUoJlzhiBOsLhiVRmE1X6dhYAjVpf7iXA/krxcVAgSN6MARn ryH1yHge6QleThMNsjtRciU/wuDhkRFwONWdGnUE+ZXY3TpodRLKTSur/oZIPMsCBTkxxmc3 Tm4GR0z+OvH+dc01PLrhqm0iZijPMUjP0hdHkjdta2XMwuD9EWd4IZwasS6VhGDa3HVoYKJe vdw48znFsE+jHJmktZZAql666AT/P7trOJq9RtlF3D1cFibMLNsDX2Y181ptKcW5LtmlSape 0CI6P9IEK6oPZ77LVsvOwYVVOSP+vUKkD307/5uAkHb5jdyzYWXQ3dpIBiApyxMHoRbaLp/7 78ah/cXzAijhj4BENWM1HlU/lvRCE0wafwss5VCDbL7jgYu9Ep5XqXdLS3IsbWvcNRHN3c4L gCE3JTig6tu/WucUn4RO0WU489jq8UghBR4wmUGBWy1ofvep/pu3BRu4TU9FQtU6RNc0tNMA GtgNmwrBKCC4wZXgNNnWkayETpgHzycwFT6kHESpV3aTm6pd23DF3I8MuCz53Ik83pQUzxY3 bOAwkPnbGrOUOTu+BAtAGhJhufGT9Nj0iHjwuWcANWjDZ02RRHHk52eTzMEhDW/CPxgmXCdg /dh+dhBTJHSNAkShvYeIJab37FBcyK0DjVObt859ZxYAFyGXi+53AWPDEWDesltAfju2m3gA uxMIvN/bTiP5BysnBs6W5FVe6RVmcQ37uUsYrnofG4Kk4WOpwpT7a7/yHLMu38Jcf5Pz+ANc pjcZhCTIFy23HF0oVLAnONAG2i/YOQHWjHC4fCIwL0JOa4u4OBIWmMu44SwpESQYVdG/QrLn QbtZJ327u1FyKZwrrToCYF8FwCREor2ctip7TLp4sp8N8PLFcLoqQkui0LGOj5ONuA7QOVHl rWqsf/20njavb0wbXvrppmZG4RN5uSwROByIOutCFV7xAysANTN5TkH8ECGca15qstXvJSbd lHpefmOes4wcPYD4n9sMgx1MQsXUobzZYfe/RKNleyGUEUh4FaWPeGc1CHbaE9AfXU1ILz4M Aj/vsiu6v1+rIhhABwlBelsM6RnIW3MCLcXSNnsiQa2VmWYoEuOmr/HpyoS7TvmDnqlEsGj7 6ycF1K6PF63tbrTxd5Uj51qs1dFRDxhiO03ZQQG98Qwlzm+C3UcIP8ANYkdTKtZiTH2yIqyc QSlgLHO0skhdW8sndTADNXfssO3A+UPPpL9KGVs8R7OLSixA4yEDf1q8SIID7KavNf85LnPF D3c0iSY0tuNLlVBSuMa5/j9iuBirh8f7mxd4ljzyqQeHD5HaYjnFxVd8M5lWinOEsWLn0LOT YTwqaaoX2njIXPM/Q1cl7K51f3XUP4DD9nlUMtX/Ovihg==
- Ironport-hdrordr: A9a23:ffbL9KDHWl6mYcrlHemT55DYdb4zR+YMi2TDGXoBMCC9E/bo7/ xG+c5w6faaskd1ZJhNo6HjBEDEewK+yXcX2+gs1NWZLW3bUQKTRekI0WKh+V3d8kbFh4lgPM lbAs5D4R7LYWSST/yW3OB1KbkdKRC8npyVuQ==
- Ironport-phdr: A9a23:+91KVBW9K518VxeEt0JdN/Y4oL3V8KxwXzF92vMcY1JmTK2v8tzYM VDF4r011RmVB9idtqsP2rOempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wE ZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmjqwbalyI RmrogncstQaipZ+J6gszRfEvnRHd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U 6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4 qt3VBPljjoMOiUn+2/LlMN/kKNboAqgpxNhxY7UfJqVP+d6cq/EYN8WWXZNUsNXWidcAI2zc pEPAvIOMuZWrYbzp1UAoxijCweyGu7g1iRFiWXq0aAgyektDR3K0Q4mEtkTsHrUttL1NKIKX OCw0anIzivMb+hW2Tzg9IjIcx4gruuWXbJxbMHczkwvFx7GjlqOsozlPy+V1uUDsmeB9epgV Piji28mqwFwvjivw9whiobMho0Py1DE8T91z5oyJd29UUN2Z8OvH5RMuS+ALYR2Xt8iTH9yu CY80rALt4O3cTQUxJg72RPRZeKKfYaG7x/9SOucIit0iXNrdry/gxu+7Eytx+PzW8e7zFpHo TZJn9bOu34CyRHe6MeKR/1g9UmiwTaCzx7f5v1ALEwulqfWK4QtzqMxm5cRq0jOHjH6lUPrh 6GMbEok4PKn6+H/b7XmuJCcM4h0hxn7Mqs0m8y/Bf00MgwAX2SG4Oi82r3u8VPjTLVFif02l abZsJTEKsgBuqG5BApV3p4i6xa5ETimzMwVkWcbIF9BYh6KjIjkN0vTLP35D/qzmVShnClzy /DDJLLhA5HNLnbZkLfmeLZw80tcyBcwzd9B/JJUCq0BIPP9W0DrrtzYDwU1Mw21w+bmFNV90 5gTWW2KAqCDMaPStUWE6f4oI+mJfIMVvi3yJOA/5/HylX85hUMdfa6x0JcKcHy4BOhpI12FY XrwhdcMCXsFvg0nTODzlFKCVSNTaG2pUqIn5jA7DZqmAp3ZSoCshryBxia7EYdMamBIEFDfW UvvIr+NWfoBdmq9JdVs2mgeXLqsRpFn2ha0uSf7yrxqMqzf/ShevI+1h/Zv4OiGkAwx+Cd0R 9iczGiXTikgm34LSiQ2wKFgqFZ8jFaC0LR9q/NdHN1XofhOV1FpZtbn0+VmBoWqCUr6ddCTR QPjG43+adlQZtc4wttVJl14B83nlRfbmSyjH74SkbWPQp0y6KPVmXbrdI5m03iT8q4nghE9R 9dXc3W8j/t66gveHI7VklqQjafsdKUdwCvl+2KKzG7It0ZdA0ZrSauQZXkEfQPNqMjhoEbLT rugE7MiZw5cysOZKrdLddTzjBNHRfb/PfzRZmuwnyG7AhPbjqiUYt/MfGMQlD7YFFBCkw0X+ iOeMhMiAy66v2/EJDlnFFaqZ021tOcj8jW0SUg7ywzMZEpkv1as0jgSg/HUC/Ya37Zf/Twkt y0xB1GlmdTfF9uHoQNlOqRae9I0plldhyrfsERmM5qsIroH5BZWehlrv07oyxR8C5lR2ckso nQwyQNuKKWemFpffjKc1Jr0N/XZMG73tByobqfX3BnZ3rP0su8K9fc1sFX/vR6gDEtk8nRmz 9x93H6V55GMBw0XENrwXksx6xlmtuTCeCBuguGcnXZoMKSyrnrDw4dzXLpjmkvmJokAdv7eR 2qQW4UACsOjKfIngQ2sZxMAZ6VJ8bIsetihb72A0bKqO+BpmHSni35G6cZzyBHplWI0R+jW0 pIC2/zd0BGAUmK2iUqiv9v3hYFbbCsTWGu+yDThLIFUb6x2O40MDC39Rq//jsU7nJPrV3NCo RSmGlALw8+1eAWbdV273AxRyUE/rnmumC/+xDtx2WJMzOLXzGnFxOLscwACM2hASTx5jFviF oOzisgTQEmiawVBeAKN3U/h3OAboa1+KzKWWkJUZ23tKHkkVKKst72EasoJ6ZUysCwRXv7uK VydT7f8pVMd3UaBVyNb2TM2bDG2u4rwhR08iWOcMHNbo3/QeMU2zhDarNDRXv9e2DMaSTIw0 2GGQAjheYD3opPJzd/KqYXcHyq5W4dWcDX3wI/Irya96WBwQFW+k/21htz7AF0/2C7/2cNtU HaApxL9b4/3kqWiZLg/Lw84WRmltZU8R9st9+l4zIsd0nUbmJiPqH8OkGOodM5exbq7d30VA zgC39/S5gHhnkxlNHOAgYzjBRD/ioNsYce3ZmQO12cz9cdPXe2R8b9Jhitpo0WxtwOXYPl8g jI1xv4n6XpciOYM8llIrG3VEvUJEE9UMDa53RGV7N2lrLlWe2+1cP6x1UtimPiuCbiDpkdXX 3OzKfJAVWdgq854NlzLynj67IrpLcLRYdwkvRqRix7cjuJRJcF5hr8QiCFgI264oWw9xrtxk 0l1xZ/j9tviSS0l7OejDxVfLDGwe84D5mSnk/NFhsjPl4G3Qsc6R3NSDcOuF673VmpV76ivN h7SQmNg7C3AQvyGQ1fZsAA//hetW9iqLy3FeidflI04AkHbfAsF2EgVRGlowMB/TFz7gpy5N h8+vGhZ50ak+EQWjLs0cUCuCCGH4174D1V8AJmHcEgJskcbvRqTaYrGqbstVyBAos/49FzLc zPEIVQOVSZTAwSFHwyxZ+b1o4CRr67AQLL5dqWrA/3GqPQCBa3QlNT/j80/pWbKboLWYTFjF 6FpgBMdGy0pXZ2IwXNXDHVG3yPVM5zB/Un6oHYm6JvltqysAVOKh8PHHbJWNZ8HFwmep6CFO qbQgS94LW0dzZYQ3TrTz6BZ2lcOiiZofj3rELIatCeLQriC0qlQRwUWbS9+Lq4qp+o1wxVNN MjHi9j0yq8wj/g7DE1AXEDgncfhbNIDImW0PlfKTEiRM7HOKTrOysDxKaSyLN8YxP1TrAG1s C2HHlXLOz2Ck3ztWUnqP7wWyi6cOxNatce2dRMsQWnvQdT6awGqZd96iTplpN98znjONGMaL X19axYX9uzWvX4e26sgXTEbvR8HZaGeli2U7vfVMMMTuPpvWWFvkv5CpW890/1T5T1FQ/p8n G3TqMRvqheoiLrqqHIvXRxQpzJMnI/Os19lPPCT84RDVG3E4BMS5H+RTRULpsdgItLqsqFUj NPIkeigTVUKu8KR5sYaC8XOfYifN2E9NBPyBDPOJA4MTDruMW+GwkIAyred8XqaqpV8oZ/p0 slrKPcTRBk+EfUUDV5gFdoJLcJsXz8qprWcidYB+Xu0qBS5rCpysZXOV/bUCvLqem/xZVxsa B4BwLe+JoMWZNWTM61Kb1B7mMHOFROVU40X5CJmaQAwrQNG930sFgUO
- Ironport-sdr: 63a54420_rlBaudg5Z7ose0y3dMPtkkcw6Qqt8KcTlonbjqd/nkrxzq+ O3hZtnKV9wUfZ/3OVlL9zQ6e3AkxD0yFJcjohXg==
On Fri, 23 Dec 2022 at 16:55, Rajeev Gore <rajeev.gore AT iinet.com.au> wrote:
Hi Mukesh,
> I don’t much about sequent calculus (even though I was a part of ANU
> logic group for a long time :)),
Shame on you :)
I deserve that :)
> but my use case is to deal with an equality (equal_finite_sets) in a sane
> (* multiset represented by list *)
> Definition finite_set {A : Type) := list A.
>
> (* two multisets are equal *)
> Definition equal_finite_set {A : Type) (xs ys : @finite_set A) : Prop :=
> forall x, In x xs <-> In x ys.
> etc
But there is already a multiset package in Coq, so why redefine it?
Because I am working on a existing project (not open sourced yet) and it has its own multiset library.
I am trying to wrap my head around the existing multiset package in Coq,
and in particular, how to use it to define sequents built from multisets
in a way that is comprehensible to a proof-theorist (not a Coq expert).
I believe Dominique is an expert, that I am aware of, about the proof theory and Coq so probably he will have more to say.
Best,
Mukesh
raj
- [Coq-Club] Proof about permutation, mukesh tiwari, 12/22/2022
- Re: [Coq-Club] Proof about permutation, Marko Doko, 12/22/2022
- Re: [Coq-Club] Proof about permutation, mukesh tiwari, 12/22/2022
- Re: [Coq-Club] Proof about permutation, Marko Doko, 12/22/2022
- Re: [Coq-Club] Proof about permutation, mukesh tiwari, 12/22/2022
- Re: [Coq-Club] Proof about permutation, Marko Doko, 12/22/2022
- Re: [Coq-Club] Proof about permutation, mukesh tiwari, 12/22/2022
- Re: [Coq-Club] Proof about permutation, Dominique Larchey-Wendling, 12/22/2022
- Re: [Coq-Club] Proof about permutation, mukesh tiwari, 12/23/2022
- RE: [Coq-Club] Proof about permutation, Jason Hu, 12/23/2022
- Re: [Coq-Club] Proof about permutation, mukesh tiwari, 12/23/2022
- Message not available
- Re: [Coq-Club] Proof about permutation, mukesh tiwari, 12/23/2022
- Message not available
- Re: [Coq-Club] Proof about permutation, mukesh tiwari, 12/23/2022
- Re: [Coq-Club] Proof about permutation, Dominique Larchey-Wendling, 12/23/2022
- Re: [Coq-Club] Proof about permutation, mukesh tiwari, 12/23/2022
- Message not available
- Re: [Coq-Club] Proof about permutation, mukesh tiwari, 12/23/2022
- RE: [Coq-Club] Proof about permutation, Jason Hu, 12/23/2022
- Re: [Coq-Club] Proof about permutation, mukesh tiwari, 12/23/2022
- Re: [Coq-Club] Proof about permutation, Marko Doko, 12/22/2022
Archive powered by MHonArc 2.6.19+.