def LEByKey {α : Type} [LinearOrder α] {β : Type u_1} (a b : α × β) : Prop

Equations

• LEByKey a b = (a.1 ≤ b.1)

instance instDecidableRelProdLEByKey {α : Type} [LinearOrder α] {β : Type u_1} : DecidableRel fun (a b : α × β) => LEByKey a b

Equations

• instDecidableRelProdLEByKey a b = if h : a.1 ≤ b.1 then isTrue h else isFalse h

instance instIsTotalProdLEByKey {α : Type} [LinearOrder α] {β : Type u_1} : IsTotal (α × β) LEByKey

instance instIsTransProdLEByKey {α : Type} [LinearOrder α] {β : Type u_1} : IsTrans (α × β) LEByKey

def KeyValueList {α : Type} [LinearOrder α] {β : Type u_1} (l : List (α × β)) : Prop

Equations

• KeyValueList [] = True
• KeyValueList [hd'] = (KeyValueList [] ∧ True)
• KeyValueList (hd' :: hd'_1 :: tail_1) = (KeyValueList (hd'_1 :: tail_1) ∧ hd'.1 < hd'_1.1)

def List.addKV {α : Type} [LinearOrder α] {β : Type u_1} [DecidableEq β] [Add β] (l : List (α × β)) (a : α) (b : β) : List (α × β)

Equations

• One or more equations did not get rendered due to their size.

theorem KeyValueList.sorted {α : Type} [LinearOrder α] {β : Type u_1} (l : List (α × β)) (h : KeyValueList l) : List.Sorted LEByKey l

theorem KeyValueList.nodup {α : Type} [LinearOrder α] {β : Type u_1} (l : List (α × β)) (hl : KeyValueList l) : l.Nodup

theorem KeyValueList.nodupkey {α : Type} [LinearOrder α] {β : Type u_1} (l : List (α × β)) (h : KeyValueList l) : List.Pairwise (fun (x1 x2 : α × β) => x1.1 ≠ x2.1) l

theorem KeyValueList.functional {α : Type} [LinearOrder α] {β : Type u_1} (l : List (α × β)) (hl : KeyValueList l) (x : α × β) : x ∈ l → ∀ y ∈ l, x.1 = y.1 → x.2 = y.2

theorem KeyValueList.eq_iff_forall_mem {α : Type} [LinearOrder α] {β : Type u_1} [DecidableEq β] (l₁ l₂ : List (α × β)) (h₁ : KeyValueList l₁) (h₂ : KeyValueList l₂) : l₁ = l₂ ↔ ∀ (x : α × β), x ∈ l₁ ↔ x ∈ l₂

theorem KeyValueList.erase {α : Type} [LinearOrder α] {β : Type u_1} (l : List (α × β)) (h : KeyValueList l) (a : α) : KeyValueList (List.eraseP (fun (x : α × β) => decide (x.1 = a)) l)

theorem KeyValueList.erase_find {α : Type} [LinearOrder α] {β : Type u_1} (l : List (α × β)) (h : KeyValueList l) (a : α) : List.find? (fun (x : α × β) => decide (x.1 = a)) (List.eraseP (fun (x : α × β) => decide (x.1 = a)) l) = none

theorem KeyValueList.orderedInsert {α : Type} [LinearOrder α] {β : Type u_1} [DecidableEq β] (l : List (α × β)) (h : KeyValueList l) (a : α) (b : β) (hp : List.find? (fun (x : α × β) => decide (x.1 = a)) l = none) : KeyValueList (List.orderedInsert LEByKey (a, b) l)

theorem KeyValueList.addKV {α : Type} [LinearOrder α] {β : Type u_1} [DecidableEq β] [Add β] (l : List (α × β)) (h : KeyValueList l) (a : α) (b : β) : KeyValueList (l.addKV a b)

theorem KeyValueList.eraseP_eq_filter {α : Type} [LinearOrder α] {β : Type u_1} {l : List (α × β)} (hl : KeyValueList l) (a : α) : List.eraseP (fun (x : α × β) => decide (x.1 = a)) l = List.filter (fun (x : α × β) => decide (x.1 ≠ a)) l

theorem KeyValueList.addKV_spec_not_key {α : Type} [LinearOrder α] {β : Type u_1} [DecidableEq β] [Add β] (l : List (α × β)) (hl : KeyValueList l) (a : α) (b : β) (x : α × β) : x.1 ≠ a → (x ∈ l.addKV a b ↔ x ∈ l)

theorem KeyValueList.addKV_spec_key_not_before {α : Type} [LinearOrder α] {β : Type u_1} [DecidableEq β] [Add β] (l : List (α × β)) (hl : KeyValueList l) (a : α) (b : β) (x : α × β) : x.1 = a → (¬∃ (z : β), (a, z) ∈ l) → (x ∈ l.addKV a b ↔ x = (a, b))

theorem KeyValueList.addKV_spec_key_before {α : Type} [LinearOrder α] {β : Type u_1} [DecidableEq β] [Add β] (l : List (α × β)) (hl : KeyValueList l) (a : α) (b : β) (x : α × β) : x.1 = a → ∀ (z : β), (a, z) ∈ l → (x ∈ l.addKV a b ↔ x = (a, b + z))

theorem KeyValueList.addKV_spec {α : Type} [LinearOrder α] {β : Type u_1} [DecidableEq β] [Add β] (l : List (α × β)) (hl : KeyValueList l) (a : α) (b : β) (x : α × β) : x ∈ l.addKV a b ↔ x.1 ≠ a ∧ x ∈ l ∨ x.1 = a ∧ ((¬∃ (z : β), (a, z) ∈ l) ∧ x = (a, b) ∨ ∃ (z : β), (a, z) ∈ l ∧ x = (a, b + z))

theorem KeyValueList.addKV_mem {α : Type} [LinearOrder α] {β : Type u_1} [DecidableEq β] [Add β] (l : List (α × β)) (h : KeyValueList l) (a : α) (b : β) : ∃ (b' : β), (a, b') ∈ l.addKV a b

def KeyValueList.addKVFold {α : Type} [LinearOrder α] {β : Type u_1} [DecidableEq β] [Add β] (ab : α × β) (l : { l : List (α × β) // KeyValueList l }) : { l : List (α × β) // KeyValueList l }

Equations

• KeyValueList.addKVFold ab l = ⟨(↑l).addKV ab.1 ab.2, ⋯⟩

theorem KeyValueList.add_comm_internal {α : Type} [LinearOrder α] {β : Type u_1} [DecidableEq β] [AddCommSemigroup β] (l : List (α × β)) (hl : KeyValueList l) (a₁ a₂ a : α) (b₁ b₂ b : β) : (a, b) ∈ (l.addKV a₂ b₂).addKV a₁ b₁ → (a, b) ∈ (l.addKV a₁ b₁).addKV a₂ b₂

instance instLeftCommutativeProdSubtypeListKeyValueListAddKVFold {α : Type} [LinearOrder α] {β : Type u_1} [DecidableEq β] [AddCommSemigroup β] : LeftCommutative KeyValueList.addKVFold