coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Suneel Sarswat <suneel.sarswat AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree
- Date: Sat, 3 Sep 2022 22:58:38 +0530
- Authentication-results: mail2-smtp-roc.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-ej1-f45.google.com
- Ironport-data: A9a23:oN6NYakpy3ay0oon1xd7mwLo5gyjIERdPkR7XQ2eYbSJt1+Wr1Gzt xIfC2/SOPmMM2Kket4lb4S3p0oO65/SzINjTQNrrS5kE1tH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvykTrSs1hlZHWeIcg944f5Ys7N/09UAbeSRWVvX4 4uj+5aHYjdJ5hYtWo4qw/LbwP9QlK+q0N8olgRWiSdj4TcyP1FMZH4uDfnZw0nQGuG4LcbmL wr394xVy0uCl/sb5nxJpZ6gGqECaua60QFjERO6UYD66vRJjnRaPqrWqJPwZG8P4whlkeydx /1kqKfhDjgiMpfShcEmXxZpVDkvFvJvreqvzXiX6aR/zmXDenrohvhsVQQ4YdBe9eFwDmVDs /cfLVjhbDjZ37PwkO/9ELA8wJh+RCXoFNt3VnVI1izfAPsiB4vKWb7V7MNw0zI5h8QIFvHbD yYcQWc2NUqbOEUUUrsRILVunNmauDrTSDdBhRGojLgd7GXdzzUkhdABN/KMIoDQLSlPpW6To XuD9GDkCDkBJdmHwHyE9Gitj6nBh0vGtJk6EbS58rtnggTWyDBOThIRUlS/rL+yjUvWt89jx 1I80zcV/O8N/0CRUMTYZBG3kTmc7zVDco8FewEl0z2lxq3R6gefI2ELSD9dddAr3PPaoxR6h jdlePu5VVRSXK2ppWG1rejL8GvjUcQBBSpTOn9eFFptD8zL+dlr1nryosBf/LlZZ+AZ9Bn1y jGO6SU83vAd0ZNN2KK88lTKxTmro/AlrzLZBC2GBgpJDSsjPOZJgrBED3CFsp6sy67HEzG8U IAswZT20Qz3JcjleNaxaOsMBqq1wP2OLSfRh1Vid7F4qWr3oiL4IdoOu2EjTKuMDiriUW+5C KM0kVMBjKK/wFP3BUOKS9nsU5xykPCI+SrND6mMM4MmjmdNmP+vpXkyPyZ8Lkjil08jlaxXB HtoWZfEMJruMow+lGDeb75Fj9cDn3lirUuOG82T50n4idK2OiTJIZ9bawDmRr5ivMu5TPD9q Yk32z2ikEUBDoUTo0D/reYuELz9BSZnXM2r8JQIL4Zu4GNOQQkcNhMY+pt5E6QNokifvr6gE qiVVhAKxVzhq2fALAnWOHlvZKm+D5l6pHM/eycrOA/wiXQkZI+u6oYZdoc2LeF3rrw9kaYsQ qlXYdiED9ROVi/DpGYQYJz7m4poK0amiAeICCy6bWVtZJVnXQHIpoTpc1K3pikDBya6r+Ukp Lik2l+JSJYPXVUwA8PfafbpxFS05CBPlOV3VkrOA99SZES8qNgwe3Kt1qc6epheJw/Cyz2W0 xetLS0Z/eSd8ZUo9NTphLyfq9j7HuZ7GH1cFTaJ4LuzMx7c4TP/k4JNVeC/fQfdWnnxz6Osa LgH1Pr7KvAGwA9HvocgQbZmyaUyu4nmq7NAlF82GXzKaxGmCOolLCXbm8ZIsaJJy/lSvg7vA hCD/dxTOLOoPsL5EQ5OeFB0MLzbjfxEyCPP6fkVIVnh4HMl9rSwV0gPbQKHjzZQLecoPY55k /0tvtUat162hhYwaI3UiylV8yGBLCVFXfl68J4dB4Dvh0wgzVQbOc7QDSr/4ZeubdRQMxl1f mXF2vKa37kMlFDfd3cTFGTW2bYPj5o5vh0XnkQJIE6Em4aYi/I6tPGLHe/bkuiIItR7P+NP1 qxDMkR0IeCD/W4tipQeGW+rHA5FCVuS/UmZJ57lUoHGZxHAa4APBDRV1SWxEIQx/GdVfzwd9 7adoIogeSi/Z9n/h0PeRmY8w8EOjrVNGsnql8WuHsDDFJ4/CdYgbmlCekJQwyba7QgNaIEra AWkECucqUE2CMLIn5AGNg==
- Ironport-hdrordr: A9a23:QUds5KsvUh7ugy/94Wlzq35a7skDT9V00zEX/kB9WHVpm62j5r mTdZEgvyMc5wxhPU3I9erwWpVoBEmslqKdgrNxAV7BZniDhILAFugLhrcKgQeBJ8SUzJ876U 4PSdkZNDQyNzRHZATBjTVQ3+xO/DBPys6Vuds=
- Ironport-phdr: A9a23:ZvKRPhK9iDGCV+fTjdmcuNJsWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCFvrM33QWCBNyFo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/689pHJfQlFgCSxbbxvI BmrrAjaq9Ubj5ZlJqst0BXCv2FGe/5RxWNmJFKTmwjz68Kt95N98Cpepuws+ddYXar1Y6o3Q 7pYDC87M28u/83kqQPDTQqU6XQCVGgdjwdFDBLE7BH+WZfxrzf6u+9g0ySUIcH6UbY5Uiml4 Kl2VR/okz8HOCAl/2HLhMJwi6dbrwigpxx53oXYZI6YOf57cq7bYNgUR3dOXtxJWiNODIOzb YsBAeQCM+hFsYfyu0ADogGiCQS2Hu7j1iNEi33w0KYn0+ohCwbG3Ak4EtwTrXTUqsv6O7kWU euo0afH1y/Db+hY2Djn9IjDbxcsoeqRXbJ2b8Xe100vGxnejlqKs4zlJD2U2f4Rs2WA4OpgU Pigi28jqw1rvjevwcIsh5DPi4kIxV/K6T93z5wpJd2kVkF7e9ikHYNeuSyEKod7X8wvTmNpt Ss71rAIt4O2cSkXxJkmxRPTdfyJfoyU7hztSuqdPTd2iGxmdb+jiBu/9VSsxvP+W8Sp1ltBs yRLkt7Jtn8X1hzT7NCKSvR8/ke92TaPyhvc5vtYLkAzkKrXM5Ehwr8slpoTrETMBTX6mETxj KKQa04q+fCo5vz5brn6opKQLYx5hwHkPqgwh8CyAv40PwcOUmWd5O+yzqfs/VfjT7VPlvA2k rfWsJTdJckDo662GQ5V0oI65xmhDTeqzc0UnXcIIV9FYh6HgI/pO1bBIPD8E/izmUijkDBux /zeP73hBIvCLmTbnbv/Ybpw71RQxQkzwNxF+Z5YF7IMLOj8V0LxrNDYCwU2Mw2ww+bpEtV90 YYeVHqUAq+ENqPdr0GH5uY1L+mXfoAVoi39KvY/6P7ylnI5llodcrOo3ZsTcny3AvNmI0CBb XrqmdgOCX0KsRYmTOz2lF2CViZea2uqU6Im+j47EJ6mDZvERo21nLOB2z67EoRKaWBCF1CDC mzld56EWvcJcCKdONVtkj0CVbi7So8uzwuitAHgy+kvEu2B8SoB8JnnydJd5uvJlBh0+yYnI d6a1jS2Umd5k2dAfDYsx792vQQp0UqF3KV8xedRD8dM7u9hXQIzNJqaxOt/XYOhEjndd8uEH Q71Cu6tBis8G45gqzdvS0N0GtH4ywvGwzLvGbge0bqCGJ0z9KvYmXn3Pcd0jXjch+E6l1dzZ MxJOCW9g7JnsRDJDtvSjkOUmqLsbq0GxzHE6E+MyGOPuAdTVwsjGb7dUyUnb1DN5c/8+luES ravDbo9NQ4U0tOEJ6ZOLMbgl05ZTevLN9HXYmb3kGC1Vl6T3r3ZSo3sdi0G2TnFTkgJlwdG5 XGdKQ03HTusuUrbBT1qUF/tOgbirbQ4p3S8QUs5iQqNaiWNzpKT/RgYzbyZQvIXhPcfvTs57 i9zFxC71s7XDNyJo0xger9daJUz+gUP02WRrAF7MpG6SsIqzlcDbwR6uV/v3BRrG81Bl8Ytt nYj0At1L+qRzlpAczqS2Z24NKfQLyH++xWmaqie3V+7sp7e4boJ5fk87U7qphq2H1YK/HBu0 t0T2HyZp93LAAcUTZPtQxMv7REpwtOSKiI55o7SyThtKfzu6m6Ei49vXrJ1jEr9LLI9eOueG QT/EtMXHZ2rIe0uwR2yaw4cefpV/+gyNt+ncP2P3OiqOvxhlXSolzcigsg130SS+i57UuON0 YwCxqTSxRaBWjr4ykyoqNvokJxsajQbH275wi/hTt00BOU6bcMQBGGiLtfijM5jgZPgXzhD/ US4GFoa8MCscBuWKVf62EcDsCZf6Wzikiy+wTtuljgvpafKxy3CzdPpcx8fM3JKTm1v5bv1C bC9lMtSHE2hbgxz0QCg+V6/3a9Q4qJ2M2jUR05MOSnwNWBrFKWq5PKOZMtG6ZVgtisyMqz0e k2cR7P55QATyTj8Fnd2yzUydjXssZL81xB3k2OSKn9voWGRI5khg0eCooaFFbgNg3IPX0waw XHPC0K5PsW18NncjJrFvu2kFiqgWpBVbSj33NaFvSq/63dtBE73lPSyl9v7VAkihHWjhp86C GOS9Ua6PtS4ssbyefhqdURpGlLmvs9zG4Uk15A1mIlVw38RwJOc4XsAl273d9Rdw6P3KnQXF ltpi5bY5hbo3Ep7IzeH3YX8Az+G381sat38eWoMwT008+hFDa6V6PpPmi4/8T/a5UrBJONwm DsQ065k82McjuwN/hEk1D6CC6w6EkxRPCiqnBONpYPbzu0fdCOkdr6+01B7lNaqAeSZow1Sb 33+f48rAS566sgseEKJynD47ZvoPcXBdd9G/APBiA/O1qIGTfB53upPnydsPnjx+GEo2/Jux wI7xom05cCGMzk/p///W08AcGepOIVLvWuxxadGwpTIg8b1Rc4nQ2tTGsOvFKPNcnpatOy7Z VjQVmRk8DHDX+KYR1fX6V86/SyRVcr3ZjfHfD9Bio86DBiFeB4A2kZNAHNjz8R/TkfzlKmDO A94/mxDuQK+80ERjLoub16mDC/evFv6M29kDsHAc1wGqFkFvR6dMNTCvLssRGcBr8Hn9ErVb TXFAmYARWARBh7eXwGlbuTovIOQtbDfX7X2LuOSM+/X96oDB7HRlMjpisw/rn6NLpndZCA8S adgiwwYBzYhXJ2I/ldHAzoekyaHByKCjDG7/CA/7sW28fCxHRnq+ZPKEbxZd9Nm5xGxh66Hc e+WnidwbzhChNsKwjfTxb4T0UR36WkmfiSxEbkGqS/GTb7B0q5RARkBbipvNcxOp6si1whJM MTfh5v7zLl9xvIyDl5EUxTmlKTLLYQSJHqhMVrcGEuRHLGPJDmOzsOuJK3gFPtfi+JbsxD2s jGeUgfiMjmFizj1RkWvPOVL30T5dFRVvICwdAooCHC2Foq3LE3mdoUu3XtqnO5R5DuCL2MXP DliflkYq7SR6XkdmfBjAylb6XEjK+CYmiGf5u2eK5AMsPItDD4n8oASqHk81bZR6zlJAfJvn y6H5MVzpVyrlq+UwyB8TxNSgjlOjYOP+05lPO+Kk/sIEWaB5x8L4WiKXl4SoMB5D9T0p61K4 t3Glaa2JTUbttyIoI0TAM/bLM/BO30ke0mMenacHE4OSjilMnvajkpWnaSJ93GbmZM9r4Dlh JsETrIzvLkdGfYTC0AjF9sHcs8fttIMlLeaiIsF5yP7okWMAspduZ/DW7SZBvC9cF5xYpFLY hIJxfXzKoFBb+XG
- Ironport-sdr: pb/GvsMo4t+5iyCou5mmp4nqcok4BQDf8G6ZVOocEuKudi+k5xG6sJABiirBCvZdR3Gr8qkSLY IEAVJJWzQAw8mGIMyTkZpbetrW+lJughzgspM5O22TnqIM8xehjJASQnXevo30Qd4IRt8Nbje7 9ktHcMji48eTMAQU07oBbFLjibenBTA28vzM20sw7snR7mJVDgHXuKYx47Zpx+UOwEjRteco4x UM6zeRwzh8nTwZMUfyTqMnk2ozPYOAXWViXHbbt7W9RXYQ0bvgRX03xdrJa22yW85e1mxQPwQR Ur81Yub1qAlkhmndtU+811MM
Thanks Pierre again. Will look into the book when I have this. I was also thinking of this book for the chapter on Module.
Thanks again,
Suneel
On Sat, Sep 3, 2022 at 6:59 PM Castéran Pierre <pierre.casteran AT gmail.com> wrote:
Hi, Mukesh and Suneel,Indeed, if you are working on binary search trees, you may write two structurally recursive functions.The following code is given without any formal guarantee (i.e. proof), since it is a ***manual*** translation in Coq of the code extracted from a proof on search trees( chapter 11 of the coq-art). The potential errors may come from typos made during this translation back into Coq.PierreLe 3 sept. 2022 à 14:03, mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> a écrit :Hi Suneel,I have written the function [1] but it hinges on an admitted lemma [2], which requires you prove that when you delete an element from a tree, the size decreases. The idea is same as suggested by Pierre because ‘remove_min’ is not structurally recursive and you need to use well founded induction.Best,MukeshOn Sat, 3 Sep 2022 at 09:34, Castéran Pierre <pierre.casteran AT gmail.com> wrote:Removing the minimum element of a tree doesn’t give you a subtree (structurally speaking) of the original tree.Nevertheless, you can define a function by well-founded recursion over the tree’s size.- First, notice that removing an element of a tree strictly reduces its size- you will find some examples of well founded-recursion in https://mattam82.github.io/Coq-Equations/examples/Examples.Basics.htmlLe 2 sept. 2022 à 19:42, Suneel Sarswat <suneel.sarswat AT gmail.com> a écrit :Dear friend,Is there a way to write a fixpoint using a tree such that in each recursive call the tree after removing the minimum element is used?I am getting the following error.Require Import MSets MSetRBT ZArith.
Module M := MSetRBT.Ops Nat_as_OT.
Fixpoint test (tb ta : M.t)(a:M.elt) :M.t.
destruct (M.remove_min tb) eqn:H.
destruct p eqn:Hp.
unfold M.elt in a.
destruct (a-e) eqn:Hae.
exact (test t ta a).
exact ta.
exact ta.
Defined.(* Cannot guess decreasing argument of fix. *)Also the {struct tb} failed.
- [Coq-Club] Fixpoint decreasing argument with remove_min in tree, Suneel Sarswat, 09/02/2022
- Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree, D. Ben Knoble, 09/02/2022
- Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree, Suneel Sarswat, 09/06/2022
- Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree, Castéran Pierre, 09/03/2022
- Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree, mukesh tiwari, 09/03/2022
- Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree, Castéran Pierre, 09/03/2022
- Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree, Suneel Sarswat, 09/03/2022
- Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree, Suneel Sarswat, 09/03/2022
- Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree, mukesh tiwari, 09/03/2022
- Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree, Castéran Pierre, 09/03/2022
- Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree, Suneel Sarswat, 09/03/2022
- Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree, mukesh tiwari, 09/03/2022
- Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree, D. Ben Knoble, 09/02/2022
Archive powered by MHonArc 2.6.19+.