coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 10:33:52 +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-wm1-f43.google.com
- Ironport-data: A9a23:23eqt6uVmnfdwiRPo0QyN0k7R+fnVHpYMUV32f8akzHdYApBsoF/q tZmKWGFafmOMzH0c98lOoyy8U8Gv5bSyNViTFRk/Ho9RCtEgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCYEidfCc8IMsboUsLd9UR38g52rBVPyvX4 Ymo+5yHYwf8s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCnbiaSyNwJaLcpLQccV5HInBsHKtBoqCSdBBTseTLp6HHW37lwvErE0RveINEoaB4BmZB8 fFeIzcIBvyBr7jukfTrF6813JRlcJKD0IA34hmMyRnBDPs8W52FSKzR+dJC1TEYicVHHPKYb M0cAdZqRE6aPEMVYglLYH44tP73nHTvUxsClEiyv/MSwFTf7E9e6Ke4ZbI5ffTTHZkP9qqCn UrN+H28CRUHPvSE2D+d+zStgPXOlGX1Quov+KaQ8/drhBiMwzVWBkFNE1S8pva9hwi1XNc3x 1EoFjQGiYIw0BWwQcnBDxya52G17ww9Xd0KDLhvgO2S8Zb87wGcD2kCazdObt06qcM7LQDGM HfZz7sF4hQ/4NWopWKhGqS89mztZHBERYMWTWpVEltfuoiLTJQb10qXFr5e/LiJYsoZ8AwcL hiPpSk6wqoW1IsFi/798lfAjDah4JPOS2bZBzk7vEr1vmuVh6b/P+REDGQ3C94edu51qXHf5 RA5dzC2trxmMH10vHXlrB8xNL+o/e2ZFzbXnERiGZIsnxz0pSD5JNwLvGsgfxc0WirhRdMPS B+D0e+2zM8DVEZGkYcqC25MI593lfC4SIyNug78N4MWP8EZmPC7ENFGPBbMhQgBYWAjlqYwP ZrzTCpfJSdyNEiT9xLvH711+eZzmEgWnDqPLbimkUnP+efBPBa9F+1ZWHPQNbtRxP3f8G3oH yN3bZTiJ+N3C72gPEE6MOc7cTg3EJTMLcqt8ZIOLLXffVoO9aNII6a5/I7NsrdNx8x9/tokN FnnMqOB4Fag13DBNyuQbXVvNOHmUZpl/CA0OCUtORCj3H16OdSj66IWdp0We7g79bw7naQkE aVdI8jQUO5STjnn+igGacavoYFnciOtj13cMiegZg85YJM9FRfC/cXpf1e0+SRXVni3uMIyr qeOzATeRZZfFQ1uANyHOv2qxlK1+3ManbsqDUfPJ9BSfmTq8ZRre3Sh1K9pf5lUJEyalDWA1 guQDRMJnsX3otc4oIvTmKSJj4a1CO8hTEdXGm/s67zpZyTX+2yUx5AZDLSFcDXbY2PD+Ku4Y NJTwfyhYuYMm0xHstYlHrtmkfA+6t/oq+MIxwhoBi+QPVGiC7clPXzfmMcT7etCwbhWvQbwU UWKo4EINbKMMcLjMVgQOAt1MbjZhK9MwmHfvaYvPUH3xC5r577bA09cCB+B1X5GJ7xvPYJ5n Oos5JwM5wqkhkZ4O9qKlHoPpWGFL3hFTKB+859GW8nkjQ0kzlwEapvZU3ek7JaKYtRKE08rP j7E2/aY1uoEnhLPIygpCHzA/etBnpBS6hpE+1kPegaSkd3fi/5rgRBc/FzblOiOIsmrDg6yB oRqC6GxDaCH/jMtm80aGm7wQEdOAxqW/kG3wFwM/IEco49ESUSVRFDR+87UlKzaz46YVjde9 bCcjm3iVF4GuenvizAqVxcNR+PLFLRMG86rpCxjN8uAFpg+JzHih8dCoIbORwTPWasMuaEMm QWmECucp0E22e78bpDX07Wn6Ik=
- Ironport-hdrordr: A9a23:USzaAK/Lkn1VrIaqvGpuk+DvI+orL9Y04lQ7vn2ZKCYlEPBw8v rFoB11726StN98YgBCpTnEAtj5fZqjz+8P3WBhB8bGYOCOggLBR+FfBMnZslvd8kXFl9K1vp 0QF5SWZueAdGSSTvyX3OB7KbsdKRW8n5xA/d2utUuFhDsFV51d
- Ironport-phdr: A9a23:uO7DOxWjdcBt8Vgvy2HkyyC4KqzV8KyBXDF92vMcY1JmTK2v8tzYM VDF4r011RmVB96dsaMewLKN+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxtGiTanf79/K Au6oQrNusQYnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3Q rJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6 bpgRxj1hicaLD456H/YhdBsjKxVpxKhogZww4/SYIqIMPZzcafQcdYcSGFcXMheSjZBD5u8Y YQTAOUPIOhWr4fjqVQMrhWwAhKhC/nzxj9NnHL23bE23uYnHArb3AIgBdUOsHHModjrLqgSS vy1y7PSzTrZafNZwS3z6InWfRA7u/GDQ697fM3JyUkuCQzFlE+QppL/MzyJzOsNqHSb4PR6V e21jW4qsA5xoj21ycctjonFnJ4aylfB9Shgxos+ONK3RlJhb9G+DJtQqz+VN5FwQs46QGxlp Sg3x7wEtJC7YiQH1JQpygPfZfGIfYWF7RzuWeSVLDl4h39pZq6zigqy/EWjyODxVMe53VZWo idEnNTBqHYA3AHd5MiAT/ty5Eah2TCX2gDc6+FEPUA0lbfAJJI7w74wkZweulnAEC/ugEj6k rOae0E+9uWr6+nreKjqqoGfOoNuhQzzPLwiltKlDugkLwQDWnSU9v+h2LDn+ED0Qq5Fg/0zn 6TXrp/WOdgXq6ulDABJz4ku6xOyAjO939gGgHUKKUhKdRCZgIf1PlzBPv74Au2kjFmqjTxl3 erJPqf7DZXINnXDkKnufbJ660NEzQo819Ff55ZNBrAPJfL/R1b9tNLXAxI3KQC0zOHnCNJy1 oMaR22DGLOWMKTXsVOQ5+IvJfeDZJMNtTrjN/Qo4+TigHw5lFMHYKWlw5gaZGq3E/loO0mZZ GDjgtYFEWcEpAo+S+nqhUWaUT5SeXmyRbg86S8hBI26F4jDXZytj6Kb3CihGJ1bfW9GClWWH nfpc4WIQesDaCWXIsN5lDwLTqCuS5U92hG2qA/6171nI/LJ9iEAr5LsyMB15/HPlRE17TF7E 8Od03iUQ25ommMIWiQ50btkoU19z1eDybJ3j+ZZFdxV/fNJUx01OYTSz+xgWJjOXVfKec7MQ 1K7SP2nByswR5Q/2YwgeUF4Tv6rlQxCxSOsNIcUmqaRCdRg6qPRxWL8Yc100GrLzqAnp1YjS 8pLc2ahg/gspEDoG4fVnhDBxO6RfqMG0XuRpQ9rrEKLtUBcC0trVLndGGsYfg3QpMj44UXLS /mvD64mO01P053KMbNEP/vui1gOX/L/IJLGeWvkg2a9HwyFgLiFd5bnYWwb9CrYAUkA1QsU+ CXOLhAwUx+ouHmWFzlyDRTqakLo//N5rSajT0Iu1QzMZER6y7ev8xg9ivmVSvdV1bUB6286s zshOlG70prNDsaY4QpseKIJedQm/FJOzn7UrSR4N52kar9n3xsQL18xsETp2BF6TI5HlKDGt VsMywx/YeKd2VJFLHaD2Izof6bQMi/09QyubKjf3hff1syX8+EB8qZwrVKrpwyvGkc4lhcvm 9BIz3uR4InLBwsOQNrwVEgw7R1zu7DdZGE0+YrV0XRmNaT8vCXF3polA+4syxDoeNk6UuvMD A7/CdcXQcOnM/AngVGvRh0BNeFWsqUzOoLudveL3rKqIPc1hCiv3gElqMh21kOB8TY5S/adh c5UhaHFmFLdB3Gg1wTE0Ii/g41PaDAME3DqzCHlANUUfahuZcMQDn/oJcSrx9J4jpqrWnhC9 VflCUlVva3hMReUcVH52hVdkEoNpnny0zO5wiZunncip7GD0TbHxcztcRMGPihAQ2wo3jKOa cCkyssXWkSldV1jjBqo/1z3gaNSv7hyNWDVaUhNdinyaWplV+Hj09jKK94K45QuvyJNVe26a l3PUb/xrSwR1Cb7FndfzjQ2H92zkq3whAcyyGeULXIo6WHcZdk13hDHotrVWf9W2DMCAih+k zjeQFambZGl+tCdlpGLte7bNSrpTpxeazPmi4iJrze2/2RsKRK6lvG33NbgFEA23DT62N9jS SjT5EykM8+7iuLja7IhIhIgDUSZiYIyAoxkl4osmJwckWMXgJmY5ztPkGv+N8laxbOraXMMQ TARxNuGqAPh2UBlMjeI39ejDiTbkpYnPoPqJD9NiUdfp4hQBayZ7aJJh35wq1u89kfKZORl2 ywa0b0o4WIbhOcAvEwsyD+cC/YcBxo9X2SkmhKW4tS5tKgSanyodO36zEtzh8qsSrqLuR1RQ n//UpgnFC50qM54NRiftR+7opGhY9TWYd8J41eMkhraleUTI5sqivcQjCxPNmf0vHljwOk+x 08Lv9nyrM2MLGNj+7i8CxhTO2juZs8dzTrqiL5Xgsec2438VoUkADgAW4HkCO65CD9H/+qyL B6ASXdvzxXTUaqaBwKU711q6m7CA4z+fW/CP2EXlJ1jXEXPfxEZ2VFMGm9mwdhhUVr2jM35L BUnunZLvQW+80UUjLovbkiaMC+XpR/0OGlqDsHHdlwOqFkFvR+dMNTCvLwtWXsEr9vx9ErVb TbDLwVQUTNWAArdWxa6b+PovZ6Zo436TqK/N6ecPunI8LYDEa/OndX2jMNn52reb53feCA9U LtrnBIEBykxGtyFyWxQEGpOxn6LN4jD407in08/5sGnrKaxAFOptdbJUuECd40ook/+gL/fZ bTJ2mAkeXABh8lKnTiRmfAexAJA0XgwMWP2QPJb72iVC/uB/80fRwgSbyc5XCdRx4Q72AQFe cvSi9euk6V9kuZwEFBdE1rohsCuY8UOZWC7LlLOQkiRZvyAInXQzsf7bLnZK/UYhfhItxC2p TeQElPydjWFmT7zUhmzMOZKxCiFNR1asYu5f15jE2/mBN7hbxS6Npdwg1hUifUsgWjWMGcHL TVmW0ZEr7nV8iYBx/sjQCpO6X1qKeTCkCGcrqHZJpsQrfp3E3F0muZdsxFYg/Ne6CBJQuAwm TOH9IY/5QH71LDVmnw7C0kryH4Dno+AsER8NL+M85BBXS2B5xcR9SCLDAxModJ5C9rpsqQWy 97Vlau1Ji0RlrCctcYaGcXQL9qKdXQ7Nh+8UibVAREfQHigPHrDilZUltmd83SUqt4xrZ2my /9sAvdLEUc4EP8XEBEvBNsZPJJ+RS8pi5aehc8MoGW79VzfGJ4csZfAWfafR/7oLXzK6NsML wtNyrT+I4MJM4T90EE3cVh2krPBHE/IVMxMqClsBufViEBE8Xw7UWhqnky5MUWi53gcEfPyl Rkz2FMWiQEF+zLl4lNxLV3P9nNYeKYZltDsgDTXezn0fv7YYA==
- Ironport-sdr: VoPV3auybTujZOmAuKN2Rn7Uqbq0ASIiyrrNhCHjZ+ckzeBPzGFVn/96fu7q+RVg60Ivt76Gdj aQKH3o6zLxIJWp9c6llUfCwN7u+dRvu1Pc79GE+SfyvyOHPFie3N/xtoXLBkEdrJ0mzWZvYGyV 1dlskRE+08KQWE8z5S7tpy4TrOBUiXs7GuPJJaUjE34SXHGVsmQ0vlUPdbOBNvPWjcxMttVP/M dzRWYjZDON/r9sRL3mY7qlSOcj2SwKTij7YU2Al8agvdyDlUtEkIxkq//WUMr5N0bqCqvgtN6n zCD1quLu+Xjx8ultPnZDgVDa
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.
- [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+.