Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Suneel Sarswat <suneel.sarswat AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Fixpoint decreasing argument with remove_min in tree
  • Date: Fri, 2 Sep 2022 23:12:18 +0530
  • Authentication-results: mail3-smtp-sop.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-f47.google.com
  • Ironport-data: A9a23:ioDE4KxO6AGL5g98SoR6t+cuxyrEfRIJ4+MujC+fZmUNrF6WrkUDy GdOWDiFOK3ZMGagf412at6+phwCv5/QyN9mTwo9pVhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefQAOCU5NfsYkidfyc9IMsaoU8lyrVRbrJA24DjWVvc4 Ymq+KUzBXf8s9JKGjJMg068gEg31BjCkGtwUosWOJinFHeH/5UkJMp3yZOZdxMUcaEIdgKOf Nsv+Znilo/vE7jBPfv++lrzWhVirrc/pmFigFIOM0SpqkAqSiDfTs/XOdJEAXq7hQllkPgr5 fFOpJfsVD4OFYnUpvwiUhlaOSdxaPguFL/veRBTsOSWxkzCNnbumrBgUB5wMoof9eJ6R2pJ8 JT0KhhXNkHF17/wmuvrDLUz7iggBJGD0Ic3oWxmwDzdS+0vW4vcSrni6tpR3TN2jcdLdRrbT 5BDNmEzN0+YC/FJEmwLA6wv3/2yvHnAYx9BpknWrLAa5VGGmWSd15CoarI5YOeiTsJM202cu 2ju5HX8GhhcNdqFyDPD/GjEuwPUtSbyWYZXGb/hs/A23xucwWscDBBQXly+yRWktnODtxtkA xR80kITQWIarSRH4/GtB0PQTKKs1vLdZzZRLwH+wASEy66R7gTAQ2ZYEXhOb9spsMJwTjsvv rNMcxUFGhQ32IB5i1rEnltXkd92EScQJG4GIyQDSGPpJvH99ZorgEunoslLScaIYx6cJd006 z+PpSk6wb4UiKbnEkl9EU/v21qRm3QCcuL5Csg7kI5oAsOVqbNJv7CV1GU=
  • Ironport-hdrordr: A9a23:ad/AF6BWmataVF7lHemh55DYdb4zR+YMi2TDtnoBLiC9F/bzqy nApoV56faZslYssRIb+OxoWpPwI080nKQdieIs1NyZLWzbUQWTXeVfBEjZrwEI2ReSygeQ78 hdmmFFZuHNMQ==
  • Ironport-phdr: A9a23:AEtkIRQbj07+UraBLhsiOKetBdpsoqaVAWYlg6HPa5pwe6iut67vI FbYra00ygOTBsOBuqoP0rOG+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxtGiTanf79/K Am6oQrMusULgoZpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQ bNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu8 6FmQwLuhSwaNTA27XvXh9R/g6xbrhyvpAFxzZDIb4yOLvVyYrnQcMkGSWZdXMtcUTFKDIOmb 4sICuoMJftWr5T7p1QQsxS+ARSnCv71xT9SnX/307c10/g8GgzBxwwgAtQOv2rKo9XxLqsSS vq6zLPTzTTNdfxWxSzw6IfNch87oPGMWah8ftbWyUkqDg7IiEibpoP5MT2PzOsNr3Sb4PR6V eKpk2MppQ9/rzyry8owl4XEm4AYxk3E+Ct2z4s4IcO1RFB7b9CrH5Vdsz+WOoV0T84tTWxmu CU3xqAJt5C1fCUG1pAqyhjCYPKEa4iF+gzvWPqVLDtih39oeKiziwiv/UWj0OHxWcu53VBXp SRfiNbMrGoC1xnL58iHVPR9+kCh1C6K1w/J6+FEJVk4mrTZK5I827IwmJUevEbZEi/5n0X2i 6CWdkE69eSy9+vnZbDmqoedN49ylA7+LrwjltKjDek8KAQDXGiW9f6i2LH+/kD1WrpHg/8un qncqp/aJMAbpqCjAw9S14Yu8w2/Dyqg0NsGg3YHKEhJeAmdgIjzIFHPLur3DeukjlSjlTdk3 fHGPrn7DprRKXjDla/tfbBm5EFE0go80chf545ICrEGOP//R1f9tMbEAR8hLwy03+HnBc1h2 YMZQGKDG7OWMKfPsVCT/e8vOOmNZIoNuDnnMfQl5vjujWU4mVAHZ6Wp04EXOziEGaFtJFzca n7xiJ9VGmAT+wE6UebCiVuYUDcVaWzkDIwm4TRuM5+gAIrHDrukmqee1TvzSoZLYG1LDhaXG G3zaIyYc/gJYSOWZMRml2pXBvCaV4Y92ET250fBwL19I7+MksV5nZfq1dwuovbWiQl37jtsS cKUz2CKSWhw2GIOXT4/mq5l8gRm0lnW969+jrRDEMBLoetTW1IhKJjRwug8ENnoQR3IYv+GT V+nRpOtBjRiBskpzYo2al1mU86nkgiF2iOrB7EPkLneH4Ey/6/YmWP4Pd1iwmru26wojl1gS cxKZiW9nqAq0Q/VCsbSllmB0aancaNJxCnW6GKK1naDpmldWQ90FKjHBDUROhSQotP+6UfPC bSpDNzLKyNnzsiPYutPY9zt1hBdQev7fc/ZeyS3knuxAhCBwvWNapDrciMTxneVDk9MiA0V8 XucUGp2Ti68v2LTCiBvHlPzcgvt9+d5snayUk4zyUmDcURg07O//hNdi+abTrsf2bcNuSFpr DsRfh71xM/QBteE4RFoZr5DaM8V71JO1GafvAt4f9ShI61kml8CYlFvpUq9snc/Qo5EkMUss DYr1F8ocfPegA4HLWrIm8yvadi1YiHo8RuiarDbwATb2deSoeIU7egg7k7kpEevH1Yj9HNu1 59U1WGd79PEFll3M9q5X0Ap+hx9v7yfbDM64taezmBqPKSw9CTLwck2DfcNxROpftMZO6SBX lyXcYVSF421JeomlkL8JAkZOu1f8OgvNtm9aPKa8KGuNedk2jmhiC4UheI1mlLJ/C16ROnS2 p8DyPzNxQqLWQD3i1K5u9z2k4RJDd0LNlK20jOsRItYZ6kpOJ0OFX/rOMqvgNN3m5/qXXdcs l+lHVIPnsGzK1KeaFn03AsY0kpywzTvgja+wjFw1SogtLGA1TDmzOHrdR5BMWlODGVvllbjJ 4GogstSBhD5KVh00kH8tQCmmOBSv8EdZyHLTF1NfjTqIm0qSaa2ureYIoZO5J4urSRLQbG5a FGeRKT6pkhS2CfiEm1CgTEjImvy69Opwlog0TLbcCkgyRiRMdt9zhre+tHGEPtY3z5dATJ9l SGSHV+ked+g4dSTkZ7H9OG4TWOoEJNJIkyJhcuNsjW24WpyDFixhfe2z5f8DA433Cu9zNBwT jrBsD7zZ4Dq0+KxNuctLSwKTBfsrtF3HI1ziN56n4wW1HUewI6c52EYmHvbPtBS2Ka4Z30ID 21uoZad8E3u30ttKWiMzoTyWyCGw8dvUNK9Z3sfxiM3680ZQLfR9rFPmjF550aptQ+EK+Yoh S8TkLF9jRxSy/FMogcmyT+RR6wfDVUNdzK5jAyGtpi/tPkFPzvpKOnokhAiwpb5S+ve6gBEB CSnJtF4RnQ2t5sndgqLiSyWiMmsecGMP4xN8ETMyVGYybAScsp5l+JW13Q5fzih7Dt1k6hjy kY2lZCi4NrYcSM0oOTgU0QebnqsN6ZxsnnslfoMwZrQhtryWM0nQnJSAtPpVa76SWpC8624a EDeVmV78C7TGKKDT1bAswE//i6JS9bzcCjJQRtRhdR6GEvHfB0Z0F1SBW9q2MZ+T1/ixdS9I h0guHZMthih+0EKkqUxZlH+SjuN/l72LG1vGd7EdlwOqVgTgiWdedqX6uY5d81B1rumqgHFa mmSZgATSHoMRlTBHFf7eL+n+djH9eGcQOu4NfrHJ7uU+6RYUL+TyJSj35EDnX7EP9iTPnRkE /ww21ZSFXF/FcPDnjwTSisR3yvTZs+frR2492V5tMe6uPjsXQvu48OIBd4weZ13/AuqhK6YK +OKrCNwKDId25FVgHGUl/4Q21kdjywofD6oUPwBuSPLUKPMi/pXAhocOEYRfIND66Mx2BUIO NaO0IukkO4lyKRsWxEZCg+E+Inhf8EBLmCjOUmSAU+KMO/DPjjX24TsZrv6T7RMjeJSvhn2u DCBEkalMC7Q8luhHx2pL+xIizmWeRJEv4ToOA1wD2XuSJT9YwegL9ZrpTIzyLwwwHjNMCRPV Fo0O1MItbCW4S5C179nHHdd63N+MeSesyOQ7u2dJ5RP9PU3XWJ7kOVV5Hl8wLxQpnIhJrQ9i G7ZqdhgpEujm++Ex298URZAnT1MgZqCoURoPaixHnxoVnPN/RZL5mKVWUxiTzpND9Tuv+Vdy IGKmv6sbjhF9N3Q8I0XAM2GcKpv31IuNBPoHHjfCw5XFFaW
  • Ironport-sdr: om3dVwq9WmiQAo27Fn57cQ8FmXkfhG8wTM0bcCSd3Ao2Z/XyzmAZik2+be3n01d7N0kcWxHOx9 SvyJRYQLrzBnBeNJbm2x0Pu5cwy8HpKQmYkIJPIjUgsOHlvXhUzef4V8rcUo/JnUw5B4JTfgP2 8U3Auwe9aWf10xkZyzsGlZeQ1KnHk+vESZvcEb7N816vQEiqndonzYrK0023bA8xqFwdlIPjUX sClMKlny2JsRGJ2WTX3goYkPro7XuliTeo6EAum0gv+546409qc3szgPAdrxSET1jQGu1J3ZGz jvA=

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