The Coq mailing list

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

Thank you Mukesh,

Lets wait for more suggestions and meantime let me try this.

-Suneel 

On Wed, 24 Aug 2022, 19:05 mukesh tiwari, <mukeshtiwari.iiitm AT gmail.com> wrote:

Hi Suneel, 

My suggestion would be to stick to MSetAVL because I can see, “This is just a compatibility layer, the real implementation is now in MSetAVL”, in the FSetAVL.v file but I will wait for someone more expert  to comment on this. 

I faced a similar problem as yours but it went away when I imported Orders  before OrderEx because it has the definition of eq_equiv. This works but unfortunately it does not have remove_max.

Require Import MSets 

  ZArith Coq.ZArith.Int FunInd

  Psatz Orders OrdersEx.

Module M := MSetAVL.Ops Int.Z_as_Int Z_as_OT.

(* 

You can contruct an OrderedType lexicographic product from 

two OrderedType

*)

Module W := PairOrderedType Z_as_OT Z_as_OT.

Module V := MSetAVL.Ops Int.Z_as_Int W.

Check V.remove_min.

Check V.add.

Check V.remove.

(* Unfortunately, it does not have remove_max*)

Check V.remove_max.

Best,

Mukesh 

On Wed, 24 Aug 2022 at 12:51, Suneel Sarswat <suneel.sarswat AT gmail.com> wrote:

Dear Mukesh,

Thanks for this information. What I have understood is that some of the functions are defined for some specific modules only.

It seems even the OrderType is differently specified for different modules. For example, the equivalence requirement on the order type in MSetAVL (eq_equiv) is different from the same in FSetAVL.

Require Import MSets ZArith Coq.ZArith.Int Psatz FSets FSetAVL.
From Coq Require Import OrderedTypeEx.

Module T := MSetAVL.Make OrderTypeB.

(*

The field eq_equiv is missing in Test.OrderTypeB.

*)

but Module T := FSetAVL.Make(OrderTypeB). works for a lexicographical order OrderTypeB defined on elements of type record.

Regards,

Suneel 

On Wed, Aug 24, 2022 at 1:27 PM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

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