coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof about permutation

From: Rajeev Gore <rajeev.gore AT iinet.com.au>
To: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proof about permutation
Date: Fri, 23 Dec 2022 16:55:06 +1100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=rajeev.gore AT iinet.com.au; spf=Pass smtp.mailfrom=rajeev.gore AT iinet.com.au; spf=None smtp.helo=postmaster AT icp-osb-irony-out3.external.iinet.net.au
Ironport-data: A9a23:jFYQpqPQrURThTHvrR3SlsFynXyQoLVcMsEvi/4bfWQNrUog3jQAy jBLDGjSO/zfMWDxLYp0Otnl80MOu8OHm4dnTlY+pC08FStAoJSfDo7EIxb7NXOeI5XOE0k6s 8wUM9WZcJlkH3TRjyn2P+m6pxGQ900oqpkQqQLgEnosLeOxYH550XqPowO462JRqYDR7zml4 LsemOWCfg77s9JIGjhMsfja8kk05K2aVA4w5zTSW9ga5DcyqFFIVPrzFYnpR5cvatAJdgISb 7+rIICRpgs1zT90Yj+Wuu+Tnnkxf1LnFVPmZky6+kSVqkMqSiQais7XPdJAMh0P023hc9pZk L2hvrToIeslFvGXwrxFC3G0HgkmVZCq9oMrLlC5kpGX7WP4K0DigOs+FQYaJq448+ZOVDQmG fwwcFjhbziZjuC7zaz+buBwh9g+IMSuEdxD5SkIITPxVKx/B8yeBf+SupkHgF/chegXdRraT 9AQazdiclLPZAdCElYWDp8i2uyvgz/2blW0rXrJ/PZpujONnVIZPL7FMsXcetmHf9Rvz227h DjA837XKzNHO4nKodaC2jf27gPVpgvwX5tXH7ml/NZrhkeSzyodEnU+UEa4rOK5lk+hUsheb U0V+zYrhac3/U2vCNL6WnWFTGWspgYEAoAJVrFnrVvVle+Lv0CSDHJBUiRHLdohroo8XzUxj Q/Pg8vmQz1prLCPT3WR+/GTq3W0NDR9wXI+WBLohDAtu7HLyLzfRDqVJjq/OMZZVuHIJAw=
Ironport-hdrordr: A9a23:DEMKO6wjFNxm0sgJz9A1KrPwN71zdoMgy1knxilNoHtuA6+lfq GV/MjzuiWftN98YhwdcLO7WZVoI0myyXcd2+B4VotKNzOJhILHFu1fBPDZsl/dJxE=
Ironport-phdr: A9a23:ZrObABDyfatia+kQFEznUyQU2kkY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua8wygKQFtWKo9t/yMPo8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PTbglShDexfLx+I RayoA7MqsQYnIxuJ7o+xRfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQ rNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4 qF2QxLulSwJNSM28HvPh8JwkqxWvg+vpxJxzYHWY4+aOvVxcb/Sc94BWWpBR9xcWzBdDo6mb YYCCfcKM+ZCr4n6olsDtQewChOuBOzx1DBImGL906w90+Q7Dw7NwQstH8gUv3TWstr6KrkSX fq6zKnP1zXMcehb2Tb86IjObB8hveuAUq53ccrU00UgDR7Fg0yWpIf4MDybyv4DvHKH7+p8S +2vkWgnphltrjSz28ohiYfHiIwXx13K9St13oY7KcClRUN5fdKqHoVcuS6EOoZ2Tc0vX29lt SYkx7EapZO3YDQHxZYkyhPbbfGMbouG4gr7WeqPPTt1imhpdbK7ihqo7ESs0PDwW8m63VpSs yZJjMTAumoC2hHT8MSLVOdx80W71TuN2A3e7PxPL1oumqrBMZEhx6Y9lpoNvkTHGS/7gET2g 7OOdkk9/eio8P/obqznpp+GMI90jAH/Pr0pmsyiHeQ1PBICUHaU+OSgyrLj50v5T69OjvEsk 6nZsZbaKtoHpqKjBQ9azJoj5wylADe7yNgYnH8HI0xZeB+fkYTlJ1/DLOr4APq7mVigjS1ny +3GM7DvGpnNK2LMkLblfbZz8U5czw8zwMhF551OCLEOPuz8WlHruNzXCR85KRK7zv3mCNV80 IMRR36PDrWFP6PVtF+E/PggI/SUaI8ToznyM+Il6OL2jX8lhV8derGk0YYPZHCiAvtmO1mZY WbrgtoZDWgKuRM+QPX2h12GTD5cfG2/X7k85zE+EIKpF53PRoGrgLyb3Se0BIdaZm5cCgPEL XC9cpiHVuwMID6TPcZ7k3RQUKWiRpQhyRCxvRX7jbtmL/bR0iIdvJPnktNy4ruAuws18GlOB saQ3n/FYGZukytcXTY00a1h50N60Fqr0Kl+juAeHttWofpUBFRpfaXAxvB3XoihEjnKec2EH Q7OqrSOBDgwSol02NoSewNmHM3kiBnf3i2sCrtTlrqRBZVy/LiPl2PpKZNbzHDLnLIkk0FgW tFGYHevhKNy6U7cAJTEu0SYkau2M68b2WjE6TTL1nKA6XlRSxU4SqDZRTYab0rSo87+4xbYR r2jBKphPQxbxOaDK61HdpviilAATeqwcM/GbTeXnGG9TQ2N2qvKbIfufDAF2z7BDUEfjw0J1 XeNLU05HS3konjZCi0rEk/zOAXh4fVzsnWySgk1zgeHcwtn2qbz8wN9aeW0bfQV0/pEvS4gr 24xB1Ohx5fNDMLGoQN9faJaaNd74VFd1GufuRYvdpqnZ7tvgFITaWEV9wvnygl3B4NckMMrs GJizQx8Lrid2U9AcDXQ1I75O7neIG3/tB61bKue1lbb2deQsqABjZZw40/qvgykCAwt9G9q+ 9hU1XaAoJ7NCUwbTNO5U0o68QR7u6CPejM0tOa2nTVnNai5tCOH2sp8XrN+jEvxOY4Zaf7fR 2qQW4UACsOjKfIngQ2sZxMAZ6VJ8bIsetihb72A0bKqO+BpmHSni35G6cZzyBHplWI0R+jW0 pIC2/zd0BGAUmK2ll6jv83p349Dfzw6H2u5xDSiD4lUIKRvN9Vuay/mM4isy9NyioS4EWRR9 lOuGRUJ39WkURuTaVHhmwZX0AIevDb0/EnwhywxmDYvoK2F2SXIyOm3bxsLNFlAQ2x6hEvtK 4y55zwDdHChdBNh1B6s5EKhgrNeuLw6NG7LB0FBYynxKWhmFKq2rLuLJcBVutsktiBeUeL0Z l7/KPa1uRIY3i79WWRZ3j0TdjCst4m/lBt/zmuAZHp+t3vWf8hsyAyXvoSHA6MAmGNAHXQjw TDMTkCxJdyo4cmZm/Kh+qilWmStW4cSOSjnwIWctTeqsGhjABmxhfe2yZXsFQk31zO+1sE/D 32T6kutJNCtjvnhYocFNgFyCVTx6tR3ANR7m4o039QL3GQCw46S5TwBmHvyNtNS3eT/amAMT HgF2Y2wgkCt1Ut9I3aO34+8WG+ax54rfdC4b24InC069c1iCaaS4aAClixw5FOl51G0A7A1j nIGxP0i5WRPyfsAugcg0GOSBaofNUhZOyHw0R+P6pa3se8EAQTnOaj13014k9e7CbiEqQwJQ 3f1dKApGipo59l+OlbBgzXjr5vpc97KYZcPpwWZxl3e2vNNJst7xZ9ozWJ3fHjwtno/x6sng AxyiNuk6ZOfJTwl/brlUEQAbXuoNoVKvGmq1/oWn97Kjdr3RdM4Q25NBsCwC6rvSm5317yvN h7SQmdk8THBQOWZQUnHrx0653PXT8LxbyrRfD9AkoUkHkHNbE1H3FJOBG58wMV/RlHsnZGEE g8x5yhNtASg8F0VkbwubkCnFD2D+0+pcmtmEsDFakMNsEcbvh+Ta5DPi4A7VyBAos/79FbLc zfFIV0RVSdTARLDXAirKLCq4ZOoH/GwIO24IrOOZLyPrbcbTPKU3de01ZMg+T+QN8KJN30kD vsh20MFU2orU8Le0y4CTSAajUevJ4aSuQu89ytrr8u+7OWjWQTh4pGKAqdTNtMn8g6/gKOKP eqdzChjLjMQ2pQJzH7OgL8RuTxawzlpbCWoGK8cuDTlTanI36hMBVsacSR1JY5P8r5nmARdJ cPBjNrxkL95iPMpTVFISRroh4DMB4RCIm2wMk/GGFfeNLmCIm6DyMX2bKWgDLxI2b8M7Fvt6 HDCVRa+ZWfm9XGhTR2kPOBSgTvOORVfvNr4aRNxES34S8qgbBSnMdhxhDlwwLsuh3qMO3RPV Fo0O05LsLCU6jtVx/tlHGkUpGBsL+SJhWCW6PPVApcXt/Z3RC9zkqRT/T5prtkdpDEBX/Fzl CbI+5R2pEq6l+CU1jd9eBtFsnNMn4jOvF9lP7Sc8YRcAjDJ7A4A92OZD1ILpt1oFpvptrwWw 8WFx8eRYH9SttnT+8UbHc3dLsmKZWEgPRTeEznRFAIZTDSvOAk3YmRckfef6jueqZ18o4W+w PLmq5daX0RwEegQT0V/G9oTZZBqQmhinK6HgdQO7H74rRjXSdkcuJ3bEPuPU62HwNmxjLhCa gdOyrT9a40OZNST5g==
Ironport-sdr: 63a542c3_AmIR2IAprmuz+h0QVH2s0oOo9Q/M9jeUZs/KLlHcI0XsFUJ UPrd0PLqGyLuVquhwZtN9uRela/lfEZU5uMxGVQ==
Ironport-sdr: j4+HLxfC+rfTQU8uFVFrkPp1ZHjrge3dQzbE2TcLZtM7trzbdaUT2vcPSChGQ891BIEshjFaq2 soYE+mjNmdtPRroqIVg2szwpJ4o3ra8YZz4l5Nsod3w8JHWwHN8Scpqt/wj4rc4rh10TEp9MQ4 v8IkoYDstc8gRo7E7A10Yr+xKLDX0m2DEyOAYnDc82pTQ0xBhDIHaG7D3d1+Fj0ft4nWn/Ao39 JrNki0laL1cRvOWjrPC6Q44mAM8XszqBLiG/40PDSNwdCRalzIlVYIOZhKxPXisIAw8extim6/ arM=

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 :)

> 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?

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).

raj

Re: [Coq-Club] Proof about permutation, D. Ben Knoble, 12/23/2022
- <Possible follow-up(s)>
- Re: [Coq-Club] Proof about permutation, Rajeev Gore, 12/23/2022
  - Message not available
    - Re: [Coq-Club] Proof about permutation, Rajeev Gore, 12/23/2022
      - Message not available
        
        Message not available
        
        Re: [Coq-Club] Proof about permutation, Rajeev Gore, 12/24/2022
      - Message not available
        
        Message not available
        
        Re: [Coq-Club] Proof about permutation, Frederik Krogsdal Jacobsen, 01/02/2023