The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

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