The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

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