coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Frédéric Fort <ac AT ffort.fr>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] How to use (well) the FMap* modules ?
- Date: Tue, 28 Jan 2025 17:43:48 +0100 (CET)
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ac AT ffort.fr; spf=Pass smtp.mailfrom=ac AT ffort.fr; spf=None smtp.helo=postmaster AT mout-p-103.mailbox.org
- Importance: Normal
- Ironport-data: A9a23:kJPlgKN6z/FYuoHvrR1xk8FynXyQoLVcMsEvi/4bfWQNrUol0WcGz mtLWW2DMqqPZDf9edp3ad+z9RhS7ZLTz98wHnM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/vgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5OZYQTNNwJcaDpOtvra8kM35pwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGXqdVy82st0JX0fHpAeofxQX0FF9 vYxfWVlghCr34pawZq+TfRww9xmdZGweoYWu3VqyiGfCuwpKXzBa/WSo4UEhXFt2IYXQ6+2i 8kxMVKDaDzJaDVBNFANFNQwho9Eg1GlK2AE8w7K+ftfD2775y4h6b/pGdXpU8WqV+togRmUn GH38DGsav0dHIfGlGTZrSvEavX0tSj8QccZEKCy3uV7hUWagG0VEhwfE1WhycRVkWa7XM9Db lRRo3J166079UihScm7WAe3yJKZgvICc/ZWNL0j1huk9oP3/gDCHE9abjVCYvVz4afaWgcW/ lOOmtroAxlmv7uUVW+R+9+oQdWaZHd9wYgqO3dscOcV3+QPtr3fmTrjY75e/EOdi9roBXToh mnS9247jrQXh8kbkaKh8jgrYg5ARLCWH2bZBS2NBwpJCz+Vgqb5POREDnCHs559wH6xFAXpg ZT9s5H2ABoyJZ+MjjeRZ+4GAauk4f2IWBWF3gU/R8F7qGrwpyP8FWy13N2YDBkwWirjUWGzC HI/RSsItPe/wVPxPfMvC25PI55zkcAM6ugJptiPN4cQPscoHON21CFjZEiU0mHr1VMxibk4I 4vTfsOmDR4n5VdPk1KLqxMm+eZznEgWnDqLLbiilkTP+eTFPha9F+xaWGZim8hlt8toVi2Jq I4Hb6NnCnx3DIXDX8Ug2dBMcQlbcyNnW/gbaaV/L4a+H+avI0l5Y9e5/F/rU9UNc319x7mWr EKuEFRV0kT+jnDhIACHICIrIrD2UJo16TpxMSUwNBz6kzIucKS+3pc5LpEXRLgA8PA87PhWS /JeRd6MLM4SQRv6+hMcT6LHkqpcSDqRizmjBRGVOAoEQ8Y4Riji2MPVQQ/0xSxfUgu1rZQfp pOj5CP6QL0CZQFQCZfHZNnyyliwnGM8ndhqVBDiOehje0TL8alrJRfuj/QxHdo+FBXbyhae1 CeUGR0onvbMqIoL79X5v6CIgIO3Ge9YHEABPW3kwZupFCvdpEyP/JRhVbuWQDXjS2/EwqWuS uFLxfXaMvdcvlJrsZJ5Iol735AF+NrjiL9L/DtKREyRQQyQNYphBX2a0e1klK5HnOZZsDTrf HO/wIBRPLHRNf71FFIUGhEeUd2C8vMpgRjX0+U+JRTrxS1w/Yffa35oATu3tHV/Iod2YaQf+ sVwnO4N6ge6tAgmDcbesABQ6Fa3DyIhV4cJi8gkJbHF2ysR90F6QJ3DCyXJzomFRPdSP2ILf DKFpqrwqI5N50jFcnAMRCHB9rNCoagjpzVbkUMzGFCSq9+U2tsyjQxj4BUsbwFv1h4c+flCC mtqEExUJKu14DZjgvZYbV2sAw1sAB64+FT77kkgzkn1fhKNbXPcClE9NcKm3lErw0gFchd1p LinmXvYCxD0d8TP7w4OcE9Cqc27a+du9wfHyfuVL+7cE7YUOTPa07KTP0wWoB7aAOQ0tk3Nh c9u2M1SMaTbFyohk5cXOrmg94Y7aU67fTRZYPRb4qk2M3nWe2iy1RiwOkmBQJ5xCMKQw3CoK f5FB5xpbAu/5hasvzpAJK8rIp1IptALyucGWIvWIT8hj+PCgBtv6Ind5wrvtl8NGt9Oq/swG qnVVjCFE1GTu0dqpn/wnJF6HVS8MPY5Z1za/eGq8e82OYoJn8NyfGoTjLalnXWnHzF23hCTv THGVbHdydV/+4JNnq/HMKZKNyOrI/zdCcWK9wGStYxVTNXtaM3hiSIcmmPFDS93Y4RIA89Wk 5aJu/7JhHL1hq48CT3lqsPQBpt36tWXd8sJFMDOdV1xvzaIAe3o6Ds9o1GIE4RDyo5h15P2V jmDSZWCcPAOUI1g31xTUS9VFigdB4nRbqvNoSCcreyGOiMC0D7ofc+Wynv0UV51LiM4GYXyK gvRicac4tp1qIdtBhhdI9pEB5R+AkHoWIp4VtnXmASbMFKVgQK5iuO/rSYj1DDFNCDVWoKyq 5fIXQP3exmOqbnFhoMR+ZB7uhoMSm1xm68sd0Ya4MR7kC2+EHVAF+kGLJEaEdtBp0QeDn0ji O3lNwPOyBkRXAiotT3558n/Gx/aX7RVfNLwJzgj+FPSbD25bG9F7H2N6Q84i0qauBO6pA1kF T3a0nP+OQKthJ9zLQrWzuLumv9pn5s22VpRkX0QUKXO79I2D7sNzmAnEhAluekr1S3SvB2jG FXZjlyojK12pYAd3Cqgl7No9MklgQ7S
- Ironport-hdrordr: A9a23:vIRhRqOcJKMsScBcTtCjsMiBIKoaSvp037BL7TETdfUxSKalfq +V8cjzuSWZtN8xYgBEpTniAsm9qBHnm6KdiLN5VdyftWLd2VdAQrsM0WKY+UyDJxHD
- Ironport-phdr: A9a23:YaLksxLq5Ra8ZqsAjdmcuJltWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCEv7M11BSUDc2bs6sC17GP9fi4GCQp2tWojjMrSN92a1c9k8IYnggtUoauKHbQC7rUVRE8B 9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9I Ri4swndrNUajZdtJqsxyRbCv39Ed/hLyW9yKl+ekQvw6t2s8JJ/9ihbpu4s+dNHXajmcKs0S qBVAi4hP24p+sPgqAPNTRGI5nsSU2UWlgRHDg3Y5xzkXZn/rzX3uPNl1CaVIcP5Q7Y0WS+/7 6hwUx/nlD0HNz8i/27JjMF7kb9Wrwigpxx7xI7UfZ2VOf9jda7TYd8WWWxMVdtXWidcAI2zc pEPAvIPM+hYsYfzpEYAohSiCge2B+zi0SVHimPt0qIhz+gtDQPL0Qo9FNwOqnTUq9D1Ob8SX +Cv1q7H0C/Eb+lX2Tjh9YPGchchoeuQXbltdsfe01UgGhjLjlWerozlJS+V2v4Ds2iB9udtU /+khGE7pQ9ruDev2tsshZfThoIT0l3J+yt3zYI6KNGlVkJ2f96qHIVNuyyUK4Z7Qt0vTn10t CokyrMLtoO3cSgKxpoo2xPSb+CKfpSH7x/9WuucLjZ1iXR4c7y8nxa/6UutxvHmWsWq31tGs zBJn9nNu3wXyhDe69WLR/1g9Uq/3TaPyhvT6v1aLkAuiKTbKp8gzaAom5YPt0nIAzX4l1/sj KCMc0Up4uio5PrjYrXhvpKcMoh0ihziMqg3gsyzGPk0PhQAUmSB/OSzzrzj/UniT7VNgfw6i K7ZsIrVJcgDp665BRFa0po75hu8EzuqysoUkHYaIF5feB+KjpLlN0zPLfzlFfu/hk6jkDZvx /DIJL3hBZDNI2DZn7j9Zrt95UBcyA0pzdBD/Z5UBKsBLOr1WkDqrNPYFAM2MxSow+b7D9Vwz p4SVXqVAqCFKKPSrUOI5uU3LuaQY48VoS/xJOQh5/7zlnA0gkQdfKms3ZsPcn+0BPVmI0ODY XrtmNgNC2kKvhBtBNDt3ReJVicWbHKvVYo94Cs6AcSoF82LEouqmfmK2DqxNpxQfGFPTF6WR yTGbYKBDtkW6S4TOM5q2hIDT6TpH4Yq/R+gsxXmjbR9eLmHshYEvI7ugYAmr9bYkgs/oGQc5 6W11miMSzsxhWYUX3os26s5p0Vhy1CF2Kw+gvpCFNUV6ekaGhwiO8v6yOp3Q8v3RhqHZs2AH V+tatuoBistCNwrkJcVe0goI9y5lVjY2jayRboclriFHpsxp6vX93b/INxhjXjch+E6l1dzZ MxJOCW9g7JnsQjeA4mci0KCi6OjbrgRxgbI83qfiHLL5RkDFgt5UKHPWmBZYVHZxTjgzmXFS bLmSbEuMw8bjNWHNrMPcNriy1NPWPbkPt3aJWO3gWa5QxiSlPuKa8LxdmMR0T+4agBMmh0P/ XuAKQk1Bzuw62PYAjt0EFvzYkTqueBgoXK/R0UwwkmEdUpkn7ay/xcUg7SbRZZxlvoNsw8vp TJuABCzxZOeCtaNoRZgYLQJeck0sx9M0WPUsRA4P4T1f/gk3AJHNVkp+RqwjkYSaM0Ii8Uho XI0wRAnLKuZ1AkEbDaExdXqPbaRLGDu/RepYqqQ21fE0d/Q9L1cjZZw41jlogytEVIvtnt91 NwAmXKXzpvECxAOF5zrGBV/511hqrfWbzNorYrf/XNiNrOo9DHYkYFMZqNt2lOreNFRN7mBH Qn5HpgBBsSgH+ctnkCgchMOOO06GLccB8q9bLPG3aeqOLwlhze6lSFd54s71EuQ9i16Q+qO3 pAfwvje0BHVHzv7iV6gtIjwl+UmLXkbFUKxxy/+GMhffOV+cJ0KBmGnP8CsjoUmwcSxAjgFq hj6WQpO0dThYReIal3hwQBcnV8ap3Cqg2rdrXQ8kj0kqLaewD2bxu3jcBQdPWsYDGJmjFrqP c21l4VKBA7yM1FvyUXjvBijlM057OxlImLeQFlFZX3zJmBmCO6rs6aaJtRI49UuuDlWV+K1Z RabTKT8ql0UyXCGfSMWyTYlejWtopi8kQZ9jTfXJX1bonTeY902yw2Vt5TMAOVc2DYLXnwyg DL/CFa7JcXv88/exPKh+qiuEmmmUJNUayziy4iN4TC66WNdChq6h/mvm9fjHFtywWrh2tJtT ymNsAfkb9yhyfGhKew+NBoNZhe0+49gF4p5iId1mJwAxS1QmMCO5XRe2WbrbYcBgPm4NiJWA 2RQk5iNp1K4vS8rZnORm9CgByjbm5MnPYHqJDtRgH517tgWWvbNquUVzW0v/wL+9UWLPbB8h mtPmaNosiJDxbxX/lJqlHz4YPhaHFEGb3a0z03asY+1/v8POT79I//shAJ7jZi3BbWG6GmwQ V7ffZEvVW9158R7ahfX1WHrr5vjc5/WZM4SsRudl1HBifJUIdQ/jKhCgy0vIm/7sXA/roxzx RVzwZG3upSGIGRx7eq4BBBfLDj8e8IU/Hnkk69fms+c243nEI9mH30HW57hTPTgFzx317yvL wGVDDg1sWuWA5LaGhKDrV8j9iqUVZWiNnWdI2lfys9tBVGcKEFZnAEITWA6k5o+RWXIjITqd EZ04CxU50at+kMKkL4xcUShFD6B/VTNCH98UpWUIRtI4xsX4k7UNZbb9edvB2RC+ZbnqgWRK 2udbgAODGcTW0XCCUqwW9vmrdTG7eWcAfKzavXUZrDb4+VVf/mGwoizlIV8tWXpVI3HLjx5A vs311AWF2h+ANjcki4TRjY/kiXQc4uD4U7koWtyp8G7+vP7HgX16sHcbtkaecUq8Bewj6CZM ueWjyssMjdU2KQHwnrQwaQe1lof48mLXzejFq4c8yDXHvq4ckB/ARAccT81OtEatsrUPyFIP tPHz8uwj+YjyPs8ClNPUkynndumN5RiHg==
- Ironport-sdr: 67990947_ZLLauV3AlGu2nAJ0LRIEwcMP6r7ZCn6iwyK428rNfXltQuv VPmwMyxV499FGxSiTxcmTGA5hl+RUz46hRlqXiA==
Hello,
For some proof, I'd like to use a well-defined Map-module instead of
some (most likely buggy) ad-hoc implementation using lists. However,
the FMap* modules seem to be lacking some basic facts, or I don't see
how to exploit the existing lemmas.
some (most likely buggy) ad-hoc implementation using lists. However,
the FMap* modules seem to be lacking some basic facts, or I don't see
how to exploit the existing lemmas.
I could prove some preliminary lemmas such as
forall A m, Equal (update (empty A) m) m.
forall A m, Equal (update (empty A) m) m.
However, it seems to me like there are always some "obvious" things which are missing.
For instance,
forall A m, Empty m -> Equal m (empty A)
forall A k e m, { M.MapsTo (elt:=A) k e m } + { ~ M.MapsTo (elt:=A) k e m }.
forall A k m, M.In k m -> exists e, M.MapsTo (elt:=A) k e m.
forall A k e m, M.MapsTo (elt:=A) k e m -> M.In k m.
For instance,
forall A m, Empty m -> Equal m (empty A)
forall A k e m, { M.MapsTo (elt:=A) k e m } + { ~ M.MapsTo (elt:=A) k e m }.
forall A k m, M.In k m -> exists e, M.MapsTo (elt:=A) k e m.
forall A k e m, M.MapsTo (elt:=A) k e m -> M.In k m.
From my understanding, the Map* functors provide many rewrites "for
free" via the "Generalized Rewriting" feature, however I don't see how
to obtain these facts from it.
free" via the "Generalized Rewriting" feature, however I don't see how
to obtain these facts from it.
Yours sincerely,
Frédéric Fort
Frédéric Fort
- [Coq-Club] How to use (well) the FMap* modules ?, Frédéric Fort, 01/28/2025
Archive powered by MHonArc 2.6.19+.