From 655c9af702bf47b6b149fd8a25211e09087065f8 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 23 Jan 2024 17:19:21 +1100 Subject: [PATCH 01/18] OrderedAssocList --- Std/Classes/Order.lean | 5 + Std/Data/AssocList.lean | 33 +- Std/Data/OrderedAssocList.lean | 919 +++++++++++++++++++++++++++++++++ Std/Logic.lean | 8 + 4 files changed, 964 insertions(+), 1 deletion(-) create mode 100644 Std/Data/OrderedAssocList.lean diff --git a/Std/Classes/Order.lean b/Std/Classes/Order.lean index c5f70db253..dcd3f58fd1 100644 --- a/Std/Classes/Order.lean +++ b/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 diff --git a/Std/Data/AssocList.lean b/Std/Data/AssocList.lean index fa0c49f80d..885ab21aa2 100644 --- a/Std/Data/AssocList.lean +++ b/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 diff --git a/Std/Data/OrderedAssocList.lean b/Std/Data/OrderedAssocList.lean new file mode 100644 index 0000000000..f7c145d43c --- /dev/null +++ b/Std/Data/OrderedAssocList.lean @@ -0,0 +1,919 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +import Std.Data.AssocList +import Std.Classes.Order +import Std.Data.Option.Lemmas +import Std.Tactic.Ext +import Std.Tactic.LeftRight +import Std.Tactic.Omega + +/-! +# Ordered association lists + +`OrderedAssocList` is a wrapper around `AssocList`, +with the additional invariant that the keys are in strictly increasing order. + +As a consequence, an `OrderedAssocList` is determined by the `find?` function, that is +`(∀ a, l₁.find? a = l₂.find? a) → l₁ = l₂` +and this makes providing identities between operations more plausible than with `AssocList`. + +We will later add another wrapper requiring that a "default" value does not appear, +so e.g. finitely supported functions can be uniquely represented. + +The main operations defined are: +* `find?`, which linearly searches the list, stopping if the keys get too large. +* `insert`, which inserts a new key-value pair, maintaining the order invariant. +* `filterMapVal f`, for `f : α → β → Option γ`, which applies a function to values, + dropping some values. +* `merge f` for `f : α → Option β → Option γ → Option δ` which merges two lists, + dropping some values. It runs in time `O(l₁.length + l₂.length)`. +-/ + +namespace Std + +/-! +We first define some predicates and operations in the `AssocList` namespace. + +* `keysOrdered cmp l` asserts that the keys of an `l : AssocList` are strictly increasing + with respect to a comparator `cmp`. +* `ltHeadKey? cmp a l` asserts that `a` is less than (according to `cmp`) the first key of `l`, + or that `l` is empty. +-/ + +namespace AssocList + +/-- +The predicate that the keys of an `AssocList` are +in strictly increasing order according to the comparator `cmp`. +-/ +def keysOrdered (cmp : α → α → Ordering) : AssocList α β → Prop + | .nil => True + | .cons _ _ .nil => True + | .cons a _ (.cons x y t) => cmp a x = .lt ∧ keysOrdered cmp (.cons x y t) + +instance instKeysOrderedDecidablePred : DecidablePred (keysOrdered cmp : AssocList α β → Prop) := by + rintro (_|⟨a, b, _|_⟩) <;> dsimp [keysOrdered] + · infer_instance + · infer_instance + · exact @instDecidableAnd _ _ _ (instKeysOrderedDecidablePred _) + +theorem keysOrdered.tail (h : keysOrdered cmp (.cons a b t)) : keysOrdered cmp t := + match t with + | .nil => trivial + | .cons .. => h.2 + +/-- The head key of an `AssocList`, or `none` if the list is empty. -/ +def headKey? (l : AssocList α β) : Option α := + match l with + | .nil => none + | .cons a _ _ => some a + +@[simp] theorem headKey?_nil : headKey? (.nil : AssocList α β) = none := rfl +@[simp] theorem headKey?_cons : headKey? (.cons a b t) = some a := rfl + +/-- +The condition that an element is less than the first key of an `AssocList`, or that list is empty. +-/ +abbrev ltHeadKey? (cmp : α → α → Ordering) (a : α) (t : AssocList α β) : Prop := + match headKey? t with | none => True | some x => cmp a x = .lt + +@[simp] theorem ltHeadKey?_nil {cmp : α → α → Ordering} : + ltHeadKey? cmp a (.nil : AssocList α β) = True := rfl +@[simp] theorem ltHeadKey?_cons : ltHeadKey? cmp a (.cons x y t) = (cmp a x = .lt) := rfl + +theorem ltHeadKey?_of_keysOrdered_cons (w : keysOrdered cmp (cons a b t)) : ltHeadKey? cmp a t := + match t with + | .nil => trivial + | .cons _ _ _ => w.1 + +theorem ltHeadKey?_of_cons [TransCmp cmp] (w : ltHeadKey? cmp a (cons x y t)) + (h : keysOrdered cmp (cons x y t)) : + ltHeadKey? cmp a t := by + have h := ltHeadKey?_of_keysOrdered_cons h + revert w h + dsimp [ltHeadKey?] + split + · simp + · exact TransCmp.lt_trans + +theorem ltHeadKey?_of_le [TransCmp cmp] (h : cmp x a ≠ .gt) (w : ltHeadKey? cmp a t) : + ltHeadKey? cmp x t := by + revert w + dsimp [ltHeadKey?] + split + · simp + · exact TransCmp.le_lt_trans h + +/-- +The head key of the first list is at most the head key of the second list, +or the second list is empty. +-/ +abbrev headKey?_le_headKey? (cmp : α → α → Ordering) (s : AssocList α β) (t : AssocList α γ) : Prop := + match s.headKey?, t.headKey? with + | some a₁, some a₂ => cmp a₁ a₂ ≠ .gt + | none, some _ => False + | _, none => True + +@[simp] theorem headKey?_le_headKey?_cons_cons : + headKey?_le_headKey? cmp (cons a b t) (cons x y s) = (cmp a x ≠ .gt) := rfl + +theorem ltHeadKey?_of_headKey?_le_headKey? [TransCmp cmp] + (w : ltHeadKey? cmp a s) (h : headKey?_le_headKey? cmp s t) : + ltHeadKey? cmp a t := by + dsimp [ltHeadKey?, headKey?_le_headKey?] at * + revert h w + match headKey? s, headKey? t with + | some a, some b => exact TransCmp.lt_le_trans + | some a, none => intros; trivial + | none, some b => simp + | none, none => intros; trivial + +theorem headKey?_le_headKey?_cons [TransCmp cmp] + (h : keysOrdered cmp (cons x y t)) (w : headKey?_le_headKey? cmp t s) : + headKey?_le_headKey? cmp (cons x y t) s := by + have p := ltHeadKey?_of_keysOrdered_cons h + dsimp [ltHeadKey?, headKey?_le_headKey?] at * + revert p w + match headKey? s, headKey? t with + | some a, some b => + intro p w + simp [TransCmp.lt_le_trans w p] + | some a, none => intros; trivial + | none, some b => simp + | none, none => intros; trivial + +theorem keysOrdered_cons {cmp : α → α → Ordering} + (w : ltHeadKey? cmp a t) (h : keysOrdered cmp t) : + keysOrdered cmp (.cons a b t) := by + match t with + | .nil => trivial + | .cons x y s => exact ⟨w, h⟩ + +theorem find?_eq_none_of_ltHeadKey? {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEq α] + (w : ltHeadKey? cmp a l) (h : keysOrdered cmp l) : + l.find? a = none := by + match l with + | nil => rfl + | cons x y t => + rw [find?] + split + · simp_all [OrientedCmp.cmp_refl] + · exact find?_eq_none_of_ltHeadKey? (ltHeadKey?_of_cons w h) h.tail + +/-! +# Ordered-respecting operations on `AssocList` + +We now define `orderedInsert`, and `orderedMerge`, +which will later be wrapped as `OrderedAssocList.insert` and `OrderedAssocList.merge`. + +We prove that with `keysOrdered` input these functions produce `keysOrdered` outputs. +We prove that same about `AssocList.filterMapVal`. +-/ + +/-- +Insert a key-value pair into an `AssocList`, +in such a way that if the original list has keys in increasing order, +so does the result. +(Otherwise, it is inserted before the first key the new key is smaller than, +or replaces the first key the new key is equal to.) + +We later wrap this as `OrderedAssocList.insert`. +-/ +def orderedInsert (cmp : α → α → Ordering) (l : AssocList α β) (a : α) (b : β) : AssocList α β := + match l with + | .nil => .cons a b .nil + | .cons x y t => match w : cmp a x with + | .lt => .cons a b l + | .eq => .cons a b t + | .gt => .cons x y (orderedInsert cmp t a b) + +theorem headKey?_orderedInsert {l : AssocList α β} : + headKey? (orderedInsert cmp l a b) = + match headKey? l with + | none => some a + | some x => match cmp a x with | .lt | .eq => some a | .gt => some x := by + match l with + | .nil => rfl + | .cons x _ _ => dsimp [headKey?, orderedInsert]; cases cmp a x <;> rfl + +theorem headKey?_orderedInsert_or (cmp) (l : AssocList α β) (a) (b) : + headKey? (orderedInsert cmp l a b) = some a ∨ + headKey? (orderedInsert cmp l a b) = headKey? l := by + rw [headKey?_orderedInsert] + match l with + | .nil => left; rfl + | .cons x y s => dsimp; cases cmp a x <;> simp + +theorem orderedInsert_keysOrdered [AntisymmCmp cmp] [OrientedCmp cmp] (h : keysOrdered cmp l) : + keysOrdered cmp (orderedInsert cmp l a b) := by + match l with + | .nil => trivial + | .cons x y t => + dsimp [orderedInsert] + match w : cmp a x with + | .lt => exact ⟨w, h⟩ + | .eq => + rcases AntisymmCmp.eq_of_cmp_eq w with rfl + cases t <;> exact h + | .gt => exact aux h w +-- I've split this step out with a name as it is useful to fill in a proof term later. +where aux [AntisymmCmp cmp] [OrientedCmp cmp] {x y t} + (h : keysOrdered cmp (cons x y t)) (w : cmp a x = Ordering.gt) : + keysOrdered cmp (cons x y (orderedInsert cmp t a b)) := by + apply keysOrdered_cons + · dsimp [ltHeadKey?] + rcases headKey?_orderedInsert_or cmp t a b with (p|p) + · rw [p] + exact OrientedCmp.cmp_eq_gt.mp w + · rw [p] + exact ltHeadKey?_of_keysOrdered_cons h + · apply orderedInsert_keysOrdered + exact h.tail + +theorem headKey?_le_headKey?_filterMapVal [TransCmp cmp] (h : keysOrdered cmp l) : + headKey?_le_headKey? cmp l (l.filterMapVal f) := by + match l with + | .nil => simp [headKey?_le_headKey?] + | .cons x y t => + simp [filterMapVal] + match f x y with + | none => + exact headKey?_le_headKey?_cons h (headKey?_le_headKey?_filterMapVal h.tail) + | some _ => simp [OrientedCmp.cmp_refl] + +theorem filterMapVal_keysOrdered [TransCmp cmp] (h : keysOrdered cmp l) : + keysOrdered cmp (l.filterMapVal f) := by + match l with + | .nil => exact h + | .cons x y t => + simp only [filterMapVal] + split + · exact filterMapVal_keysOrdered h.tail + · apply keysOrdered_cons + · exact ltHeadKey?_of_headKey?_le_headKey? (ltHeadKey?_of_keysOrdered_cons h) + (headKey?_le_headKey?_filterMapVal h.tail) + · exact filterMapVal_keysOrdered h.tail + +/-- +Merge two `AssocList`s, +at each stage taking the first key-value pair from whichever list has a smaller first key. +If both inputs have keys in strictly increasing order, so does the result. +(We later wrap this as `OrderedAssocList.merge`.) + +We combine values using a function `f : α → Option β → Option γ → Option δ` which we call as +`f a (some b) none` when encountering a key present only in the first list (with value `b`), +`f a none (some g)` when encountering a key present only in the second list (with value `g`), and +`f a (some b) (some g)` when encountering a key present in both lists. +(Note the value of `f a none none` is never used.) +-/ +def orderedMerge (cmp : α → α → Ordering) (f : α → Option β → Option γ → Option δ) : + AssocList α β → AssocList α γ → AssocList α δ + | .nil, .nil => nil + | .nil, .cons a₂ g t₂ => filterMapVal (fun a g => f a none (some g)) (.cons a₂ g t₂) + | .cons a₁ b t₁, .nil => filterMapVal (fun a b => f a (some b) none) (.cons a₁ b t₁) + | .cons a₁ b t₁, .cons a₂ g t₂ => match cmp a₁ a₂ with + | .lt => match (f a₁ (some b) none) with + | some d => .cons a₁ d (orderedMerge cmp f t₁ (.cons a₂ g t₂)) + | none => orderedMerge cmp f t₁ (.cons a₂ g t₂) + | .eq => match (f a₁ (some b) (some g)) with + | some d => .cons a₁ d (orderedMerge cmp f t₁ t₂) + | none => orderedMerge cmp f t₁ t₂ + | .gt => match (f a₂ none (some g)) with + | some d => .cons a₂ d (orderedMerge cmp f (.cons a₁ b t₁) t₂) + | none => orderedMerge cmp f (.cons a₁ b t₁) t₂ +termination_by _ l₁ l₂ => l₁.length + l₂.length +decreasing_by simp_wf; omega + +theorem ltHeadKey?_orderedMerge [TransCmp cmp] + (h₁ : ltHeadKey? cmp a l₁) (h₂ : ltHeadKey? cmp a l₂) + (w₁ : keysOrdered cmp l₁) (w₂ : keysOrdered cmp l₂) : + ltHeadKey? cmp a (orderedMerge cmp f l₁ l₂) := by + match l₁, l₂ with + | .nil, .nil => simp [orderedMerge] + | .nil, .cons a₂ g t₂ => + rw [orderedMerge] + exact ltHeadKey?_of_headKey?_le_headKey? h₂ (headKey?_le_headKey?_filterMapVal w₂) + | .cons a₁ b t₁, .nil => + rw [orderedMerge] + exact ltHeadKey?_of_headKey?_le_headKey? h₁ (headKey?_le_headKey?_filterMapVal w₁) + | .cons a₁ b t₁, .cons a₂ g t₂ => + rw [orderedMerge] + match cmp a₁ a₂ with + | .lt => + dsimp + split + · exact h₁ + · exact ltHeadKey?_orderedMerge (ltHeadKey?_of_cons h₁ w₁) h₂ w₁.tail w₂ + | .eq => + dsimp + split + · exact h₁ + · exact ltHeadKey?_orderedMerge (ltHeadKey?_of_cons h₁ w₁) (ltHeadKey?_of_cons h₂ w₂) + w₁.tail w₂.tail + | .gt => + dsimp + split + · exact h₂ + · exact ltHeadKey?_orderedMerge h₁ (ltHeadKey?_of_cons h₂ w₂) w₁ w₂.tail + +theorem orderedMerge_keysOrdered [AntisymmCmp cmp] [TransCmp cmp] + (h₁ : keysOrdered cmp l₁) (h₂ : keysOrdered cmp l₂) : + keysOrdered cmp (orderedMerge cmp f l₁ l₂) := by + match l₁, l₂ with + | .nil, .nil => trivial + | .nil, .cons a₂ g t₂ => exact filterMapVal_keysOrdered h₂ + | .cons a₁ b t₁, .nil => exact filterMapVal_keysOrdered h₁ + | .cons a₁ b t₁, .cons a₂ g t₂ => + rw [orderedMerge] + match h : cmp a₁ a₂ with + | .lt => match (f a₁ (some b) none) with + | some d => + apply keysOrdered_cons + · apply ltHeadKey?_orderedMerge (ltHeadKey?_of_keysOrdered_cons h₁) (ltHeadKey?_cons.mpr h) + h₁.tail h₂ + · exact orderedMerge_keysOrdered h₁.tail h₂ + | none => exact orderedMerge_keysOrdered h₁.tail h₂ + | .eq => match (f a₁ (some b) (some g)) with + | some d => + dsimp + apply keysOrdered_cons + · rcases (AntisymmCmp.eq_of_cmp_eq h) with rfl + exact ltHeadKey?_orderedMerge (ltHeadKey?_of_keysOrdered_cons h₁) + (ltHeadKey?_of_keysOrdered_cons h₂) h₁.tail h₂.tail + · exact orderedMerge_keysOrdered h₁.tail h₂.tail + | none => exact orderedMerge_keysOrdered h₁.tail h₂.tail + | .gt => match (f a₂ none (some g)) with + | some d => + apply keysOrdered_cons + · apply ltHeadKey?_orderedMerge (ltHeadKey?_cons.mpr (OrientedCmp.cmp_eq_gt.mp h)) + (ltHeadKey?_of_keysOrdered_cons h₂) h₁ h₂.tail + · exact orderedMerge_keysOrdered h₁ h₂.tail + | none => exact orderedMerge_keysOrdered h₁ h₂.tail + +end AssocList + +/-- +An `OrderedAssocList` is an `AssocList` with the additional invariant that +the keys are in strictly increasing order according to some specified comparator function. +-/ +structure OrderedAssocList {α : Type u} (cmp : α → α → Ordering) (β : Type v) where + /-- The underlying `AssocList` of an `OrderedAssocList`. -/ + list : AssocList α β + /-- The invariant that the keys are in strictly increasing order according to `cmp`. -/ + keysOrdered : list.keysOrdered cmp + +namespace OrderedAssocList + +variable {α : Type u} {cmp : α → α → Ordering} + +/-- The empty `OrderedAssocList`. -/ +def nil : OrderedAssocList cmp β := ⟨.nil, trivial⟩ + +/-- The length of an `OrderedAssocList`. -/ +def length (l : OrderedAssocList cmp β) : Nat := l.list.length + +@[simp] theorem length_nil : length (nil : OrderedAssocList cmp β) = 0 := rfl +@[simp] theorem length_mk_cons : length ⟨.cons a b t, h⟩ = length ⟨t, h.tail⟩ + 1 := + rfl + +/-- The first key-value pair in an `OrderedAssocList`. -/ +def head? (l : OrderedAssocList cmp β) : Option (α × β) := + match l with + | ⟨.nil, _⟩ => none + | ⟨.cons a b _, _⟩ => some (a, b) + +/-- The tail of an `OrderedAssocList`. -/ +def tail (l : OrderedAssocList cmp β) : OrderedAssocList cmp β := + match l with + | ⟨.nil, _⟩ => l + | ⟨.cons _ _ t, h⟩ => ⟨t, h.tail⟩ + +@[simp] theorem length_tail : length (tail l) = length l - 1 := by + match l with + | ⟨.nil, _⟩ => rfl + | ⟨.cons _ _ _, _⟩ => rfl + +/-- +Find the value associated to a key by traversing left to right, +short-circuiting once we are considering larger keys. +-/ +def find? (l : OrderedAssocList cmp β) (x : α) : Option β := + match l with + | ⟨.nil, _⟩ => none + | ⟨.cons a b t, h⟩ => match cmp x a with + | .lt => none + | .eq => some b + | .gt => find? ⟨t, h.tail⟩ x + +theorem find?_eq_find?_list [AntisymmCmp cmp] [TransCmp cmp] [BEq α] [LawfulBEq α] + {l : OrderedAssocList cmp β} : l.find? x = l.list.find? x := by + match l with + | ⟨.nil, _⟩ => rfl + | ⟨.cons a b t, h⟩ => + rw [find?, AssocList.find?] + split + · split + · simp_all [OrientedCmp.cmp_refl] + · rw [AssocList.find?_eq_none_of_ltHeadKey? (cmp := cmp)] + · exact AssocList.ltHeadKey?_of_le (by simp_all) + (AssocList.ltHeadKey?_of_keysOrdered_cons h) + · exact h.tail + · simp_all [AntisymmCmp.eq_of_cmp_eq ‹_›] + · split + · simp_all [OrientedCmp.cmp_refl] + · apply find?_eq_find?_list + +@[simp] theorem find?_nil : find? (nil : OrderedAssocList cmp β) x = none := rfl +@[simp] theorem find?_mk_nil : find? ⟨.nil, h⟩ x = none := rfl + +/-- The first key in an `OrderedAssocList`, or `none` if the list is empty. -/ +def headKey? (l : OrderedAssocList cmp β) : Option α := l.list.headKey? + +@[simp] theorem headKey?_nil : headKey? (nil : OrderedAssocList cmp β) = none := rfl +@[simp] theorem headKey?_mk_cons : headKey? ⟨.cons a b t, h⟩ = some a := rfl + +/-- Either `a` is less than the first key of `l`, or `l` is empty. -/ +def ltHeadKey? (a : α) (l : OrderedAssocList cmp β) : Prop := AssocList.ltHeadKey? cmp a l.list + +/-- The head key of a tail is either `none`, or greater than the original head key. -/ +theorem headKey?_tail (h : AssocList.keysOrdered cmp (.cons a b t)) : + ltHeadKey? a ⟨t, h.tail⟩ := by + dsimp [ltHeadKey?] + match t with + | .nil => trivial + | .cons _ _ _ => exact h.1 + +theorem find?_eq_none_of_ltHeadKey? (l : OrderedAssocList cmp β) (w : ltHeadKey? x l) : + find? l x = none := by + match l with + | ⟨.nil, _⟩ => rfl + | ⟨.cons a b t, h⟩ => + match p : cmp x a with + | .lt => simp [find?, p] + | .eq => simp_all [ltHeadKey?] + | .gt => simp_all [ltHeadKey?] + +theorem find?_mk_cons [OrientedCmp cmp] [TransCmp cmp] + {h : (AssocList.cons a b t).keysOrdered cmp} : + find? ⟨.cons a b t, h⟩ x = if cmp x a = .eq then some b else find? ⟨t, h.tail⟩ x := by + simp only [find?] + split <;> rename_i w <;> simp only [w, ite_true, ite_false] + rw [find?_eq_none_of_ltHeadKey?] + have p := headKey?_tail h + revert p + simp only [ltHeadKey?, AssocList.ltHeadKey?] + split + · trivial + · exact TransCmp.lt_trans w + +@[simp] theorem find?_mk_cons_self [OrientedCmp cmp] {h : (AssocList.cons a b t).keysOrdered cmp} : + find? ⟨.cons a b t, h⟩ a = some b := by + simp [find?, OrientedCmp.cmp_refl] + +theorem ext_list {l₁ l₂ : OrderedAssocList cmp β} (w : l₁.list = l₂.list) : l₁ = l₂ := by + cases l₁; cases l₂; congr + +theorem ext [AntisymmCmp cmp] [OrientedCmp cmp] [TransCmp cmp] {l₁ l₂ : OrderedAssocList cmp β} + (w : ∀ a, l₁.find? a = l₂.find? a) : l₁ = l₂ := by + match h₁ : l₁, h₂ : l₂ with + | ⟨.nil, _⟩, ⟨.nil, _⟩ => rfl + | ⟨.cons a b t, _⟩, ⟨.nil, _⟩ => + exfalso + specialize w a + simp_all + | ⟨.nil, _⟩, ⟨.cons a b t, _⟩ => + exfalso + specialize w a + simp_all + | ⟨.cons a₁ b₁ t₁, p₁⟩, ⟨.cons a₂ b₂ t₂, p₂⟩ => + match h : cmp a₁ a₂ with + | .lt => + exfalso + have w₂ : l₂.find? a₁ = none := by + simp [find?_eq_none_of_ltHeadKey?, h₂, ltHeadKey?, h] + specialize w a₁ + simp_all + | .eq => + rcases AntisymmCmp.eq_of_cmp_eq h + have w' := w a₁ + simp only [find?_mk_cons_self, Option.some.injEq] at w' + congr + suffices (⟨t₁, p₁.tail⟩ : OrderedAssocList cmp β) = ⟨t₂, p₂.tail⟩ by injections + apply ext + intro a + specialize w a + simp only [find?_mk_cons] at w + split at w <;> rename_i h + · rcases AntisymmCmp.eq_of_cmp_eq h + rw [find?_eq_none_of_ltHeadKey?, find?_eq_none_of_ltHeadKey?] + apply headKey?_tail p₂ + apply headKey?_tail p₁ + · exact w + | .gt => + exfalso + have w₁ : l₁.find? a₂ = none := by + simp [find?_eq_none_of_ltHeadKey?, h₁, ltHeadKey?, h, ← OrientedCmp.cmp_eq_gt] + specialize w a₂ + simp_all + +-- Since this was a recursive theorem we have to add the attribute after the fact. +attribute [ext] ext + +/-- Check if an `OrderedAssocList` contains a specific key. -/ +def contains (l : OrderedAssocList cmp β) (x : α) : Bool := (l.find? x).isSome + +@[simp] theorem contains_nil : contains (nil : OrderedAssocList cmp β) x = false := rfl +@[simp] theorem contains_mk_cons_self [OrientedCmp cmp] + {h : (AssocList.cons a b t).keysOrdered cmp} : + contains ⟨.cons a b t, h⟩ a = true := by + simp [contains] + +/-- +Prepend a key-value pair, +requiring a proof that the key is smaller than the existing smallest key. +-/ +def cons (a : α) (b : β) (l : OrderedAssocList cmp β) (w : ltHeadKey? a l) : + OrderedAssocList cmp β := + match l with + | ⟨.nil, _⟩ => ⟨.cons a b .nil, trivial⟩ + | ⟨.cons x y t, h⟩ => ⟨.cons a b (.cons x y t), ⟨w, h⟩⟩ + +@[simp] theorem list_cons : (cons a b l w).list = .cons a b l.list := by + dsimp [cons] + match l with + | ⟨.nil, _⟩ => rfl + | ⟨.cons x y t, h⟩ => rfl + +@[simp] theorem find?_cons [TransCmp cmp] {l : OrderedAssocList cmp β} {w} : + (cons a b l w).find? x = if cmp x a = .eq then some b else l.find? x := by + simp only [cons] + split <;> simp [find?_mk_cons] + +@[simp] theorem headKey?_cons : headKey? (cons a b l w) = some a := by + match l with + | ⟨.nil, _⟩ + | ⟨.cons _ _ _, _⟩ => rfl + +section insert +variable [AntisymmCmp cmp] + +section +variable [OrientedCmp cmp] + +/-- +Insert a key-value pair into an `OrderedAssocList`. +This replaces the current value if the key is already present, +and otherwise inserts it before the first key which is greater than the inserted key. +-/ +def insert (l : OrderedAssocList cmp β) (a : α) (b : β) : OrderedAssocList cmp β := + ⟨l.list.orderedInsert cmp a b, AssocList.orderedInsert_keysOrdered l.keysOrdered⟩ + +@[simp] theorem insert_mk_nil : + insert (⟨.nil, h⟩ : OrderedAssocList cmp β) a b = ⟨.cons a b .nil, trivial⟩ := rfl + +@[simp] theorem insert_mk_cons : + insert (⟨.cons x y t, h⟩ : OrderedAssocList cmp β) a b = match w : cmp a x with + | .lt => ⟨.cons a b (.cons x y t), ⟨w, h⟩⟩ + | .eq => ⟨.cons a b t, by + cases (AntisymmCmp.eq_of_cmp_eq w); cases t <;> exact h⟩ + | .gt => .cons x y (insert ⟨t, h.tail⟩ a b) (AssocList.ltHeadKey?_of_keysOrdered_cons + (AssocList.orderedInsert_keysOrdered.aux h w)) := by + dsimp [insert, AssocList.orderedInsert] + congr + split <;> simp + +theorem length_insert_ne_zero {l : OrderedAssocList cmp β} : (insert l a b).length ≠ 0 := by + match l with + | ⟨.nil, _⟩ => simp + | ⟨.cons x y t, _⟩ => + dsimp [insert, AssocList.orderedInsert, length] + split <;> simp + +end + +variable [TransCmp cmp] + +theorem find?_insert (l : OrderedAssocList cmp β) (a : α) (b : β) : + (insert l a b).find? x = if cmp x a = .eq then some b else l.find? x := by + match l with + | ⟨.nil, _⟩ => simp only [insert_mk_nil, find?_mk_cons] + | ⟨.cons a' b' t, h⟩ => + simp only [insert_mk_cons] + split <;> rename_i h₁ + · simp [find?_mk_cons] + · rcases AntisymmCmp.eq_of_cmp_eq h₁ + simp [find?_mk_cons] + · rw [find?_cons, find?_insert ⟨t, h.tail⟩, find?_mk_cons] + split <;> rename_i h₂ + · rcases (AntisymmCmp.eq_of_cmp_eq h₂).symm + simp_all [OrientedCmp.cmp_eq_gt] + · rfl +termination_by _ => l.length + +theorem find?_insert_self (l : OrderedAssocList cmp β) (a : α) (b : β) : + (insert l a b).find? a = some b := by + simp [find?_insert, OrientedCmp.cmp_refl] + +theorem insert_contains (l : OrderedAssocList cmp β) (a : α) (b : β) : + (l.insert a b).contains x = ((cmp x a = .eq) || l.contains x) := by + simp only [contains, find?_insert] + split <;> rename_i h + · simp [h] + · cases find? l x <;> simp [h] + +theorem insert_contains_self (l : OrderedAssocList cmp β) (a : α) (b : β) : + (l.insert a b).contains a = true := by + simp [insert_contains, OrientedCmp.cmp_refl] + +end insert + +section filterMapVal + +variable [TransCmp cmp] + +/-- +Apply a function to each key-value pair, +either replacing the value or dropping it if the function returns `none`. +-/ +def filterMapVal (f : α → β → Option δ) (l : OrderedAssocList cmp β) : + OrderedAssocList cmp δ := + ⟨l.list.filterMapVal f, AssocList.filterMapVal_keysOrdered l.keysOrdered⟩ + +@[simp] theorem filterMapVal_nil {f : α → β → Option γ} : + filterMapVal f (nil : OrderedAssocList cmp β) = nil := rfl + +private theorem filterMapVal_mk_cons_list (f : α → β → Option γ) (x) (y) (t) (h) : + (filterMapVal f (⟨.cons x y t, h⟩ : OrderedAssocList cmp β)).list = + match f x y with + | none => AssocList.filterMapVal f t + | some g => .cons x g (filterMapVal f ⟨t, h.tail⟩).1 := by + dsimp [filterMapVal, AssocList.filterMapVal] + split <;> simp_all + +private theorem filterMapVal_mk_cons {f : α → β → Option γ} : + filterMapVal f (⟨.cons x y t, h⟩ : OrderedAssocList cmp β) = + match w : f x y with + | none => filterMapVal f ⟨t, h.tail⟩ + | some g => ⟨.cons x g (filterMapVal f ⟨t, h.tail⟩).1, by + have p := filterMapVal_mk_cons_list f x y t h + simp only [w] at p + simp only [← p] + exact (filterMapVal f ⟨.cons x y t, h⟩).keysOrdered⟩ := by + apply ext_list + simp only [filterMapVal_mk_cons_list] + split <;> simp_all [filterMapVal] + +@[simp] +theorem find?_filterMapVal [AntisymmCmp cmp] (l : OrderedAssocList cmp β) : + (filterMapVal f l).find? a = (l.find? a).bind (fun b => f a b) := by + -- This isn't true at the level of `AssocList`; we need uniqueness of keys. + match l with + | ⟨.nil, _⟩ => rfl + | ⟨.cons x y t, h⟩ => + simp only [filterMapVal_mk_cons, find?_mk_cons] + split + · rw [find?_filterMapVal ⟨t, h.tail⟩] + split <;> rename_i h' + · have h' := AntisymmCmp.eq_of_cmp_eq h' + rw [find?_eq_none_of_ltHeadKey?] + · simp_all + · rcases h' with rfl + exact AssocList.ltHeadKey?_of_keysOrdered_cons h + · rfl + · simp only [find?_mk_cons] + split <;> rename_i h' + · simp_all [AntisymmCmp.eq_of_cmp_eq h'] + · rw [find?_filterMapVal] +termination_by _ l => l.length + +theorem filterMapVal_filterMapVal [AntisymmCmp cmp] [TransCmp cmp] + {f : α → γ → Option δ} {g : α → β → Option γ} + {l : OrderedAssocList cmp β} : + filterMapVal f (filterMapVal g l) = filterMapVal (fun a b => (g a b).bind (fun c => f a c)) l := by + ext a d + simp only [find?_filterMapVal, Option.mem_def, Option.bind_eq_some] + constructor + · rintro ⟨c, ⟨⟨b, hb, hc⟩, hd⟩⟩ + refine ⟨b, hb, c, hc, hd⟩ + · rintro ⟨b, hb, c, hc, hd⟩ + refine ⟨c, ⟨⟨b, hb, hc⟩, hd⟩⟩ + +end filterMapVal + +section merge + +variable [AntisymmCmp cmp] [TransCmp cmp] + +/-- +Merge two `OrderedAssocList`s using a function `α → Option β → Option γ → Option δ`, +dropping values where the function returns `none`. +-/ +def merge (f : α → Option β → Option γ → Option δ) + (l₁ : OrderedAssocList cmp β) (l₂ : OrderedAssocList cmp γ) : OrderedAssocList cmp δ := + ⟨AssocList.orderedMerge cmp f l₁.list l₂.list, + AssocList.orderedMerge_keysOrdered l₁.keysOrdered l₂.keysOrdered⟩ + +@[simp] theorem list_merge {l₁ : OrderedAssocList cmp β} : + (merge f l₁ l₂).list = AssocList.orderedMerge cmp f l₁.list l₂.list := + rfl + +@[simp] theorem merge_nil_nil {f : α → Option β → Option γ → Option δ} : + merge f (nil : OrderedAssocList cmp β) nil = nil := rfl + +@[simp] theorem merge_mk_nil_mk_cons {f : α → Option β → Option γ → Option δ} : + merge f (⟨.nil, h⟩ : OrderedAssocList cmp β) ⟨.cons x' y' t', h'⟩ = + filterMapVal (fun a g => f a none (some g)) ⟨.cons x' y' t', h'⟩ := rfl + +@[simp] theorem merge_mk_cons_mk_nil {f : α → Option β → Option γ → Option δ} : + merge f ⟨.cons x y t, h⟩ (⟨.nil, h'⟩ : OrderedAssocList cmp γ) = + filterMapVal (fun a b => f a (some b) none) ⟨.cons x y t, h⟩ := rfl + +private theorem merge_mk_cons_mk_cons_list + (f : α → Option β → Option γ → Option δ) (x y t h x' y' t' h') : + (merge f (⟨.cons x y t, h⟩ : OrderedAssocList cmp β) ⟨.cons x' y' t', h'⟩).list = + match cmp x x' with + | .lt => match f x (some y) none with + | none => AssocList.orderedMerge cmp f t (.cons x' y' t') + | some d => .cons x d (AssocList.orderedMerge cmp f t (.cons x' y' t')) + | .eq => match f x (some y) (some y') with + | none => AssocList.orderedMerge cmp f t t' + | some d => .cons x d (AssocList.orderedMerge cmp f t t') + | .gt => match f x' none (some y') with + | none => AssocList.orderedMerge cmp f (.cons x y t) t' + | some d => .cons x' d (AssocList.orderedMerge cmp f (.cons x y t) t') := by + dsimp [merge] + rw [AssocList.orderedMerge] + split <;> split <;> simp_all + +private theorem merge_mk_cons_mk_cons {f : α → Option β → Option γ → Option δ} : + merge f (⟨.cons x y t, h⟩ : OrderedAssocList cmp β) ⟨.cons x' y' t', h'⟩ = + match i: cmp x x' with + | .lt => match w : f x (some y) none with + | none => merge f ⟨t, h.tail⟩ ⟨.cons x' y' t', h'⟩ + | some d => ⟨.cons x d (merge f ⟨t, h.tail⟩ ⟨.cons x' y' t', h'⟩).list, by + have p := merge_mk_cons_mk_cons_list f x y t h x' y' t' h' + simp only [w, i] at p + simp only [list_merge] + simp only [← p] + exact (merge f _ _).keysOrdered⟩ + | .eq => match w : f x (some y) (some y') with + | none => merge f ⟨t, h.tail⟩ ⟨t', h'.tail⟩ + | some d => ⟨.cons x d (merge f ⟨t, h.tail⟩ ⟨t', h'.tail⟩).list, by + have p := merge_mk_cons_mk_cons_list f x y t h x' y' t' h' + simp only [w, i] at p + simp only [list_merge] + simp only [← p] + exact (merge f _ _).keysOrdered⟩ + | .gt => match w : f x' none (some y') with + | none => merge f ⟨.cons x y t, h⟩ ⟨t', h'.tail⟩ + | some d => ⟨.cons x' d (merge f ⟨.cons x y t, h⟩ ⟨t', h'.tail⟩).list, by + have p := merge_mk_cons_mk_cons_list f x y t h x' y' t' h' + simp only [w, i] at p + simp only [list_merge] + simp only [← p] + exact (merge f _ _).keysOrdered⟩ := by + apply ext_list + simp only [merge_mk_cons_mk_cons_list] + split <;> split <;> simp_all [merge] + +@[simp] theorem find?_merge {f : α → Option β → Option γ → Option δ} + (hf : f a none none = none) {l₁ : OrderedAssocList cmp β} {l₂} : + (merge f l₁ l₂).find? a = f a (l₁.find? a) (l₂.find? a) := by + match l₁, l₂ with + | ⟨.nil, _⟩, ⟨.nil, _⟩ => exact hf.symm + | ⟨.nil, _⟩, ⟨.cons x' y' t', h'⟩ => + rw [merge_mk_nil_mk_cons, find?_filterMapVal, find?_mk_nil, Option.bind] + split <;> (rename_i w; rw [w]) + rw [hf] + | ⟨.cons x y t, h⟩, ⟨.nil, _⟩ => + rw [merge_mk_cons_mk_nil, find?_filterMapVal, find?_mk_nil, Option.bind] + split <;> (rename_i w; rw [w]) + rw [hf] + | ⟨.cons x y t, h⟩, ⟨.cons x' y' t', h'⟩ => + rw [merge_mk_cons_mk_cons] + split <;> rename_i h₁ + · split <;> rename_i h₂ + · rw [find?_merge hf] + rw [find?_mk_cons (a := x)] + split <;> rename_i h₃ + · rcases AntisymmCmp.eq_of_cmp_eq h₃ with rfl + rw [find?_eq_none_of_ltHeadKey?, find?_eq_none_of_ltHeadKey?, hf] + · simp_all + · exact h₁ + · exact AssocList.ltHeadKey?_of_keysOrdered_cons h + · rfl + · rw [find?_mk_cons] + split <;> rename_i h₃ + · rcases AntisymmCmp.eq_of_cmp_eq h₃ with rfl + simp only [← h₂, find?_mk_cons_self] + rw [find?_eq_none_of_ltHeadKey?] + exact h₁ + · rw [find?_merge hf, find?_mk_cons (a := x), if_neg h₃] + · rcases (AntisymmCmp.eq_of_cmp_eq h₁) + split <;> rename_i h₂ + · rw [find?_merge hf] + rw [find?_mk_cons, find?_mk_cons] + split <;> rename_i h₃ + · rcases (AntisymmCmp.eq_of_cmp_eq h₃) + rw [find?_eq_none_of_ltHeadKey?, find?_eq_none_of_ltHeadKey?, hf, h₂] + · exact AssocList.ltHeadKey?_of_keysOrdered_cons h' + · exact AssocList.ltHeadKey?_of_keysOrdered_cons h + · rfl + · rw [find?_mk_cons] + split <;> rename_i h₃ + · rcases (AntisymmCmp.eq_of_cmp_eq h₃) + rw [find?_mk_cons_self, find?_mk_cons_self, h₂] + · rw [find?_merge hf, find?_mk_cons (a := x), if_neg h₃, find?_mk_cons (a := x), if_neg h₃] + · split <;> rename_i h₂ + · rw [find?_merge hf] + rw [find?_mk_cons (a := x')] + split <;> rename_i h₃ + · rcases (AntisymmCmp.eq_of_cmp_eq h₃) + rw [find?_eq_none_of_ltHeadKey?, find?_eq_none_of_ltHeadKey?, hf] + · exact h₂.symm + · exact AssocList.ltHeadKey?_of_keysOrdered_cons h' + · exact OrientedCmp.cmp_eq_gt.mp h₁ + · rfl + · rw [find?_mk_cons] + split <;> rename_i h₃ + · rcases (AntisymmCmp.eq_of_cmp_eq h₃) + simp only [find?_mk_cons_self] + rw [find?_eq_none_of_ltHeadKey?, h₂] + exact OrientedCmp.cmp_eq_gt.mp h₁ + · rw [find?_merge hf, find?_mk_cons (a := x'), if_neg h₃] + +theorem merge_comm + (f : α → Option β → Option γ → Option δ) (g : α → Option γ → Option β → Option δ) + (hf : ∀ a, f a none none = none) (hg : ∀ a, g a none none = none) + (w : ∀ a x y, f a x y = g a y x) + (l₁ : OrderedAssocList cmp β) (l₂) : merge f l₁ l₂ = merge g l₂ l₁ := by + ext + simp [w, hf, hg] + +theorem merge_assoc + (f₁ : α → Option β₁ → Option β₂ → Option γ₁) (f₂ : α → Option γ₁ → Option β₃ → Option ε) + (g₁ : α → Option β₂ → Option β₃ → Option γ₂) (g₂ : α → Option β₁ → Option γ₂ → Option ε) + (hf₁ : ∀ a, f₁ a none none = none) (hf₂ : ∀ a, f₂ a none none = none) + (hg₁ : ∀ a, g₁ a none none = none) (hg₂ : ∀ a, g₂ a none none = none) + (w : ∀ a x y z, f₂ a (f₁ a x y) z = g₂ a x (g₁ a y z)) + (l₁ : OrderedAssocList cmp β₁) (l₂) (l₃) : + merge f₂ (merge f₁ l₁ l₂) l₃ = merge g₂ l₁ (merge g₁ l₂ l₃) := by + ext + simp [w, hf₁, hf₂, hg₁, hg₂] + +/-- +Add two `OrderedAssocList`s, taking the value from one list if the other value is missing. +(That is, treating missing values as `0`.) +-/ +def add [Add β] (l₁ : OrderedAssocList cmp β) (l₂ : OrderedAssocList cmp β) : + OrderedAssocList cmp β := + merge (fun _ => addOption) l₁ l₂ +where addOption : Option β → Option β → Option β + | some x, some y => some (x + y) + | some x, none => some x + | none, some y => some y + | none, none => none + +-- This statement will look better on the version of `OrderedAssocList` with default values, +-- where we can just write `(add l₁ l₂).find a = l₁.find a + l₂.find a`. + +@[simp] theorem find?_add [Add β] {l₁ : OrderedAssocList cmp β} : + (add l₁ l₂).find? a = + match l₁.find? a, l₂.find? a with + | some x, some y => some (x + y) + | some x, none => some x + | none, some y => some y + | none, none => none := by + rw [add, find?_merge rfl] + rfl + +/-- +Multiply two `OrderedAssocList`s, +dropping any values where the corresponding value in the other list is missing. +(That is, treating missing values as `0`.) +-/ +def mul [Mul β] (l₁ : OrderedAssocList cmp β) (l₂ : OrderedAssocList cmp β) : + OrderedAssocList cmp β := + merge (fun _ => mulOption) l₁ l₂ +where mulOption : Option β → Option β → Option β + | some x, some y => some (x * y) + | some _, none => none + | none, some _ => none + | none, none => none + +@[simp] theorem find?_mul [Mul β] {l₁ : OrderedAssocList cmp β} : + (mul l₁ l₂).find? a = + match l₁.find? a, l₂.find? a with + | some x, some y => some (x * y) + | some _, none => none + | none, some _ => none + | none, none => none := by + rw [mul, find?_merge rfl] + rfl + +end merge + +end OrderedAssocList diff --git a/Std/Logic.lean b/Std/Logic.lean index 2afce52521..879dec9afc 100644 --- a/Std/Logic.lean +++ b/Std/Logic.lean @@ -870,6 +870,14 @@ theorem ite_some_none_eq_none [Decidable P] : (if P then some x else none) = some y ↔ P ∧ x = y := by split <;> simp_all +@[simp] theorem ite_self_left [Decidable P] : + (if P then if P then x else y else z) = if P then x else z := by + by_cases h : P <;> simp_all + +@[simp] theorem ite_self_right [Decidable P] : + (if P then x else if P then y else z) = if P then x else z := by + by_cases h : P <;> simp_all + /-! ## miscellaneous -/ attribute [simp] inline From 1a1d1a1821ec12bc9b8a3183151c6dbb3d2f5e34 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 23 Jan 2024 17:48:22 +1100 Subject: [PATCH 02/18] add to Std.lean --- Std.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Std.lean b/Std.lean index 2b6980dcf3..6b7ad6a1da 100644 --- a/Std.lean +++ b/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 From ceaf996aa97cab87a01eb7f2c0701c12c6067a92 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 23 Jan 2024 17:55:37 +1100 Subject: [PATCH 03/18] lint --- Std/Data/OrderedAssocList.lean | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/Std/Data/OrderedAssocList.lean b/Std/Data/OrderedAssocList.lean index f7c145d43c..cc7f713d7b 100644 --- a/Std/Data/OrderedAssocList.lean +++ b/Std/Data/OrderedAssocList.lean @@ -111,7 +111,8 @@ theorem ltHeadKey?_of_le [TransCmp cmp] (h : cmp x a ≠ .gt) (w : ltHeadKey? cm The head key of the first list is at most the head key of the second list, or the second list is empty. -/ -abbrev headKey?_le_headKey? (cmp : α → α → Ordering) (s : AssocList α β) (t : AssocList α γ) : Prop := +abbrev headKey?_le_headKey? + (cmp : α → α → Ordering) (s : AssocList α β) (t : AssocList α γ) : Prop := match s.headKey?, t.headKey? with | some a₁, some a₂ => cmp a₁ a₂ ≠ .gt | none, some _ => False @@ -456,7 +457,7 @@ theorem find?_eq_none_of_ltHeadKey? (l : OrderedAssocList cmp β) (w : ltHeadKey | .eq => simp_all [ltHeadKey?] | .gt => simp_all [ltHeadKey?] -theorem find?_mk_cons [OrientedCmp cmp] [TransCmp cmp] +theorem find?_mk_cons [TransCmp cmp] {h : (AssocList.cons a b t).keysOrdered cmp} : find? ⟨.cons a b t, h⟩ x = if cmp x a = .eq then some b else find? ⟨t, h.tail⟩ x := by simp only [find?] @@ -692,7 +693,8 @@ termination_by _ l => l.length theorem filterMapVal_filterMapVal [AntisymmCmp cmp] [TransCmp cmp] {f : α → γ → Option δ} {g : α → β → Option γ} {l : OrderedAssocList cmp β} : - filterMapVal f (filterMapVal g l) = filterMapVal (fun a b => (g a b).bind (fun c => f a c)) l := by + filterMapVal f (filterMapVal g l) = + filterMapVal (fun a b => (g a b).bind (fun c => f a c)) l := by ext a d simp only [find?_filterMapVal, Option.mem_def, Option.bind_eq_some] constructor @@ -845,6 +847,7 @@ private theorem merge_mk_cons_mk_cons {f : α → Option β → Option γ → Op exact OrientedCmp.cmp_eq_gt.mp h₁ · rw [find?_merge hf, find?_mk_cons (a := x'), if_neg h₃] +@[nolint unusedArguments] -- falsely reports that `hf` is not used. theorem merge_comm (f : α → Option β → Option γ → Option δ) (g : α → Option γ → Option β → Option δ) (hf : ∀ a, f a none none = none) (hg : ∀ a, g a none none = none) @@ -871,11 +874,13 @@ Add two `OrderedAssocList`s, taking the value from one list if the other value i def add [Add β] (l₁ : OrderedAssocList cmp β) (l₂ : OrderedAssocList cmp β) : OrderedAssocList cmp β := merge (fun _ => addOption) l₁ l₂ -where addOption : Option β → Option β → Option β - | some x, some y => some (x + y) - | some x, none => some x - | none, some y => some y - | none, none => none +where + /-- Add two values, treating missing values as `0`. -/ + addOption : Option β → Option β → Option β + | some x, some y => some (x + y) + | some x, none => some x + | none, some y => some y + | none, none => none -- This statement will look better on the version of `OrderedAssocList` with default values, -- where we can just write `(add l₁ l₂).find a = l₁.find a + l₂.find a`. @@ -898,11 +903,13 @@ dropping any values where the corresponding value in the other list is missing. def mul [Mul β] (l₁ : OrderedAssocList cmp β) (l₂ : OrderedAssocList cmp β) : OrderedAssocList cmp β := merge (fun _ => mulOption) l₁ l₂ -where mulOption : Option β → Option β → Option β - | some x, some y => some (x * y) - | some _, none => none - | none, some _ => none - | none, none => none +where + /-- Multiply two values, treating missing values as `0`. -/ + mulOption : Option β → Option β → Option β + | some x, some y => some (x * y) + | some _, none => none + | none, some _ => none + | none, none => none @[simp] theorem find?_mul [Mul β] {l₁ : OrderedAssocList cmp β} : (mul l₁ l₂).find? a = From aa2147cd26be9008e4865ad84a1d569d571d759e Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 30 Jan 2024 17:29:13 +1100 Subject: [PATCH 04/18] Update Std/Data/OrderedAssocList.lean Co-authored-by: Mario Carneiro --- Std/Data/OrderedAssocList.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Std/Data/OrderedAssocList.lean b/Std/Data/OrderedAssocList.lean index cc7f713d7b..e9edb437c3 100644 --- a/Std/Data/OrderedAssocList.lean +++ b/Std/Data/OrderedAssocList.lean @@ -875,7 +875,7 @@ def add [Add β] (l₁ : OrderedAssocList cmp β) (l₂ : OrderedAssocList cmp OrderedAssocList cmp β := merge (fun _ => addOption) l₁ l₂ where - /-- Add two values, treating missing values as `0`. -/ + /-- Add two values, treating missing values as `0`. -/ addOption : Option β → Option β → Option β | some x, some y => some (x + y) | some x, none => some x From 6de3b0897b38a880ee71786470288edfe2f8fcf9 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 1 Feb 2024 12:10:57 +1100 Subject: [PATCH 05/18] start unbundling --- Std/Data/OrderedAssocList.lean | 84 ++++++++++++++++++++-------------- 1 file changed, 50 insertions(+), 34 deletions(-) diff --git a/Std/Data/OrderedAssocList.lean b/Std/Data/OrderedAssocList.lean index e9edb437c3..3c8b2c5619 100644 --- a/Std/Data/OrderedAssocList.lean +++ b/Std/Data/OrderedAssocList.lean @@ -354,6 +354,47 @@ theorem orderedMerge_keysOrdered [AntisymmCmp cmp] [TransCmp cmp] · exact orderedMerge_keysOrdered h₁ h₂.tail | none => exact orderedMerge_keysOrdered h₁ h₂.tail +/-- +Find the value associated to a key by traversing left to right, +short-circuiting once we are considering larger keys. +-/ +def orderedFind? (cmp : α → α → Ordering) (l : AssocList α β) (x : α) : Option β := + match l with + | .nil => none + | .cons a b t => match cmp x a with + | .lt => none + | .eq => some b + | .gt => orderedFind? cmp t x + +theorem orderedFind?_eq_find? + {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] [BEq α] [LawfulBEq α] + (l : AssocList α β) (h : l.keysOrdered cmp) (x : α) : l.orderedFind? cmp x = l.find? x := by + match l with + | .nil => rfl + | .cons a b t => + rw [find?, AssocList.orderedFind?] + split + · split + · simp_all [OrientedCmp.cmp_refl] + · rw [AssocList.find?_eq_none_of_ltHeadKey? (cmp := cmp)] + · exact AssocList.ltHeadKey?_of_le (by simp_all) + (AssocList.ltHeadKey?_of_keysOrdered_cons h) + · exact h.tail + · simp_all [AntisymmCmp.eq_of_cmp_eq ‹_›] + · split + · simp_all [OrientedCmp.cmp_refl] + · apply orderedFind?_eq_find? _ h.tail + +theorem orderedFind?_eq_none_of_ltHeadKey? (l : AssocList α β) (w : ltHeadKey? cmp x l) : + orderedFind? cmp l x = none := by + match l with + | .nil => rfl + | .cons a b t => + match p : cmp x a with + | .lt => simp [orderedFind?, p] + | .eq => simp_all [ltHeadKey?] + | .gt => simp_all [ltHeadKey?] + end AssocList /-- @@ -402,30 +443,11 @@ Find the value associated to a key by traversing left to right, short-circuiting once we are considering larger keys. -/ def find? (l : OrderedAssocList cmp β) (x : α) : Option β := - match l with - | ⟨.nil, _⟩ => none - | ⟨.cons a b t, h⟩ => match cmp x a with - | .lt => none - | .eq => some b - | .gt => find? ⟨t, h.tail⟩ x + l.list.orderedFind? cmp x -theorem find?_eq_find?_list [AntisymmCmp cmp] [TransCmp cmp] [BEq α] [LawfulBEq α] - {l : OrderedAssocList cmp β} : l.find? x = l.list.find? x := by - match l with - | ⟨.nil, _⟩ => rfl - | ⟨.cons a b t, h⟩ => - rw [find?, AssocList.find?] - split - · split - · simp_all [OrientedCmp.cmp_refl] - · rw [AssocList.find?_eq_none_of_ltHeadKey? (cmp := cmp)] - · exact AssocList.ltHeadKey?_of_le (by simp_all) - (AssocList.ltHeadKey?_of_keysOrdered_cons h) - · exact h.tail - · simp_all [AntisymmCmp.eq_of_cmp_eq ‹_›] - · split - · simp_all [OrientedCmp.cmp_refl] - · apply find?_eq_find?_list +theorem find?_eq_find?_list {α : Type u} {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] [BEq α] [LawfulBEq α] + {l : OrderedAssocList cmp β} {x : α} : l.find? x = l.list.find? x := + AssocList.orderedFind?_eq_find? l.list l.keysOrdered x @[simp] theorem find?_nil : find? (nil : OrderedAssocList cmp β) x = none := rfl @[simp] theorem find?_mk_nil : find? ⟨.nil, h⟩ x = none := rfl @@ -448,21 +470,15 @@ theorem headKey?_tail (h : AssocList.keysOrdered cmp (.cons a b t)) : | .cons _ _ _ => exact h.1 theorem find?_eq_none_of_ltHeadKey? (l : OrderedAssocList cmp β) (w : ltHeadKey? x l) : - find? l x = none := by - match l with - | ⟨.nil, _⟩ => rfl - | ⟨.cons a b t, h⟩ => - match p : cmp x a with - | .lt => simp [find?, p] - | .eq => simp_all [ltHeadKey?] - | .gt => simp_all [ltHeadKey?] + find? l x = none := + AssocList.orderedFind?_eq_none_of_ltHeadKey? _ w theorem find?_mk_cons [TransCmp cmp] {h : (AssocList.cons a b t).keysOrdered cmp} : find? ⟨.cons a b t, h⟩ x = if cmp x a = .eq then some b else find? ⟨t, h.tail⟩ x := by - simp only [find?] + simp only [find?, AssocList.orderedFind?] split <;> rename_i w <;> simp only [w, ite_true, ite_false] - rw [find?_eq_none_of_ltHeadKey?] + rw [AssocList.orderedFind?_eq_none_of_ltHeadKey?] have p := headKey?_tail h revert p simp only [ltHeadKey?, AssocList.ltHeadKey?] @@ -472,7 +488,7 @@ theorem find?_mk_cons [TransCmp cmp] @[simp] theorem find?_mk_cons_self [OrientedCmp cmp] {h : (AssocList.cons a b t).keysOrdered cmp} : find? ⟨.cons a b t, h⟩ a = some b := by - simp [find?, OrientedCmp.cmp_refl] + simp [find?, AssocList.orderedFind?, OrientedCmp.cmp_refl] theorem ext_list {l₁ l₂ : OrderedAssocList cmp β} (w : l₁.list = l₂.list) : l₁ = l₂ := by cases l₁; cases l₂; congr From 390d17fc67dadec89a7425b0dd7e72db52eab5fa Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 1 Feb 2024 14:14:55 +1100 Subject: [PATCH 06/18] in progress --- Std/Data/OrderedAssocList.lean | 73 +++++++++++++++++++++++++++++++--- 1 file changed, 68 insertions(+), 5 deletions(-) diff --git a/Std/Data/OrderedAssocList.lean b/Std/Data/OrderedAssocList.lean index 3c8b2c5619..7258dd0300 100644 --- a/Std/Data/OrderedAssocList.lean +++ b/Std/Data/OrderedAssocList.lean @@ -366,6 +366,9 @@ def orderedFind? (cmp : α → α → Ordering) (l : AssocList α β) (x : α) : | .eq => some b | .gt => orderedFind? cmp t x +@[simp] theorem orderedFind?_nil {cmp : α → α → Ordering} : + orderedFind? cmp (nil : AssocList α β) x = none := rfl + theorem orderedFind?_eq_find? {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] [BEq α] [LawfulBEq α] (l : AssocList α β) (h : l.keysOrdered cmp) (x : α) : l.orderedFind? cmp x = l.find? x := by @@ -395,6 +398,70 @@ theorem orderedFind?_eq_none_of_ltHeadKey? (l : AssocList α β) (w : ltHeadKey? | .eq => simp_all [ltHeadKey?] | .gt => simp_all [ltHeadKey?] +theorem orderedFind?_cons [TransCmp cmp] + {h : (AssocList.cons a b t).keysOrdered cmp} : + orderedFind? cmp (.cons a b t) x = if cmp x a = .eq then some b else orderedFind? cmp t x := by + simp only [find?, AssocList.orderedFind?] + split <;> rename_i w <;> simp only [w, ite_true, ite_false] + rw [AssocList.orderedFind?_eq_none_of_ltHeadKey?] + -- have p := headKey?_tail h + -- revert p + simp only [ltHeadKey?, headKey?] + split + · trivial + · apply TransCmp.lt_trans w + sorry + +@[simp] theorem orderedFind?_cons_self [OrientedCmp cmp] : + orderedFind? cmp (.cons a b t) a = some b := by + simp [find?, AssocList.orderedFind?, OrientedCmp.cmp_refl] + +theorem ext_orderedKeys + {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] [BEq α] [LawfulBEq α] + {l₁ l₂ : AssocList α β} (h₁ : l₁.keysOrdered cmp) (h₂ : l₂.keysOrdered cmp) + (w : ∀ a, l₁.find? a = l₂.find? a) : l₁ = l₂ := by + simp only [← orderedFind?_eq_find? _ h₁, ← orderedFind?_eq_find? _ h₂] at w + match w₁ : l₁, w₂ : l₂ with + | .nil, .nil => rfl + | .cons a b t, .nil => + exfalso + specialize w a + simp_all + | .nil, .cons a b t => + exfalso + specialize w a + simp_all + | .cons a₁ b₁ t₁, .cons a₂ b₂ t₂ => + match h : cmp a₁ a₂ with + | .lt => + exfalso + have w₂ : l₂.find? a₁ = none := by + simp [find?_eq_none_of_ltHeadKey?, w₂, ltHeadKey?, h] + specialize w a₁ + simp_all + | .eq => + rcases AntisymmCmp.eq_of_cmp_eq h + have w' := w a₁ + simp only [find?_mk_cons_self, Option.some.injEq] at w' + congr + suffices (⟨t₁, p₁.tail⟩ : OrderedAssocList cmp β) = ⟨t₂, p₂.tail⟩ by injections + apply ext + intro a + specialize w a + simp only [find?_mk_cons] at w + split at w <;> rename_i h + · rcases AntisymmCmp.eq_of_cmp_eq h + rw [find?_eq_none_of_ltHeadKey?, find?_eq_none_of_ltHeadKey?] + apply headKey?_tail p₂ + apply headKey?_tail p₁ + · exact w + | .gt => + exfalso + have w₁ : l₁.find? a₂ = none := by + simp [find?_eq_none_of_ltHeadKey?, h₁, ltHeadKey?, h, ← OrientedCmp.cmp_eq_gt] + specialize w a₂ + simp_all + end AssocList /-- @@ -445,10 +512,6 @@ short-circuiting once we are considering larger keys. def find? (l : OrderedAssocList cmp β) (x : α) : Option β := l.list.orderedFind? cmp x -theorem find?_eq_find?_list {α : Type u} {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] [BEq α] [LawfulBEq α] - {l : OrderedAssocList cmp β} {x : α} : l.find? x = l.list.find? x := - AssocList.orderedFind?_eq_find? l.list l.keysOrdered x - @[simp] theorem find?_nil : find? (nil : OrderedAssocList cmp β) x = none := rfl @[simp] theorem find?_mk_nil : find? ⟨.nil, h⟩ x = none := rfl @@ -493,7 +556,7 @@ theorem find?_mk_cons [TransCmp cmp] theorem ext_list {l₁ l₂ : OrderedAssocList cmp β} (w : l₁.list = l₂.list) : l₁ = l₂ := by cases l₁; cases l₂; congr -theorem ext [AntisymmCmp cmp] [OrientedCmp cmp] [TransCmp cmp] {l₁ l₂ : OrderedAssocList cmp β} +theorem ext [AntisymmCmp cmp] [TransCmp cmp] {l₁ l₂ : OrderedAssocList cmp β} (w : ∀ a, l₁.find? a = l₂.find? a) : l₁ = l₂ := by match h₁ : l₁, h₂ : l₂ with | ⟨.nil, _⟩, ⟨.nil, _⟩ => rfl From 6ebc8d9ca84ab010b2126e49ee5841a67ee0df48 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 1 Feb 2024 14:49:13 +1100 Subject: [PATCH 07/18] ugh --- Std/Data/OrderedAssocList.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Std/Data/OrderedAssocList.lean b/Std/Data/OrderedAssocList.lean index 7258dd0300..11e8913909 100644 --- a/Std/Data/OrderedAssocList.lean +++ b/Std/Data/OrderedAssocList.lean @@ -436,6 +436,8 @@ theorem ext_orderedKeys | .lt => exfalso have w₂ : l₂.find? a₁ = none := by + simp only [find?_eq, Option.map_eq_none'] + rw [find?_eq_none_of_ltHeadKey?] simp [find?_eq_none_of_ltHeadKey?, w₂, ltHeadKey?, h] specialize w a₁ simp_all @@ -461,7 +463,7 @@ theorem ext_orderedKeys simp [find?_eq_none_of_ltHeadKey?, h₁, ltHeadKey?, h, ← OrientedCmp.cmp_eq_gt] specialize w a₂ simp_all - +#exit end AssocList /-- From 618c18c215a2b60938b907f9e261b4cb3b1fa8c8 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 1 Feb 2024 15:15:37 +1100 Subject: [PATCH 08/18] checkpoint --- Std/Data/AssocList.lean | 2 +- Std/Data/OrderedAssocList.lean | 49 ++++++++++++++++++++-------------- 2 files changed, 30 insertions(+), 21 deletions(-) diff --git a/Std/Data/AssocList.lean b/Std/Data/AssocList.lean index 885ab21aa2..d464cc604e 100644 --- a/Std/Data/AssocList.lean +++ b/Std/Data/AssocList.lean @@ -171,7 +171,7 @@ theorem find?_eq_findEntry? [BEq α] (a : α) (l : AssocList α β) : find? a l = (l.findEntry? a).map (·.2) := by induction l <;> simp [find?, List.find?_cons]; split <;> simp [*] -@[simp] theorem find?_eq [BEq α] (a : α) (l : AssocList α β) : +theorem find?_eq [BEq α] (a : α) (l : AssocList α β) : find? a l = (l.toList.find? (·.1 == a)).map (·.2) := by simp [find?_eq_findEntry?] /-- `O(n)`. Returns true if any entry in the list satisfies `p`. -/ diff --git a/Std/Data/OrderedAssocList.lean b/Std/Data/OrderedAssocList.lean index 11e8913909..25542fec25 100644 --- a/Std/Data/OrderedAssocList.lean +++ b/Std/Data/OrderedAssocList.lean @@ -399,25 +399,32 @@ theorem orderedFind?_eq_none_of_ltHeadKey? (l : AssocList α β) (w : ltHeadKey? | .gt => simp_all [ltHeadKey?] theorem orderedFind?_cons [TransCmp cmp] - {h : (AssocList.cons a b t).keysOrdered cmp} : + (h : (AssocList.cons a b t).keysOrdered cmp) : orderedFind? cmp (.cons a b t) x = if cmp x a = .eq then some b else orderedFind? cmp t x := by simp only [find?, AssocList.orderedFind?] split <;> rename_i w <;> simp only [w, ite_true, ite_false] rw [AssocList.orderedFind?_eq_none_of_ltHeadKey?] - -- have p := headKey?_tail h - -- revert p simp only [ltHeadKey?, headKey?] - split + split <;> rename_i h' · trivial · apply TransCmp.lt_trans w - sorry + revert h' + split + · simp + · simp only [Option.some.injEq] + rintro rfl + exact h.1 @[simp] theorem orderedFind?_cons_self [OrientedCmp cmp] : orderedFind? cmp (.cons a b t) a = some b := by simp [find?, AssocList.orderedFind?, OrientedCmp.cmp_refl] +/-- +If two `AssocList`s have ordered keys + we can check if they are equal by checking if their `find?` functions are equal. +-/ theorem ext_orderedKeys - {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] [BEq α] [LawfulBEq α] + (cmp : α → α → Ordering) [AntisymmCmp cmp] [TransCmp cmp] [BEq α] [LawfulBEq α] {l₁ l₂ : AssocList α β} (h₁ : l₁.keysOrdered cmp) (h₂ : l₂.keysOrdered cmp) (w : ∀ a, l₁.find? a = l₂.find? a) : l₁ = l₂ := by simp only [← orderedFind?_eq_find? _ h₁, ← orderedFind?_eq_find? _ h₂] at w @@ -436,34 +443,36 @@ theorem ext_orderedKeys | .lt => exfalso have w₂ : l₂.find? a₁ = none := by - simp only [find?_eq, Option.map_eq_none'] - rw [find?_eq_none_of_ltHeadKey?] - simp [find?_eq_none_of_ltHeadKey?, w₂, ltHeadKey?, h] + rwa [w₂, find?_eq_none_of_ltHeadKey? _ h₂] specialize w a₁ - simp_all + simp [orderedFind?_cons_self] at w + simp_all [orderedFind?_eq_find?] | .eq => rcases AntisymmCmp.eq_of_cmp_eq h have w' := w a₁ - simp only [find?_mk_cons_self, Option.some.injEq] at w' + simp only [orderedFind?_cons_self, Option.some.injEq] at w' congr - suffices (⟨t₁, p₁.tail⟩ : OrderedAssocList cmp β) = ⟨t₂, p₂.tail⟩ by injections - apply ext + apply ext_orderedKeys cmp h₁.tail h₂.tail intro a specialize w a - simp only [find?_mk_cons] at w + rw [← orderedFind?_eq_find? _ h₁.tail, ← orderedFind?_eq_find? _ h₂.tail] + rw [orderedFind?_cons h₁, orderedFind?_cons h₂] at w split at w <;> rename_i h · rcases AntisymmCmp.eq_of_cmp_eq h - rw [find?_eq_none_of_ltHeadKey?, find?_eq_none_of_ltHeadKey?] - apply headKey?_tail p₂ - apply headKey?_tail p₁ + rw [orderedFind?_eq_none_of_ltHeadKey?, orderedFind?_eq_none_of_ltHeadKey?] + apply ltHeadKey?_of_keysOrdered_cons h₂ + apply ltHeadKey?_of_keysOrdered_cons h₁ · exact w | .gt => exfalso have w₁ : l₁.find? a₂ = none := by - simp [find?_eq_none_of_ltHeadKey?, h₁, ltHeadKey?, h, ← OrientedCmp.cmp_eq_gt] + rw [w₁] + rw [find?_eq_none_of_ltHeadKey? _ h₁] + simp_all [OrientedCmp.cmp_eq_gt] specialize w a₂ - simp_all -#exit + simp [orderedFind?_cons_self] at w + simp_all [orderedFind?_eq_find?] + end AssocList /-- From 50a48f61cb1d6ed79baf43785ee022b19ffcc0fa Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 5 Feb 2024 23:19:05 +1100 Subject: [PATCH 09/18] more progresss unbundling --- Std/Classes/Order.lean | 19 +++ Std/Data/AssocList.lean | 6 + Std/Data/OrderedAssocList.lean | 292 ++++++++++++++++----------------- 3 files changed, 168 insertions(+), 149 deletions(-) diff --git a/Std/Classes/Order.lean b/Std/Classes/Order.lean index dcd3f58fd1..cbef87afca 100644 --- a/Std/Classes/Order.lean +++ b/Std/Classes/Order.lean @@ -15,6 +15,10 @@ import Std.Tactic.Simpa namespace Std +/-- Construct a `BEq` instance from a comparator function. -/ +def beqOfCmp (cmp : α → α → Ordering) : BEq α where + beq x y := cmp x y = .eq + /-- `TotalBLE le` asserts that `le` has a total order, that is, `le a b ∨ le b a`. -/ class TotalBLE (le : α → α → Bool) : Prop where /-- `le` is total: either `le a b` or `le b a`. -/ @@ -47,6 +51,21 @@ theorem cmp_refl [OrientedCmp cmp] : cmp x x = .eq := end OrientedCmp +/-- +The `BEq` instance from a comparator `cmp : α → α → Ordering` with `[AntisymmCmp cmp]` and +`[OrientedCmp cmp]` is a `LawfulBEq`. +-/ +def lawfulBEqOfCmp (cmp : α → α → Ordering) [AntisymmCmp cmp] [OrientedCmp cmp] : + let i := beqOfCmp cmp + LawfulBEq α := + let _ := beqOfCmp cmp + { eq_of_beq := fun h => by + apply AntisymmCmp.eq_of_cmp_eq (cmp := cmp) + simpa [beqOfCmp] using h + rfl := by + intro a + simpa [beqOfCmp] using OrientedCmp.cmp_refl } + /-- `TransCmp cmp` asserts that `cmp` induces a transitive relation. -/ class TransCmp (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where /-- The comparator operation is transitive. -/ diff --git a/Std/Data/AssocList.lean b/Std/Data/AssocList.lean index d464cc604e..c7db6bc409 100644 --- a/Std/Data/AssocList.lean +++ b/Std/Data/AssocList.lean @@ -123,6 +123,12 @@ def filterMapVal (f : α → β → Option δ) : AssocList α β → AssocList @[simp] theorem filterMapVal_nil : filterMapVal f nil = nil := rfl +theorem filterMapVal_cons (f : α → β → Option γ) (k) (v) (t) : + filterMapVal f (.cons k v t) = + match f k v with + | none => filterMapVal f t + | some d => .cons k d (filterMapVal f t) := 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 diff --git a/Std/Data/OrderedAssocList.lean b/Std/Data/OrderedAssocList.lean index 25542fec25..ffacefc8f1 100644 --- a/Std/Data/OrderedAssocList.lean +++ b/Std/Data/OrderedAssocList.lean @@ -45,6 +45,27 @@ We first define some predicates and operations in the `AssocList` namespace. namespace AssocList +/-- The head key of an `AssocList`, or `none` if the list is empty. -/ +def headKey? (l : AssocList α β) : Option α := + match l with + | .nil => none + | .cons a _ _ => some a + +@[simp] theorem headKey?_nil : headKey? (.nil : AssocList α β) = none := rfl +@[simp] theorem headKey?_cons : headKey? (.cons a b t) = some a := rfl + +/-- +The condition that an element is less than the first key of an `AssocList`, or that list is empty. +-/ +abbrev ltHeadKey? (cmp : α → α → Ordering) (a : α) (t : AssocList α β) : Prop := + match headKey? t with | none => True | some x => cmp a x = .lt + +@[simp] theorem ltHeadKey?_nil {cmp : α → α → Ordering} : + ltHeadKey? cmp a (.nil : AssocList α β) = True := rfl +@[simp] theorem ltHeadKey?_cons : ltHeadKey? cmp a (.cons x y t) = (cmp a x = .lt) := rfl + +-- TODO redefine using ltHeadKey? + /-- The predicate that the keys of an `AssocList` are in strictly increasing order according to the comparator `cmp`. @@ -60,30 +81,14 @@ instance instKeysOrderedDecidablePred : DecidablePred (keysOrdered cmp : AssocLi · infer_instance · exact @instDecidableAnd _ _ _ (instKeysOrderedDecidablePred _) +@[simp] theorem keysOrdered_cons_nil : keysOrdered cmp (.cons a b nil) := trivial + +-- TODO rename theorem keysOrdered.tail (h : keysOrdered cmp (.cons a b t)) : keysOrdered cmp t := match t with | .nil => trivial | .cons .. => h.2 -/-- The head key of an `AssocList`, or `none` if the list is empty. -/ -def headKey? (l : AssocList α β) : Option α := - match l with - | .nil => none - | .cons a _ _ => some a - -@[simp] theorem headKey?_nil : headKey? (.nil : AssocList α β) = none := rfl -@[simp] theorem headKey?_cons : headKey? (.cons a b t) = some a := rfl - -/-- -The condition that an element is less than the first key of an `AssocList`, or that list is empty. --/ -abbrev ltHeadKey? (cmp : α → α → Ordering) (a : α) (t : AssocList α β) : Prop := - match headKey? t with | none => True | some x => cmp a x = .lt - -@[simp] theorem ltHeadKey?_nil {cmp : α → α → Ordering} : - ltHeadKey? cmp a (.nil : AssocList α β) = True := rfl -@[simp] theorem ltHeadKey?_cons : ltHeadKey? cmp a (.cons x y t) = (cmp a x = .lt) := rfl - theorem ltHeadKey?_of_keysOrdered_cons (w : keysOrdered cmp (cons a b t)) : ltHeadKey? cmp a t := match t with | .nil => trivial @@ -191,6 +196,15 @@ def orderedInsert (cmp : α → α → Ordering) (l : AssocList α β) (a : α) | .eq => .cons a b t | .gt => .cons x y (orderedInsert cmp t a b) +@[simp] theorem orderedInsert_nil : (nil : AssocList α β).orderedInsert cmp a b = .cons a b nil := + rfl + +@[simp] theorem orderedInsert_cons : + orderedInsert cmp (.cons x y t) a b = match w : cmp a x with + | .lt => .cons a b (.cons x y t) + | .eq => .cons a b t + | .gt => .cons x y (orderedInsert cmp t a b) := rfl + theorem headKey?_orderedInsert {l : AssocList α β} : headKey? (orderedInsert cmp l a b) = match headKey? l with @@ -419,15 +433,51 @@ theorem orderedFind?_cons [TransCmp cmp] orderedFind? cmp (.cons a b t) a = some b := by simp [find?, AssocList.orderedFind?, OrientedCmp.cmp_refl] +theorem orderedFind?_orderedInsert {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] + (l : AssocList α β) (h : keysOrdered cmp l) (a : α) (b : β) : + (orderedInsert cmp l a b).orderedFind? cmp x = + if cmp x a = .eq then some b else l.orderedFind? cmp x := by + match l with + | .nil => + simp only [orderedInsert, orderedFind?_cons, keysOrdered_cons_nil] + | .cons a' b' t => + simp only [orderedInsert_cons] + split <;> rename_i h₁ + · apply orderedFind?_cons + exact ⟨h₁, h⟩ + · rcases AntisymmCmp.eq_of_cmp_eq h₁ + rw [orderedFind?_cons h, orderedFind?_cons] + · split <;> rfl + · cases t <;> exact h + · rw [orderedFind?_cons, orderedFind?_orderedInsert t h.tail, orderedFind?_cons h] + · split <;> rename_i h₂ + · rcases (AntisymmCmp.eq_of_cmp_eq h₂).symm + simp_all [OrientedCmp.cmp_eq_gt] + · rfl + · exact orderedInsert_keysOrdered.aux h h₁ +termination_by _ => l.length + +theorem orderedFind?_orderedInsert_self {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] + (l : AssocList α β) (h : keysOrdered cmp l) (a : α) (b : β) : + (orderedInsert cmp l a b).orderedFind? cmp a = some b := by + simp [h, orderedFind?_orderedInsert, OrientedCmp.cmp_refl] + +-- theorem orderedInsert_contains {cmp : α → α → Ordering} [BEq α] (l : AssocList α β) (a : α) (b : β) : +-- (l.orderedInsert cmp a b).contains x = ((cmp x a = .eq) || l.contains x) := by +-- sorry + +-- theorem orderedInsert_contains_self {cmp : α → α → Ordering} [BEq α] (l : AssocList α β) (a : α) (b : β) : +-- (l.orderedInsert cmp a b).contains a = true := by +-- sorry + /-- If two `AssocList`s have ordered keys - we can check if they are equal by checking if their `find?` functions are equal. +we can check whether they are equal by checking if their `find?` functions are equal. -/ theorem ext_orderedKeys - (cmp : α → α → Ordering) [AntisymmCmp cmp] [TransCmp cmp] [BEq α] [LawfulBEq α] + (cmp : α → α → Ordering) [AntisymmCmp cmp] [TransCmp cmp] {l₁ l₂ : AssocList α β} (h₁ : l₁.keysOrdered cmp) (h₂ : l₂.keysOrdered cmp) - (w : ∀ a, l₁.find? a = l₂.find? a) : l₁ = l₂ := by - simp only [← orderedFind?_eq_find? _ h₁, ← orderedFind?_eq_find? _ h₂] at w + (w : ∀ a, l₁.orderedFind? cmp a = l₂.orderedFind? cmp a) : l₁ = l₂ := by match w₁ : l₁, w₂ : l₂ with | .nil, .nil => rfl | .cons a b t, .nil => @@ -442,8 +492,8 @@ theorem ext_orderedKeys match h : cmp a₁ a₂ with | .lt => exfalso - have w₂ : l₂.find? a₁ = none := by - rwa [w₂, find?_eq_none_of_ltHeadKey? _ h₂] + have w₂ : l₂.orderedFind? cmp a₁ = none := by + rw [w₂, orderedFind?_eq_none_of_ltHeadKey? _ h] specialize w a₁ simp [orderedFind?_cons_self] at w simp_all [orderedFind?_eq_find?] @@ -455,7 +505,6 @@ theorem ext_orderedKeys apply ext_orderedKeys cmp h₁.tail h₂.tail intro a specialize w a - rw [← orderedFind?_eq_find? _ h₁.tail, ← orderedFind?_eq_find? _ h₂.tail] rw [orderedFind?_cons h₁, orderedFind?_cons h₂] at w split at w <;> rename_i h · rcases AntisymmCmp.eq_of_cmp_eq h @@ -465,14 +514,59 @@ theorem ext_orderedKeys · exact w | .gt => exfalso - have w₁ : l₁.find? a₂ = none := by - rw [w₁] - rw [find?_eq_none_of_ltHeadKey? _ h₁] - simp_all [OrientedCmp.cmp_eq_gt] + have w₁ : l₁.orderedFind? cmp a₂ = none := by + rw [w₁, orderedFind?_eq_none_of_ltHeadKey? _ (OrientedCmp.cmp_eq_gt.mp h)] specialize w a₂ simp [orderedFind?_cons_self] at w simp_all [orderedFind?_eq_find?] +@[simp] +theorem orderedFind?_filterMapVal {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] + {l : AssocList α β} (h : keysOrdered cmp l) : + (filterMapVal f l).orderedFind? cmp a = (l.orderedFind? cmp a).bind (fun b => f a b) := by + -- This isn't true at the level of `AssocList`; we need uniqueness of keys. + match l with + | .nil => rfl + | .cons x y t => + simp only [filterMapVal_cons, orderedFind?_cons, h] + split + · rw [orderedFind?_filterMapVal h.tail] + split <;> rename_i h' + · have h' := AntisymmCmp.eq_of_cmp_eq h' + rw [orderedFind?_eq_none_of_ltHeadKey?] + · simp_all + · rcases h' with rfl + exact ltHeadKey?_of_keysOrdered_cons h + · rfl + · rw [orderedFind?_cons] + · split <;> rename_i h' + · simp_all [AntisymmCmp.eq_of_cmp_eq h'] + · rw [orderedFind?_filterMapVal h.tail] + · exact keysOrdered_cons + (ltHeadKey?_of_headKey?_le_headKey? (ltHeadKey?_of_keysOrdered_cons h) + (headKey?_le_headKey?_filterMapVal h.tail)) + (filterMapVal_keysOrdered h.tail) +termination_by _ l _ => l.length + +theorem filterMapVal_filterMapVal {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] + {f : α → γ → Option δ} {g : α → β → Option γ} + {l : AssocList α β} (h : keysOrdered cmp l) : + filterMapVal f (filterMapVal g l) = + filterMapVal (fun a b => (g a b).bind (fun c => f a c)) l := by + apply ext_orderedKeys (cmp := cmp) + · exact filterMapVal_keysOrdered (filterMapVal_keysOrdered h) + · exact filterMapVal_keysOrdered h + · intro a + rw [orderedFind?_filterMapVal, orderedFind?_filterMapVal h, orderedFind?_filterMapVal h] + · ext d + simp only [orderedFind?_filterMapVal, h, Option.mem_def, Option.bind_eq_some] + constructor + · rintro ⟨c, ⟨⟨b, hb, hc⟩, hd⟩⟩ + refine ⟨b, hb, c, hc, hd⟩ + · rintro ⟨b, hb, c, hc, hd⟩ + refine ⟨c, ⟨⟨b, hb, hc⟩, hd⟩⟩ + · exact filterMapVal_keysOrdered h + end AssocList /-- @@ -567,51 +661,11 @@ theorem find?_mk_cons [TransCmp cmp] theorem ext_list {l₁ l₂ : OrderedAssocList cmp β} (w : l₁.list = l₂.list) : l₁ = l₂ := by cases l₁; cases l₂; congr -theorem ext [AntisymmCmp cmp] [TransCmp cmp] {l₁ l₂ : OrderedAssocList cmp β} +@[ext] theorem ext [AntisymmCmp cmp] [TransCmp cmp] {l₁ l₂ : OrderedAssocList cmp β} (w : ∀ a, l₁.find? a = l₂.find? a) : l₁ = l₂ := by - match h₁ : l₁, h₂ : l₂ with - | ⟨.nil, _⟩, ⟨.nil, _⟩ => rfl - | ⟨.cons a b t, _⟩, ⟨.nil, _⟩ => - exfalso - specialize w a - simp_all - | ⟨.nil, _⟩, ⟨.cons a b t, _⟩ => - exfalso - specialize w a - simp_all - | ⟨.cons a₁ b₁ t₁, p₁⟩, ⟨.cons a₂ b₂ t₂, p₂⟩ => - match h : cmp a₁ a₂ with - | .lt => - exfalso - have w₂ : l₂.find? a₁ = none := by - simp [find?_eq_none_of_ltHeadKey?, h₂, ltHeadKey?, h] - specialize w a₁ - simp_all - | .eq => - rcases AntisymmCmp.eq_of_cmp_eq h - have w' := w a₁ - simp only [find?_mk_cons_self, Option.some.injEq] at w' - congr - suffices (⟨t₁, p₁.tail⟩ : OrderedAssocList cmp β) = ⟨t₂, p₂.tail⟩ by injections - apply ext - intro a - specialize w a - simp only [find?_mk_cons] at w - split at w <;> rename_i h - · rcases AntisymmCmp.eq_of_cmp_eq h - rw [find?_eq_none_of_ltHeadKey?, find?_eq_none_of_ltHeadKey?] - apply headKey?_tail p₂ - apply headKey?_tail p₁ - · exact w - | .gt => - exfalso - have w₁ : l₁.find? a₂ = none := by - simp [find?_eq_none_of_ltHeadKey?, h₁, ltHeadKey?, h, ← OrientedCmp.cmp_eq_gt] - specialize w a₂ - simp_all - --- Since this was a recursive theorem we have to add the attribute after the fact. -attribute [ext] ext + apply ext_list + apply AssocList.ext_orderedKeys _ l₁.keysOrdered l₂.keysOrdered + simpa [find?, AssocList.orderedFind?_eq_find?, l₁.keysOrdered, l₂.keysOrdered] using w /-- Check if an `OrderedAssocList` contains a specific key. -/ def contains (l : OrderedAssocList cmp β) (x : α) : Bool := (l.find? x).isSome @@ -688,36 +742,23 @@ end variable [TransCmp cmp] theorem find?_insert (l : OrderedAssocList cmp β) (a : α) (b : β) : - (insert l a b).find? x = if cmp x a = .eq then some b else l.find? x := by - match l with - | ⟨.nil, _⟩ => simp only [insert_mk_nil, find?_mk_cons] - | ⟨.cons a' b' t, h⟩ => - simp only [insert_mk_cons] - split <;> rename_i h₁ - · simp [find?_mk_cons] - · rcases AntisymmCmp.eq_of_cmp_eq h₁ - simp [find?_mk_cons] - · rw [find?_cons, find?_insert ⟨t, h.tail⟩, find?_mk_cons] - split <;> rename_i h₂ - · rcases (AntisymmCmp.eq_of_cmp_eq h₂).symm - simp_all [OrientedCmp.cmp_eq_gt] - · rfl -termination_by _ => l.length + (insert l a b).find? x = if cmp x a = .eq then some b else l.find? x := + AssocList.orderedFind?_orderedInsert l.list l.keysOrdered a b theorem find?_insert_self (l : OrderedAssocList cmp β) (a : α) (b : β) : (insert l a b).find? a = some b := by simp [find?_insert, OrientedCmp.cmp_refl] -theorem insert_contains (l : OrderedAssocList cmp β) (a : α) (b : β) : - (l.insert a b).contains x = ((cmp x a = .eq) || l.contains x) := by - simp only [contains, find?_insert] - split <;> rename_i h - · simp [h] - · cases find? l x <;> simp [h] +-- theorem insert_contains (l : OrderedAssocList cmp β) (a : α) (b : β) : +-- (l.insert a b).contains x = ((cmp x a = .eq) || l.contains x) := by +-- simp only [contains, find?_insert] +-- split <;> rename_i h +-- · simp [h] +-- · cases find? l x <;> simp [h] -theorem insert_contains_self (l : OrderedAssocList cmp β) (a : α) (b : β) : - (l.insert a b).contains a = true := by - simp [insert_contains, OrientedCmp.cmp_refl] +-- theorem insert_contains_self (l : OrderedAssocList cmp β) (a : α) (b : β) : +-- (l.insert a b).contains a = true := by +-- simp [insert_contains, OrientedCmp.cmp_refl] end insert @@ -733,65 +774,18 @@ def filterMapVal (f : α → β → Option δ) (l : OrderedAssocList cmp β) : OrderedAssocList cmp δ := ⟨l.list.filterMapVal f, AssocList.filterMapVal_keysOrdered l.keysOrdered⟩ -@[simp] theorem filterMapVal_nil {f : α → β → Option γ} : - filterMapVal f (nil : OrderedAssocList cmp β) = nil := rfl - -private theorem filterMapVal_mk_cons_list (f : α → β → Option γ) (x) (y) (t) (h) : - (filterMapVal f (⟨.cons x y t, h⟩ : OrderedAssocList cmp β)).list = - match f x y with - | none => AssocList.filterMapVal f t - | some g => .cons x g (filterMapVal f ⟨t, h.tail⟩).1 := by - dsimp [filterMapVal, AssocList.filterMapVal] - split <;> simp_all - -private theorem filterMapVal_mk_cons {f : α → β → Option γ} : - filterMapVal f (⟨.cons x y t, h⟩ : OrderedAssocList cmp β) = - match w : f x y with - | none => filterMapVal f ⟨t, h.tail⟩ - | some g => ⟨.cons x g (filterMapVal f ⟨t, h.tail⟩).1, by - have p := filterMapVal_mk_cons_list f x y t h - simp only [w] at p - simp only [← p] - exact (filterMapVal f ⟨.cons x y t, h⟩).keysOrdered⟩ := by - apply ext_list - simp only [filterMapVal_mk_cons_list] - split <;> simp_all [filterMapVal] - @[simp] theorem find?_filterMapVal [AntisymmCmp cmp] (l : OrderedAssocList cmp β) : - (filterMapVal f l).find? a = (l.find? a).bind (fun b => f a b) := by - -- This isn't true at the level of `AssocList`; we need uniqueness of keys. - match l with - | ⟨.nil, _⟩ => rfl - | ⟨.cons x y t, h⟩ => - simp only [filterMapVal_mk_cons, find?_mk_cons] - split - · rw [find?_filterMapVal ⟨t, h.tail⟩] - split <;> rename_i h' - · have h' := AntisymmCmp.eq_of_cmp_eq h' - rw [find?_eq_none_of_ltHeadKey?] - · simp_all - · rcases h' with rfl - exact AssocList.ltHeadKey?_of_keysOrdered_cons h - · rfl - · simp only [find?_mk_cons] - split <;> rename_i h' - · simp_all [AntisymmCmp.eq_of_cmp_eq h'] - · rw [find?_filterMapVal] -termination_by _ l => l.length + (filterMapVal f l).find? a = (l.find? a).bind (fun b => f a b) := + AssocList.orderedFind?_filterMapVal l.keysOrdered theorem filterMapVal_filterMapVal [AntisymmCmp cmp] [TransCmp cmp] {f : α → γ → Option δ} {g : α → β → Option γ} {l : OrderedAssocList cmp β} : filterMapVal f (filterMapVal g l) = filterMapVal (fun a b => (g a b).bind (fun c => f a c)) l := by - ext a d - simp only [find?_filterMapVal, Option.mem_def, Option.bind_eq_some] - constructor - · rintro ⟨c, ⟨⟨b, hb, hc⟩, hd⟩⟩ - refine ⟨b, hb, c, hc, hd⟩ - · rintro ⟨b, hb, c, hc, hd⟩ - refine ⟨c, ⟨⟨b, hb, hc⟩, hd⟩⟩ + apply ext_list + exact AssocList.filterMapVal_filterMapVal l.keysOrdered end filterMapVal From 1f0f20d8c5700d003f192e6bb5980133b26274f0 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 5 Feb 2024 23:34:21 +1100 Subject: [PATCH 10/18] fix after merge --- Std/Data/OrderedAssocList.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Std/Data/OrderedAssocList.lean b/Std/Data/OrderedAssocList.lean index ffacefc8f1..a841cae625 100644 --- a/Std/Data/OrderedAssocList.lean +++ b/Std/Data/OrderedAssocList.lean @@ -299,8 +299,8 @@ def orderedMerge (cmp : α → α → Ordering) (f : α → Option β → Option | .gt => match (f a₂ none (some g)) with | some d => .cons a₂ d (orderedMerge cmp f (.cons a₁ b t₁) t₂) | none => orderedMerge cmp f (.cons a₁ b t₁) t₂ -termination_by _ l₁ l₂ => l₁.length + l₂.length -decreasing_by simp_wf; omega +termination_by l₁ l₂ => l₁.length + l₂.length +decreasing_by all_goals simp_wf; omega theorem ltHeadKey?_orderedMerge [TransCmp cmp] (h₁ : ltHeadKey? cmp a l₁) (h₂ : ltHeadKey? cmp a l₂) @@ -455,7 +455,7 @@ theorem orderedFind?_orderedInsert {cmp : α → α → Ordering} [AntisymmCmp c simp_all [OrientedCmp.cmp_eq_gt] · rfl · exact orderedInsert_keysOrdered.aux h h₁ -termination_by _ => l.length +termination_by l.length theorem orderedFind?_orderedInsert_self {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] (l : AssocList α β) (h : keysOrdered cmp l) (a : α) (b : β) : @@ -546,7 +546,7 @@ theorem orderedFind?_filterMapVal {cmp : α → α → Ordering} [AntisymmCmp cm (ltHeadKey?_of_headKey?_le_headKey? (ltHeadKey?_of_keysOrdered_cons h) (headKey?_le_headKey?_filterMapVal h.tail)) (filterMapVal_keysOrdered h.tail) -termination_by _ l _ => l.length +termination_by l.length theorem filterMapVal_filterMapVal {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] {f : α → γ → Option δ} {g : α → β → Option γ} From 009746cec5555bbf00a6f5d04cb6965b1180b5a9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 23 Nov 2024 21:18:31 +1100 Subject: [PATCH 11/18] merge main --- Batteries/Classes/Order.lean | 2 +- Batteries/Data/HashMap/Lemmas.lean | 2 +- Batteries/Data/OrderedAssocList.lean | 41 ++++++++++++++-------------- 3 files changed, 23 insertions(+), 22 deletions(-) diff --git a/Batteries/Classes/Order.lean b/Batteries/Classes/Order.lean index 6efccce2c2..7fabe67c96 100644 --- a/Batteries/Classes/Order.lean +++ b/Batteries/Classes/Order.lean @@ -73,7 +73,7 @@ The `BEq` instance from a comparator `cmp : α → α → Ordering` with `[Antis `[OrientedCmp cmp]` is a `LawfulBEq`. -/ def lawfulBEqOfCmp (cmp : α → α → Ordering) [AntisymmCmp cmp] [OrientedCmp cmp] : - let i := beqOfCmp cmp + letI := beqOfCmp cmp LawfulBEq α := let _ := beqOfCmp cmp { eq_of_beq := fun h => by diff --git a/Batteries/Data/HashMap/Lemmas.lean b/Batteries/Data/HashMap/Lemmas.lean index 2e9df0770d..15f79feb0b 100644 --- a/Batteries/Data/HashMap/Lemmas.lean +++ b/Batteries/Data/HashMap/Lemmas.lean @@ -24,7 +24,7 @@ namespace Imp end Imp @[simp] theorem empty_find? [BEq α] [Hashable α] {a : α} : - (∅ : HashMap α β).find? a = none := by simp [find?, Imp.find?] + (∅ : HashMap α β).find? a = none := by simp [find?, Imp.find?, AssocList.find?] -- `Std.HashMap` has this lemma (as `getElem?_insert`) and many more, so working on this -- `proof_wanted` is likely not a good use of your time. diff --git a/Batteries/Data/OrderedAssocList.lean b/Batteries/Data/OrderedAssocList.lean index a841cae625..8e2fc624ac 100644 --- a/Batteries/Data/OrderedAssocList.lean +++ b/Batteries/Data/OrderedAssocList.lean @@ -1,14 +1,10 @@ /- Copyright (c) 2023 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Scott Morrison +Authors: Kim Morrison -/ -import Std.Data.AssocList -import Std.Classes.Order -import Std.Data.Option.Lemmas -import Std.Tactic.Ext -import Std.Tactic.LeftRight -import Std.Tactic.Omega +import Batteries.Data.AssocList +import Batteries.Classes.Order /-! # Ordered association lists @@ -32,7 +28,7 @@ The main operations defined are: dropping some values. It runs in time `O(l₁.length + l₂.length)`. -/ -namespace Std +namespace Batteries /-! We first define some predicates and operations in the `AssocList` namespace. @@ -176,7 +172,7 @@ We now define `orderedInsert`, and `orderedMerge`, which will later be wrapped as `OrderedAssocList.insert` and `OrderedAssocList.merge`. We prove that with `keysOrdered` input these functions produce `keysOrdered` outputs. -We prove that same about `AssocList.filterMapVal`. +We prove the same about `AssocList.filterMapVal`. -/ /-- @@ -191,7 +187,7 @@ We later wrap this as `OrderedAssocList.insert`. def orderedInsert (cmp : α → α → Ordering) (l : AssocList α β) (a : α) (b : β) : AssocList α β := match l with | .nil => .cons a b .nil - | .cons x y t => match w : cmp a x with + | .cons x y t => match _w : cmp a x with | .lt => .cons a b l | .eq => .cons a b t | .gt => .cons x y (orderedInsert cmp t a b) @@ -200,7 +196,7 @@ def orderedInsert (cmp : α → α → Ordering) (l : AssocList α β) (a : α) rfl @[simp] theorem orderedInsert_cons : - orderedInsert cmp (.cons x y t) a b = match w : cmp a x with + orderedInsert cmp (.cons x y t) a b = match _w : cmp a x with | .lt => .cons a b (.cons x y t) | .eq => .cons a b t | .gt => .cons x y (orderedInsert cmp t a b) := rfl @@ -300,7 +296,6 @@ def orderedMerge (cmp : α → α → Ordering) (f : α → Option β → Option | some d => .cons a₂ d (orderedMerge cmp f (.cons a₁ b t₁) t₂) | none => orderedMerge cmp f (.cons a₁ b t₁) t₂ termination_by l₁ l₂ => l₁.length + l₂.length -decreasing_by all_goals simp_wf; omega theorem ltHeadKey?_orderedMerge [TransCmp cmp] (h₁ : ltHeadKey? cmp a l₁) (h₂ : ltHeadKey? cmp a l₂) @@ -334,6 +329,7 @@ theorem ltHeadKey?_orderedMerge [TransCmp cmp] · exact h₂ · exact ltHeadKey?_orderedMerge h₁ (ltHeadKey?_of_cons h₂ w₂) w₁ w₂.tail +unseal orderedMerge in theorem orderedMerge_keysOrdered [AntisymmCmp cmp] [TransCmp cmp] (h₁ : keysOrdered cmp l₁) (h₂ : keysOrdered cmp l₂) : keysOrdered cmp (orderedMerge cmp f l₁ l₂) := by @@ -416,7 +412,7 @@ theorem orderedFind?_cons [TransCmp cmp] (h : (AssocList.cons a b t).keysOrdered cmp) : orderedFind? cmp (.cons a b t) x = if cmp x a = .eq then some b else orderedFind? cmp t x := by simp only [find?, AssocList.orderedFind?] - split <;> rename_i w <;> simp only [w, ite_true, ite_false] + split <;> rename_i w <;> simp only [w, reduceCtorEq, reduceIte] rw [AssocList.orderedFind?_eq_none_of_ltHeadKey?] simp only [ltHeadKey?, headKey?] split <;> rename_i h' @@ -645,7 +641,7 @@ theorem find?_mk_cons [TransCmp cmp] {h : (AssocList.cons a b t).keysOrdered cmp} : find? ⟨.cons a b t, h⟩ x = if cmp x a = .eq then some b else find? ⟨t, h.tail⟩ x := by simp only [find?, AssocList.orderedFind?] - split <;> rename_i w <;> simp only [w, ite_true, ite_false] + split <;> rename_i w <;> simp only [w, reduceCtorEq, reduceIte] rw [AssocList.orderedFind?_eq_none_of_ltHeadKey?] have p := headKey?_tail h revert p @@ -779,7 +775,7 @@ theorem find?_filterMapVal [AntisymmCmp cmp] (l : OrderedAssocList cmp β) : (filterMapVal f l).find? a = (l.find? a).bind (fun b => f a b) := AssocList.orderedFind?_filterMapVal l.keysOrdered -theorem filterMapVal_filterMapVal [AntisymmCmp cmp] [TransCmp cmp] +theorem filterMapVal_filterMapVal [AntisymmCmp cmp] {f : α → γ → Option δ} {g : α → β → Option γ} {l : OrderedAssocList cmp β} : filterMapVal f (filterMapVal g l) = @@ -806,13 +802,16 @@ def merge (f : α → Option β → Option γ → Option δ) (merge f l₁ l₂).list = AssocList.orderedMerge cmp f l₁.list l₂.list := rfl +unseal AssocList.orderedMerge in @[simp] theorem merge_nil_nil {f : α → Option β → Option γ → Option δ} : merge f (nil : OrderedAssocList cmp β) nil = nil := rfl +unseal AssocList.orderedMerge in @[simp] theorem merge_mk_nil_mk_cons {f : α → Option β → Option γ → Option δ} : merge f (⟨.nil, h⟩ : OrderedAssocList cmp β) ⟨.cons x' y' t', h'⟩ = filterMapVal (fun a g => f a none (some g)) ⟨.cons x' y' t', h'⟩ := rfl +unseal AssocList.orderedMerge in @[simp] theorem merge_mk_cons_mk_nil {f : α → Option β → Option γ → Option δ} : merge f ⟨.cons x y t, h⟩ (⟨.nil, h'⟩ : OrderedAssocList cmp γ) = filterMapVal (fun a b => f a (some b) none) ⟨.cons x y t, h⟩ := rfl @@ -865,17 +864,20 @@ private theorem merge_mk_cons_mk_cons {f : α → Option β → Option γ → Op simp only [merge_mk_cons_mk_cons_list] split <;> split <;> simp_all [merge] +unseal AssocList.orderedMerge in @[simp] theorem find?_merge {f : α → Option β → Option γ → Option δ} (hf : f a none none = none) {l₁ : OrderedAssocList cmp β} {l₂} : (merge f l₁ l₂).find? a = f a (l₁.find? a) (l₂.find? a) := by match l₁, l₂ with | ⟨.nil, _⟩, ⟨.nil, _⟩ => exact hf.symm | ⟨.nil, _⟩, ⟨.cons x' y' t', h'⟩ => - rw [merge_mk_nil_mk_cons, find?_filterMapVal, find?_mk_nil, Option.bind] + rw [merge_mk_nil_mk_cons, find?_filterMapVal, find?_mk_nil] + unfold Option.bind split <;> (rename_i w; rw [w]) rw [hf] | ⟨.cons x y t, h⟩, ⟨.nil, _⟩ => - rw [merge_mk_cons_mk_nil, find?_filterMapVal, find?_mk_nil, Option.bind] + rw [merge_mk_cons_mk_nil, find?_filterMapVal, find?_mk_nil] + unfold Option.bind split <;> (rename_i w; rw [w]) rw [hf] | ⟨.cons x y t, h⟩, ⟨.cons x' y' t', h'⟩ => @@ -931,14 +933,13 @@ private theorem merge_mk_cons_mk_cons {f : α → Option β → Option γ → Op exact OrientedCmp.cmp_eq_gt.mp h₁ · rw [find?_merge hf, find?_mk_cons (a := x'), if_neg h₃] -@[nolint unusedArguments] -- falsely reports that `hf` is not used. theorem merge_comm (f : α → Option β → Option γ → Option δ) (g : α → Option γ → Option β → Option δ) - (hf : ∀ a, f a none none = none) (hg : ∀ a, g a none none = none) + (hg : ∀ a, g a none none = none) (w : ∀ a x y, f a x y = g a y x) (l₁ : OrderedAssocList cmp β) (l₂) : merge f l₁ l₂ = merge g l₂ l₁ := by ext - simp [w, hf, hg] + simp [w, hg] theorem merge_assoc (f₁ : α → Option β₁ → Option β₂ → Option γ₁) (f₂ : α → Option γ₁ → Option β₃ → Option ε) From 552b38a169a8c74ddb782f3889d8d459b905f84d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 23 Nov 2024 21:37:20 +1100 Subject: [PATCH 12/18] GetElem? --- Batteries/Data/OrderedAssocList.lean | 131 +++++++++++++++------------ 1 file changed, 71 insertions(+), 60 deletions(-) diff --git a/Batteries/Data/OrderedAssocList.lean b/Batteries/Data/OrderedAssocList.lean index 8e2fc624ac..2fb3bb4ca4 100644 --- a/Batteries/Data/OrderedAssocList.lean +++ b/Batteries/Data/OrderedAssocList.lean @@ -609,12 +609,23 @@ def tail (l : OrderedAssocList cmp β) : OrderedAssocList cmp β := /-- Find the value associated to a key by traversing left to right, short-circuiting once we are considering larger keys. + +This is the internal implementation of `l[x]?`, which should be preferred. -/ def find? (l : OrderedAssocList cmp β) (x : α) : Option β := l.list.orderedFind? cmp x -@[simp] theorem find?_nil : find? (nil : OrderedAssocList cmp β) x = none := rfl -@[simp] theorem find?_mk_nil : find? ⟨.nil, h⟩ x = none := rfl +/-- Check if an `OrderedAssocList` contains a specific key. -/ +def contains (l : OrderedAssocList cmp β) (x : α) : Bool := (l.find? x).isSome + +instance : GetElem? (OrderedAssocList cmp β) α β (fun l a => l.contains a) where + getElem? l a := l.find? a + getElem l a h := (l.find? a).get h + +@[simp] theorem getElem?_nil {x : α} : (nil : OrderedAssocList cmp β)[x]? = none := rfl +@[simp] theorem getElem?_mk_nil {x : α} : (⟨.nil, h⟩ : OrderedAssocList cmp β)[x]? = none := rfl + +theorem contains_def {l : OrderedAssocList cmp β} : l.contains a = l[a]?.isSome := rfl /-- The first key in an `OrderedAssocList`, or `none` if the list is empty. -/ def headKey? (l : OrderedAssocList cmp β) : Option α := l.list.headKey? @@ -626,51 +637,50 @@ def headKey? (l : OrderedAssocList cmp β) : Option α := l.list.headKey? def ltHeadKey? (a : α) (l : OrderedAssocList cmp β) : Prop := AssocList.ltHeadKey? cmp a l.list /-- The head key of a tail is either `none`, or greater than the original head key. -/ -theorem headKey?_tail (h : AssocList.keysOrdered cmp (.cons a b t)) : +theorem ltheadKey?_tail (h : AssocList.keysOrdered cmp (.cons a b t)) : ltHeadKey? a ⟨t, h.tail⟩ := by dsimp [ltHeadKey?] match t with | .nil => trivial | .cons _ _ _ => exact h.1 -theorem find?_eq_none_of_ltHeadKey? (l : OrderedAssocList cmp β) (w : ltHeadKey? x l) : - find? l x = none := +theorem getElem?_eq_none_of_ltHeadKey? (l : OrderedAssocList cmp β) (w : ltHeadKey? x l) : + l[x]? = none := AssocList.orderedFind?_eq_none_of_ltHeadKey? _ w -theorem find?_mk_cons [TransCmp cmp] +theorem getElem?_mk_cons [TransCmp cmp] {h : (AssocList.cons a b t).keysOrdered cmp} : - find? ⟨.cons a b t, h⟩ x = if cmp x a = .eq then some b else find? ⟨t, h.tail⟩ x := by - simp only [find?, AssocList.orderedFind?] + (⟨.cons a b t, h⟩ : OrderedAssocList _ _)[x]? = + if cmp x a = .eq then some b else (⟨t, h.tail⟩ : OrderedAssocList _ _)[x]? := by + simp only [getElem?, find?, AssocList.orderedFind?] split <;> rename_i w <;> simp only [w, reduceCtorEq, reduceIte] rw [AssocList.orderedFind?_eq_none_of_ltHeadKey?] - have p := headKey?_tail h + have p := ltheadKey?_tail h revert p simp only [ltHeadKey?, AssocList.ltHeadKey?] split · trivial · exact TransCmp.lt_trans w -@[simp] theorem find?_mk_cons_self [OrientedCmp cmp] {h : (AssocList.cons a b t).keysOrdered cmp} : - find? ⟨.cons a b t, h⟩ a = some b := by - simp [find?, AssocList.orderedFind?, OrientedCmp.cmp_refl] +@[simp] theorem getElem?_mk_cons_self [OrientedCmp cmp] {h : (AssocList.cons a b t).keysOrdered cmp} : + (⟨.cons a b t, h⟩ : OrderedAssocList _ _)[a]? = some b := by + simp [getElem?, find?, AssocList.orderedFind?, OrientedCmp.cmp_refl] theorem ext_list {l₁ l₂ : OrderedAssocList cmp β} (w : l₁.list = l₂.list) : l₁ = l₂ := by cases l₁; cases l₂; congr @[ext] theorem ext [AntisymmCmp cmp] [TransCmp cmp] {l₁ l₂ : OrderedAssocList cmp β} - (w : ∀ a, l₁.find? a = l₂.find? a) : l₁ = l₂ := by + (w : ∀ a : α, l₁[a]? = l₂[a]?) : l₁ = l₂ := by apply ext_list apply AssocList.ext_orderedKeys _ l₁.keysOrdered l₂.keysOrdered simpa [find?, AssocList.orderedFind?_eq_find?, l₁.keysOrdered, l₂.keysOrdered] using w -/-- Check if an `OrderedAssocList` contains a specific key. -/ -def contains (l : OrderedAssocList cmp β) (x : α) : Bool := (l.find? x).isSome - @[simp] theorem contains_nil : contains (nil : OrderedAssocList cmp β) x = false := rfl @[simp] theorem contains_mk_cons_self [OrientedCmp cmp] {h : (AssocList.cons a b t).keysOrdered cmp} : contains ⟨.cons a b t, h⟩ a = true := by - simp [contains] + rw [contains_def] + simp /-- Prepend a key-value pair, @@ -688,10 +698,10 @@ def cons (a : α) (b : β) (l : OrderedAssocList cmp β) (w : ltHeadKey? a l) : | ⟨.nil, _⟩ => rfl | ⟨.cons x y t, h⟩ => rfl -@[simp] theorem find?_cons [TransCmp cmp] {l : OrderedAssocList cmp β} {w} : - (cons a b l w).find? x = if cmp x a = .eq then some b else l.find? x := by +@[simp] theorem getElem?_cons [TransCmp cmp] {l : OrderedAssocList cmp β} {w} : + (cons a b l w)[x]? = if cmp x a = .eq then some b else l[x]? := by simp only [cons] - split <;> simp [find?_mk_cons] + split <;> simp [getElem?_mk_cons] @[simp] theorem headKey?_cons : headKey? (cons a b l w) = some a := by match l with @@ -737,13 +747,13 @@ end variable [TransCmp cmp] -theorem find?_insert (l : OrderedAssocList cmp β) (a : α) (b : β) : - (insert l a b).find? x = if cmp x a = .eq then some b else l.find? x := +theorem getElem?_insert (l : OrderedAssocList cmp β) (a : α) (b : β) : + (insert l a b)[x]? = if cmp x a = .eq then some b else l[x]? := AssocList.orderedFind?_orderedInsert l.list l.keysOrdered a b -theorem find?_insert_self (l : OrderedAssocList cmp β) (a : α) (b : β) : - (insert l a b).find? a = some b := by - simp [find?_insert, OrientedCmp.cmp_refl] +theorem getElem?_insert_self (l : OrderedAssocList cmp β) (a : α) (b : β) : + (insert l a b)[a]? = some b := by + simp [getElem?_insert, OrientedCmp.cmp_refl] -- theorem insert_contains (l : OrderedAssocList cmp β) (a : α) (b : β) : -- (l.insert a b).contains x = ((cmp x a = .eq) || l.contains x) := by @@ -771,8 +781,8 @@ def filterMapVal (f : α → β → Option δ) (l : OrderedAssocList cmp β) : ⟨l.list.filterMapVal f, AssocList.filterMapVal_keysOrdered l.keysOrdered⟩ @[simp] -theorem find?_filterMapVal [AntisymmCmp cmp] (l : OrderedAssocList cmp β) : - (filterMapVal f l).find? a = (l.find? a).bind (fun b => f a b) := +theorem getElem?_filterMapVal [AntisymmCmp cmp] (l : OrderedAssocList cmp β) : + (filterMapVal f l)[a]? = l[a]?.bind (fun b => f a b) := AssocList.orderedFind?_filterMapVal l.keysOrdered theorem filterMapVal_filterMapVal [AntisymmCmp cmp] @@ -865,18 +875,18 @@ private theorem merge_mk_cons_mk_cons {f : α → Option β → Option γ → Op split <;> split <;> simp_all [merge] unseal AssocList.orderedMerge in -@[simp] theorem find?_merge {f : α → Option β → Option γ → Option δ} +@[simp] theorem getElem?_merge {f : α → Option β → Option γ → Option δ} (hf : f a none none = none) {l₁ : OrderedAssocList cmp β} {l₂} : - (merge f l₁ l₂).find? a = f a (l₁.find? a) (l₂.find? a) := by + (merge f l₁ l₂)[a]? = f a l₁[a]? l₂[a]? := by match l₁, l₂ with | ⟨.nil, _⟩, ⟨.nil, _⟩ => exact hf.symm | ⟨.nil, _⟩, ⟨.cons x' y' t', h'⟩ => - rw [merge_mk_nil_mk_cons, find?_filterMapVal, find?_mk_nil] + rw [merge_mk_nil_mk_cons, getElem?_filterMapVal, getElem?_mk_nil] unfold Option.bind split <;> (rename_i w; rw [w]) rw [hf] | ⟨.cons x y t, h⟩, ⟨.nil, _⟩ => - rw [merge_mk_cons_mk_nil, find?_filterMapVal, find?_mk_nil] + rw [merge_mk_cons_mk_nil, getElem?_filterMapVal, getElem?_mk_nil] unfold Option.bind split <;> (rename_i w; rw [w]) rw [hf] @@ -884,54 +894,55 @@ unseal AssocList.orderedMerge in rw [merge_mk_cons_mk_cons] split <;> rename_i h₁ · split <;> rename_i h₂ - · rw [find?_merge hf] - rw [find?_mk_cons (a := x)] + · rw [getElem?_merge hf] + rw [getElem?_mk_cons (a := x)] split <;> rename_i h₃ · rcases AntisymmCmp.eq_of_cmp_eq h₃ with rfl - rw [find?_eq_none_of_ltHeadKey?, find?_eq_none_of_ltHeadKey?, hf] + rw [getElem?_eq_none_of_ltHeadKey?, getElem?_eq_none_of_ltHeadKey?, hf] · simp_all · exact h₁ · exact AssocList.ltHeadKey?_of_keysOrdered_cons h · rfl - · rw [find?_mk_cons] + · rw [getElem?_mk_cons] split <;> rename_i h₃ · rcases AntisymmCmp.eq_of_cmp_eq h₃ with rfl - simp only [← h₂, find?_mk_cons_self] - rw [find?_eq_none_of_ltHeadKey?] + simp only [← h₂, getElem?_mk_cons_self] + rw [getElem?_eq_none_of_ltHeadKey?] exact h₁ - · rw [find?_merge hf, find?_mk_cons (a := x), if_neg h₃] + · rw [getElem?_merge hf, getElem?_mk_cons (a := x), if_neg h₃] · rcases (AntisymmCmp.eq_of_cmp_eq h₁) split <;> rename_i h₂ - · rw [find?_merge hf] - rw [find?_mk_cons, find?_mk_cons] + · rw [getElem?_merge hf] + rw [getElem?_mk_cons, getElem?_mk_cons] split <;> rename_i h₃ · rcases (AntisymmCmp.eq_of_cmp_eq h₃) - rw [find?_eq_none_of_ltHeadKey?, find?_eq_none_of_ltHeadKey?, hf, h₂] + rw [getElem?_eq_none_of_ltHeadKey?, getElem?_eq_none_of_ltHeadKey?, hf, h₂] · exact AssocList.ltHeadKey?_of_keysOrdered_cons h' · exact AssocList.ltHeadKey?_of_keysOrdered_cons h · rfl - · rw [find?_mk_cons] + · rw [getElem?_mk_cons] split <;> rename_i h₃ · rcases (AntisymmCmp.eq_of_cmp_eq h₃) - rw [find?_mk_cons_self, find?_mk_cons_self, h₂] - · rw [find?_merge hf, find?_mk_cons (a := x), if_neg h₃, find?_mk_cons (a := x), if_neg h₃] + rw [getElem?_mk_cons_self, getElem?_mk_cons_self, h₂] + · rw [getElem?_merge hf, getElem?_mk_cons (a := x), if_neg h₃, getElem?_mk_cons (a := x), + if_neg h₃] · split <;> rename_i h₂ - · rw [find?_merge hf] - rw [find?_mk_cons (a := x')] + · rw [getElem?_merge hf] + rw [getElem?_mk_cons (a := x')] split <;> rename_i h₃ · rcases (AntisymmCmp.eq_of_cmp_eq h₃) - rw [find?_eq_none_of_ltHeadKey?, find?_eq_none_of_ltHeadKey?, hf] + rw [getElem?_eq_none_of_ltHeadKey?, getElem?_eq_none_of_ltHeadKey?, hf] · exact h₂.symm · exact AssocList.ltHeadKey?_of_keysOrdered_cons h' · exact OrientedCmp.cmp_eq_gt.mp h₁ · rfl - · rw [find?_mk_cons] + · rw [getElem?_mk_cons] split <;> rename_i h₃ · rcases (AntisymmCmp.eq_of_cmp_eq h₃) - simp only [find?_mk_cons_self] - rw [find?_eq_none_of_ltHeadKey?, h₂] + simp only [getElem?_mk_cons_self] + rw [getElem?_eq_none_of_ltHeadKey?, h₂] exact OrientedCmp.cmp_eq_gt.mp h₁ - · rw [find?_merge hf, find?_mk_cons (a := x'), if_neg h₃] + · rw [getElem?_merge hf, getElem?_mk_cons (a := x'), if_neg h₃] theorem merge_comm (f : α → Option β → Option γ → Option δ) (g : α → Option γ → Option β → Option δ) @@ -967,17 +978,17 @@ where | none, some y => some y | none, none => none --- This statement will look better on the version of `OrderedAssocList` with default values, +-- This statement will look better on a version of `OrderedAssocList` with default values, -- where we can just write `(add l₁ l₂).find a = l₁.find a + l₂.find a`. -@[simp] theorem find?_add [Add β] {l₁ : OrderedAssocList cmp β} : - (add l₁ l₂).find? a = - match l₁.find? a, l₂.find? a with +@[simp] theorem getElem?_add [Add β] {l₁ : OrderedAssocList cmp β} {a : α} : + (add l₁ l₂)[a]? = + match l₁[a]?, l₂[a]? with | some x, some y => some (x + y) | some x, none => some x | none, some y => some y | none, none => none := by - rw [add, find?_merge rfl] + rw [add, getElem?_merge rfl] rfl /-- @@ -996,14 +1007,14 @@ where | none, some _ => none | none, none => none -@[simp] theorem find?_mul [Mul β] {l₁ : OrderedAssocList cmp β} : - (mul l₁ l₂).find? a = - match l₁.find? a, l₂.find? a with +@[simp] theorem getElem?_mul [Mul β] {l₁ : OrderedAssocList cmp β} {a : α} : + (mul l₁ l₂)[a]? = + match l₁[a]?, l₂[a]? with | some x, some y => some (x * y) | some _, none => none | none, some _ => none | none, none => none := by - rw [mul, find?_merge rfl] + rw [mul, getElem?_merge rfl] rfl end merge From 247641810937f8c1edc8c2852a2560033fa02378 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 23 Nov 2024 21:47:09 +1100 Subject: [PATCH 13/18] cleanup --- Batteries/Data/OrderedAssocList.lean | 44 +++++++++++----------------- 1 file changed, 17 insertions(+), 27 deletions(-) diff --git a/Batteries/Data/OrderedAssocList.lean b/Batteries/Data/OrderedAssocList.lean index 2fb3bb4ca4..445bea1678 100644 --- a/Batteries/Data/OrderedAssocList.lean +++ b/Batteries/Data/OrderedAssocList.lean @@ -12,15 +12,15 @@ import Batteries.Classes.Order `OrderedAssocList` is a wrapper around `AssocList`, with the additional invariant that the keys are in strictly increasing order. -As a consequence, an `OrderedAssocList` is determined by the `find?` function, that is -`(∀ a, l₁.find? a = l₂.find? a) → l₁ = l₂` -and this makes providing identities between operations more plausible than with `AssocList`. +As a consequence, an `OrderedAssocList` is determined by the lookup function `l[x]?`, that is +`(∀ a, l₁[a]? = l₂[a]?) → l₁ = l₂` +and this makes proving identities between operations much easier than with `AssocList`. We will later add another wrapper requiring that a "default" value does not appear, so e.g. finitely supported functions can be uniquely represented. The main operations defined are: -* `find?`, which linearly searches the list, stopping if the keys get too large. +* `l[x]?`, which linearly searches the list, stopping if the keys get too large. * `insert`, which inserts a new key-value pair, maintaining the order invariant. * `filterMapVal f`, for `f : α → β → Option γ`, which applies a function to values, dropping some values. @@ -60,8 +60,6 @@ abbrev ltHeadKey? (cmp : α → α → Ordering) (a : α) (t : AssocList α β) ltHeadKey? cmp a (.nil : AssocList α β) = True := rfl @[simp] theorem ltHeadKey?_cons : ltHeadKey? cmp a (.cons x y t) = (cmp a x = .lt) := rfl --- TODO redefine using ltHeadKey? - /-- The predicate that the keys of an `AssocList` are in strictly increasing order according to the comparator `cmp`. @@ -79,7 +77,6 @@ instance instKeysOrderedDecidablePred : DecidablePred (keysOrdered cmp : AssocLi @[simp] theorem keysOrdered_cons_nil : keysOrdered cmp (.cons a b nil) := trivial --- TODO rename theorem keysOrdered.tail (h : keysOrdered cmp (.cons a b t)) : keysOrdered cmp t := match t with | .nil => trivial @@ -109,8 +106,8 @@ theorem ltHeadKey?_of_le [TransCmp cmp] (h : cmp x a ≠ .gt) (w : ltHeadKey? cm · exact TransCmp.le_lt_trans h /-- -The head key of the first list is at most the head key of the second list, -or the second list is empty. +A relation on two `AssocList`s, asserting that the head key of the first list is at most +the head key of the second list, or that the second list is empty. -/ abbrev headKey?_le_headKey? (cmp : α → α → Ordering) (s : AssocList α β) (t : AssocList α γ) : Prop := @@ -458,14 +455,6 @@ theorem orderedFind?_orderedInsert_self {cmp : α → α → Ordering} [Antisymm (orderedInsert cmp l a b).orderedFind? cmp a = some b := by simp [h, orderedFind?_orderedInsert, OrientedCmp.cmp_refl] --- theorem orderedInsert_contains {cmp : α → α → Ordering} [BEq α] (l : AssocList α β) (a : α) (b : β) : --- (l.orderedInsert cmp a b).contains x = ((cmp x a = .eq) || l.contains x) := by --- sorry - --- theorem orderedInsert_contains_self {cmp : α → α → Ordering} [BEq α] (l : AssocList α β) (a : α) (b : β) : --- (l.orderedInsert cmp a b).contains a = true := by --- sorry - /-- If two `AssocList`s have ordered keys we can check whether they are equal by checking if their `find?` functions are equal. @@ -755,16 +744,17 @@ theorem getElem?_insert_self (l : OrderedAssocList cmp β) (a : α) (b : β) : (insert l a b)[a]? = some b := by simp [getElem?_insert, OrientedCmp.cmp_refl] --- theorem insert_contains (l : OrderedAssocList cmp β) (a : α) (b : β) : --- (l.insert a b).contains x = ((cmp x a = .eq) || l.contains x) := by --- simp only [contains, find?_insert] --- split <;> rename_i h --- · simp [h] --- · cases find? l x <;> simp [h] +theorem insert_contains (l : OrderedAssocList cmp β) (a : α) (b : β) : + (l.insert a b).contains x = ((cmp x a = .eq) || l.contains x) := by + rw [contains_def, contains_def] + simp only [getElem?_insert] + split <;> rename_i h + · simp [h] + · cases find? l x <;> simp [h] --- theorem insert_contains_self (l : OrderedAssocList cmp β) (a : α) (b : β) : --- (l.insert a b).contains a = true := by --- simp [insert_contains, OrientedCmp.cmp_refl] +theorem insert_contains_self (l : OrderedAssocList cmp β) (a : α) (b : β) : + (l.insert a b).contains a = true := by + simp [insert_contains, OrientedCmp.cmp_refl] end insert @@ -979,7 +969,7 @@ where | none, none => none -- This statement will look better on a version of `OrderedAssocList` with default values, --- where we can just write `(add l₁ l₂).find a = l₁.find a + l₂.find a`. +-- where we can just write `(add l₁ l₂)[a] = l₁[a] + l₂[a]`. @[simp] theorem getElem?_add [Add β] {l₁ : OrderedAssocList cmp β} {a : α} : (add l₁ l₂)[a]? = From 161e49bcd9ade6f4af44c2d94298d89d8ab71338 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 23 Nov 2024 21:51:02 +1100 Subject: [PATCH 14/18] module doc --- Batteries/Data/OrderedAssocList.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Batteries/Data/OrderedAssocList.lean b/Batteries/Data/OrderedAssocList.lean index 445bea1678..e5c8ed2b41 100644 --- a/Batteries/Data/OrderedAssocList.lean +++ b/Batteries/Data/OrderedAssocList.lean @@ -16,6 +16,11 @@ As a consequence, an `OrderedAssocList` is determined by the lookup function `l[ `(∀ a, l₁[a]? = l₂[a]?) → l₁ = l₂` and this makes proving identities between operations much easier than with `AssocList`. +As the operations on `OrderedAssocList` are defined in terms of `AssocList`, +they evaluate well in the kernel, but inherit the `O(n)` time complexity +(i.e. are not suitable for large data). Their advantage relative to an ordered map is the +simple extensionality property above. + We will later add another wrapper requiring that a "default" value does not appear, so e.g. finitely supported functions can be uniquely represented. From 17d52495536977a2bda1f479b7f8215a7faed0fc Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 23 Nov 2024 21:59:40 +1100 Subject: [PATCH 15/18] lint --- Batteries/Classes/Order.lean | 2 +- Batteries/Data/OrderedAssocList.lean | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Batteries/Classes/Order.lean b/Batteries/Classes/Order.lean index 7fabe67c96..6e38ddcc1b 100644 --- a/Batteries/Classes/Order.lean +++ b/Batteries/Classes/Order.lean @@ -72,7 +72,7 @@ end OrientedCmp The `BEq` instance from a comparator `cmp : α → α → Ordering` with `[AntisymmCmp cmp]` and `[OrientedCmp cmp]` is a `LawfulBEq`. -/ -def lawfulBEqOfCmp (cmp : α → α → Ordering) [AntisymmCmp cmp] [OrientedCmp cmp] : +theorem lawfulBEqOfCmp (cmp : α → α → Ordering) [AntisymmCmp cmp] [OrientedCmp cmp] : letI := beqOfCmp cmp LawfulBEq α := let _ := beqOfCmp cmp diff --git a/Batteries/Data/OrderedAssocList.lean b/Batteries/Data/OrderedAssocList.lean index e5c8ed2b41..4b4571ea99 100644 --- a/Batteries/Data/OrderedAssocList.lean +++ b/Batteries/Data/OrderedAssocList.lean @@ -656,7 +656,8 @@ theorem getElem?_mk_cons [TransCmp cmp] · trivial · exact TransCmp.lt_trans w -@[simp] theorem getElem?_mk_cons_self [OrientedCmp cmp] {h : (AssocList.cons a b t).keysOrdered cmp} : +@[simp] theorem getElem?_mk_cons_self [OrientedCmp cmp] + {h : (AssocList.cons a b t).keysOrdered cmp} : (⟨.cons a b t, h⟩ : OrderedAssocList _ _)[a]? = some b := by simp [getElem?, find?, AssocList.orderedFind?, OrientedCmp.cmp_refl] From 22fd20ea3f370495c637125a52902fe7e49c9282 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 23 Nov 2024 22:01:06 +1100 Subject: [PATCH 16/18] . --- Batteries/Data/OrderedAssocList.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Batteries/Data/OrderedAssocList.lean b/Batteries/Data/OrderedAssocList.lean index 4b4571ea99..dcc5d82bbe 100644 --- a/Batteries/Data/OrderedAssocList.lean +++ b/Batteries/Data/OrderedAssocList.lean @@ -17,7 +17,7 @@ As a consequence, an `OrderedAssocList` is determined by the lookup function `l[ and this makes proving identities between operations much easier than with `AssocList`. As the operations on `OrderedAssocList` are defined in terms of `AssocList`, -they evaluate well in the kernel, but inherit the `O(n)` time complexity +they evaluate in the kernel, but inherit the `O(n)` time complexity (i.e. are not suitable for large data). Their advantage relative to an ordered map is the simple extensionality property above. From eae28d1a736f2acefce2be1b96d2e5216b936855 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 23 Nov 2024 22:01:57 +1100 Subject: [PATCH 17/18] updateBatteries --- Batteries.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Batteries.lean b/Batteries.lean index b645334bf4..ef967f8f4f 100644 --- a/Batteries.lean +++ b/Batteries.lean @@ -27,6 +27,7 @@ import Batteries.Data.LazyList import Batteries.Data.List import Batteries.Data.MLList import Batteries.Data.Nat +import Batteries.Data.OrderedAssocList import Batteries.Data.PairingHeap import Batteries.Data.RBMap import Batteries.Data.Range From 00f278086405060077b181085c38ee24aadd2651 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 10 Jan 2025 16:59:22 +1100 Subject: [PATCH 18/18] casing --- Batteries/Data/OrderedAssocList.lean | 232 +++++++++++++-------------- 1 file changed, 113 insertions(+), 119 deletions(-) diff --git a/Batteries/Data/OrderedAssocList.lean b/Batteries/Data/OrderedAssocList.lean index dcc5d82bbe..2e8666ace8 100644 --- a/Batteries/Data/OrderedAssocList.lean +++ b/Batteries/Data/OrderedAssocList.lean @@ -38,9 +38,9 @@ namespace Batteries /-! We first define some predicates and operations in the `AssocList` namespace. -* `keysOrdered cmp l` asserts that the keys of an `l : AssocList` are strictly increasing +* `KeysOrdered cmp l` asserts that the keys of an `l : AssocList` are strictly increasing with respect to a comparator `cmp`. -* `ltHeadKey? cmp a l` asserts that `a` is less than (according to `cmp`) the first key of `l`, +* `LTHeadKey? cmp a l` asserts that `a` is less than (according to `cmp`) the first key of `l`, or that `l` is empty. -/ @@ -58,54 +58,48 @@ def headKey? (l : AssocList α β) : Option α := /-- The condition that an element is less than the first key of an `AssocList`, or that list is empty. -/ -abbrev ltHeadKey? (cmp : α → α → Ordering) (a : α) (t : AssocList α β) : Prop := +abbrev LTHeadKey? (cmp : α → α → Ordering) (a : α) (t : AssocList α β) : Prop := match headKey? t with | none => True | some x => cmp a x = .lt @[simp] theorem ltHeadKey?_nil {cmp : α → α → Ordering} : - ltHeadKey? cmp a (.nil : AssocList α β) = True := rfl -@[simp] theorem ltHeadKey?_cons : ltHeadKey? cmp a (.cons x y t) = (cmp a x = .lt) := rfl + LTHeadKey? cmp a (.nil : AssocList α β) = True := rfl +@[simp] theorem ltHeadKey?_cons : LTHeadKey? cmp a (.cons x y t) = (cmp a x = .lt) := rfl /-- The predicate that the keys of an `AssocList` are in strictly increasing order according to the comparator `cmp`. -/ -def keysOrdered (cmp : α → α → Ordering) : AssocList α β → Prop +def KeysOrdered (cmp : α → α → Ordering) : AssocList α β → Prop | .nil => True | .cons _ _ .nil => True - | .cons a _ (.cons x y t) => cmp a x = .lt ∧ keysOrdered cmp (.cons x y t) + | .cons a _ (.cons x y t) => cmp a x = .lt ∧ KeysOrdered cmp (.cons x y t) -instance instKeysOrderedDecidablePred : DecidablePred (keysOrdered cmp : AssocList α β → Prop) := by - rintro (_|⟨a, b, _|_⟩) <;> dsimp [keysOrdered] - · infer_instance - · infer_instance - · exact @instDecidableAnd _ _ _ (instKeysOrderedDecidablePred _) +@[simp] theorem KeysOrdered_cons_nil : KeysOrdered cmp (.cons a b nil) := trivial -@[simp] theorem keysOrdered_cons_nil : keysOrdered cmp (.cons a b nil) := trivial - -theorem keysOrdered.tail (h : keysOrdered cmp (.cons a b t)) : keysOrdered cmp t := +theorem KeysOrdered.tail (h : KeysOrdered cmp (.cons a b t)) : KeysOrdered cmp t := match t with | .nil => trivial | .cons .. => h.2 -theorem ltHeadKey?_of_keysOrdered_cons (w : keysOrdered cmp (cons a b t)) : ltHeadKey? cmp a t := +theorem ltHeadKey?_of_keysOrdered_cons (w : KeysOrdered cmp (cons a b t)) : LTHeadKey? cmp a t := match t with | .nil => trivial | .cons _ _ _ => w.1 -theorem ltHeadKey?_of_cons [TransCmp cmp] (w : ltHeadKey? cmp a (cons x y t)) - (h : keysOrdered cmp (cons x y t)) : - ltHeadKey? cmp a t := by +theorem ltHeadKey?_of_cons [TransCmp cmp] (w : LTHeadKey? cmp a (cons x y t)) + (h : KeysOrdered cmp (cons x y t)) : + LTHeadKey? cmp a t := by have h := ltHeadKey?_of_keysOrdered_cons h revert w h - dsimp [ltHeadKey?] + dsimp [LTHeadKey?] split · simp · exact TransCmp.lt_trans -theorem ltHeadKey?_of_le [TransCmp cmp] (h : cmp x a ≠ .gt) (w : ltHeadKey? cmp a t) : - ltHeadKey? cmp x t := by +theorem ltHeadKey?_of_le [TransCmp cmp] (h : cmp x a ≠ .gt) (w : LTHeadKey? cmp a t) : + LTHeadKey? cmp x t := by revert w - dsimp [ltHeadKey?] + dsimp [LTHeadKey?] split · simp · exact TransCmp.le_lt_trans h @@ -125,9 +119,9 @@ abbrev headKey?_le_headKey? headKey?_le_headKey? cmp (cons a b t) (cons x y s) = (cmp a x ≠ .gt) := rfl theorem ltHeadKey?_of_headKey?_le_headKey? [TransCmp cmp] - (w : ltHeadKey? cmp a s) (h : headKey?_le_headKey? cmp s t) : - ltHeadKey? cmp a t := by - dsimp [ltHeadKey?, headKey?_le_headKey?] at * + (w : LTHeadKey? cmp a s) (h : headKey?_le_headKey? cmp s t) : + LTHeadKey? cmp a t := by + dsimp [LTHeadKey?, headKey?_le_headKey?] at * revert h w match headKey? s, headKey? t with | some a, some b => exact TransCmp.lt_le_trans @@ -136,10 +130,10 @@ theorem ltHeadKey?_of_headKey?_le_headKey? [TransCmp cmp] | none, none => intros; trivial theorem headKey?_le_headKey?_cons [TransCmp cmp] - (h : keysOrdered cmp (cons x y t)) (w : headKey?_le_headKey? cmp t s) : + (h : KeysOrdered cmp (cons x y t)) (w : headKey?_le_headKey? cmp t s) : headKey?_le_headKey? cmp (cons x y t) s := by have p := ltHeadKey?_of_keysOrdered_cons h - dsimp [ltHeadKey?, headKey?_le_headKey?] at * + dsimp [LTHeadKey?, headKey?_le_headKey?] at * revert p w match headKey? s, headKey? t with | some a, some b => @@ -149,15 +143,15 @@ theorem headKey?_le_headKey?_cons [TransCmp cmp] | none, some b => simp | none, none => intros; trivial -theorem keysOrdered_cons {cmp : α → α → Ordering} - (w : ltHeadKey? cmp a t) (h : keysOrdered cmp t) : - keysOrdered cmp (.cons a b t) := by +theorem KeysOrdered_cons {cmp : α → α → Ordering} + (w : LTHeadKey? cmp a t) (h : KeysOrdered cmp t) : + KeysOrdered cmp (.cons a b t) := by match t with | .nil => trivial | .cons x y s => exact ⟨w, h⟩ -theorem find?_eq_none_of_ltHeadKey? {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEq α] - (w : ltHeadKey? cmp a l) (h : keysOrdered cmp l) : +theorem find?_eq_none_of_LTHeadKey? {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEq α] + (w : LTHeadKey? cmp a l) (h : KeysOrdered cmp l) : l.find? a = none := by match l with | nil => rfl @@ -165,7 +159,7 @@ theorem find?_eq_none_of_ltHeadKey? {cmp : α → α → Ordering} [TransCmp cmp rw [find?] split · simp_all [OrientedCmp.cmp_refl] - · exact find?_eq_none_of_ltHeadKey? (ltHeadKey?_of_cons w h) h.tail + · exact find?_eq_none_of_LTHeadKey? (ltHeadKey?_of_cons w h) h.tail /-! # Ordered-respecting operations on `AssocList` @@ -173,7 +167,7 @@ theorem find?_eq_none_of_ltHeadKey? {cmp : α → α → Ordering} [TransCmp cmp We now define `orderedInsert`, and `orderedMerge`, which will later be wrapped as `OrderedAssocList.insert` and `OrderedAssocList.merge`. -We prove that with `keysOrdered` input these functions produce `keysOrdered` outputs. +We prove that with `KeysOrdered` input these functions produce `KeysOrdered` outputs. We prove the same about `AssocList.filterMapVal`. -/ @@ -220,8 +214,8 @@ theorem headKey?_orderedInsert_or (cmp) (l : AssocList α β) (a) (b) : | .nil => left; rfl | .cons x y s => dsimp; cases cmp a x <;> simp -theorem orderedInsert_keysOrdered [AntisymmCmp cmp] [OrientedCmp cmp] (h : keysOrdered cmp l) : - keysOrdered cmp (orderedInsert cmp l a b) := by +theorem orderedInsert_KeysOrdered [AntisymmCmp cmp] [OrientedCmp cmp] (h : KeysOrdered cmp l) : + KeysOrdered cmp (orderedInsert cmp l a b) := by match l with | .nil => trivial | .cons x y t => @@ -234,19 +228,19 @@ theorem orderedInsert_keysOrdered [AntisymmCmp cmp] [OrientedCmp cmp] (h : keysO | .gt => exact aux h w -- I've split this step out with a name as it is useful to fill in a proof term later. where aux [AntisymmCmp cmp] [OrientedCmp cmp] {x y t} - (h : keysOrdered cmp (cons x y t)) (w : cmp a x = Ordering.gt) : - keysOrdered cmp (cons x y (orderedInsert cmp t a b)) := by - apply keysOrdered_cons - · dsimp [ltHeadKey?] + (h : KeysOrdered cmp (cons x y t)) (w : cmp a x = Ordering.gt) : + KeysOrdered cmp (cons x y (orderedInsert cmp t a b)) := by + apply KeysOrdered_cons + · dsimp [LTHeadKey?] rcases headKey?_orderedInsert_or cmp t a b with (p|p) · rw [p] exact OrientedCmp.cmp_eq_gt.mp w · rw [p] exact ltHeadKey?_of_keysOrdered_cons h - · apply orderedInsert_keysOrdered + · apply orderedInsert_KeysOrdered exact h.tail -theorem headKey?_le_headKey?_filterMapVal [TransCmp cmp] (h : keysOrdered cmp l) : +theorem headKey?_le_headKey?_filterMapVal [TransCmp cmp] (h : KeysOrdered cmp l) : headKey?_le_headKey? cmp l (l.filterMapVal f) := by match l with | .nil => simp [headKey?_le_headKey?] @@ -257,18 +251,18 @@ theorem headKey?_le_headKey?_filterMapVal [TransCmp cmp] (h : keysOrdered cmp l) exact headKey?_le_headKey?_cons h (headKey?_le_headKey?_filterMapVal h.tail) | some _ => simp [OrientedCmp.cmp_refl] -theorem filterMapVal_keysOrdered [TransCmp cmp] (h : keysOrdered cmp l) : - keysOrdered cmp (l.filterMapVal f) := by +theorem filterMapVal_KeysOrdered [TransCmp cmp] (h : KeysOrdered cmp l) : + KeysOrdered cmp (l.filterMapVal f) := by match l with | .nil => exact h | .cons x y t => simp only [filterMapVal] split - · exact filterMapVal_keysOrdered h.tail - · apply keysOrdered_cons + · exact filterMapVal_KeysOrdered h.tail + · apply KeysOrdered_cons · exact ltHeadKey?_of_headKey?_le_headKey? (ltHeadKey?_of_keysOrdered_cons h) (headKey?_le_headKey?_filterMapVal h.tail) - · exact filterMapVal_keysOrdered h.tail + · exact filterMapVal_KeysOrdered h.tail /-- Merge two `AssocList`s, @@ -300,9 +294,9 @@ def orderedMerge (cmp : α → α → Ordering) (f : α → Option β → Option termination_by l₁ l₂ => l₁.length + l₂.length theorem ltHeadKey?_orderedMerge [TransCmp cmp] - (h₁ : ltHeadKey? cmp a l₁) (h₂ : ltHeadKey? cmp a l₂) - (w₁ : keysOrdered cmp l₁) (w₂ : keysOrdered cmp l₂) : - ltHeadKey? cmp a (orderedMerge cmp f l₁ l₂) := by + (h₁ : LTHeadKey? cmp a l₁) (h₂ : LTHeadKey? cmp a l₂) + (w₁ : KeysOrdered cmp l₁) (w₂ : KeysOrdered cmp l₂) : + LTHeadKey? cmp a (orderedMerge cmp f l₁ l₂) := by match l₁, l₂ with | .nil, .nil => simp [orderedMerge] | .nil, .cons a₂ g t₂ => @@ -332,39 +326,39 @@ theorem ltHeadKey?_orderedMerge [TransCmp cmp] · exact ltHeadKey?_orderedMerge h₁ (ltHeadKey?_of_cons h₂ w₂) w₁ w₂.tail unseal orderedMerge in -theorem orderedMerge_keysOrdered [AntisymmCmp cmp] [TransCmp cmp] - (h₁ : keysOrdered cmp l₁) (h₂ : keysOrdered cmp l₂) : - keysOrdered cmp (orderedMerge cmp f l₁ l₂) := by +theorem orderedMerge_KeysOrdered [AntisymmCmp cmp] [TransCmp cmp] + (h₁ : KeysOrdered cmp l₁) (h₂ : KeysOrdered cmp l₂) : + KeysOrdered cmp (orderedMerge cmp f l₁ l₂) := by match l₁, l₂ with | .nil, .nil => trivial - | .nil, .cons a₂ g t₂ => exact filterMapVal_keysOrdered h₂ - | .cons a₁ b t₁, .nil => exact filterMapVal_keysOrdered h₁ + | .nil, .cons a₂ g t₂ => exact filterMapVal_KeysOrdered h₂ + | .cons a₁ b t₁, .nil => exact filterMapVal_KeysOrdered h₁ | .cons a₁ b t₁, .cons a₂ g t₂ => rw [orderedMerge] match h : cmp a₁ a₂ with | .lt => match (f a₁ (some b) none) with | some d => - apply keysOrdered_cons + apply KeysOrdered_cons · apply ltHeadKey?_orderedMerge (ltHeadKey?_of_keysOrdered_cons h₁) (ltHeadKey?_cons.mpr h) h₁.tail h₂ - · exact orderedMerge_keysOrdered h₁.tail h₂ - | none => exact orderedMerge_keysOrdered h₁.tail h₂ + · exact orderedMerge_KeysOrdered h₁.tail h₂ + | none => exact orderedMerge_KeysOrdered h₁.tail h₂ | .eq => match (f a₁ (some b) (some g)) with | some d => dsimp - apply keysOrdered_cons + apply KeysOrdered_cons · rcases (AntisymmCmp.eq_of_cmp_eq h) with rfl exact ltHeadKey?_orderedMerge (ltHeadKey?_of_keysOrdered_cons h₁) (ltHeadKey?_of_keysOrdered_cons h₂) h₁.tail h₂.tail - · exact orderedMerge_keysOrdered h₁.tail h₂.tail - | none => exact orderedMerge_keysOrdered h₁.tail h₂.tail + · exact orderedMerge_KeysOrdered h₁.tail h₂.tail + | none => exact orderedMerge_KeysOrdered h₁.tail h₂.tail | .gt => match (f a₂ none (some g)) with | some d => - apply keysOrdered_cons + apply KeysOrdered_cons · apply ltHeadKey?_orderedMerge (ltHeadKey?_cons.mpr (OrientedCmp.cmp_eq_gt.mp h)) (ltHeadKey?_of_keysOrdered_cons h₂) h₁ h₂.tail - · exact orderedMerge_keysOrdered h₁ h₂.tail - | none => exact orderedMerge_keysOrdered h₁ h₂.tail + · exact orderedMerge_KeysOrdered h₁ h₂.tail + | none => exact orderedMerge_KeysOrdered h₁ h₂.tail /-- Find the value associated to a key by traversing left to right, @@ -383,7 +377,7 @@ def orderedFind? (cmp : α → α → Ordering) (l : AssocList α β) (x : α) : theorem orderedFind?_eq_find? {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] [BEq α] [LawfulBEq α] - (l : AssocList α β) (h : l.keysOrdered cmp) (x : α) : l.orderedFind? cmp x = l.find? x := by + (l : AssocList α β) (h : l.KeysOrdered cmp) (x : α) : l.orderedFind? cmp x = l.find? x := by match l with | .nil => rfl | .cons a b t => @@ -391,7 +385,7 @@ theorem orderedFind?_eq_find? split · split · simp_all [OrientedCmp.cmp_refl] - · rw [AssocList.find?_eq_none_of_ltHeadKey? (cmp := cmp)] + · rw [AssocList.find?_eq_none_of_LTHeadKey? (cmp := cmp)] · exact AssocList.ltHeadKey?_of_le (by simp_all) (AssocList.ltHeadKey?_of_keysOrdered_cons h) · exact h.tail @@ -400,23 +394,23 @@ theorem orderedFind?_eq_find? · simp_all [OrientedCmp.cmp_refl] · apply orderedFind?_eq_find? _ h.tail -theorem orderedFind?_eq_none_of_ltHeadKey? (l : AssocList α β) (w : ltHeadKey? cmp x l) : +theorem orderedFind?_eq_none_of_LTHeadKey? (l : AssocList α β) (w : LTHeadKey? cmp x l) : orderedFind? cmp l x = none := by match l with | .nil => rfl | .cons a b t => match p : cmp x a with | .lt => simp [orderedFind?, p] - | .eq => simp_all [ltHeadKey?] - | .gt => simp_all [ltHeadKey?] + | .eq => simp_all [LTHeadKey?] + | .gt => simp_all [LTHeadKey?] theorem orderedFind?_cons [TransCmp cmp] - (h : (AssocList.cons a b t).keysOrdered cmp) : + (h : (AssocList.cons a b t).KeysOrdered cmp) : orderedFind? cmp (.cons a b t) x = if cmp x a = .eq then some b else orderedFind? cmp t x := by simp only [find?, AssocList.orderedFind?] split <;> rename_i w <;> simp only [w, reduceCtorEq, reduceIte] - rw [AssocList.orderedFind?_eq_none_of_ltHeadKey?] - simp only [ltHeadKey?, headKey?] + rw [AssocList.orderedFind?_eq_none_of_LTHeadKey?] + simp only [LTHeadKey?, headKey?] split <;> rename_i h' · trivial · apply TransCmp.lt_trans w @@ -432,12 +426,12 @@ theorem orderedFind?_cons [TransCmp cmp] simp [find?, AssocList.orderedFind?, OrientedCmp.cmp_refl] theorem orderedFind?_orderedInsert {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] - (l : AssocList α β) (h : keysOrdered cmp l) (a : α) (b : β) : + (l : AssocList α β) (h : KeysOrdered cmp l) (a : α) (b : β) : (orderedInsert cmp l a b).orderedFind? cmp x = if cmp x a = .eq then some b else l.orderedFind? cmp x := by match l with | .nil => - simp only [orderedInsert, orderedFind?_cons, keysOrdered_cons_nil] + simp only [orderedInsert, orderedFind?_cons, KeysOrdered_cons_nil] | .cons a' b' t => simp only [orderedInsert_cons] split <;> rename_i h₁ @@ -452,11 +446,11 @@ theorem orderedFind?_orderedInsert {cmp : α → α → Ordering} [AntisymmCmp c · rcases (AntisymmCmp.eq_of_cmp_eq h₂).symm simp_all [OrientedCmp.cmp_eq_gt] · rfl - · exact orderedInsert_keysOrdered.aux h h₁ + · exact orderedInsert_KeysOrdered.aux h h₁ termination_by l.length theorem orderedFind?_orderedInsert_self {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] - (l : AssocList α β) (h : keysOrdered cmp l) (a : α) (b : β) : + (l : AssocList α β) (h : KeysOrdered cmp l) (a : α) (b : β) : (orderedInsert cmp l a b).orderedFind? cmp a = some b := by simp [h, orderedFind?_orderedInsert, OrientedCmp.cmp_refl] @@ -466,7 +460,7 @@ we can check whether they are equal by checking if their `find?` functions are e -/ theorem ext_orderedKeys (cmp : α → α → Ordering) [AntisymmCmp cmp] [TransCmp cmp] - {l₁ l₂ : AssocList α β} (h₁ : l₁.keysOrdered cmp) (h₂ : l₂.keysOrdered cmp) + {l₁ l₂ : AssocList α β} (h₁ : l₁.KeysOrdered cmp) (h₂ : l₂.KeysOrdered cmp) (w : ∀ a, l₁.orderedFind? cmp a = l₂.orderedFind? cmp a) : l₁ = l₂ := by match w₁ : l₁, w₂ : l₂ with | .nil, .nil => rfl @@ -483,7 +477,7 @@ theorem ext_orderedKeys | .lt => exfalso have w₂ : l₂.orderedFind? cmp a₁ = none := by - rw [w₂, orderedFind?_eq_none_of_ltHeadKey? _ h] + rw [w₂, orderedFind?_eq_none_of_LTHeadKey? _ h] specialize w a₁ simp [orderedFind?_cons_self] at w simp_all [orderedFind?_eq_find?] @@ -498,21 +492,21 @@ theorem ext_orderedKeys rw [orderedFind?_cons h₁, orderedFind?_cons h₂] at w split at w <;> rename_i h · rcases AntisymmCmp.eq_of_cmp_eq h - rw [orderedFind?_eq_none_of_ltHeadKey?, orderedFind?_eq_none_of_ltHeadKey?] + rw [orderedFind?_eq_none_of_LTHeadKey?, orderedFind?_eq_none_of_LTHeadKey?] apply ltHeadKey?_of_keysOrdered_cons h₂ apply ltHeadKey?_of_keysOrdered_cons h₁ · exact w | .gt => exfalso have w₁ : l₁.orderedFind? cmp a₂ = none := by - rw [w₁, orderedFind?_eq_none_of_ltHeadKey? _ (OrientedCmp.cmp_eq_gt.mp h)] + rw [w₁, orderedFind?_eq_none_of_LTHeadKey? _ (OrientedCmp.cmp_eq_gt.mp h)] specialize w a₂ simp [orderedFind?_cons_self] at w simp_all [orderedFind?_eq_find?] @[simp] theorem orderedFind?_filterMapVal {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] - {l : AssocList α β} (h : keysOrdered cmp l) : + {l : AssocList α β} (h : KeysOrdered cmp l) : (filterMapVal f l).orderedFind? cmp a = (l.orderedFind? cmp a).bind (fun b => f a b) := by -- This isn't true at the level of `AssocList`; we need uniqueness of keys. match l with @@ -523,7 +517,7 @@ theorem orderedFind?_filterMapVal {cmp : α → α → Ordering} [AntisymmCmp cm · rw [orderedFind?_filterMapVal h.tail] split <;> rename_i h' · have h' := AntisymmCmp.eq_of_cmp_eq h' - rw [orderedFind?_eq_none_of_ltHeadKey?] + rw [orderedFind?_eq_none_of_LTHeadKey?] · simp_all · rcases h' with rfl exact ltHeadKey?_of_keysOrdered_cons h @@ -532,20 +526,20 @@ theorem orderedFind?_filterMapVal {cmp : α → α → Ordering} [AntisymmCmp cm · split <;> rename_i h' · simp_all [AntisymmCmp.eq_of_cmp_eq h'] · rw [orderedFind?_filterMapVal h.tail] - · exact keysOrdered_cons + · exact KeysOrdered_cons (ltHeadKey?_of_headKey?_le_headKey? (ltHeadKey?_of_keysOrdered_cons h) (headKey?_le_headKey?_filterMapVal h.tail)) - (filterMapVal_keysOrdered h.tail) + (filterMapVal_KeysOrdered h.tail) termination_by l.length theorem filterMapVal_filterMapVal {cmp : α → α → Ordering} [AntisymmCmp cmp] [TransCmp cmp] {f : α → γ → Option δ} {g : α → β → Option γ} - {l : AssocList α β} (h : keysOrdered cmp l) : + {l : AssocList α β} (h : KeysOrdered cmp l) : filterMapVal f (filterMapVal g l) = filterMapVal (fun a b => (g a b).bind (fun c => f a c)) l := by apply ext_orderedKeys (cmp := cmp) - · exact filterMapVal_keysOrdered (filterMapVal_keysOrdered h) - · exact filterMapVal_keysOrdered h + · exact filterMapVal_KeysOrdered (filterMapVal_KeysOrdered h) + · exact filterMapVal_KeysOrdered h · intro a rw [orderedFind?_filterMapVal, orderedFind?_filterMapVal h, orderedFind?_filterMapVal h] · ext d @@ -555,7 +549,7 @@ theorem filterMapVal_filterMapVal {cmp : α → α → Ordering} [AntisymmCmp cm refine ⟨b, hb, c, hc, hd⟩ · rintro ⟨b, hb, c, hc, hd⟩ refine ⟨c, ⟨⟨b, hb, hc⟩, hd⟩⟩ - · exact filterMapVal_keysOrdered h + · exact filterMapVal_KeysOrdered h end AssocList @@ -567,7 +561,7 @@ structure OrderedAssocList {α : Type u} (cmp : α → α → Ordering) (β : Ty /-- The underlying `AssocList` of an `OrderedAssocList`. -/ list : AssocList α β /-- The invariant that the keys are in strictly increasing order according to `cmp`. -/ - keysOrdered : list.keysOrdered cmp + KeysOrdered : list.KeysOrdered cmp namespace OrderedAssocList @@ -628,36 +622,36 @@ def headKey? (l : OrderedAssocList cmp β) : Option α := l.list.headKey? @[simp] theorem headKey?_mk_cons : headKey? ⟨.cons a b t, h⟩ = some a := rfl /-- Either `a` is less than the first key of `l`, or `l` is empty. -/ -def ltHeadKey? (a : α) (l : OrderedAssocList cmp β) : Prop := AssocList.ltHeadKey? cmp a l.list +def LTHeadKey? (a : α) (l : OrderedAssocList cmp β) : Prop := AssocList.LTHeadKey? cmp a l.list /-- The head key of a tail is either `none`, or greater than the original head key. -/ -theorem ltheadKey?_tail (h : AssocList.keysOrdered cmp (.cons a b t)) : - ltHeadKey? a ⟨t, h.tail⟩ := by - dsimp [ltHeadKey?] +theorem ltheadKey?_tail (h : AssocList.KeysOrdered cmp (.cons a b t)) : + LTHeadKey? a ⟨t, h.tail⟩ := by + dsimp [LTHeadKey?] match t with | .nil => trivial | .cons _ _ _ => exact h.1 -theorem getElem?_eq_none_of_ltHeadKey? (l : OrderedAssocList cmp β) (w : ltHeadKey? x l) : +theorem getElem?_eq_none_of_LTHeadKey? (l : OrderedAssocList cmp β) (w : LTHeadKey? x l) : l[x]? = none := - AssocList.orderedFind?_eq_none_of_ltHeadKey? _ w + AssocList.orderedFind?_eq_none_of_LTHeadKey? _ w theorem getElem?_mk_cons [TransCmp cmp] - {h : (AssocList.cons a b t).keysOrdered cmp} : + {h : (AssocList.cons a b t).KeysOrdered cmp} : (⟨.cons a b t, h⟩ : OrderedAssocList _ _)[x]? = if cmp x a = .eq then some b else (⟨t, h.tail⟩ : OrderedAssocList _ _)[x]? := by simp only [getElem?, find?, AssocList.orderedFind?] split <;> rename_i w <;> simp only [w, reduceCtorEq, reduceIte] - rw [AssocList.orderedFind?_eq_none_of_ltHeadKey?] + rw [AssocList.orderedFind?_eq_none_of_LTHeadKey?] have p := ltheadKey?_tail h revert p - simp only [ltHeadKey?, AssocList.ltHeadKey?] + simp only [LTHeadKey?, AssocList.LTHeadKey?] split · trivial · exact TransCmp.lt_trans w @[simp] theorem getElem?_mk_cons_self [OrientedCmp cmp] - {h : (AssocList.cons a b t).keysOrdered cmp} : + {h : (AssocList.cons a b t).KeysOrdered cmp} : (⟨.cons a b t, h⟩ : OrderedAssocList _ _)[a]? = some b := by simp [getElem?, find?, AssocList.orderedFind?, OrientedCmp.cmp_refl] @@ -667,12 +661,12 @@ theorem ext_list {l₁ l₂ : OrderedAssocList cmp β} (w : l₁.list = l₂.lis @[ext] theorem ext [AntisymmCmp cmp] [TransCmp cmp] {l₁ l₂ : OrderedAssocList cmp β} (w : ∀ a : α, l₁[a]? = l₂[a]?) : l₁ = l₂ := by apply ext_list - apply AssocList.ext_orderedKeys _ l₁.keysOrdered l₂.keysOrdered - simpa [find?, AssocList.orderedFind?_eq_find?, l₁.keysOrdered, l₂.keysOrdered] using w + apply AssocList.ext_orderedKeys _ l₁.KeysOrdered l₂.KeysOrdered + simpa [find?, AssocList.orderedFind?_eq_find?, l₁.KeysOrdered, l₂.KeysOrdered] using w @[simp] theorem contains_nil : contains (nil : OrderedAssocList cmp β) x = false := rfl @[simp] theorem contains_mk_cons_self [OrientedCmp cmp] - {h : (AssocList.cons a b t).keysOrdered cmp} : + {h : (AssocList.cons a b t).KeysOrdered cmp} : contains ⟨.cons a b t, h⟩ a = true := by rw [contains_def] simp @@ -681,7 +675,7 @@ theorem ext_list {l₁ l₂ : OrderedAssocList cmp β} (w : l₁.list = l₂.lis Prepend a key-value pair, requiring a proof that the key is smaller than the existing smallest key. -/ -def cons (a : α) (b : β) (l : OrderedAssocList cmp β) (w : ltHeadKey? a l) : +def cons (a : α) (b : β) (l : OrderedAssocList cmp β) (w : LTHeadKey? a l) : OrderedAssocList cmp β := match l with | ⟨.nil, _⟩ => ⟨.cons a b .nil, trivial⟩ @@ -715,7 +709,7 @@ This replaces the current value if the key is already present, and otherwise inserts it before the first key which is greater than the inserted key. -/ def insert (l : OrderedAssocList cmp β) (a : α) (b : β) : OrderedAssocList cmp β := - ⟨l.list.orderedInsert cmp a b, AssocList.orderedInsert_keysOrdered l.keysOrdered⟩ + ⟨l.list.orderedInsert cmp a b, AssocList.orderedInsert_KeysOrdered l.KeysOrdered⟩ @[simp] theorem insert_mk_nil : insert (⟨.nil, h⟩ : OrderedAssocList cmp β) a b = ⟨.cons a b .nil, trivial⟩ := rfl @@ -726,7 +720,7 @@ def insert (l : OrderedAssocList cmp β) (a : α) (b : β) : OrderedAssocList cm | .eq => ⟨.cons a b t, by cases (AntisymmCmp.eq_of_cmp_eq w); cases t <;> exact h⟩ | .gt => .cons x y (insert ⟨t, h.tail⟩ a b) (AssocList.ltHeadKey?_of_keysOrdered_cons - (AssocList.orderedInsert_keysOrdered.aux h w)) := by + (AssocList.orderedInsert_KeysOrdered.aux h w)) := by dsimp [insert, AssocList.orderedInsert] congr split <;> simp @@ -744,7 +738,7 @@ variable [TransCmp cmp] theorem getElem?_insert (l : OrderedAssocList cmp β) (a : α) (b : β) : (insert l a b)[x]? = if cmp x a = .eq then some b else l[x]? := - AssocList.orderedFind?_orderedInsert l.list l.keysOrdered a b + AssocList.orderedFind?_orderedInsert l.list l.KeysOrdered a b theorem getElem?_insert_self (l : OrderedAssocList cmp β) (a : α) (b : β) : (insert l a b)[a]? = some b := by @@ -774,12 +768,12 @@ either replacing the value or dropping it if the function returns `none`. -/ def filterMapVal (f : α → β → Option δ) (l : OrderedAssocList cmp β) : OrderedAssocList cmp δ := - ⟨l.list.filterMapVal f, AssocList.filterMapVal_keysOrdered l.keysOrdered⟩ + ⟨l.list.filterMapVal f, AssocList.filterMapVal_KeysOrdered l.KeysOrdered⟩ @[simp] theorem getElem?_filterMapVal [AntisymmCmp cmp] (l : OrderedAssocList cmp β) : (filterMapVal f l)[a]? = l[a]?.bind (fun b => f a b) := - AssocList.orderedFind?_filterMapVal l.keysOrdered + AssocList.orderedFind?_filterMapVal l.KeysOrdered theorem filterMapVal_filterMapVal [AntisymmCmp cmp] {f : α → γ → Option δ} {g : α → β → Option γ} @@ -787,7 +781,7 @@ theorem filterMapVal_filterMapVal [AntisymmCmp cmp] filterMapVal f (filterMapVal g l) = filterMapVal (fun a b => (g a b).bind (fun c => f a c)) l := by apply ext_list - exact AssocList.filterMapVal_filterMapVal l.keysOrdered + exact AssocList.filterMapVal_filterMapVal l.KeysOrdered end filterMapVal @@ -802,7 +796,7 @@ dropping values where the function returns `none`. def merge (f : α → Option β → Option γ → Option δ) (l₁ : OrderedAssocList cmp β) (l₂ : OrderedAssocList cmp γ) : OrderedAssocList cmp δ := ⟨AssocList.orderedMerge cmp f l₁.list l₂.list, - AssocList.orderedMerge_keysOrdered l₁.keysOrdered l₂.keysOrdered⟩ + AssocList.orderedMerge_KeysOrdered l₁.KeysOrdered l₂.KeysOrdered⟩ @[simp] theorem list_merge {l₁ : OrderedAssocList cmp β} : (merge f l₁ l₂).list = AssocList.orderedMerge cmp f l₁.list l₂.list := @@ -849,7 +843,7 @@ private theorem merge_mk_cons_mk_cons {f : α → Option β → Option γ → Op simp only [w, i] at p simp only [list_merge] simp only [← p] - exact (merge f _ _).keysOrdered⟩ + exact (merge f _ _).KeysOrdered⟩ | .eq => match w : f x (some y) (some y') with | none => merge f ⟨t, h.tail⟩ ⟨t', h'.tail⟩ | some d => ⟨.cons x d (merge f ⟨t, h.tail⟩ ⟨t', h'.tail⟩).list, by @@ -857,7 +851,7 @@ private theorem merge_mk_cons_mk_cons {f : α → Option β → Option γ → Op simp only [w, i] at p simp only [list_merge] simp only [← p] - exact (merge f _ _).keysOrdered⟩ + exact (merge f _ _).KeysOrdered⟩ | .gt => match w : f x' none (some y') with | none => merge f ⟨.cons x y t, h⟩ ⟨t', h'.tail⟩ | some d => ⟨.cons x' d (merge f ⟨.cons x y t, h⟩ ⟨t', h'.tail⟩).list, by @@ -865,7 +859,7 @@ private theorem merge_mk_cons_mk_cons {f : α → Option β → Option γ → Op simp only [w, i] at p simp only [list_merge] simp only [← p] - exact (merge f _ _).keysOrdered⟩ := by + exact (merge f _ _).KeysOrdered⟩ := by apply ext_list simp only [merge_mk_cons_mk_cons_list] split <;> split <;> simp_all [merge] @@ -894,7 +888,7 @@ unseal AssocList.orderedMerge in rw [getElem?_mk_cons (a := x)] split <;> rename_i h₃ · rcases AntisymmCmp.eq_of_cmp_eq h₃ with rfl - rw [getElem?_eq_none_of_ltHeadKey?, getElem?_eq_none_of_ltHeadKey?, hf] + rw [getElem?_eq_none_of_LTHeadKey?, getElem?_eq_none_of_LTHeadKey?, hf] · simp_all · exact h₁ · exact AssocList.ltHeadKey?_of_keysOrdered_cons h @@ -903,7 +897,7 @@ unseal AssocList.orderedMerge in split <;> rename_i h₃ · rcases AntisymmCmp.eq_of_cmp_eq h₃ with rfl simp only [← h₂, getElem?_mk_cons_self] - rw [getElem?_eq_none_of_ltHeadKey?] + rw [getElem?_eq_none_of_LTHeadKey?] exact h₁ · rw [getElem?_merge hf, getElem?_mk_cons (a := x), if_neg h₃] · rcases (AntisymmCmp.eq_of_cmp_eq h₁) @@ -912,7 +906,7 @@ unseal AssocList.orderedMerge in rw [getElem?_mk_cons, getElem?_mk_cons] split <;> rename_i h₃ · rcases (AntisymmCmp.eq_of_cmp_eq h₃) - rw [getElem?_eq_none_of_ltHeadKey?, getElem?_eq_none_of_ltHeadKey?, hf, h₂] + rw [getElem?_eq_none_of_LTHeadKey?, getElem?_eq_none_of_LTHeadKey?, hf, h₂] · exact AssocList.ltHeadKey?_of_keysOrdered_cons h' · exact AssocList.ltHeadKey?_of_keysOrdered_cons h · rfl @@ -927,7 +921,7 @@ unseal AssocList.orderedMerge in rw [getElem?_mk_cons (a := x')] split <;> rename_i h₃ · rcases (AntisymmCmp.eq_of_cmp_eq h₃) - rw [getElem?_eq_none_of_ltHeadKey?, getElem?_eq_none_of_ltHeadKey?, hf] + rw [getElem?_eq_none_of_LTHeadKey?, getElem?_eq_none_of_LTHeadKey?, hf] · exact h₂.symm · exact AssocList.ltHeadKey?_of_keysOrdered_cons h' · exact OrientedCmp.cmp_eq_gt.mp h₁ @@ -936,7 +930,7 @@ unseal AssocList.orderedMerge in split <;> rename_i h₃ · rcases (AntisymmCmp.eq_of_cmp_eq h₃) simp only [getElem?_mk_cons_self] - rw [getElem?_eq_none_of_ltHeadKey?, h₂] + rw [getElem?_eq_none_of_LTHeadKey?, h₂] exact OrientedCmp.cmp_eq_gt.mp h₁ · rw [getElem?_merge hf, getElem?_mk_cons (a := x'), if_neg h₃]