Add ZUtil.Sorting

1 files changed, 21 insertions, 0 deletions

diff --git a/src/Util/ZUtil/Sorting.v b/src/Util/ZUtil/Sorting.v
new file mode 100644
index 000000000..1f25ff80b
--- /dev/null
+++ b/src/Util/ZUtil/Sorting.v
@@ -0,0 +1,21 @@
+Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
+Require Import Coq.Sorting.Mergesort Coq.Structures.Orders.
+
+Module Z.
+  Module Order <: TotalLeBool.
+    Definition t := Z.
+    Definition leb := Z.leb.
+    Infix "<=?" := leb.
+    Local Coercion is_true : bool >-> Sortclass.
+    Theorem leb_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
+    Proof. intros x y; destruct (Z.le_ge_cases x y); [ left | right ]; unfold is_true, leb; rewrite Z.leb_le; omega. Qed.
+  End Order.
+
+  Module Sort := Mergesort.Sort Order.
+
+  Notation sort := Sort.sort.
+  Notation Sorted_sort := Sort.Sorted_sort.
+  Notation LocallySorted_sort := Sort.LocallySorted_sort.
+  Notation StronglySorted_sort := Sort.StronglySorted_sort.
+  Notation Permuted_sort := Sort.Permuted_sort.
+End Z.