The Coq mailing list

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

Dear Pierre,

My requirements are any tree data structure so that I can write efficient algorithms which are otherwise inefficient on lists.

My elements are records with lexicographic order. The operations I am going to perform are insert, remove_min/max, delete.

In the case of a list, min/max extraction takes O(1) time but delete and insert takes O(n). But in a tree data structure all

these can be done in O(logn) time. Instead of implementing a tree for my specific purpose, I would like to try the already

built library so that my proof obligations are less. Also, use of the existing library makes more sense than inventing everything yourself.

Hence, I was looking for some documents or use case examples to save time.

Regards,

Suneel

On Wed, Aug 24, 2022 at 2:59 PM Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

Hi,

Actually if T has inner module. In particular the Raw module, where
you can find the remove_min function, together with some properties
about it.

Import MSets ZArith Coq.ZArith.Int Psatz.
Module M := MSetAVL.Make Z_as_OT.
Print M.Raw.
Print M.Raw.remove_min.
(* More facts about MSets:*)
Module MFacts := MSetFacts.Facts(M).

You can't perform an induction or destruct directly on trees, this is
on purpose: to prevent depending on the current implementation of AVL
and be robust against further changes of the internal definitions.
Only the MSet.Interface and MSet.Facts are unlikely to change
significantly.
For desperate cases you can perform an induction on the list of
elements given by M.elements, but I think the whole idea is that you
shouldn't need it.

BUT, this is probably not what you want to do anyways, as Mukesh
suggested iIf you are interested by remove_min, you are reasoning
about *ordered* sets instead of sets, which suggests to look for the
corresponding functors: MSetInterface.Ops and MSetAVL.Ops. And if you
are interested in AVLs specifically you may have a look at
MSetGenTree.v [3].

[1] https://coq.inria.fr/library/Coq.MSets.MSetInterface.html#HasOrdOps
[2] https://coq.inria.fr/stdlib/Coq.MSets.MSetAVL.html#Ops
[3] https://coq.inria.fr/library/Coq.MSets.MSetGenTree.html#Ops
Best
Pierre

Le mer. 24 août 2022 à 09:56, mukesh tiwari
<mukeshtiwari.iiitm AT gmail.com> a écrit :
>
> Hi Suneel,
>
> I just quickly looked at the source code [1] and wrote a simple code:
>
>
> Require Import MSets
> ZArith Coq.ZArith.Int FunInd
> Psatz.
>
>
> Module M := MSetAVL.Ops Int.Z_as_Int Z_as_OT.
> Check M.remove_min.
> (*
> M.remove_min
> : M.tree -> M.elt -> M.t -> M.t * M.elt
> *)
>
> Unfortunately, I can't do induction on 't' because the induction
> principle is unset [2],
> but you can still do functional programming using the 'refine' tactic,
> so I believe it should
> not be a problem. I believe the challenge would to find the concrete instance of
> modules, e.g., in this case 'Int.Z_as_Int' and 'Z_as_OT' for instantiation, but
> if you search you can get it, otherwise you can alway ask here.
>
>
> Lemma tree_proof : forall (t : M.tree), (0 <= M.height t)%Z.
> Proof.
> refine(
> fix fn t {struct t} :=
> match t with
> | M.Leaf => _
> | M.Node h _ _ _ => _
> end).
> Admitted.
>
>
> Best,
> Mukesh
>
> [1] https://github.com/coq/coq/blob/master/theories/MSets/MSetAVL.v
> [2] https://github.com/coq/coq/blob/master/theories/MSets/MSetAVL.v#L42
>
> On Tue, Aug 23, 2022 at 9:03 PM Suneel Sarswat <suneel.sarswat AT gmail.com> wrote:
> >
> > Dear friends,
> > I am new to the FSet or MSet library of Coq. I have got a simple task of implementing a program (current version involving lists) using trees.
> > My elements are of record type with lexicographic order. I am able to define (thanks to xavier leroy) ordertype X using Module X <: OrderedType and can initiate Module T:= FSetAVL.Make(OrderedB).
> > I could do simple things like creating a tree using T.add but I could understand how to use many other functions. For example,  T.remove_min (not recognized!). Also, how to do case (destruct) on trees similar to lists.
> > I am sorry if my question is elementary but due to lack of documents/use cases I am finding it difficult to proceed. Also, I have a deadline fast approaching.
> > Please suggest some documentation or some use cases for quick help.
> > Many thanks,
> > Suneel
> >
> >