The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

Hi Suneel,

The part of the OG module that computes is the compare function, which 
you've defined as a constant function. It should actually compare the 
fields of its arguments.

Cheers,
Li-yao

On 2022-09-12 12:18 PM, Suneel Sarswat wrote:
> Dear Friends,
> I am using MSets.MSetRBT to implement an algorithm on record type 
> elements. I am able to successfully implement the program.
> Before I started proving correctness, I wanted to check on some 
> numerical examples. Unfortunately, I am not able to see what went 
> wrong (possibly with OrderedType).
> The elements are not added only using add and only one element is 
> added. Here is the toy program. Please help.
> Thanks in advance.
> -Suneel
>
> --------------------------
>
> Require Export Coq.MSets.MSetInterface.
> From Coq Require Import OrderedType.
> Require Export MSetGenTree.
> Require Export MSets.MSetRBT.
> Require Import Coq.Arith.PeanoNat Lia.
>
>
> Record game:Type:= Mk_order{
>                         val1: nat;
>                         val2: nat; }.
>
> Definition ltg (b b':game):=
> (Nat.lt (val1 b') (val1 b)) \/
> ((Nat.eq (val1 b') (val1 b)) /\ (Nat.lt (val2 b) (val2 b') )).
>
> Definition eqg (b b':game):=
> ((Nat.eq (val1 b') (val1 b)) /\ (Nat.eq (val2 b) (val2 b') )).
>
> Module OG <: Orders.OrderedType.
>
> Definition t := game.
> Definition eq (x y: t) := eqg x y.
>
> Definition lt (x y: t):= ltg y x.
>
>  Lemma eq_refl : forall x : t, eq x x.
>   intros. unfold eq. unfold eqg. split.
>   all:unfold Nat.eq;auto. Defined.
>
>  Lemma eq_sym : forall x y : t, eq x y -> eq y x.
>   unfold eq. unfold eqg. unfold Nat.eq. lia. Defined.
>
>  Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
>   unfold eq. unfold eqg. unfold Nat.eq. lia. Defined.
>
>  Definition eq_equiv: Equivalence eq.
>   intros. constructor.
>     unfold Reflexive. apply eq_refl.
>     unfold Symmetric. apply eq_sym.
>     unfold Transitive. apply eq_trans. Defined.
>
>  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
>   unfold lt. unfold ltg. unfold Nat.eq. unfold Nat.lt. lia. Defined.
>
>  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
>   unfold lt. unfold ltg. unfold Nat.lt.
>   unfold eq. unfold eqg. unfold Nat.eq. lia. Defined.
>
>  Definition lt_strorder: StrictOrder lt.
>   constructor. unfold Irreflexive. unfold Reflexive. unfold complement.
>   unfold lt. unfold ltg.  unfold Nat.eq.
>   unfold Nat.lt. intros x H. lia.
>   unfold Transitive. apply lt_trans. Defined.
>
>  Definition lt_compat: Proper (eq ==> eq ==> iff) lt.
>   unfold Proper. intros x y H. intro x0. intros y0 H1.
>   unfold eq in H. unfold eq in H1.
>   unfold eqg in H. unfold eqg in H1.
>   unfold Nat.eq in H. unfold Nat.eq in H1.
>   unfold lt. unfold ltg. unfold Nat.eq. unfold Nat.lt.
>   lia. Defined.
>
>
>  Definition compare : t -> t -> comparison.
>   intros. constructor. Defined.
>
>  Definition compare_spec : forall x y : t,
>      CompareSpec (eq x y) (lt x y) (lt y x) (compare x y).
>      intros. elim (compare x y). Admitted.
>
>  Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
>  Admitted.
>
> End OG.
>
> Module G. Include MakeRaw OG. End G.
> Include MSetInterface.Raw2Sets OG G.
>
> Definition A := G.add {|val1 :=1;val2:=1|}
>                       ( G.add {|val1 :=2;val2:=4|}
>                         ( G.add {|val1 :=2;val2:=2|}
>                           ( G.add {|val1 :=1;val2:=2|}
>                             ( G.add {|val1 :=3;val2:=2|} G.empty)))).
>
> Eval compute in (G.max_elt A).
> (*Some {| val1 := 3; val2 := 2 |}*)
> Eval compute in (G.min_elt A).
> (*Some {| val1 := 3; val2 := 2 |}*)
> Eval compute in (G.elements A).
> (* = {| val1 := 3; val2 := 2 |} :: nil
>      : list game *)