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: Castéran Pierre <pierre.casteran 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 15:29:01 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.casteran AT gmail.com; spf=Pass smtp.mailfrom=pierre.casteran AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f51.google.com
  • Ironport-data: A9a23:kwv1q6oYRRFtl2Ma/1Dq9vLLCJReBmI0YxIvgKrLsJaIsI4StFCzt garIBmAPP7cYWanKNolPYS/ph5T7ZLSxtJgGQZsqC81RisUoOPIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKicfHoZqTZMEE/Nszo68wICqtMu0IPR7z+l4 4uo+ZWOYAT9gVaYD0pNg069gEM31BjNkGhA1rAOTagjUIj2yhH5pLpGTU2AByOQrrt8RoZWd M6fpF2NxV41yj92Yj+TfhkXRWVRKlLaFVDmZnO7wMFOiDAazsA5+v5T2Pbx9S67hh3R9+2dx umhurSpFVcYNPXwh90EXkFhAQtbHvx51pXudC3XXcy7lyUqclPpyvRqSV4sZMgWp78xDmZJ+ vgVbjsKa3hvhcrsmOP9GrQq3J56apSyVG8ckikIITXxFfcrW4rOBa7D/sNVxj42rs9LFPfaI cEebFKDaTyaOUIQYwtKVfrSms+EilL+fBJymWm0rJJmwiv0lxdW85PUZY+9ltuiHJ0JxC50v Fnu9GPgRxoeKda30iuA6nvqh+nVnCq9Vph6KVGj3vtjgVnW2XZKTRNLDB20pv62jkP4UNVaQ 6AJxsYwhbFupH2hFuXiZgS1+EeWlDs/CuV+OcRvvWlh1ZHoywqeA2EFSBtIZ9onqNI6SFQWO rmhz4OB6dtH4O39dJ6NyluHhWjtZnVNfAfucQdBHFRVuYCyyG0mpkuXFo4LLUKjsjHi9djNL 92iqSE/g/AMl5dO2fjiu1/AhD2oq97CSQtdCuTrsoCNvlIRiG2NPdTABb3nARBoct3xor6p4 iJspiRmxLpSZaxhbQTUKAn3IJmn5uyeLBrXikN1Ep8q+lyFoiD9J9kMu20kehw5b67onAMFh meD6Wu9A7cDbBOXgVNfPupd9uxxkPC4TYm9PhwqRoMXOsUoHON4wM2eTRfIgzqFfLkEnqY4N pOWGftA/l5LYZmLOAGeHr9HuZdynn5W7TqKGfjTkkr6uZLDOyb9YelfbDOmMLtihIva+1W9z jqqH5HVo/mpeLauPHe/HE96BQxiEEXX8rit+5cGK7Paf1c4cIzjYteIqY4cl0Vet/w9vo/1E ruVAye0EXLz2i/KLxukcHdmZO+9VJpztyNpMiklPFLu0H8mON794KAafpoxXL8m6O0zla4uH 6dZI52NUqZVVzDK2zUBdp2i/oFvcRKcgwjRbSeoZT4IeYFtGl7S8dj+cwqzryQDV3LltcY3r 7C6+BncRJ4PG1ZrAMrMOaCgylqwuT4Wn+crBxnEJdxaeUPN9ol2Knyp3qVnfZ1UcRian2mUz QebBxsctNLhmY5t/Ymbn72AoqeoD/B6QRhXEmzd2rC8anvX82+l9olfCbracD3YUlT0z6Wsf +Biyf/xba8cl1FQvosgSrtmwP5s59broLMGnA1oEG+RNAauA7JkZ2achIxB6/QLybhetg+7H EmI/4ACa7mOPcrkFn8XJRYkPrvfj6BKwmGK4KRnOlj+6Q924KGDDRdYMS6KhXEPN7ByKo4kn bostZJE8QC5kRZ2YN+KgjoOrDaJJ30EFro979QUXdathQ0sxVVPJ5fbD3ausp2IbtxNNGgsI yOV1PWe3eUCnhKafiphD2XJ0MpcmY8K5EJAwmgEKgnbgdHCnPI2gEBc/Dlfot65FfmbPz+f+ 1SHNnGZ4Y2L9jZswddZBiWiRlgHCxqe9Uj8jVAOkQU1iqVuunPldAUA1SSlpSj1MF6wuhBU+ biZzCDuVjOCkATZwH4pQUA8wxD8ZYUZy+AB8fxL2+yKGpA7ZXzuharGia/kbff4KZtZuXArb tWGMAq9hWMX+MLQT2AG51Gm6Ikt
  • Ironport-hdrordr: A9a23:hOjepKmF9F09N3nEyLXLqgr5PhTpDfIb3DAbv31ZSRFFG/Fw9v re/sjzsCWftN9/YgBGpTntAtjifZqYz+8M3WBuB8bYYOCWghrMEGgK1+KLqF3d8m/Fh4hgPM 9bEpSWY+eAaWSS4/yKmTVQ0OxN/DBEys2VbCvloEuFNTsaEZ2IJj0WNjqm
  • Ironport-phdr: A9a23:5eZiMhTpbQYhqjZYe+SY+G7Fitpsou6WAWYlg6HPa5pwe6iut67vI FbYra00ygOTBsOBuqgP1bWempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffQtFiCCjbb52M hm6ogTcu8sLioZ+N6g9zQfErGFVcOpM32NoIlyTnxf45siu+ZNo7jpdtfE8+cNeSKv2Z6s3Q 6BWAzQgKGA1+dbktQLfQguV53sTSXsZnxxVCAXY9h76X5Pxsizntuph3SSRIMP7QawoVTmk8 qxkTwLmiDocNz4h7m7YltBwgqxcoBKkvRN/wojUa5yROPdxeq7ReNUXTndDUMlMTSxMGoOyY JcAAOQcM+hYoZfzqFkNoxW5HgSjHv/jyjpSi3/2waE30eIsGhzG0gw6GNIOtWzZocvvO6cJT eCy1rPIwi/Fb/xOwzn96ZbHcgo7of6SQLl9dtLRyUgxGAPflFWft5bpMC+P2eQWr2iU8fBgW vipi2M8pAFxpyKgxsYoioXTmo0VzVXE+Dx/zY0oKtK2VFR1bsS4EJtMqS6aLY12T9stTWxpt ys3zrMLtJ20ciUEypkpyBrSZfOFfoWK/B7uW/qdLzdliXxre7+ymQi+/VS+xuD4SMS531ZHo y5Gn9TRsH0GyhLd6s+CSvRn/0eh3y6C1w/S6uFYIUA0iLHUJ4Q9zb43k5ofqUvDHi7qmEX2k a+ZbV8o+umv6+nhf77opYecOpdqhg3iNqkigM+yDOQiPgQQQWSX5P6w2b3+8UHhXrlFlOE6n rTcvZ/GPssXu6q0DgpX34k46xuyCjmr38oEkXUbKV9KZA6IgJXpNlzLJP33Fumzj0mpnThxx f3JIKHuD5DTIXjNirjuZrBw4FNGxgUp19BQ/ZdUB6kBIP3tXk/xs8TVDhojPAy1x+brEdt81 pkDVW6WDK+UML7evUWH5uIoJOmMa4sVtyjnJ/c54P7uiGc1mV4bfaa3wZsacG60EuhiLkmDY nfhgs0NHXkUsgYjVuDniECOXSZWZ3moXqI84j87CJihDYfGXo2tmL2B0zmhHp1MeG9KEEyDH m3zd4WYRfgMcjidIsl6nzwLULiuUY4h1RW0uADmzLpnK/LY+isDup37zth6+/XTlQ0u9TxzF 8mRznmBT3tokWMQWz82wKd/rFRhxVeEyKh0muBXFdhO5/xSSQo6Lp7dz+liC9/oQA7Bf9GJS EynQtq8Gz0xQMgxkJcyZBN2HMznhRTe1QKrBaUUnvqFHs8a6KXZilP4PNr80X/A45EggkM8T 4MbLWyrnLRysQPaHJLEiUyfv6mvfKUYmiXK8THQniK1oEhEXVsoAu3+VncFax6K/LwRh2vHR r6qUvE8NxdZjNWFMu1MY8HoilNPQLHiPs7faiS/gTT4Hg6Gk5WLaoeiYGABxGPFEkFRiwEe5 2yLcwM3HTusuWvYJDNrHFPrJUjr9Lo2s2u1G3c91BrCdEh9z/yw8x8Ri+abTqYL378eoipno DxvAFun1tT+BN+Jpg4nd6JZMpsm+FkS82XfukRmO4C4aaBvgllLawNso0bnzAl6EK1FmMku6 WwwlU98dPve31RGeDeVm5v3P9U7M0HU+xaiI+7T01Dai5ON/7sXre8/sxPltR2oEUwr9zNm1 cNU2j2S/MeCCg1aSp/3Xkstknoy77jHfikw4Z/V3nxwIOG1tDHFwdcgGOoizF6pYd5eNKqOE AK6HdcdAoCiL+kjml7haRxhXqga7K85JdmrMfCPw7KmJu9mtD2jhGVDpot61wPE9iZxTPLJw 4dQ2+uRjW7lH3/3iFastNyymJgRP2lDWDrij3K+XcgMP/4XH85DE2qlLsypy88rgpfsXyUd7 1u/HxYd39fvfxOOblv71AkW1EINoHXhlzHrql482zwvsKeb2zTDhur4cx9ScHZKSXN4gBHnK JOogsoTWmCnagEokF2u4kOwlM057OxvanLeR0tFZX28N2BvSLG98LGLeNJC8poumSpSWeW4J 1udT/SuxnlSmzOmFGxYyjchcjissZishB12hlWWK3NrpWbYc8V9rfvGzOTVXuUZnj8PRS0jz CLSGkD5JN6xu9Odi5bEtOm6EWOnTJxaNyfxn8uMsy6y5GsiBhPa/bj7gtzqCxI3lyTyzMVnT yzOhBn5a4jvka+9NKprc1JpC1n198dhUtsmw81g2ddKgyFc28zd9GFi8y+7KdhB3KPicHcBD SUGxdLY+kmt2UFuKG6I25OsU3ycxsV7YNzpKmgS2y8784VLEPLOtO0CzXYz+ADh61+IMp0f1 n8HxPAj6WAXmbQMsQsplWCGB6wKWFJfJWrqngiJ6Na3qONWYnyueP6+zhkb/5jpAbecrwVbQ Hu8dI0lGHo69sRyKkjBlnb68Z3pYtDWRd0WvxyQ1RzHiqIGTfB53upPnidhNW/n6Dc9yuMhl xEo1pihoIWdImNF86ewAxoePTrwLZB2mHmlneNVmcCY2JqqF5NqF2AQXZfmevmvFSobqfXtM wvdWC15sHqQHqDTWBOO8Eoz5WyaCIilbjvEQRtRhcUnXhSWI1ZTxRwZTClv1IBsDRiknYTga BsrvW1Xvw+g7EEQlaQwcEOjGmbH+FX2NnFuE8PZdUQOqFkFvhawU4TW7/ovTX8GuMT59krVb DTcPVwADHlVCBLaQQq/b//+vZ+YtLLATuumc6mRO/PX9aoHBq3OndX2gu4Et36NLpndYSUkV qdmnBIFBTcgRYzYg2ldEnRH0XuSMIjL4k/7oHQ/r9jjoq20A0S2tNfJU/0KdowxnnL+yaaba 7zK3Hc/eWsej8lcgyePkedX3UZO2Xs3KX/wQfJZ5HSLFOWJy+dWF0JJMXotcpETvuRnhE8Vf peK77G9nqhxivp/Y7tcfXrmnMzhJckDImXmcUjCGF7OL7OeYzvC38DwZ6q4D7xWluRd8ROq6 36dFAf4MzKPmiOMNVjnOPxQjCydIB1VuZ2sOhdrB2/5Sdv6axq9eNZphDwyyLcwizvEL2kZe TR7dkpMqPWX40Y6yr1nHHdd63N+MeSesyOQ7u2dNYxP9PU2W2J7kOVV5Hl8wLxQrWlFSPFzh CrOv4turlWhwYztgnJsVBtDrCoOhZre5x0zf/WEsMMaADCZpUFojy3YERkBqtp7B8e6vqlRz oOKj6fvMHJZ9MqS+8IABs/SIcbBMXw7MBOvFiSHaWlNBTOtK2zbgFRQ1f+I8XjA5IA7p4L2l dwFQ6RHWUY8ENsVD01kGJoJJ5I9DVZG2faLydUF43aztkybXMJBopXOTe6fG93qITedyKZeP l4GnOq+IoMUOYn2nUdlbxMp+eaCU1qVVtdLrCp7awYyq0gY63lyQFo43Ef9Yx+s6nsefRZRt hEzgwp6J+8q8WW0i7/WDl/DpS91j1No3Nu42Haedzn+KKr2VoZTWXKcX6cZPZbyQgIzZgq3z xUMCQ==
  • Ironport-sdr: E9fnJnfa+5lOwcpEweJBRSJCQQ11cYUGDxcmTZkRcprJTGB0FIInwSi97/IWxaMsYeaHPtE2U6 hvOSgni7qtGXYVq4quf8+J882eEDXwTJpfd2feUApEw+eUFhuXfrckRBDoHkCGh1BrP/D0u+fL TQzn7GP/W6cDkZPlQai2YuGR7qvuw8nHXveo3004uemti89geDMylZRV+QNxsYi1MdvVxQXzWz ueIWM9ZCjSM6mLj/2xTzVNz/S6oAsldr5sr4OGmB/TFrZVzK+PNaexnHTwzlM0tobtURx/t4fz XT2ckzPBteCyK5oPxfawdmay

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.

https://gist.github.com/Casteran/cc3e39cec590aae0c0a7541d25972493


Pierre



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