The Coq mailing list

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

Thanks Pierre again. Will look into the book when I have this. I was also thinking of this book for the chapter on Module.

Thanks again,

Suneel

On Sat, Sep 3, 2022 at 6:59 PM Castéran Pierre <pierre.casteran AT gmail.com> wrote:

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 

[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.