blob: 1f25ff80b52a24084466f5d9d18969a716c8220b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
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.
|
