Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree


Chronological Thread 
  • From: mukesh tiwari <mukeshtiwari.iiitm 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 19:00:05 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf1-f42.google.com
  • Ironport-data: A9a23:ngHw96C/Q6ROlhVW/wflw5YqxClBgxIJ4kV8jS/XYbTApGlxgj1Uy GEeXWuHM6mKajb1Kt5ya9jl9k8B7ZbUyN8xOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yE6j8lkf5KkYAL+EnkZqTRMFWFw0nqPp8Zj2tQy2YnhWFvX0 T/Pi5S31GGNi2Yc3l08sPrrRCNH5JwebxtF1rCWTakjUG72zxH5PrpHTU2CByeQrr1vIwKPb 72rIIdVUY/u10xF5tuNyt4Xe6CRK1LYFVDmZnF+A8BOjvXez8A/+v5TCRYSVatYozjYnMBMk PdBjIOhbi4HBYHFvPQzVBYNRkmSPYUekFPGCX22sMjWy0OfNnWwmbNhC0Y5OYBe8eFyaY1M3 aZAeXZdM1ba2b3wnOjTpupE3qzPKOHuIYASoXF8zC7QF/dgQJHCX6Di6tpR3TN2jcdLdRrbT 5BDNmo3NEScC/FJEksWArIf3/WIun6hSgdfskPJvao2xWeGmWSd15C0aIaPEjCQfu1emV/dr Wbb9UziExQCPZqezyCE+zSinIfycTjTXYsTEPi8+KcvjgHJgGMUDxISWB2wpvzRZlOCt8x3J h0X6hd2j6QL612MZ/fGcxScsFCDsUtJMzZPKNES5AaIw6vSxg+WAGkYUzJMAODKUudmFVTGM XfZz7vU6SxTXK69Ei3Cq+/Fxd+mEW1Ecj9YPH5soR4tuoG7+OkOYgTzosGP+ZNZY/XwEDD0h jSE9W0w2+9VgskM2KG2u1vAhlpAR6QlrCZlu207vUr/tWuVgbJJgaT2tTA3Ct4ed+6koqGp5 iRspiRnxLlm4WuxvCKMWv4RO7qi+uyINjbR6XY2Qcd7rmj2pyT9JtANiN2bGKuPGpZUEdMOS B+D0T69GLcOVJdXRfQqO9rpVpxCIVbITI29C6m8giVyjmhZLVfbpkmClGaf2GfilEVErE3ME cbzTCpYNl5DUf4P5GPuGY81iOZ3rghjmz67bc2kl3yPj+DCDFbLEuxtGAXVPogEAFas+lq9H yB3bJvUlX2ykYTWPkHqzGLkBQ5WdCVmXsip8qS6tIere2JbJY3oMNeJqZtJRmCvt/09ej7g8 i7vV0lG5kD4gHGbewyGZmoyOrzqVJd763k8OHV0b1qv3nEiZ6ep7bseJ8NnJ+l5qLQ7wK4mV eQBduWBHu9LFWbK9jEbWp/3895veRGtsgSRMnf3ezM4ZZNhG1fE94a8LAvi/SUDFAStss46r +Hy3w/XW8tRSAFrDcKQY/WqlgvjsX8YkeN0fk3JPtgDIBW2oNY2c3T816ZlLdsNJBPPwiqh+ zyXWRpI9/PQp4IV8cXSgf/WooqsFdx4FBUIEmTe64GwKnCGrGeuxIl3UNGIcyrYY2X69fjwf u5S1fz9bKQKkVsW4YpxF7FnkfA369f1/eQIyw1lGDDPYQ3uBO86ZHaB2sZLu+tGwboA4Vm6X UeG+997P7SVOZO6TARAelJ9NunTh+sJnjTy7OguJBmo7iFA+rfaA15ZOAOBiXAAIbYpYpkpx /wt5Jwf5wCl0EF4N9+HimVQ+T3JICBaFaogsZ4eDcngjQ9ykgNOZpnVCynX5pCTaoUTbhN7f GfM3KeS1a5BwkficmYoESSf1+Rqg5lT6gtBy0UPJgjUl9fI7hPtMMa9LdjqosVpIhR7PyZbP 2FqMwhxK/zL8WsywsdEWG+oFkdKAxjxFokdDbcWvDWxcqVqfjWlwK4B1SKl80UQ8mYadT9el F1d4HiwSi7kJakdwQNrMXOIaJXfoRhZ+QjLmcThFMOAd3X/jfwJnYf2DVc1R9Db7Q/dSaEJS SSGPAq9VEEjCRMtng==
  • Ironport-hdrordr: A9a23:LHATVqgIdDaEDyV6RyEHJTCTenBQXuMji2hC6mlwRA09TyX4rb HWoB1/73XJYVkqKRQdcLy7Scu9qDbnhP1ICOoqXItKPjOW3FdARbsKheDfKn/bexEWndQtsp uIHZIObuEYzmIXsS852mSF+hobr+VvOZrHudvj
  • Ironport-phdr: A9a23:pVHVsh0wnXsAc2vZsmDO5w0yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaEo6881hSQB9+TwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnA JYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7ye6/94fNbwhMmjaxbq5+I AuooQ7MqsQYnIxuJ7orxBDUuHVIYeNWxW1pJVKXgRnx49q78YBg/SpNpf8v7tZMXqrmcas2S 7xYFykmPHsu5ML3rxnDTBCA6WUaX24LjxdHGQnF7BX9Xpfsriv3s/d21SeGMcHqS70/RDOt4 bp2SB/zkCcIKSI28H3ZhMx3iaJUuhOhpxpiyILQb4yYMP9yc6XAdt0YWGVBRN5cWCNPAoy+b 4UBAekPM/tGoYbhvFYBtweyCBO2Ce/z1jNFhHn71rA63eQ7FgHG2RQtH9cTsHTXstr1L6cSW v2pzKnJwzTMdelW2Tbg44XPdxAhvPKMUqxrccrR1UkvFg3EgU+KqYzkJT+V1+UNs2mH7+plT u+vhGsnpBtwojir3Msjlo7JhocMx13C6C52z5o7K8eiR05nfd6rDoFQtyeCOoZ3X84uXmFmt SQnx7AFtpC2YCcHxZc5yxLCd/GKcIeF7BztWuuTITp0mm9odK+xihuu8UWs1+PxW9W63ltIs CdIlMTHuH4K1xzW8MeHS/1981+u2TaOywDT6vxELlsumaXHLJ4hx6Y8loEPsUvZAiD2m0L2j LGIeUU+9Oio7+PnY7v8qpCAMI90jxnyMqsvmsyjAeQ4LxMBU3Ka+eS70rDo4E73QK1Sg/Eoj qXUtIrWKMcbq6KjHgNY04Qu5wywAju41tkTgGMJI0hfeB2diojkI1HOL+78Dfe4m1mslS1kx /HCPrH4BpXNIGXPnK7vfbty9UJQ0gUzzddY55JbDrEOPuj/VVP2tNzdFhM5Mgq0zPj7CNhly I8SRWaCDrWaPa7Sq1OE++MiLuuWaIIapjrxM/0l6OTvjX89l18dZ66p3Z4PZXC9A/RmIFuWY WHsgtcdEGcLsBAxTPbriFGYUD5TZneyX7455jwgB4KmCJ3MRoGpgLCbwCi7GZhWanhACl+XC XjobZmLW+8QaCKOJc9siiEIWaC7S4A9zRGuqBP6y71/I+XI/S0YrIvv28Rx5+3Ojh4/7id0D sSY02GVVW54hGIIRzks3KB+u0Nx0FmD0bIry8BfQNdU/rZCVhowHZ/a1e1zTd7oCSzbedLcT UulT86mSS0wUdsrwpdaZlt+Fs6ikhHc1jCrRb4UlqCOLJMx+6PYmXP2IpAumD79yKA9ggx+E YN0Pmq8i/sjpmA7ZqbMmkSdzOOxcLgEmTXK7CGFxHaPu0dRVEhxV7/EVDYRfBietsz3s2XFS bLmErE7Kk1Z08fXL7ZJZ8bpkVRZTe3iftXfYn60s2i1DBeMgLiLadmiYH0TiR3UE1NMiAUP5 TCDPAk6CD2mpjfbET9jDlLzYlzl6+g4qXK6UkocwASDbkkn3L2wqVYOnfLJbfQV0/ofvTs57 TV5GFHox9XNF9+JvBZsZo1ZaNI5pVNJjCfX61Y7MZunIKRvwFUZdmybpmvI0BN6QsVFmMku9 zYxyRZqbLmfyBVHfi+Z2pb5PvvWLHPz9Vahcfye3FaWy9uQ9qoVjZZw41z+oAGkEFYj+HR7w pFU1XWb/JDDEAsVV9r4TE828xFwo7ySbDM64svY0nhlMK/8tTGnuZphAfYmxw2gY9ZAObmFU g7zEtEfL8erIe0u3VOua1NMPexf8rI1I9Lzb+GPi8vJdK5rmDOri3gC4ZgoiBrdsXohDLeWg NBZmaL9vEPPTTr3gVa/v9qinIlFYWpXBW+j0W3/A5YXYKRufIENAGPoIsutx9w4iYS+PhwQv FOlGV4C39ekPBSIaFmolwhN1kkMoWCmhiKiznp1kjA1q4KQ2SXPx6Lpcx9NaQspDCFyyEzhJ 4S5lYVQWVWrYhMpiBq67Fz7galapbh6B2bWSEZMOSPxKisxN8n4/qrHaMlJ5pQytCxRW+npe lGWRIn2pB4C2j/iFW9TrNwiXwmjoY6x3xlziWbGaW12sGKcYsZogxHW+N3bQ/dVmDsAXihxz zfNVBCwONyg/NPckJmm0Kj2Un+iW4ZTbSj0xJmB8iq65HFvKRK6lvG33NbgFEA23DT62N9jS SjT5EykM8+7iuLjb70hIhMgDUSZiYIyAoxkl4osmJwckWMXgJmY5ztPkGv+N8laxbOraXMMQ TARxNuGqAPh2UBlMjeI39ejDiTbkpYnPoflJD9MiUdfp4hQBayZ7aJJh35wq1u89kfKZORl2 ywa0b0o4WIbhOcAvEwsyD+cC/YcBxo9X2SkmhKW4tS5tKgSanyodO360Vd9kMuhELCdqxtdH nf4e4snNSB158R7dlnL1Tegj+OsMMmVdt8VuhCOxl3FkutYM5Itl+UDnyshOGP8oXgNxOsyj Bgo1pa/9tviSS0l7OeyBRhWMSfwbsUY92T2jKpQqc2R2pimApRrHjhYFIutV/+jFyge8Oj2L wvbWiNpsW+VQPCMeG3XoFcjtX/EFIqncm2aNGVMh8s3XwGTfQRemFxGB2h8x89hUFr2m4q5N x0lrjEJugym9l0WkbkubkenFD+Y/VbNCH98SYDDfkQIqFgavQGNd5TZtLo7HjkErMP/6lbRe yrLP0IQSjtREk2cWwK8ZP/3uZ+ZorLeXq3nf56sKf2PsbAMCKvOnMjylNMgp3HVaI2OJiUwV qVrnBMcAjYpXZyewWxHSjRLxXuSNIjC9Uv6omsv6ZnhlZajEAP3udnVU+oUYYgpokrmx//Eb rHYhT4le2wBiNVRlTmRmeJZhBlL2mlvb2X/S+1e83SWHeSLwOkPSEdKDkE7fN1B66Z2tuVUE ejcjN69lrtxj/puTkxASUSkgcaxI8oDP2C6MlrDQkeNLrWPYzPRkYnxZuunRLtcgf8x1VX4s CuHE0LlIjWIliX4HxGpP+ZWiSiHPRtY8IijexdpAGLnQZrocBq+eNNwiDQ3x/UziBaofSYEN iNgdkpWsrCKxSZRg/E6H2IYq3Q5d6+LnCGW6+SeIZET8LNqDilyi+NG8SE6xr9Sv0QmDLR+n CrfqMIroknzyLHejGo6FkMQ9XAX3tHu3w0qI6jS+5heVGyR+RsM6T7VEBEWv55+DcWpvalMy 9/Jnaa1KTFY8tuS89FPYqqcYM+BLnclNgLkXTDOCw5QBzu2NmzEh1Bcj/iI9zuUr5kmr7Djn ZMPTvlQU1l/RZZ4Qgx1WccPJpt6RGZuibmAkMsB/maztjHUTcRe+5TJD7ecXa+pJzGegr1JI RAPxPmrSOZbfp2+0EtkZF5gmY3MEEeFRtFBrBpqaQosqVlM+nxzJoXc803gYwKppnQUEKzt9 vbXog53YOBo8Dm1pllrfBzFoyw/lER3ktLg02j5mNvZI6K5XIUQAC3x5RBZDw==
  • Ironport-sdr: hKbQhNQNoS2S/nT5qdFrxVWYsPC385SWlQabOHiGKWoHNZdVF1qbqMUoNmYGZIuM/DsSgLZWZo ga/GI7bElTbH+4AgPsM9WuNn6Lswj9rnLgFlrtLSk5zlgNbjdjYeNvxKbWhiGD57PljYLoPxUm H30ZQZ55AMSrs+HKR5YFGL2dgeAaOzVpFPFv3ti0YerbPT6Jxr5Asc63/AQnQsCxN7fbLBhRvq gvAYJh2pRuoulBXlb5ovi2Jyf4poMf6CYCJ6DXD34HB10Rnx/OT1TiWNwqtPQry2sWKC+8o5lf oSEpUQzDQ5OCt+s9aCmrzmzt

No problem. Also, if you are into reading Coq codes, then have a look at Dominique’s library [1]. 

Best,
Mukesh 

[1] https://github.com/DmxLarchey/The-Braga-Method/blob/main/theories/utils/measure_induction.v

On Sat, 3 Sep 2022 at 18:08, Suneel Sarswat <suneel.sarswat AT gmail.com> wrote:
Dear Mukesh,
Thanks for the solution. This is the kind of generic solution I was looking for. I did an unsuccessful attempt with
passing n with (prf : n = M.cardinal tb) mentioned at link. Your solution is very close to the second answer, I guess.
The code along with details is extremely helpful.
Thanks again.
Suneel


On Sat, Sep 3, 2022 at 5:34 PM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:
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, 
Mukesh 


On 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.html




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






Archive powered by MHonArc 2.6.19+.

Top of Page