coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Suneel Sarswat <suneel.sarswat AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Red-Black tree and OrderedType on records
- Date: Mon, 12 Sep 2022 16:48:19 +0530
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=suneel.sarswat AT gmail.com; spf=Pass smtp.mailfrom=suneel.sarswat AT gmail.com; spf=None smtp.helo=postmaster AT mail-ej1-f48.google.com
- Ironport-data: A9a23:sD0kB6sikTJ/56NugMnMGQsEWOfnVHRYMUV32f8akzHdYApBsoF/q tZmKTyDbv3bZmf0c4t/bN/j8xkP75HQx4BgSwpt+3thQSobgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCYEidfCc8IMsboUsLd9UR38g52rBVPyvX4 Ymo+5yGYgf8s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCnaS5UD0KYKboodgceTpeDCwjY4p4xaCSdBBTseTLp6HHW37lwvErAUNveINEqqB4BmZB8 fFeIzcIBvyBr7jukfTrF68235RlcJmD0IA34hmMyRnCEPArTJSFWKzQ/sBRwB8/g8lPGbDVY M9xhT9HNk+cPUEQZQt/5JQWtcjrn3veNBli9VuwgJA3+Eny6jZf3+24WDbSUoXSGZ89clyjj mnB5iHyBgwQHMeOzCKMtHOqnO7G2y3hML/+D5W9//9uxVCRnykdVE1QWly8rv20zEW5XrqzN nD45AIWpLEI1xKgauDBXjebpmGJ40A7ZedPRrhSBB629oLY5AOQB24hRzFHacA7uMJeedDM/ g/Z9z8OLWw/2IB5WU5x5Z/P8mzvYXl9wXsqIH5bHVFcsrEPtalq1kqXJuuPBpJZmTEcJN0d6 zWDrSx7irdKyMBXh+O0+lfIhz/qrZ/MJuLU2uk1djP6hu+aTNT9D2BN1bQ9xagdRGp+Zgfc1 EXoY+DEsIgz4WilzURhutklErCz/OqiOzbBm1NpFJRJ323zpSTyJ9kIu2sjehoB3iM4ldnBM B+7VeR5tM87AZdWRfIfj3+ZUJlzlPC9RbwJqNiNNoUXOPCdizNrDAk3PRLKt4wcuEcrlq47N P+mnTWEXB4n5VBc5GPuHY81iOd1rghnnD+7bc2lknyPjOXGDFbLE+ttGAXVNYgRsvjUyDg5B v4FaKNmPT0EALOgCsQWmKZPRW03wY8TW8+v85ULKLLaSuekcUl4Y8LsLXoaU9QNt8xoei3gp RlRg2dUlwjyg2PpMwKPZiwxYb/jR8ctoncyPChqNlGtgiBxbYGq5aYZVp02Ybh3rLw5naAoF 6EIK5eaH/BCajXb4DBCP5TwqYpVch701w+DOiySZicyIsx7TAvT9964JQbirXFcDie+ucYkj aen0wfXHcgKSwh4XZTZbfuuyxW6un1EwLB+WE7BI99yfkTw8dgye3ah0KNve8xVcEfN3DqX0 QqSECw0n+iVrt9n6sTNiICFs5ytTLlzE09cKG/RsuS7OCzcyWy8mNMSXeuNewfdY2P64qCVY +tYkqPnO/odkVcW6odxHuo5za864Nez9bZWwh4+RyfOZlWvT75iezyIgZkJuapKybtU/wCxX xvXqNVdPLyIPuLjEUIQdFV5NLXdjalMl2mA9+kxLWX7+DRzoOiNX3JUMkTekydaNrZ0bN4oz LtzosIQ8ADj2BMmPszc1XJR/mWIa3ECCuAp6sFcD4jshQ4mjFpFZMWEWCPx5ZiObfRKM1Urc mDI3vuc3+wEyxqQaWc3GFjMwfFZ2cYEtidMwQJQPF+OgNfE2qI60RA5He7bleiJIsirEt6fO 1SH82VwLKSKujpq3Y1NAzDqFAZGCxmUvEf2zjPlUYEfo1aADgTwwK8VYI5hP3z1N0pTezFa+ PeTz2ONvfPCYpTqxiVrMaJ6g6WLcDGynzEuXOioGs2EG98xZj+NbmpCo4YXg0OPPP7dT3Era QWnECicpEE72eMtT3UHNrSn
- Ironport-hdrordr: A9a23:7CUeG6pNCiN/4Ikd0tg3vogaV5omeYIsimQD101hICG9E/bo8P xG+c5w6faaskdzZJhNo7C90cq7IE80l6QFg7X5VI3KNGLbUQCTXeRfBOXZslnd8u7FmtK1F5 0MT0GzMrLN5JFB4/rH3A==
- Ironport-phdr: A9a23:NxaryhFVSbk2LNVgaZ/jR51GfzhGhN3EVzX9CrIZgr5DOp6u447ld BSGo6k31xmSBN+QsKMMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5ZPebx9GiTagf79+I xu7oAHMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2Q rxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6 bpgRh31hycdLzM2/2HZhMJzgqxGvhyuuwdyzJTIbIyPLvdyYr/RcNEcSGFcXshRTStBAoakY oUSEuoBO/hXoJf5p1ATsBWxHxOsBPjhyzBSmn/9wKo30/88EQHAwgMvAdYOvG7PrNrvLqcSS u60w7PUzTjYYPNW3C3y6InMchw7vf6MWrdwfNPXxEIyGAzLkk+eppb5PzOJyOsNqW6b4vJuW +yhj2Mqrx18riWyy8oul4XEho0bx1/A+Chn3oo7JdK2RkF/bNK6HpZdtS6XOoV2TM4hXm1mt yg0x70YtZO/eiUB1ZcpxwbHZvCZb4SF5gjvWeWRLDtimn5pZbGyiwy9/EWjzOD3S9O630xQr iVfl9nBrnAN2ALX6siAUvZ9+12u2TeL1wzK9O5EI104mbPVK5MuwbM8jJUTsUPEHi/5nEX5k rWaeVkj+uit8+jnY7PmqYGAN4JslA3yLqAjlta8DOk4KAQCQXWX9Oem2LDs/kD1WLBKgec3k qndvpDaP8MbpquhDg9Oz4Yj7QiwACmi0NgChnkINkhFeAmJjofzJ1HDO//4DfKljFStlDdn3 ezJPrrkApnVKHjMi6/ufaxh5E5E1Aoz0ddf6opJBr0ZOvL8RlfxtMDEDh8+KwG73+HnCMxk2 owCXWKPH7SWPbjJsV6I4+IvO/ODaJUUuDb7Mfgl5uThgWU3mV8HLuGV2s4cb2n9FfB7KQ3Na n31x9wFDG0ivwwkTeWshkfUAhBJYHPnZL866zw/QLmvF5zcT5zl1Kec2iq2GttNb3pdFVmQO XjtfoSAHfwLbXTBcYdajjUYWO35GMca3ha0uVqio1IGBu/d+ylD8InmyMAw/OrL0xc76T1zC c2ZlWCLVWB92G0SFHctxK4qh0t7xx+Y1LRgxeRCHIlI+vVEXwN8LpfG1PNzF/j9XwvAepGCT 1P1Cs6+D2QJR8kqi8QLf147Htyjih7Z2C//GKITmrGPQoc96LnD1mTZKMN0ynKA364k3BE9W sUaE2qgi+Zk8hTLQY7El0LMj6GxaaEVxzLA7k+GxGuK+UxaCUt+DfWDUncYaU/b69/+4ysuV peIDrIqektEwM+Gce5Rb8HxyE5BXLHlMcjfZGS4nyGxAwyJz/WCdtiifWJVxyjbBEUe9mJbt X+bKQgzADugqGPCHXRvE1zoeUbl7eh5rjuyUEY1ywiAa0Ap2aCy/1YZgvmVSvVb2bxh2m9ps ChyEVu5mcnfEcGfrhZJc6BVYNd761BClCrYuwF7Ip28PvV6nFdNFmY/90jq1hhxFsBBiZ1w9 CJsnFc0c/vIlg8RJFb6ldjqN7baK3f/5kWqYq/SgRTF1cqOv7wI8LI+okniuwegEgwj9W9m2 p9bySj5hN2CAQwMXJb2Skty+QJ9ouSQeTQ76o7Qk2ZlK7KruyPq1NcgBe9jwRGlNYQ6UuvMB ErpHssWCtL7Yvc3nVWkalQfNfpJ66coF8yjfvqCnqWsOawz+VDuxXQC64d73EWW8iN6QeOdx JcJzcaT2Q6fXiv9hlOs2izusbhNfipaXm+2yCy/QZVUerU3ZoETT2GnP8ywwNx6wZ/rQX9Rs lC5VRsK38qgeBzaaFKYv0UYzlkRrHGj3zCx1Sdrmi0Boa+W3SiIyOPnPBYKIW9EQmB+gEyke 9DlyYBHGhLxP051xFOs/iOYj+BDqb56LnXPTEsAZCXwI2x4E+OxureEf89T+cYtuCRTXv67Z APSQbr8rh0GliL7SjEGlXZrKnfw48W/w0wp7QDVZGx+p3fYZ8xqkBLW5diHAOVUwiJDXy5gz z/eGlm7OdCtu9SSjZbK9O6kBAfDHtVedzfmyYSYuW61/2pvVFekgva+l9mhCgEgyjDyy/FlU CzJqFD3ZYyhhMHYeap3O1JlAlPx8Z8wAZx4n4Y0wooZw2MFj4m98n8OkGO1OtJek/GbDjJFV XsAxNjb5xLg0UtoIyeSxo73YX6ax9Noe9iwZm5FkjJ49c1BD72YqaBVhSYg6ETtthrfOLIu+ 1VVgetr8nMRhPsF/RYg3jnISK5HBlFWZGTtj0jatI349fQPIjzzLv7okxAi1dG5UOPc/kcGA y2/I8l6W3c3t5QaUhqE0WWvuN+6PoCIN5RL8EXTyU+IjvAJesxv0KBW1Gw3YSSl+id9g+8j0 U4xh9fj4M7eej8rpOXgUns6fnX0f59BpW2r1PwD2J7Qh8f2QN1gAmlZBcO4C6v3T3RC86ygb V/GESVg+C7EQvyGTFPZsAE+6CuRdvLjf3CPeCtDlYQkFETbfRYPxlhTBWpyn4ZlRFrzmoq8I AEgt2pXvhmh+1NN0r46bUChFD2E9UHzMHFsD8HOSXgephdL40OfWSCHxsR0GSwQvpiorQjWb 3eeexwNFmYRHEqNG1HkOLCqo9jG6emRQOSkfbPIZv2VpOpSWu3tp9rn25Z6/zuKKsSEP2VzR /w91E1ZWHllGsPf0zwRQi0TnijJYoaVvhC5siFwq8m+9rzsVmeNrcOXDKBONNx05x2sqaKKN urViSQgbDgEhtUDwnjHzLVZ11kXymlvezSrDbUcpHvNQabXyco1R1YQbyJ+MtcN7rpphFEcf 56GzImshvgk3q1QaR8NT1Hql8C3aNZfJmi8MAiCH0OXLPGdIiWNxcjrYKS6QLkWjeNOthT2t yzIdi2rdjmFiTTtUAiidO9WiyTOdgdDvoywdlB2AHL4U9v6QhK+Od5zyzYxxPdn4xGCfX5ZK jV6f05X+/eI6jhEh/xkB2Fbxn9sLO3BliTAqueEetAZtvxkBikynOVfqidfqfMd/GRPQ/p7n zHXp9hlrgS9k+WB/TFgVQJHtjdBgI/jVaBKNqDQ950GUnHBrkplBYS4Dh0Lo55oCISqtfwAj NfIk633JXFJ9NeGpaP06ODbLcuGNDwqNh+7QVbp
- Ironport-sdr: sdtMBEN7G4GbfpoYjkzqqoiP8W+xQLQNg3Hz/UWEYj1G6PzvN9DX7IS9c34ds2ilHtJG1iR6ju kI1m3HWIvtsyDYJOM13UJ/TkpmApPOf9+K1I5X8BPu49JtbHibmglMk/TEpyF+L6HuVDImy2Cx GhQR4C4WgkdYVwxYpLpalNNheJk17dMk56zk3M1eXSksqdtW/+wIVYqtHdBucevU/K/76kCZkV rhX25Ij4ha7qa4NSQVQR7mXAtfAfGKf3uDXIo2EaIa+TlPYCNldNI4rGmVnv/oLiV/DrmUg+lN x31xEV9l+JrhNT94lSEfUmHV
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 *)
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 *)
- [Coq-Club] Red-Black tree and OrderedType on records, Suneel Sarswat, 09/12/2022
- Re: [Coq-Club] Red-Black tree and OrderedType on records, Li-yao Xia, 09/12/2022
Archive powered by MHonArc 2.6.19+.