The Coq mailing list

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

Dear Mukesh,

Thanks a lot for this code. This is very useful. Couple of questions, if anyone can help me to figure it out.

1. Where do I find results proved for max_elt/min_elt or add etc?

2. How do I define compare_specs with Prop eq and lt in the Orders.OrderType module?

3. How to claim complexity of the extracted programs using RBT?

Thanks,

Suneel

On Sun, Aug 28, 2022 at 1:40 AM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

Hi Suneel,

Does this help [1]?

"If I use Module Ops (Ordered:OrderedType) <: MSetInterface.Ops
Ordered., then I get eq_eqiv is missing even though it is present!"
Can you post a snippet of your code? Let me know if you have any
questions.

Best,
Mukesh


(* Begin Coq code *)
Require Import MSets MSetRBT
ZArith Coq.ZArith.Int FunInd
Psatz List.

Import ListNotations.


Print Orders.OrderedType.

Module M := MSetRBT.Ops Z_as_OT.

Print M.elt.
Print M.tree.

(* Construct Order Type
Z_as_OT
*)
Module OT <: Orders.OrderedType.

Definition t := Z.
Definition eq := Z.eq.
Definition eq_equiv : Equivalence eq.
Proof.
econstructor.
+ apply Z.eq_refl.
+ apply Z.eq_sym.
+ apply Z.eq_trans.
Defined.
Definition lt := Z.lt.
Definition lt_strorder : StrictOrder lt.
Proof.
econstructor.
+ intro x.
apply Z.lt_irrefl.
+ intros ? ? ? Hx Hy.
apply Z.lt_trans with (m := y);
try auto.
Defined.
Definition lt_compat := Z.lt_compat.
Definition compare := Z.compare.
Definition compare_spec := Z.compare_spec.
Definition eq_dec := Z.eq_dec.
End OT.

(* Get a concrete instance *)
Module W := MSetRBT.Ops OT.

Print W.

(* Let's construct some tree *)

Definition ttree := W.treeify [1; 2; 3; 4; 5]%Z.
Eval compute in ttree.
(*
= W.Node Black (W.Node Black (W.Node Red W.Leaf 1 W.Leaf) 2 W.Leaf) 3
(W.Node Black (W.Node Red W.Leaf 4 W.Leaf) 5 W.Leaf)
: W.tree
*)

(*end Coq code *)

[1] https://gist.github.com/mukeshtiwari/328d9a299807a87ee75127f1effc0117

On Fri, Aug 26, 2022 at 9:09 AM Suneel Sarswat <suneel.sarswat AT gmail.com> wrote:
>
> Dear Coq-Club members,
> What is the correct order type module for MSetRBT? My order defined for the elements are total. The issue I am facing is the following.
>
> Module Ordered <: OrderedType.
>
> (*
> Definition t := instruction.
> Definition eq (x y: t) := eqi x y.
> Definition lt (x y: t):= lti x y/\~eqi x y.
>
> .........
> .........
> ......... equivalence of eq and transitive/compare for lt
> *)
> End Ordered.
>
> Inductive color := Red | Black.
> Module Color.
>  Definition t := color.
> End Color.
>
> Module Ops (Ordered:Orders.OrderedType) <: MSetInterface.Ops Ordered.
> Include MSetGenTree.Ops Ordered Color.
> Module TB := MSetRBT.Ops Ordered.
> (*Error: Signature components for label compare do not match: expected type "Ordered.t -> Ordered.t -> comparison" but found type "forall x y : Ordered.t, Compare Ordered.lt Ordered.eq x y".  *)
> If I use Module Ops (Ordered:OrderedType) <: MSetInterface.Ops Ordered., then I get eq_eqiv is missing even though it is present!
>
> What signature of OrderType are required for RBT tree and which Module to be used for that?
>
> Thanks again,
> -Suneel