The Coq mailing list

[Suneel Sarswat <suneel.sarswat AT gmail.com>]

Dear Pierre,

Thanks for the suggestion. I had this as an alternate solution in mind, as I have used the Equation in one of my earlier work.

This time I was looking for a more generic solution without any extra installation.

Thanks again,

Suneel

On Sat, Sep 3, 2022 at 2:04 PM 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.