coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "D. Ben Knoble" <ben.knoble AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Fixpoint decreasing argument with remove_min in tree
- Date: Fri, 2 Sep 2022 14:37:31 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ben.knoble AT gmail.com; spf=Pass smtp.mailfrom=ben.knoble AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f51.google.com
- Ironport-data: A9a23:tWNrGqutf6D2NnvEMNL+cmzsvefnVEtfMUV32f8akzHdYApBsoF/q tZmKW+Ab6uJMTf1cosgOd7i8EkH7JHUzdU3SAI9/ihmRX9GgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCYEidfCc8IMsboUsLd9UR38g52rBVPyvX4 Ymo+5yHYgf+s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCnaG+WCcrFJbIo+ciSgIFLhhvAINX25aSdBBTseTLp6HHW37lwvErDUZveINFo6B4BmZB8 fFeIzcIBvyBr7jukfTrF6812JplcZCD0IA34hmMyRnTAPBgQpbESaHHzdBd1TY0wMtJGJ4yY uJEMGM3NkSaOXWjPH9NCr8s3/75iUX7amR4l0+uiYtw43LcmVkZPL/FdYC9lsaxbc5ShwOTo n/M13/oBwkTct2Z0zuMtHy27tIjhgv+UYMWUby/r7tk3QTVyWsUBxkbE1C8pJFVl3KDZj6WE GRMkgJGkET43BXDonTVD0XmyJJYlnbwmua8EtHWLCmIw6vQpgeeXy0KE2cHZ9shu8s7Azct0 zdlWj8v6SNH6NWopbC1r994bg9e/QAaKGYDYWkPSg5tDxzLvtQolhyWJjp8OPfdszA2cA0cB xiFqSE/g/MYistjO2BXO7zYq2rEm6UlhTLZKukasqxJI++5iEOYi1SU1GXm
- Ironport-hdrordr: A9a23:dnlTUqhwRYY2rTERDqkT493XT3BQXuMji2hC6mlwRA09TyX4rb HWoB1/73XJYVkqKRQdcLy7Scu9qDbnhP1ICOoqXItKPjOW3FdARbsKheDfKn/bexEWndQtsp uIHZIObuEYzmIXsS852mSF+hobr+VvOZrHudvj
- Ironport-phdr: A9a23:0QWTdRwDKURvhevXCzLhwFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z heZv6Q1xwaTAs3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmT owZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsip2e2+4YPfbgFUiDayfL9+M he7phjNu8cLhodvNrw/wQbTrHtSfORWy2JoJVaNkBv5+8y94p1t/TlOtvw478JPXrn0cKo+T bxDETQpKHs169HxtRnCVgSA+H0RWXgLnxVSAgjF6Bb6Xortsib/q+Fw1jWWMdHwQLspXzmp8 qVlRwLyiCofODE5/mPYhMx+gqxYvRyvuQBwzpXIYI2JLvdyYr/Rcc8YSGdHQ81fVzZBAoS5b 4YXAeYPM/xUpJTgqlQQqxu1GAyiBOXoyjBTgn/5w6M22PkmHA7dwgMgGcgCsHfSrNXyL6gSV f66wbLHzTXGdfxW2DP95JLUfRAmpPGBRLR9etfexkczDQ3KlEmQqZD7MDOP0OQAq2aV4vZuW +yhhGMrtg98rDexy8oyhYTEh4wbx1PK+Clnzos5OMO0RFN6bNOqFJZcqiKXOYtyT80tXW1kp Sg0xL0AtJWmciYKz5EnyATea/yBa4WI4xTjVPyQIThinn5ldqi/ihCv+kaj0u3xTte43EpOo yZfkdTBtmoB2wHS58WGUPdw/lqt1DCS3A7J8O5EO1o7la/DJp4h3LEwkp0TvFzGHiDsmUX2i LaadkQj+uS18ujnbLXrqoKGO497jQH+NasumsihDugiLgcOWG2b9fy91L3l40L5XK1HguMqn qTdqpzXJsQWqrSkDwJU04sv8RayAyq+3NQdh3YHLVZFeBydj4juPlHDOOv3Aum5g1i2kzdrw ffGMablAprTNXXDn7Lhcqx8605Y0gY80ddf55dMBrEHO/38QlXxu8DADh8lLwy0xP7qBMhl2 oMERW2PGrOZML/VsVKQ+u0vJPCMaJYJtzb5Nvgq/OXjjWQ5mF8YZammx4EbaHG+HvR8IkWWe 2DggtkbETRCgg1rR+vzzVaGTDR7ZnCoXqt66CtoJpihCNKJasblqrGHlAS9GZdSayoOXlqBF zHrcYKOX/okZyebI8snmTsBA+vyA7Q93A2j4Vepg4FsKfDZr3VwXfPL0dF047eWjhQu7XluC M/b1WiRTmZyl2dORjks3ak5r1Yugkyb3/1ehPpVXcdW++sPSh0zYJTRyap5Ddf4Xg/pcdKAS VLgSdKjUnkqVtxk+9YVeA5mHsm6yBXK3i6kGbgQwraGAto39KXW23XZKMN0ynKA364k3BE9W sUaE2qgi+Zk8hTLQY7El0LMj6GxaaEVxzLA7k+GxGuK+UBfCUt+DPyDUncYaU/b69/+4ysuV peIDrIqektEwM+GcO5Rb8HxyE9BT7HlMcjfZGS4nyGxAwyJz/WCdtiifWJVxyjbBEUe9mJbt X+bKQgzADugqGPCHXRvE1zoeUbl7eh5rjuyUEY1ywiAa0Ap2aCy/1YZgvmVSvVb2bxh2m9po ThyWlW72NjSBvKPogNgeONXZtZ8qFZL2GTFthBsa4S6JvMqjVoffgJr+kL2gk8vW8MQzI5z8 i1skVMhTMDQmElMfD6Zw53qb7jeK22ouQuqd7aTwFbVltCf5qYI7v087VTlpgCgUEQ4oBAFm 5FY1WWR4pLSAU8cS5X0Bww9+h48pLfdaC0wz4zR3Hxod6Kzt3WRvrBhTPtg0Rumc9pFZemOG Qm0EMsdDcyjAOMvklmtKBkDOaoBkcx8d9PjfPyA1qmxOe9mlz/zlmVL7rd21UeU/jZ9QOrFt 3oc68mRxRDPFzL1jVP799vyhZgBfzYZWGy21SnjAodVIKx0Z4cCT2m0cYW7wdB3hpilXHA9l hbrDV4AnsyvfhCWYnTy2ARR0QIcpnnvlSajzjNymi0kteLFhH2Ik7mkLURZfDMSDGB5xU/hO 421k8wXUC3KJ0AymR2p6Fy7j6lXqaJjLnXCFEJBfiz4NWZnAeO7sruPZdIK6Yt9630GFrThJ wnEFPig+kh/sWurBWZVyTEleiv/v5z4m0Y/k2eBNDNpq3Gff8hsxBDZ7diaRPhL3zNASjMr7 FufTlW6IdSt+s2Z0pnZteXrHWisUNtQdy7hyY6ouy6y5GksChq61aPW+JWvAU0h3Cn32sM/H y/FqlD/ZI7h06mSPuduf00uD1j5oZkfeMk2gs47g5ce3mIfj5Oe8C8ckGv9Bt5c3Lr3cHsHQ TNYi86Q+gXu31dva26Y34+sHGvI2dNvPpPpBwFekjJ49c1BD72YqaBJjTcg6ETtthrfOLB8h mtPkqZosS9CxbtV50x1iX/BSrEKQRsGYWq2zE/Oto7m6v0QPTfKE/D41VIiz47/Suja+EcEH i6+IM9qHDcsvJshdgiQgTujsse8P4OIJdML6k/LyVGZ064Mech3zr1T1U8FcSr8pSF3lLJ91 EYzm8n85M/edS1s5P7rW0YIcGSqOIVDvGmq1/8Wn97KjdnwRdM4S2lNBN2wCqv2dVBa/fX/a 1TUSGx6+irdQOCPW1fYsRgurmqTQcryaTfKdD9AnI8kHF7EdQRemFxGBmxk2MRiR0bxnoq5N x4og1JZrkjxrh8Gog5xHz/4VGqX5AKhazNuDYOaMAIT9AZJoUHcLc2Z6Ot3WSBe5Jyo6gKXe CSdYExTAGcFV1bhZRirN6Sy5dTG7+mTB/avZ/rIb7KUrOVCVvCOjZux24pi9jyIO42BJH5nR /E830NCWzh+FaG7030XTDcLkivWc8OBjBK1+ykyr8fmtfq2AUTg4oyAD7YUOtJquli3jaqFK ++MlXN5JDJfhfZujTfDzLkS2kJXijk7LWH8V+Rd83eTEuSNw/wybVZTcS54OcpW4rhp2wBMP ZSekdbpzvtiifVzDV5ZVFvnk8XvZMoQImj7OkmUYSTDfLmAOzDPxNn6JK2mTrgFxu9ZsVuzv zGRF0LLMTGKlj2vXBeqe7Ip7mnTLFlFtYexfww4Q3DkV87jYwanPcVfiDQ3xfg1gSqPOzNFd zd7dExJo/ub6iYS0ZAdUyRRq3FiK+eDgSOQ6eLVf40XvfVcCSNxj+tG4X4+xtO9CQlLQfV0n G3Zqds8+zlOfcGAzzNmVFxFrTMZ3epjXG1nMKTds5hHADPKoUtL4mKXBBAH4dBiD4+3050=
- Ironport-sdr: vIFZQI7SdH3obe3REaETlmSxNcQZu4zasYNspC2L+kam+XF8OLY9/R2gV7Gemm17WEpFQQ7BuG wva3IzBEPFOVqxCobw1pine+Fudyj3aSQJTnlyCiUnOZX9r+oWH9JuxeEkBeQMwhNgowtVn80o z0xD2eRInsYxb48oYupiQWZkn/cNQU3luH+JthDKYZdr29Cr5R+sOQsP1rWhnMWqbtPKTU1EKh ZyzV/RJs/3ojmGggs9MAby8FZYvyO8k3et53YlcxWxFjK5l+f2u4d3p8hezaiXT5kaRJ87xSoS F2A=
You might need `{measure}` from `FunInd`'s `Function`:
https://coq.inria.fr/refman/using/libraries/funind.html
This will require a proof that the measure function is decreasing in
recursive calls (I've used this before with a list that Coq could not
see shrinking, but whose length was smaller by 1 in recursive calls).
D. Ben Knoble
On Fri, Sep 2, 2022 at 1:42 PM Suneel Sarswat <suneel.sarswat AT gmail.com>
wrote:
>
> 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+.