Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proof about permutation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof about permutation


Chronological Thread 
  • From: "D. Ben Knoble" <ben.knoble AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Proof about permutation
  • Date: Thu, 22 Dec 2022 18:34:35 -0500
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ben.knoble AT gmail.com; spf=Pass smtp.mailfrom=ben.knoble AT gmail.com; spf=None smtp.helo=postmaster AT mail-ej1-f48.google.com
  • Ironport-data: A9a23:waJSoqB4upVkrhVW///nw5YqxClBgxIJ4kV8jS/XYbTApD4mhDZUz jQXXT+PbPnfZDD2L95zYdzj9xwEucPXmNFgOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6jMlkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/ouOZjdJ5xYuajhOsvjZ8ksy1BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc53H5SCLW3/JyN2g3IqQ18/pvM25S3 ONNfVjhbjjb7w636LeyS+0pi8Z6ace3bMUQvXZvyTyfBvEjKXzBa/+StJkIgXFq35AIQaa2i 8kxMVKDaDzKbhsJOVEQApYztOitj3j7NTZfrTp5oIJruDOCnVcpjdABNvKNVOS0fOVugn+ev 3vXxDzlRSkEC+eQnG/tHnWE37eTx0sXQrk6H7qhs/VunVe73X0WEBRQVF2hoPD/hFTWZj5EA 0kd+y5roKprsUL3Hp/yWBq3pHPCtRkZMzZNLwEkwD2y8fPu/wGFPUEFURdsYcA+hsAqbCN/g zdlgOjVLTBotbSUT1eU+bGVsS6+NEApwYkqNX9soewts4mLnW0jsv7cZo08T/Pt37UZDRm1k m/a9nFv71kGpZdTj/3TwLzRv967SnH0ouMd4wzWWieo7Fo8atL1IYOv7lff4LBLK4Pxori9U JosypH2AAMmV8nleMmxrAMlQuzBCxGtbmO0vLKXN8N9nwlBAlb6FWyq3BlwJV1yLuEPciLzb UnYtGt5vcEMZSTxNv8tONjhVazGKJQM8/y1Bpg4ifIeMvBMmPOvoUmCmGbKjj6zyBNw+U3BE cbBK57E4Ykm5VRPlWLqHY/xIJckwScxwW67eHwI50XP7FZqX1bMEe1tGALWMIgRtfrYyC2Ir Ys3H5bVk313DreiCgGJqtV7BQ5RfRAG6WXe8ZM/mhireVo4RgnMypb5ndscRmCSt/4JyL+Uo SHiAh8wJZiWrSSvFDhmo0tLMNvHNauTZ1piVcD1FQfzgyoQcsy04b0BdpA6W7Ai+aYxhbR3V vQJMYHISPhGVj2NqXxXYIjfvb5SUk2hpTuPGC65Pxk5XZprHDLS9vHeIwDAySgpDwiMj/UYn YGO7A3gbKQmexVDF+fTMfKm8EOwtyMSmcV0REr5HeNQc0TNrqlvciz4seArEf4LOTH892O9/ FuQC01Jo+PinpIEqojVpKGbrrWGF/l1MVpaElL6s5e3F3j+1UiyzbBQVN2neWjma1r136G5d 8B5/urZMsBbrG1VsoF5Laln/Zg+6/TrubVe6AZuR1fPUHiGFZJiJSOg8fRUl6gQ2IJchxS6a niP9vZeJ7+NHsHvS3wVBQg9a9W8xeMmoSbT4ds1MXfFyndOppTfanprPj6IlCB5B5l2Otl8w e4e5egn2zbmgR8uatu7niRY8lqXFUM5UoIliMA+IJTqgQ8V2F19ccTiKivp0qquNfRIEGcXe wGxuoSTqYhY9ET4d1gLKUPsxstY3JQHhwBLxgQNJnOPgdv0ucU01xxwrxUyQhhk8RFc9+dVJ GJQFlZUIJ+W9GxCn/lzXGGLGiBACiaG+0f39UA7qW3BQ2SsVU3PNGcYO9vR2Gw87ERnYWF90 JyD7WTqQxLGXZvU5TQjf1xhp9jIb81DxieblO+JR826ToQHOxz7iaqQVE80ghrAA+ZqoWbYp ONvrd1CWYeiOQE++6QEWpSnj5IOQxW5JUtHc/Fr3IUNOUr+IDiS+zy/G3qdS/N3Bc7h0BGHU pR1B8d1SR6B+j6ErWkbCY4yMrZEpqMVy+RYSIz7B1wtkuW5nmJyvYPy5xrOojYhY+9TnPYXL qLTcDO/EVKsu0ZEpl+VrOR5PjuXXNpVQiz9w+G/z8sRHb0hruxHUB8/w5m0jVqvISpl+BOm5 lrDbpDJ0t04mJhNnpTtIIpHFQ6bOdP+b8XW0QGR4vBlT8LDDtfKjCwR8mLYBgVxOaAAfeh4j pGfmYfT8H6dmY0pQkf1voKkFZhZwemTB81patnWKltelgu8AP7c2QMJoT2EGMYYgeFj6dmCb CrmTdm7avo+ecpXnV9RYAhgSyctMbz9NPrclHnsvsa3K0Yv1CLcJ4ma7l7vV2ZQcxEIN7DYC gPZv/WP5MhSnL9TBS0rVu1XPJtlHGDNAacWVcX9lT29PFmahlmvvrjDlx155w+SWzPAWIz/7 IneTxfzSAWqteuahJtFuoh1pVsMAGw7neA0eVkH9sVrjyyhSlQLNvkZLY5MH6Q8fvYeD30kT GqlgKoe5STBsfBsdBz95JHuXF7aCLBefNj+ITMt8gWfbCLe6EZsxld+3n8I3pu0UmKLICKbx RU29Xj5Pxz3yZZsLQrWzuLumv9pn5s22VpRkX0QUKXO79I2DrAD1XgnFw1IPcAC/wchi22TT VUIqat4rI1XhKI//QuMu5KYJf3BgA7S8g==
  • Ironport-hdrordr: A9a23:0T05dKA2b0kfc9nlHemV55DYdb4zR+YMi2TDtnoBMCC9F/bzqy nApoV/6faZskdyZJhko6HiBEDiexLhHPxOkO0s1N6ZNWGMhILrFuFfBODZslrd8kPFh4hgPG RbH5SWyuecMbG3t6nHCcCDfeod/A==
  • Ironport-phdr: A9a23:GcWEXxRaN2bHZou1PfBzT9B/ddpsouKVAWYlg6HPa5pwe6iut67vI FbYra00ygOTAMOGsrkd0qL/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T 4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglWhDexe7N/I Ai5oQnMq8UdnJdvJLs2xhbVrXREfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmV LJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv4 7t3RBLulSwKMSMy/mPKhcxqlK9UrxyhqB5/zYDaY4+bKeRwcb/GcNMGWWZMRNpdWzBdDo6+a YYEEuoPPfxfr4n4v1YCoxWwCROxD+7y1DBIgGL906g80+QmCg7G2BIvE9wTu3nTt9r6KqESX fq2zKnOyjXMdPdW1inm5YjHdxAuu/CMXbZqfcXNzkkvEhrIg1ONooPqIz2bzP4Cs3SH7+V+T +KvjXYqpgFsrzWhx8ohi5XEi54Ux17K9ih0w5o5K9OmRUB0YNOpE5VduiGGO4Z0XM4sQ31kt SU0xLMItpC2fCoHxpo6yhPZdveJcJCI7wr9WOqNJTp0nnFodbKlixqs7EStyffwW8a33VtMs yFLiMPDtmoX2BzW8sWHSuVy/kOm2TuX0gDc8OBEIUQtmaXFKZ4t36c8lpQcvEnABCP2l0L2j KiZdkUg5Oek8fjoYrLjppOENo90jB/xMrg2l8ChHeg1NhICUmub9OimyrHv4E70TK9Fg/A1i qXZtYrVJcUfpq63GQ9V1YMj5g6kADi41tQUh3oHLFRCeB2ci4jmJUrDIP/9DfilglSslC1ny OzBPr3kGpnNKGPMn6/7fblh805c1BYzzddH6p5JEr0BOu78WlfttNzECR80KxC7w+H+CNlky oweXX+PDbSCPaPJsV6I4/ovLPOWaI8Uvjb9Mfkl6OT0gX83g19ONZWuiJAQcTWzGulsC0Sfe 3vlxNkbQkkQuQ9rBsCswHePV3ZwYXG4W692rmUxBYTgDoHETISgqLOE1Sa/WJZRYzYVWRi3D X70etDcCL83YyWIL5o5+tRlfb2oSot6kAqrqBe/0L1/aOzd5iwfs5vnktlz/eza0x8opnRvF 8rI9WaLQilvm38QAScs1fV1rEo7yVGE26x1q/NdHN1XofhOV1RyLobSmtRzEMu6QQfdZpGMQ VeiTM+hBGQ7Q9R3wNkJaUJwM9qnhxHHmSGtBuxdjKSFUboz9K+UxH3tP4B9xnLBgbEmlEUjS 9BTOHeOg6d+803eBdeMnRnJ0amtcqsY0WjG82LrIXOmmkZeXUYwVKzEWStafU7KtZHi4VuES bayCLMhOw8HyMiYK6IMZMe7xVNBDOzuPtjTeQfT0y+5GAqIy7WQbYHrZ3RV3SPTD1IBmhwS+ nDOPBY3ByOoqWbTRDJ0Elenb0Tp+Oh44HS1Ky18hwuHaQti0b2//hM9ivmVSvdV1bUB+W8gp zhyAFehzofOEdPT7wFlfahafZY8+AIdjTOf51E7ZMXwafwy1Tt8O0xtskjj1gt6ENBFmMku9 zYxyRZqbLmfyBVHfi+Z2pb5PvvWLHPz9Vahcf2zuBmW3dCI96MI8Pl9pU/kuVTjHEcktXZh1 NNR3lOT45zLCEwZVpe7ASNVv1Bq4qrXZCUw/dae33Bqd6qytTXG1vomAeIkzlCreNIVY8bmX EfiVsYdAcapMukjnVOkOwkFMO5l/6kxJ8q6dvGC1cZHJc5YlSm9xSRC6YF5iQeX8jZkD/XPx 9ADyu2Z2Q2OU3H9ik2gu4b5g9IMaTYXF2u5gS/qYewZLqd/e8AID2CkJ8CfydB3hpqrUHldv FKuHFIJ3sa1dAHaNQSsm10Nkx5O8Tr7yWOx1HRsnissr7aD0SCroayqbxcBNmNRBSFjgVrqP YmonoUfVUmsYRIukUjt7kL7yq5H4aVnejOLEAEYIm6sdjEkDvvj09jKK9RC454pryhNBeG1Y FTBD6X4vwNfyCT7WW1X2DE8cTiu/JT/hR1zzmyHfxMR5DLUf999wRDH6ZnSX/lUi3AMSS8+i j/QDFyxF9as9NSQ0ZzEt6rtMgDpHo0WaiTtwY6a4WGx6GssAhu4lfS+stLiGAk+lyT80pM5M EeA5Aa5aY7t2aOgNOthdUQ9H17w5f1xHYRmm5cxjpUdijAKw4+Y9n0dnSLvIM1WjOjgOWEVS 2dBkLu3qED1nVduJXWTy8flW2WBl4F/MsKibDpe2zphvZsXTv7FtPoewXQz+h3i8UrQeaQvw Gtbk6B1ridE26dR/1N8q0fVSrEKQRsGY2q1z07Ot5bm6/8PLGe3LeruigwkwYHnXOnE+kYGA D74YstwQnU2t5k5aQOWliW0s9GBGpGYbMpP5ELI1U6a0q4Nbsp2z6RChDI7azul7Tt8lLF93 Vo2msvj9Imfdzc0o/n/W08EcGWzP4RKpFSPxe5fhprEhdj+WMU8XGxRDN2wCqv3WDMK6aa9b ljITW168ybBX+KYRF7X6V86/SiWTdbxbCDRfyNflZI7FXz/bARJiQQQFl3Wh7YfEQanjIzke UZ9vXUK40Lg7wBL0qRuPgX+VWHWoEGpbC01Qd6RNkge6AYK/ErTPcGEi4A7VyhF4p2sqhCMI W2HdkxJC28OQEmNG1HkOPGn+9DB9+GSAuf2IeHJZP2CrulXVvHAwpzKsMMu5zGXKsCGJWVvF dU+00tHGH17QoHXx2VJRCsQmCbAKcWcoVb0+yF6qNy+7OW+WA/r4tjqafMaOtFu9haqxKabY rTI1WApdHACj8NKmS+brdpXlEQfgCxvaTS3RLEJtCqWCbnVhrcSFBkDLSV6KMpP6as4mAhLI 8/SzN3vhdsaxrY4DUlIUVv5l4Snf8sPdiu3OVWBB0CMPrCLDTLOysDzJ6i7TPcD6Ycc/w31o judH0L5a36bkCL1Uhm0LexWpCSSPRgbtYPkNxgxWS7sS9XpbhD9O9hyx25To/V8ljbBMmgSN iJ5ekVGo+iL7C9Wtf54HnRI8ntvKeTsc8Ox4OzRK5JQuvxuUHwcfw1y73Ezyr8T5yZBFqUdc Mr6q9dvpxSrkLDKxGY3FhVJrTlPicSAukAwYc3k
  • Ironport-sdr: 63a4e998_9NPhDL1U3Bhd0KpZIveRudhAemP/YuUizoz3WjAispE+DQn FlhS3JhZtE4RlUH9LvsUoPdRhI6zzFGDXZeqPDA==

On Thu, Dec 22, 2022 at 6:17 PM Jason Hu <fdhzs2010 AT hotmail.com> wrote:
> If Permutation (ys ++ zs) xs, then Permutation (x :: ys ++ zs) (x :: xs) /\
> Permutation (ys ++ x :: zs) (x :: xs)
>
>
>
> Did you try this path? I suppose to prove the second part of the
> conjunction you need to do another induction.

The first conjunct is a form of perm_skip; the second can be solved by
symmetry with Permutation_cons_app.



Archive powered by MHonArc 2.6.19+.

Top of Page