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: [Coq-Club] Correct order type Module for the MSetRBT
- Date: Fri, 26 Aug 2022 13:38:59 +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-f48.google.com
- Ironport-data: A9a23:FH484al+9V3I+zCXOKa9l3Xo5gysIERdPkR7XQ2eYbSJt1+Wr1Gzt xIaCG7XPKyPM2XxLt11PNuwoxgO6p6Aztc3HlRuqS5hRltH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvykTrSs1hlZHWeIcg944f5Ys7N/09UAbeSRWVvX4 4ui+ZCHYzdJ5hYtWo4qw/LbwP9QlK+q0N8olgRWiSdj4TcyP1FMZH4uDfnZw0nQGuG4LcbmL wr394xVy0uCl/sb5nxJpZ6gGqECaua60QFjERO6UYD66vRJjnRaPqrWqJPwZG8P4whlkeydx /1MiJGTTSs4PJbGnboASABkKhtXev1/reqvzXiX6aR/zmXDenrohvhiVQQ4Yd1e9eFwDmVDs /cfLVjhbDjZ37PwkO/9ELE8wJhzRCXoFNt3VnVI1izfAPsiB4vKWb7V7MNw0zI5h8QIFvHbD yYcQWA1NU+QP0IUUrsRILwVjsWHiCLvTzNzuWOJma40uEqNnTUkhdABN/KMIoDQLSlPpW6To XuD9GDkCDkBJdmHwHyE9Gitj6nBh0vGtJk6EbS58rtnjATWyDBDThIRUlS/rL+yjUvWt89jx 1I8+xcjjqwe5U6QRNyjQgahnEe+l1lMYo8FewEl0z2lxq3R6gefI2ELSD9dddAr3PPaoxR6h jdlePu5VVRSXK2ppWG1rejL8GvjUcQBBSpTOn9eFFptD8zL+dlr1nryosBf/LlZZ+AZ9Bn1y jGO6SUy3vAd0Z5N2KK88lTKxTmro/AlrzLZBC2GBwpJDSsjPOZJgrBED3CFsZ6sy67HEjG8U IAswZT20Qz3JcjleNaxaOsMBqq1wP2OLSfRh1Vid7F4qWr0pyP5J9oNvmEiTKuMDiriUW+5C KM0kVMBjKK/wFP3BUOKS9nsVZpynPiI+SrND6mKNYQmjmdNmP+vpXkyPyZ8Lkjil08jlaxXB HtoWZfEMJruMow+lGDeb75Fj9cDn3lirUuOG82T50n4idK2OiTJIZ9bawDmRr5ivMu5TPD9q Yk32z2ikEUBDoUTo0D/reYuELz9BSJgVM6v8ZQOLrLrz8gPMDhJNsI9CIgJI+RN95m5XM+Sl p1kckMHmlf5m1PdLgCGNiJqZL/1DMRwqHs6OWonOlPxgyovZoOm7aE+cZorfOl/pLYzk6IsF /RVKd+dBvlvSyjc/2tPYJT4qrtkfkv5iA+LOR2jfzViLYVrQBbE+4O/cwa2rHsOAyO7uNEQu bql0g+HE5MPSx4zXsnTYfOriVi2uCFFyu51WkLJJPhVeVntoNA6cXyv0qdvLphVexvZxzac2 wKHOjsipLHA890v7d3EpaGYtIP2QeZzG0xtGWOEv7u7MC/t+HX6nd1NXeOOSjDqVG3u/ZKka +gIner3N+cKnQoTvodxT+RrwKY564e9rrNW1F4/TnDCblDuB785Z3fajY9AsapCwrIfsgyzA xrd9t5fMLSPGcXkDF9Be1Z/P7rbjakZymvI8PA4AETm/ysrrrCJZkNfYkuXgytHIbopbY4on bU7tMgN51DtgxYmKIzd3CVd9mDJI3BZFqt75tcVB4jkjgdtwVZHOMSOBijz6ZCJStNNLkh6f WPO1fSa3+xRlhjYbn4+NXnRxu4B154AjxZHkQ0ZLFOTl9uZ2/I60XW9K9jsoti5E/mG7w5yB oSvH0h8JKHL8jsxwcYfDyajHAZOABDf8Uv0o7fMeKs1UGHwPlEh7kVkUQpOwKzd221Zdzlfu rqfzQ4JlB70Kdrp0HJatVFN8pTeoB8YyuEGsM+iFsWBWZI9ZFIJR0NoiXUg83PaPC/6uKELS SSGMgq9hW0X+BP8e5EGNrQ=
- Ironport-hdrordr: A9a23:p68+cKjuRtdvO7jT0GqyOFtEqXBQXtcji2hC6mlwRA09TyX4rb HIoB1/73XJYVkqKRIdcLy7WJVoIkm8yXcW2/hyAV7KZmCP01dAR7sSiLcKrQeQfxEWNdQw6U 6jScVD4RHLYmSSRPyV3DWF
- Ironport-phdr: A9a23:wTPlRh3JYoGk4rClsmDOsg4yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaEo68y0BSQB9qTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnA JYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7ye6/94fNbwhKizexbq5+I Au0oA7MqsQYnIxuJ7orxBDUuHVIYeNWxW1pJVKXgRnx49q78YBg/SpNpf8v7tZMXqrmcas2S 7xYFykmPHsu5ML3rxnDTBCA6WUaX24LjxdHGQnF7BX9Xpfsriv3s/d21SeGMcHqS70/RDKv5 LppRhD1kicKLzE2/mHZhMJzkaxVvg6uqgdlzILIeoyYLuZycr/fcN4cWGFPXtxRVytEAo6kc oUPEuwBMvhGoIn5ulAAsAGxBRO3BOLh0DBImmL90Koh0+Q8FwHJwhIvH9YUvHTPttr1LrwSU O6vw6nU1jjDYPZW1i386IjMaBwuvfaMXbdpfMfX1EIgGB/LgE+Kpoz5IzOayP4Ns26D4uRuW +yij2oqph1srjWyxMogl4nEiI0ax13A6yh13oY7K9K3RkN/f9KpHpldui6UOoV2Qc4uXm5mt ig6x7EYvZO2ejUBxpc/xxPHdfCLb4yF7gjgWeuROzt0mm5pdbGlixu98kWtzPD3WNOu31ZQt CVFl8HBtnAT2BzX7ciKUv598V2g2TaLzgzc9PxLLV0tmarVJJMswaQ8lpUUsUTEES/2nFv5g LWKeUUj/+ik8+XnYrP4qZ+AL4J4lB3yP6A0lsG8Aek0KBYCU3SY9Oim27Du/lX1QLBQgf03l qnZvoraJcMepqOhGA9Vz4Aj5AihADeiytgYhmMILEheeBOJlYfpJ0rDIP/9DfilglSslC1ny OzBPr3kGpnNKGPMn6/7fblh805c1BYzzddH6p5JEr0BOu78WlfttNzECR80KxC7w+H+CNlky oweXX+PDbSCPaPJsV6I4/ovLPOWaI8Uvjb9Mfkl6OT0gX83g19ONZWuiJAQcTWzGulsaxGSZ mOpidMcG08LuBA/RarkkgvRfyRUYiOJQqQx6zVzM4u8FpjKWsj5m6GH0Sq/WIZffHtZA0ykH nLhdoHCUPAJPnHBavR9myAJAODyA7Qq0guj4VeSI9tPK+PV/nZdrpf/zJ1u4PWVkxgu9DtyB sDb0meXTmgykHlbDyQu0vVZpkpwgkyGzbA+m+ZRQMdO4f5EVkEhPITH0OVmI9/3UwPFONyOT QXuWc2oVAk4Vcl52NoSewB4EtSmgArE2n+xHrkYmrjNH5Uu6b3Vw1D+Is98zzDN06xyx0I+T J5pMmurzrV66xCVB4PNlBCBkL22cK0HwCPX3GKKzG7LsU0BFQAsAePKWncQYkaQptP8jq/bZ 5mpD7lvcg5IyMrZb7BPdsWsllJeAvHqJNXZZWu13Wa2HxeBgL2WPsLsfC0G0SPRBVJh8Uhb9 GuaNQU4Giaqon7PRD1oG1X1Zkrw8O544HqlR04wxguOYgVvzb2wshISgPWdTbsU0Ndm8G86t jN5EVL7xNvMEMWJuyJueaxdZZU251IGnWPVugphP4Cxerh4jw17EUw/tEfv2hNrT4RYxJJy/ TV6kUwocfLejAMSElHQlYr9MbDWNGToqRWmaqqNn0rbzM7T4aAXrvIxt1TkugitUEsk6XRul ddPgB7+rt3HChQfVZXpXwM57R9/8vvBfy8w6oeSznR2Kra9rhfN3tsoAK0uzRPqLLI9eOuUU RT/FcEXHZ3kM/EsllWtKAkNJvtN/bIcMMavdv/A06mudrUF/nrunSFM54Zz1ViJ/ix3R7vT3 poL9Pqf2xOOSzb2iFrJXtnfoYlffnlSG2O+zXOhH4tNfuhpep5ND26yIsqxz9E4hpj3Wnce+ kTxT18B3caof1KVYTmflUVLyEIarHjhgiKi1CN9jxkmq6Oe2GrFxOGqeBccO2FNTXVvlh+2e dny341cBhD4KVR53BK+gCSyj7BWvqF+M3XeTQ9Tci76InsjGqq8u7yeYtJevZYhsCFZSuO5M hiRTr/wpQdf0ju2RTMPgmBmMWvy6tOlz08f6irVNnt4oXvHdNslwB7e4IeZXvtNxn8dQzE+j zDLB1+6Nt3v/NOOlp6FvPrtMgDpHpBVbyTvypuN8SWh4mg/Swaimf2+npv8GBIhzibn/9ZvX CTM6h37Z8O4ssbyefIiZURuCFLmvoBhB4dzn492n5gKwmcTmr2a+HMGlSH4NtARisecJDIdA DUMxdDS+g3s3kZue2mIy4zOXXKY2sJ9ZtO+bzBeymcn4stNEqvR8K1ckH4/vA+jtQyIK6sY/ H9V2b405XUdme1MpAc90nDXHOUJBUcBdS30y0bTspbn/f0RPjrwN+D3jhY2nMj9Xu/e5FsHA zCgJM9kRWgpv6AdeBrNyCGhtN+iIYGKK4pV7lrOy1/Bl7QHdsx3zKZbw3o/fzq65yVtyvZn3 0M0m8jm+tHWcSM1u/vpZ3wQfjztO5FMpne01/sYxoDOmNnxVpR5RmdSBMuuFK33VmJU7bO9b k6PCGFu8yjAX+OOQUnHrh8h9iyqcdjjNmnLdiNBnJMyGV/EfhwZ2EdNA307hsJrTFn0gpGxN h4ovHZJoQep4hpUlrAybke5CDyO4lzyLG9zEcn6TlIe+AhG4w293dW2yOV1EmkY+5SgqFfIM WmHf0FTCnlPXEWYBlflN73o5N/a8uHeCPDsZ/3JKa6Dr+BTTZLqjdqmz5dm8jCQN86OImgqD vs13VBGVGx4HMKRkisGSigenSbAJ8CBoxL09ipyp8G5uPPlPWCnrZOIEKdXOM5z9gqehK6CM 6udiH88J2oIkJwLwnDMxf4U21tTwyBiej+xEKgR4C7ASKWD/80fRxUfai51KI5J9/dmhlgLa ZOd0IulkOIo3ZtXQx9fWFfsm9+kf5kPKmC5bxbcAVqTca+BPXvNyt32ZqW1TftRiv9Vvlu+o 2X+cQerMzKdmj3uTx3qP/tLiXTRJwFYtYy5NA1kE3P8Rc7OZRiyMdsxhjozi+5R5DuCJSsHP D5wflkY5KWX9j9di+5jFnZp63NkKayJl3/c4bWIbJkRtvRvD2J/kOcQsxFYg/NFqSpDQvJyg i7bqNVj9kqnnue4wT1iSBNSqzxPiepjWG1tPKzY8t9LXnOWpHrlDE2VAhUO4tZpU5jh5/AWx d/Im6b+bjxF9oCMlSPzL8fRIcODdnEmNEiwcAM=
- Ironport-sdr: BRRrwuW6apVlBi4mbM/sV8clkP0dy8InIG/Ol7XZ6LqnhG8jMCJsJwdIUQ74CWs51LR81WZUAz 5PwHiy6Uk4vG3ULNdn+2o7qFhZVAlsax7zZwRGpnlQ8No2k5RNi5za+1il83kA3uw112jQMsJ6 kpg9qxquk/CY8YEIq40ZVf8NtGLE+Le9Y81hiuIAH165MFt2t9ud+ECLMDY/5TTWOHOaAuXc9P DAprOWn1qWoY+rZ+TFArFdR48BUNUfBx/UUOmclweGfnTRRRw1geW4SQcASyIBLYMCUf5+gsCc /L9F9XnagRY5SUwskKRNonKL
Dear Coq-Club members,
What is the correct order type module for MSetRBT? My order defined for the elements are total. The issue I am facing is the following.
Module Ordered <: OrderedType.
(*
Definition t := instruction.
Definition t := instruction.
Definition eq (x y: t) := eqi x y.
Definition lt (x y: t):= lti x y/\~eqi x y.
Definition lt (x y: t):= lti x y/\~eqi x y.
.........
.........
......... equivalence of eq and transitive/compare for lt
*)
End Ordered.
Inductive color := Red | Black.
Module Color.
Definition t := color.
End Color.
Module Ops (Ordered:Orders.OrderedType) <: MSetInterface.Ops Ordered.
Inductive color := Red | Black.
Module Color.
Definition t := color.
End Color.
Module Ops (Ordered:Orders.OrderedType) <: MSetInterface.Ops Ordered.
Include MSetGenTree.Ops Ordered Color.
Module TB := MSetRBT.Ops Ordered.
Module TB := MSetRBT.Ops Ordered.
(*Error: Signature components for label compare do not match: expected type "Ordered.t -> Ordered.t -> comparison" but found type "forall x y : Ordered.t, Compare Ordered.lt Ordered.eq x y". *)
If I use Module Ops (Ordered:OrderedType) <: MSetInterface.Ops Ordered., then I get eq_eqiv is missing even though it is present!
What signature of OrderType are required for RBT tree and which Module to be used for that?
Thanks again,
-Suneel
- [Coq-Club] Correct order type Module for the MSetRBT, Suneel Sarswat, 08/26/2022
- Re: [Coq-Club] Correct order type Module for the MSetRBT, mukesh tiwari, 08/27/2022
- Re: [Coq-Club] Correct order type Module for the MSetRBT, Suneel Sarswat, 08/29/2022
- Re: [Coq-Club] Correct order type Module for the MSetRBT, mukesh tiwari, 08/27/2022
Archive powered by MHonArc 2.6.19+.