feat: OrderedAssocList

Std.lean

@@ -32,6 +32,7 @@ import Std.Data.MLList
 import Std.Data.Nat
 import Std.Data.Option
 import Std.Data.Ord
+import Std.Data.OrderedAssocList
 import Std.Data.PairingHeap
 import Std.Data.Prod
 import Std.Data.RBMap

Std/Classes/Order.lean

@@ -20,6 +20,11 @@ class TotalBLE (le : α → α → Bool) : Prop where
   /-- `le` is total: either `le a b` or `le b a`. -/
   total : le a b ∨ le b a
 
+/-- `AntisymmCmp cmp` asserts that `cmp x y = .eq` only if `x = y`. -/
+class AntisymmCmp (cmp : α → α → Ordering) : Prop where
+  /-- If two terms compare as `.eq`, then they are equal. -/
+  eq_of_cmp_eq : cmp x y = .eq → x = y
+
 /-- `OrientedCmp cmp` asserts that `cmp` is determined by the relation `cmp x y = .lt`. -/
 class OrientedCmp (cmp : α → α → Ordering) : Prop where
   /-- The comparator operation is symmetric, in the sense that if `cmp x y` equals `.lt` then

Std/Data/AssocList.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
-import Std.Data.List.Basic
+import Std.Data.List.Lemmas
 
 namespace Std
 
@@ -113,6 +113,37 @@ def toListTR (as : AssocList α β) : List (α × β) :=
 @[simp] theorem length_mapVal : (mapVal f l).length = l.length := by
   induction l <;> simp_all
 
+
+/-- `O(n)`. Map a function `f` over the values of the list, dropping `none`. -/
+def filterMapVal (f : α → β → Option δ) : AssocList α β → AssocList α δ
+  | nil        => nil
+  | cons k v t => match f k v with
+    | none => filterMapVal f t
+    | some d => cons k d (filterMapVal f t)
+
+@[simp] theorem filterMapVal_nil : filterMapVal f nil = nil := rfl
+
+@[simp] theorem toList_filterMapVal (f : α → β → Option δ) (l : AssocList α β) :
+    (filterMapVal f l).toList =
+      l.toList.filterMap (fun (a, b) => (f a b).map fun v => (a, v)) := by
+  induction l with
+  | nil => simp
+  | cons k v t ih =>
+    revert ih
+    simp only [filterMapVal, toList, List.filterMap_cons]
+    match f k v with
+    | none
+    | some d => simp
+
+theorem length_filterMapVal : (filterMapVal f l).length ≤ l.length := by
+  induction l with
+  | nil => simp
+  | cons k v t ih =>
+    simp_all only [filterMapVal, length_cons]
+    match f k v with
+    | none => exact Nat.le_trans ih (Nat.le_succ _)
+    | some _ => exact Nat.succ_le_succ ih
+
 /-- `O(n)`. Returns the first entry in the list whose entry satisfies `p`. -/
 @[specialize] def findEntryP? (p : α → β → Bool) : AssocList α β → Option (α × β)
   | nil         => none