feat(data/ordmap): Ordered maps (like rb_map but better) (#5353)

This cleans up an old mathlib branch from 2 years ago, so it probably isn't in very modern style, but it would be best to get it merged and kept up to date rather than leaving it to rot.

It is an implementation of size balanced ordered maps based on Haskell's `Data.Map.Strict`. The `ordnode` structure can be used directly if one is only interested in using it for programming purposes, and the `ordset` structure bundles the proofs so that you can prove theorems about inserting and deleting doing what you expect.

docs/overview.yaml

@@ -319,6 +319,7 @@ Data structures:
     set: 'set'
     finite set: 'finset'
     multiset: 'multiset'
+    ordered set: 'ordset'
 
   Maps:
     key-value map: 'alist'
@@ -330,6 +331,7 @@ Data structures:
   Trees:
     tree: 'tree'
     red-black tree: 'rbtree'
+    size-balanced binary search tree: 'ordnode'
     W type: 'W_type'
 
 Logic and computation:

src/algebra/order.lean

@@ -236,6 +236,28 @@ lemma le_iff_le_iff_lt_iff_lt {β} [linear_order α] [linear_order β]
 
 end decidable
 
+/-- Like `cmp`, but uses a `≤` on the type instead of `<`. Given two elements
+`x` and `y`, returns a three-way comparison result `ordering`. -/
+def cmp_le {α} [has_le α] [@decidable_rel α (≤)] (x y : α) : ordering :=
+if x ≤ y then
+  if y ≤ x then ordering.eq else ordering.lt
+else ordering.gt
+
+theorem cmp_le_swap {α} [has_le α] [is_total α (≤)] [@decidable_rel α (≤)] (x y : α) :
+  (cmp_le x y).swap = cmp_le y x :=
+begin
+  by_cases xy : x ≤ y; by_cases yx : y ≤ x; simp [cmp_le, *, ordering.swap],
+  cases not_or xy yx (total_of _ _ _)
+end
+
+theorem cmp_le_eq_cmp {α} [preorder α] [is_total α (≤)]
+  [@decidable_rel α (≤)] [@decidable_rel α (<)] (x y : α) : cmp_le x y = cmp x y :=
+begin
+  by_cases xy : x ≤ y; by_cases yx : y ≤ x;
+    simp [cmp_le, lt_iff_le_not_le, *, cmp, cmp_using],
+  cases not_or xy yx (total_of _ _ _)
+end
+
 namespace ordering
 
 /-- `compares o a b` means that `a` and `b` have the ordering relation

src/data/nat/dist.lean

@@ -38,6 +38,18 @@ begin rw [dist.def, sub_eq_zero_of_le h, zero_add] end
 theorem dist_eq_sub_of_le_right {n m : ℕ} (h : m ≤ n) : dist n m = n - m :=
 begin rw [dist_comm], apply dist_eq_sub_of_le h end
 
+theorem dist_tri_left (n m : ℕ) : m ≤ dist n m + n :=
+le_trans (nat.le_sub_add _ _) (add_le_add_right (le_add_left _ _) _)
+
+theorem dist_tri_right (n m : ℕ) : m ≤ n + dist n m :=
+by rw add_comm; apply dist_tri_left
+
+theorem dist_tri_left' (n m : ℕ) : n ≤ dist n m + m :=
+by rw dist_comm; apply dist_tri_left
+
+theorem dist_tri_right' (n m : ℕ) : n ≤ m + dist n m :=
+by rw dist_comm; apply dist_tri_right
+
 theorem dist_zero_right (n : ℕ) : dist n 0 = n :=
 eq.trans (dist_eq_sub_of_le_right (zero_le n)) (nat.sub_zero n)
 

src/data/nat/psub.lean

@@ -56,7 +56,7 @@ theorem psub_eq_some {m : ℕ} : ∀ {n k}, psub m n = some k ↔ k + n = m
     simp [psub_eq_some, add_comm, add_left_comm, nat.succ_eq_add_one]
   end
 
-theorem psub_eq_none (m n : ℕ) : psub m n = none ↔ m < n :=
+theorem psub_eq_none {m n : ℕ} : psub m n = none ↔ m < n :=
 begin
   cases s : psub m n; simp [eq_comm],
   { show m < n, refine lt_of_not_ge (λ h, _),
@@ -74,4 +74,11 @@ psub_eq_some.2 $ nat.sub_add_cancel h
 theorem psub_add (m n k) : psub m (n + k) = do x ← psub m n, psub x k :=
 by induction k; simp [*, add_succ, bind_assoc]
 
+/-- Same as `psub`, but with a more efficient implementation. -/
+@[inline] def psub' (m n : ℕ) : option ℕ := if n ≤ m then some (m - n) else none
+
+theorem psub'_eq_psub (m n) : psub' m n = psub m n :=
+by rw [psub']; split_ifs;
+  [exact (psub_eq_sub h).symm, exact (psub_eq_none.2 (not_le.1 h)).symm]
+
 end nat