Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Simplifying pattern matching

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Simplifying pattern matching


Chronological Thread 
  • From: Wendlasida Ouedraogo <ouedraogo.tertius AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Simplifying pattern matching
  • Date: Sat, 30 Jul 2022 12:25:29 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ouedraogo.tertius AT gmail.com; spf=Pass smtp.mailfrom=ouedraogo.tertius AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi1-f172.google.com
  • Ironport-data: A9a23:AqiCYapfJ/Umr+djA+ONVoRjOWpeBmLcYxIvgKrLsJaIsI4StFCzt garIBmAPvveazP2KNhwbNm39h4EvJfVzoJjG1E/qixhEHgVo+PIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKicfHoZqTZMEE/Nszo68wICqtMu0IPR7z+l4 4uo+ZWAYwf9glaYD0pNg069gEM31BjNkGhA1rAOTagjUIj2yhH5pLpGTU2AByOQrrt8RoZWd M6fpF2NxV41yj92Yj+TfhkXRWVRKlLaFVDmZnO7wMFOiDAazsA5+v5T2Pbx9S67hh3R9+2dx umhurS6VUAFOZzdx94zDRVlKgpzJJ9Hw4H+dC3XXcy7lyUqclPpyvRqSUY3ZMgWo7ktR25J8 vMcJXYGaRXra+CemurqDLkxwJ19c4+yY9l3VnJIlVk1Cd4hXJ3PWazN6tgewDoqmsFTBt7RY sMYbXxkaxGojxhnYA9LV8xhwbjAan/XUgV9g0mQqfEO6E/X8jNsyrvnFvrNZYnfLSlSth/A+ jiuE37CKhodLZmUzSeP2mm9g/fG2yL9QoMbUrOinsOGm3WWz20XTRoXDB61+KbjzEG5XN1bJ gof/S9GQbUOGFKDRMW6cxqJsSG+kEAQZuN7HvQI6Tqz8/+Bi+qGPVQsQjlEYd0gkcY5Qz02y 1OE9+8F4xQ/4NV5rlrNpt+pQSOO1Ts9djBdOHdVJecRy5yy/9Fp10OnosNLSfbt1rXI9SfML ydmRRXSap0WhM8PkqK6pBXJ2m324JfOSQEx60PcWWfNAuJFiGyNN9PABbvzt60owGOlor+p4 iFsdy+2srlmMH11vHbRKNjh5Znwjxp/DBXSgER0A74q/Cm39niocOh4uW8jdR4wY5peKWG2M Cc/XD+9ArcDbBNGiocnM+qM5zgCkMAM6Py+C66KMIMWCnSPXFbXo3w0DaJv44wduBF0zftX1 WazfsGrAnIXYZmLPxLnL9rxJYQDn3hkrUuKHc6T503+jdK2OSDIIZ9YbwPmRr1otMus/VSOm /4CZpvi40sFDIXWPHKMmaZNdgBiEJTOLcqpwyChXrXTfFQO9aBII6O5/I7NjKQ+xfoIy7qSo CHtMqKaoXKm7UD6xcyxQigLQNvSsVxX9BrX5AQgYgSl3WYNe4Gq4PtNfpc7Z+h1++lqzPoyR P4AIp3SDvNKQzXB2jIccZit9Nw4JEr33VqDb3i/fTwyX598XAiWqNLpew3Y8iNRXCe6sM0Jp aKti1HASp0ZSgU+V8vbMar9z164sXUHtvh1Wk/EfotadEn2odplLiXwirk8JMRVcUfPwT6T1 gC3BxYEpLmV89VlroWR3a3d9tWnCepzGEZeDlL317fuOHmI5HenzK9BTP2MImLQWWbyz6OoO rdYwvT6B/sYxQoYvod5FYFr+qIw/d7YobFXk1Z/F3LRYlX3U75tLyXU3cRLsaERlLZVtRHsB hCK89hefLKIYYbrSQFLYgUiaeuH2LcfnTyLtaY5J0Dz5SlW+rubUBUNY0Pd1nQFdLYlYpk4x eoBudIN71DtgBQdNNvb3Dtf8H6BLyBdXqh75IsWBpTn1lgixl1YO8CODyb35NSIaowJPBB1e Hmbg63Ng7kazU3HKiJhGX/I1OtbpJIPpBEakwNYdgrRwoLI1q0twRlc0TUrVQAJnB9J5OR+Z zpwPEpvKKTSojpliaCvhYx3992t2fFYxqDw97fNvGjQTk3tUW2UaWNkZrzL80ce/GZRODNc+ dl0DYojvSnCJKnMMukaACaJaMAPifR+8wTDnIasGMHt81wSf2/+mqH3DYYXg0KPPC7y7XErY cFl+e9xbevwMit4T2jXzWWF/ex4dS1o71CujR2sEG3l0I0clPyPNeCyFn2M
  • Ironport-hdrordr: A9a23:32ttqat2vdBSYhgJDQ+uJ9+L7skDe9V00zEX/kB9WHVpm62j5q eTdZEgvyMc5wxhO03I9erhBEDiexLhHPxOkOss1N6ZNWGMhILCFvAG0WKN+UyFJ8Q8zIJgPG VbHpSWxOeeMbGyt6jH3DU=
  • Ironport-phdr: A9a23:C2Z5nRSPmPqc6lrC8i/MHYwK6dpsomeVAWYlg6HPa5pwe6iut67vI FbYra00ygOTBsOBsqMP0bSempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffQtFiCCjbb9vK Bi6ohvdu8gLioZ+N6g9zQfErGFVcOpM32NoIlyTnxf45siu+ZNo7jpdtfE8+cNeSKv2Z6s3Q 6BWAzQgKGA1+dbktQLfQguV53sTSXsZnxxVCAXY9h76X5Pxsizntuph3SSRIMP7QawoVTmk8 qxmTgLjhiUaOD4j6GzYhcx+gqxYrhy8uRJw35XZb5uJOPdkZK7RYc8WSGhHU81MVyJBGIS8b 44XAuUBI+lYqZTyp18UohulBAmjGfngwSJRiH/rw6I1zv4hHhvB3AwvGNIFrXPZrNLoNKgMT O+11rPHzTLMb/NRwzv99JbHcgo9ofGNQLJwatHcyUYqFwzfj1WQrZbpMC+S1uQIqmWW6fdrW u2zhWA9sQ5xviSvydk2ionPno8Y11TJ+yV7zYs2JNC1TFN3b9GnHZVeqi2XK4p7T8ImTmx0u Ss21rIItIC1cSUUypkqyRzSZ+CIfYWL/B/vSOmfLDFlj3xmYLKynwi+/VSkx+HmVcS50ExGo jdEn9TOrHwByh7e5taBR/Bg5EmuwyyP2BrW6uxcIUA7i67bK5k5z741jJUTsEDDEjbxmEX3k aOab0sk9vWq5uj5eLnmqZicN4h7igH6LKsigNCwAeM9MgQWXmib//qz1KH78EHnXLlHiuc6n 6rZvZzAOMgWp6y0DxVI3osh9RqzFzKm384ZnXkDIlJFYhWHj43xNlHJPfD3E+qwg062nzdsy PDGOaftAonTIXjZjLfhfKt961VHxQo8yNBQ/ZNUCrUbLP3vXU/xscTUDhkiPAOs2eboFM191 p8CWWKIGqKVLbvesUWU6eI3P+mMeIgVtS7hJPgi/v7ilGM2mVsAfaayxpYXc3C5HvF+I0qDe 3bsg9EBEX0LvgUkVuDqhkeCAnZvYCO5WLt57TUmAqqnC53CT8ajmu+vxiC+S6JbYGxCA0uNH X6gUJiJV+0Fby2VaptmjzEIT7GmRIhnyRy0qA7n0JJoK+PV/msTspe1h4s93PHaiRxnrW88N M+ayWzYFwmc/0sNTj4yh+VkpFBlj0yEye5+iuBZEtpa47VIVB07PNjS1b8yEMj8DyTGeNrBU 1O6WpO+GzhkSc88z8UHZEl6XcmvlAzCwjGCDLoclrjND5sxoerHx3akH89m0D7d0bU5yVwvQ 89BL2qj06li+gTJDonGlAOFmry2dLkH9CHI/WaHi2GJuRIQSxZ+BIPCW31XfU7KtZL560fFG qepEqgiOxBdxNSqL6JLbpjujAwDSq68YpLRZGW+n2r2DhGNrl+VRKztfWhVnCDUCUxf1hsW4 W7DLg8mQCGov2PZCjVqU1PpeULlt+dk+ju9SQcvwgeGYlcEtfL98wMJhfGaV/IY364V8CYnp TJuGV+h3tXQQ9Oergtlda9YbJsz+lBCnW7esgV8ONSnIcUAzhYZbgl7pUrp2BIxFohajck3t 1slyQNzLeST11YAPzKU0JbsO6HGf3Ho9UPKCeae0VXf3dCKv6YXva5g+hOz4UfwSBVkqio9g Lw3mzOG657HDRQfS8f0W0czrF1hoq3CJzI6/8XS3GFtNq+9tnnD3cgoDa0r0EXFHZ8XPaWaG Qv1C8BfCdKpLblgnEWkYggNO+9VsrI5Jd+nauCu16uiPeImlzWjxzcigsg1wgeX+ixwR/Sdl ZEYzv2C1wyIUHHggU29s93ssY9BbDAWWGG4zGK3YewZLr03doENB2C0JsSxzdgrnJ/hVUlT8 1u7Dk8H0sukEfaLR2T0xhYYlUEeoHj83DC90yQxiDYx6KyWwC3Jxe3mMhsBIG9CAmd43x/gJ o29jtZSW0bNDUBhkwao6VzzwKdc4rhyNXXSXFxgcC3/LmUkWay1/raPeM9A7po0vD4fCrztJ wDHDOej/F1DjHmrFnA7pnhzbzywv5TlgxF2wHmQKnp+tjuReM19wwve+M2JQPdQ2jQcQywr7 FufTlO4PtSv4ZCVj8KZ6rH4Bz/nD8MMN3C0l9Dl1mPz/2BhDByhkurmn9TmFVN/yirnz5xxU j2Oqh/gY47t3qD8MOR9f0AuCkWvjqgyUox4jIY0g4kdnHYAgZDAt30anGvpONJU3uTiYWARR CMQ69HQ6QnhnkZkKzjaouCxHmXY2cZna9SgNykRxy8x9clNB6DS8LFegSpouXK3qAvQZb52m TJXmp5MoDYKxuoOvgQq1CCUBLsfSFJZMSLbnBON99mira9TaTXnYf2q2UF5h9zkEKCar1QWR iPiYpl7V3wVjI03IBfW3Xb08I2hZNTAcYdZqEiPixmZx+lNdMBqy7xT1HIhYz6i+yVikbJzj AQyj8/m+tLccCM0ovr/WlkBZ1iXL4sS4m2/0/gYx57MmdjpRtI7Qn0KRMe6E6zuSm5D86S/c V7JSmV0q2/HS+WFW1bDrh439TSXVMn7UhPfbHgBkYc9GF/EfhEZ2EZMG2xk1p8hSlLznJynK RgmoGBXvhmi81NN0r46bkakFD6O+EHwLG9zEcb6TlIe7xketR2NYIrOs6QqRXEeptr480SMM jDJPV0WSzxZHBXVXRa7eeD/rdjYr7rCX7T4daCfJ+7U77QZDqbtp9rnxIJi+3zk2tynGH5kA rV730NCWSs8AMHFg3AUTDRRkSvRbsmdrRP6+yttr8n5/u65EATorZCCDbdfK7ANs1i/nLuDO uiMhS14NScQ15UCwmXNwaQe21hagj9ndj2kG7AN/SDXS6eYlqhSBh8dIyR9UakAp7o7xRVIM NXHh8nd07d5irsyCg4AWwW+wIemYssFJ2z7P1TCRQ6KOLmAOTzX0pT3bKe7GtgyxK1fsxy9v yreEle2ZGzS0Wm0EUnxbqcV03vIWX4W8JuweRtsF2X5GdfvaxngdcRykSVz2roswHXDKW8bN zF4NUJLtLyZqy1C0ZAdUyRM6GRoKe6clmOX9e7df9wRrPZnGC1zmOUc/Hkg17pI9wlLQfV0n G3Zqdsk8DTE2qGfjyFqVhZDsGMBnIWQoUBrIrnU7LFFUHfAuRUMtCCeUktQ4dRiDdLrtuZbz d2Fx8eRYH9SttnT+8UbHc3dLsmKZWEgPRTeEznRFAIZTDSvOAk3aGRSlfiT8jueqZ1o8/AEf bIBT7ZaUBo+EfZIUiyN/fQHKZZzGzQlyPuV1ZFSo3W5qxbVSYNRuZWVDpqv
  • Ironport-sdr: 7gVnuon5rb08Ht24I4OQ1VT5iH6Fa/Dr8kikSXZI1sUKUYHzF+/26V82CSzVwp2U/8TN3Mt2Ri h1ERQ2aMRG+DjrAt5YY7tZAeK1vvDzt3nzFTUYSsB9XYYIqMl/nJ69p4gvVZF0LdQn627jJrIz imzCPMfFBZAGQQTAVeY4Y+RZkLQkoOKoB1AzECsImfcd5mHEeCA4faRP0W+s36BgN1unabO+MD +AJvd4RjLEs78zVvQcNdjLxRsGJhLAeX0Qzh8IBiqI3mSX6Yvkb/h8iJESa90EA9VCRfiDjjet 6QOcO3A2a6dfwVcpFslvVKDD

Dear All,
I am currently working on programs that perform a lot of pattern matchings. I am looking for a tactic or an existing library that can help me to transform an hypothesis like:

opt = match h with
| Form_1 x => Value_1
| Form_2 x1 x2 => Value_2
...
| Form_n x1... xn => Value_n
| _ => Value_others

into

(exists x, h = Form_1 x /\ opt = Value_1) \/ (exists x1 x2, h = Form_2 x1 x2 /\ opt = Value_1) ... (exists x1 ... xn, h = Form_n x1 xn /\ opt = Value_n) \/ (opt = Value_others)

Is there a tactic that can perform such transformation? I usually perform this transformation using the "assert" and "case" tactics that lead to long proofs or a high number of subgoals. Any ideas?

--
Cordialement,
M. Wendlasida Tertius OUEDRAOGO
Mobile : 0751061208                                                                  



Archive powered by MHonArc 2.6.19+.

Top of Page