The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

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 

[1] https://gist.github.com/mukeshtiwari/b77df39aabaef6fef30cd3d6ef51e45e

[2]https://gist.github.com/mukeshtiwari/b77df39aabaef6fef30cd3d6ef51e45e#file-suneel-v-L27

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.