Binary Search Trees
If the type of keys can be totally ordered -- that is, it supports a well-behaved ≤
comparison --
then maps can be implemented with binary search trees (BSTs). Insert and lookup operations on BSTs take time
proportional to the height of the tree. If the tree is balanced, the operations therefore take logarithmic time.
This example is based on a similar example found in the "Software Foundations" book (volume 3).
We use Nat
as the key type in our implementation of BSTs,
since it has a convenient total order with lots of theorems and automation available.
We leave as an exercise to the reader the generalization to arbitrary types.
inductive Tree: Type v → Type v
Tree (β: Type v
β : Type v: Type (v + 1)
Type v) where
| leaf: {β : Type v} → Tree β
leaf
| node: {β : Type v} → Tree β → Nat → β → Tree β → Tree β
node (left: Tree β
left : Tree: Type v → Type v
Tree β: Type v
β) (key: Nat
key : Nat: Type
Nat) (value: β
value : β: Type v
β) (right: Tree β
right : Tree: Type v → Type v
Tree β: Type v
β)
deriving Repr: Type u → Type u
Repr
The function contains
returns true
iff the given tree contains the key k
.
defTree.contains (Tree.contains: {β : Type u_1} → Tree β → Nat → Boolt :t: Tree βTreeTree: Type u_1 → Type u_1β) (β: Type u_1k :k: NatNat) :Nat: TypeBool := matchBool: Typet with |t: Tree βleaf =>leaf: {β : Type ?u.1346} → Tree βfalse |false: Boolnodenode: {β : Type ?u.1355} → Tree β → Nat → β → Tree β → Tree βleftleft: Tree βkeykey: Natright => ifright: Tree βk <k: Natkey thenkey: Natleft.left: Tree βcontainscontains: {β : Type u_1} → Tree β → Nat → Boolk else ifk: Natkey <key: Natk thenk: Natright.right: Tree βcontainscontains: {β : Type u_1} → Tree β → Nat → Boolk elsek: Nattruetrue: Bool
t.find? k
returns some v
if v
is the value bound to key k
in the tree t
. It returns none
otherwise.
def Tree.find?: {β : Type u_1} → Tree β → Nat → Option β
Tree.find? (t: Tree β
t : Tree: Type u_1 → Type u_1
Tree β: Type u_1
β) (k: Nat
k : Nat: Type
Nat) : Option: Type u_1 → Type u_1
Option β: Type u_1
β :=
match t: Tree β
t with
| leaf: {β : Type ?u.1645} → Tree β
leaf => none: {α : Type u_1} → Option α
none
| node: {β : Type ?u.1657} → Tree β → Nat → β → Tree β → Tree β
node left: Tree β
left key: Nat
key value: β
value right: Tree β
right =>
if k: Nat
k < key: Nat
key then
left: Tree β
left.find?: {β : Type u_1} → Tree β → Nat → Option β
find? k: Nat
k
else if key: Nat
key < k: Nat
k then
right: Tree β
right.find?: {β : Type u_1} → Tree β → Nat → Option β
find? k: Nat
k
else
some: {α : Type u_1} → α → Option α
some value: β
value
t.insert k v
is the map containing all the bindings of t
along with a binding of k
to v
.
def Tree.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
Tree.insert (t: Tree β
t : Tree: Type u_1 → Type u_1
Tree β: Type u_1
β) (k: Nat
k : Nat: Type
Nat) (v: β
v : β: Type u_1
β) : Tree: Type u_1 → Type u_1
Tree β: Type u_1
β :=
match t: Tree β
t with
| leaf: {β : Type ?u.1952} → Tree β
leaf => node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node leaf: {β : Type u_1} → Tree β
leaf k: Nat
k v: β
v leaf: {β : Type u_1} → Tree β
leaf
| node: {β : Type ?u.1967} → Tree β → Nat → β → Tree β → Tree β
node left: Tree β
left key: Nat
key value: β
value right: Tree β
right =>
if k: Nat
k < key: Nat
key then
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node (left: Tree β
left.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert k: Nat
k v: β
v) key: Nat
key value: β
value right: Tree β
right
else if key: Nat
key < k: Nat
k then
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node left: Tree β
left key: Nat
key value: β
value (right: Tree β
right.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert k: Nat
k v: β
v)
else
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node left: Tree β
left k: Nat
k v: β
v right: Tree β
right
Let's add a new operation to our tree: converting it to an association list that contains the key--value bindings from the tree stored as pairs. If that list is sorted by the keys, then any two trees that represent the same map would be converted to the same list. Here's a function that does so with an in-order traversal of the tree.
defTree.toList (Tree.toList: {β : Type u_1} → Tree β → List (Nat × β)t :t: Tree βTreeTree: Type u_1 → Type u_1β) :β: Type u_1List (List: Type u_1 → Type u_1Nat ×Nat: Typeβ) := matchβ: Type u_1t with |t: Tree βleaf =>leaf: {β : Type ?u.2284} → Tree β[] |[]: List (Nat × β)nodenode: {β : Type ?u.2296} → Tree β → Nat → β → Tree β → Tree βll: Tree βkk: Natvv: βr =>r: Tree βl.l: Tree βtoList ++ [(toList: {β : Type u_1} → Tree β → List (Nat × β)k,k: Natv)] ++v: βr.r: Tree βtoListtoList: {β : Type u_1} → Tree β → List (Nat × β)Tree.leaf.Tree.leaf: {β : Type} → Tree βinsertinsert: {β : Type} → Tree β → Nat → β → Tree β22: Nat"two" |>."two": Stringinsertinsert: {β : Type} → Tree β → Nat → β → Tree β33: Nat"three" |>."three": Stringinsertinsert: {β : Type} → Tree β → Nat → β → Tree β11: Nat"one""one": StringTree.leaf.Tree.leaf: {β : Type} → Tree βinsertinsert: {β : Type} → Tree β → Nat → β → Tree β22: Nat"two" |>."two": Stringinsertinsert: {β : Type} → Tree β → Nat → β → Tree β33: Nat"three" |>."three": Stringinsertinsert: {β : Type} → Tree β → Nat → β → Tree β11: Nat"one" |>."one": StringtoListtoList: {β : Type} → Tree β → List (Nat × β)
The implementation of Tree.toList
is inefficient because of how it uses the ++
operator.
On a balanced tree its running time is linearithmic, because it does a linear number of
concatenations at each level of the tree. On an unbalanced tree it's quadratic time.
Here's a tail-recursive implementation than runs in linear time, regardless of whether the tree is balanced:
def Tree.toListTR: {β : Type u_1} → Tree β → List (Nat × β)
Tree.toListTR (t: Tree β
t : Tree: Type u_1 → Type u_1
Tree β: Type u_1
β) : List: Type u_1 → Type u_1
List (Nat: Type
Nat × β: Type u_1
β) :=
go: Tree β → List (Nat × β) → List (Nat × β)
go t: Tree β
t []: List (Nat × β)
[]
where
go: {β : Type u_1} → Tree β → List (Nat × β) → List (Nat × β)
go (t: Tree β
t : Tree: Type u_1 → Type u_1
Tree β: Type u_1
β) (acc: List (Nat × β)
acc : List: Type u_1 → Type u_1
List (Nat: Type
Nat × β: Type u_1
β)) : List: Type u_1 → Type u_1
List (Nat: Type
Nat × β: Type u_1
β) :=
match t: Tree β
t with
| leaf: {β : Type ?u.3149} → Tree β
leaf => acc: List (Nat × β)
acc
| node: {β : Type ?u.3159} → Tree β → Nat → β → Tree β → Tree β
node l: Tree β
l k: Nat
k v: β
v r: Tree β
r => go: Tree β → List (Nat × β) → List (Nat × β)
go l: Tree β
l ((k: Nat
k, v: β
v) :: go: Tree β → List (Nat × β) → List (Nat × β)
go r: Tree β
r acc: List (Nat × β)
acc)
We now prove that t.toList
and t.toListTR
return the same list.
The proof is on induction, and as we used the auxiliary function go
to define Tree.toListTR
, we use the auxiliary theorem go
to prove the theorem.
The proof of the auxiliary theorem is by induction on t
.
The generalizing acc
modifier instructs Lean to revert acc
, apply the
induction theorem for Tree
s, and then reintroduce acc
in each case.
By using generalizing
, we obtain the more general induction hypotheses
-
left_ih : ∀ acc, toListTR.go left acc = toList left ++ acc
-
right_ih : ∀ acc, toListTR.go right acc = toList right ++ acc
Recall that the combinator tac <;> tac'
runs tac
on the main goal and tac'
on each produced goal,
concatenating all goals produced by tac'
. In this theorem, we use it to apply
simp
and close each subgoal produced by the induction
tactic.
The simp
parameters toListTR.go
and toList
instruct the simplifier to try to reduce
and/or apply auto generated equation theorems for these two functions.
The parameter *
instructs the simplifier to use any equation in a goal as rewriting rules.
In this particular case, simp
uses the induction hypotheses as rewriting rules.
Finally, the parameter List.append_assoc
instructs the simplifier to use the
List.append_assoc
theorem as a rewriting rule.
theoremTree.toList_eq_toListTR (Tree.toList_eq_toListTR: ∀ {β : Type u_1} (t : Tree β), t.toList = t.toListTRt :t: Tree βTreeTree: Type u_1 → Type u_1β) :β: Type u_1t.t: Tree βtoList =toList: {β : Type u_1} → Tree β → List (Nat × β)t.t: Tree βtoListTR :=toListTR: {β : Type u_1} → Tree β → List (Nat × β)Goals accomplished! 🐙whereGoals accomplished! 🐙go (go: ∀ {β : Type u_1} (t : Tree β) (acc : List (Nat × β)), toListTR.go t acc = t.toList ++ acct :t: Tree βTreeTree: Type u_1 → Type u_1β) (β: Type u_1acc :acc: List (Nat × β)List (List: Type u_1 → Type u_1Nat ×Nat: Typeβ)) :β: Type u_1toListTR.gotoListTR.go: {β : Type u_1} → Tree β → List (Nat × β) → List (Nat × β)tt: Tree βacc =acc: List (Nat × β)t.t: Tree βtoList ++toList: {β : Type u_1} → Tree β → List (Nat × β)acc :=acc: List (Nat × β)Goals accomplished! 🐙β: Type u_1
t: Tree β
acc: List (Nat × β)
leaftoListTR.go leaf acc = leaf.toList ++ accβ: Type u_1
t, left✝: Tree β
key✝: Nat
value✝: β
right✝: Tree β
left_ih✝: ∀ (acc : List (Nat × β)), toListTR.go left✝ acc = left✝.toList ++ acc
right_ih✝: ∀ (acc : List (Nat × β)), toListTR.go right✝ acc = right✝.toList ++ acc
acc: List (Nat × β)toListTR.go (left✝.node key✝ value✝ right✝) acc = (left✝.node key✝ value✝ right✝).toList ++ accβ: Type u_1
t: Tree β
acc: List (Nat × β)
leaftoListTR.go leaf acc = leaf.toList ++ accβ: Type u_1
t, left✝: Tree β
key✝: Nat
value✝: β
right✝: Tree β
left_ih✝: ∀ (acc : List (Nat × β)), toListTR.go left✝ acc = left✝.toList ++ acc
right_ih✝: ∀ (acc : List (Nat × β)), toListTR.go right✝ acc = right✝.toList ++ acc
acc: List (Nat × β)toListTR.go (left✝.node key✝ value✝ right✝) acc = (left✝.node key✝ value✝ right✝).toList ++ accGoals accomplished! 🐙
The [csimp]
annotation instructs the Lean code generator to replace
any Tree.toList
with Tree.toListTR
when generating code.
@[csimp] theoremTree.toList_eq_toListTR_csimp : @Tree.toList_eq_toListTR_csimp: @toList = @toListTRTree.toList = @Tree.toList: {β : Type u_1} → Tree β → List (Nat × β)Tree.toListTR :=Tree.toListTR: {β : Type u_1} → Tree β → List (Nat × β)Goals accomplished! 🐙β: Type u_1
t: Tree β
h.ht.toList = t.toListTRGoals accomplished! 🐙
The implementations of Tree.find?
and Tree.insert
assume that values of type tree obey the BST invariant:
for any non-empty node with key k
, all the values of the left
subtree are less than k
and all the values
of the right subtree are greater than k
. But that invariant is not part of the definition of tree.
So, let's formalize the BST invariant. Here's one way to do so. First, we define a helper ForallTree
to express that idea that a predicate holds at every node of a tree:
inductive ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree (p: Nat → β → Prop
p : Nat: Type
Nat → β: Type u_1
β → Prop: Type
Prop) : Tree: Type u_1 → Type u_1
Tree β: Type u_1
β → Prop: Type
Prop
| leaf: ∀ {β : Type u_1} {p : Nat → β → Prop}, ForallTree p Tree.leaf
leaf : ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree p: Nat → β → Prop
p .leaf: {β : Type u_1} → Tree β
.leaf
| node: ∀ {β : Type u_1} {p : Nat → β → Prop} {left : Tree β} {key : Nat} {value : β} {right : Tree β},
ForallTree p left → p key value → ForallTree p right → ForallTree p (left.node key value right)
node :
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree p: Nat → β → Prop
p left: Tree β
left →
p: Nat → β → Prop
p key: Nat
key value: β
value →
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree p: Nat → β → Prop
p right: Tree β
right →
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree p: Nat → β → Prop
p (.node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
.node left: Tree β
left key: Nat
key value: β
value right: Tree β
right)
Second, we define the BST invariant: An empty tree is a BST. A non-empty tree is a BST if all its left nodes have a lesser key, its right nodes have a greater key, and the left and right subtrees are themselves BSTs.
inductiveBST :BST: {β : Type u_1} → Tree β → PropTreeTree: Type u_1 → Type u_1β →β: Type u_1Prop |Prop: Typeleaf :leaf: ∀ {β : Type u_1}, BST Tree.leafBSTBST: {β : Type u_1} → Tree β → Prop.leaf |.leaf: {β : Type u_1} → Tree βnode :node: ∀ {β : Type u_1} {key : Nat} {left right : Tree β} {value : β}, ForallTree (fun k v => k < key) left → ForallTree (fun k v => key < k) right → BST left → BST right → BST (left.node key value right)ForallTree (funForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Propkk: Nat=>k <k: Natkey)key: Natleft →left: Tree ?m.4935ForallTree (funForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Propkk: Nat=>key <key: Natk)k: Natright →right: Tree ?m.4935BSTBST: {β : Type u_1} → Tree β → Propleft →left: Tree ?m.4935BSTBST: {β : Type u_1} → Tree β → Propright →right: Tree ?m.4935BST (BST: {β : Type u_1} → Tree β → Prop.node.node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree βleftleft: Tree ?m.4935keykey: Natvaluevalue: ?m.4935right)right: Tree ?m.4935
We can use the macro
command to create helper tactics for organizing our proofs.
The macro have_eq x y
tries to prove x = y
using linear arithmetic, and then
immediately uses the new equality to substitute x
with y
everywhere in the goal.
The modifier local
specifies the scope of the macro.
/-- The `have_eq lhs rhs` tactic (tries to) prove that `lhs = rhs`,
and then replaces `lhs` with `rhs`. -/
local macro "have_eq " lhs: Lean.TSyntax `term
lhs:term: Lean.Parser.Category
term:max rhs: Lean.TSyntax `term
rhs:term: Lean.Parser.Category
term:max : tactic: Lean.Parser.Category
tactic =>
`(tactic|
(have h : $lhs: Lean.TSyntax `term
lhs = $rhs: Lean.TSyntax `term
rhs :=
-- TODO: replace with linarith
by simp_arith at *; apply Nat.le_antisymm <;> assumption
try subst $lhs: Lean.TSyntax `term
lhs))
The by_cases' e
is just the regular by_cases
followed by simp
using all
hypotheses in the current goal as rewriting rules.
Recall that the by_cases
tactic creates two goals. One where we have h : e
and
another one containing h : ¬ e
. The simplifier uses the h
to rewrite e
to True
in the first subgoal, and e
to False
in the second. This is particularly
useful if e
is the condition of an if
-statement.
/-- `by_cases' e` is a shorthand form `by_cases e <;> simp[*]` -/
local macro "by_cases' " e: Lean.TSyntax `term
e:term: Lean.Parser.Category
term : tactic: Lean.Parser.Category
tactic =>
`(tactic| by_cases $e: Lean.TSyntax `term
e <;> simp [*])
We can use the attribute [simp]
to instruct the simplifier to reduce given definitions or
apply rewrite theorems. The local
modifier limits the scope of this modification to this file.
attribute [local simp] Tree.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
Tree.insert
We now prove that Tree.insert
preserves the BST invariant using induction and case analysis.
Recall that the tactic . tac
focuses on the main goal and tries to solve it using tac
, or else fails.
It is used to structure proofs in Lean.
The notation ‹e›
is just syntax sugar for (by assumption : e)
. That is, it tries to find a hypothesis h : e
.
It is useful to access hypothesis that have auto generated names (aka "inaccessible") names.
theoremTree.forall_insert_of_forall (Tree.forall_insert_of_forall: ∀ {β : Type u_1} {p : Nat → β → Prop} {t : Tree β} {key : Nat} {value : β}, ForallTree p t → p key value → ForallTree p (t.insert key value)h₁ :h₁: ForallTree p tForallTreeForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Proppp: Nat → ?m.6678 → Propt) (t: Tree ?m.6678h₂ :h₂: p key valuepp: Nat → ?m.6678 → Propkeykey: Natvalue) :value: ?m.6678ForallTreeForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Propp (p: Nat → ?m.6678 → Propt.t: Tree ?m.6678insertinsert: {β : Type u_1} → Tree β → Nat → β → Tree βkeykey: Natvalue) :=value: ?m.6678Goals accomplished! 🐙β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₁: ForallTree p t
h₂: p key valueForallTree p (t.insert key value)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
leafForallTree p (leaf.insert key value)Goals accomplished! 🐙β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
key✝: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p key✝ value✝
hr: ForallTree p right✝
ihl: ForallTree p (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
nodeForallTree p ((left✝.node key✝ value✝ right✝).insert key value)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
nodeForallTree p ((left✝.node k value✝ right✝).insert key value)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝: key < k
posForallTree p ((left✝.insert key value).node k value✝ right✝)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝: ¬key < kForallTree p (if k < key then left✝.node k value✝ (right✝.insert key value) else left✝.node key value right✝)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝: key < k
posForallTree p ((left✝.insert key value).node k value✝ right✝)Goals accomplished! 🐙β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝: ¬key < k
negForallTree p (if k < key then left✝.node k value✝ (right✝.insert key value) else left✝.node key value right✝)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝¹: ¬key < k
h✝: k < key
posForallTree p (left✝.node k value✝ (right✝.insert key value))β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝¹: ¬key < k
h✝: ¬k < keyForallTree p (left✝.node key value right✝)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝¹: ¬key < k
h✝: k < key
posForallTree p (left✝.node k value✝ (right✝.insert key value))Goals accomplished! 🐙β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝¹: ¬key < k
h✝: ¬k < key
negForallTree p (left✝.node key value right✝)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
value: β✝
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
h₂: p k value
ihl: ForallTree p (left✝.insert k value)
ihr: ForallTree p (right✝.insert k value)
h✝¹, h✝: ¬k < k
negForallTree p (left✝.node k value right✝)theoremGoals accomplished! 🐙Tree.bst_insert_of_bst {Tree.bst_insert_of_bst: ∀ {β : Type u_1} {t : Tree β}, BST t → ∀ (key : Nat) (value : β), BST (t.insert key value)t :t: Tree βTreeTree: Type u_1 → Type u_1β} (β: Type u_1h :h: BST tBSTBST: {β : Type u_1} → Tree β → Propt) (t: Tree βkey :key: NatNat) (Nat: Typevalue :value: ββ) :β: Type u_1BST (BST: {β : Type u_1} → Tree β → Propt.t: Tree βinsertinsert: {β : Type u_1} → Tree β → Nat → β → Tree βkeykey: Natvalue) :=value: βGoals accomplished! 🐙β: Type u_1
t: Tree β
h: BST t
key: Nat
value: βBST (t.insert key value)β: Type u_1
t: Tree β
key: Nat
value: β
leafBST (leaf.insert key value)Goals accomplished! 🐙β: Type u_1
t: Tree β
key: Nat
value: β
key✝: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k v => k < key✝) left✝
h₂: ForallTree (fun k v => key✝ < k) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (left✝.insert key value)
ih₂: BST (right✝.insert key value)
nodeBST ((left✝.node key✝ value✝ right✝).insert key value)β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (left✝.insert key value)
ih₂: BST (right✝.insert key value)
nodeBST ((left✝.node k value✝ right✝).insert key value)β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (left✝.insert key value)
ih₂: BST (right✝.insert key value)
nodeBST (if key < k then (left✝.insert key value).node k value✝ right✝ else if k < key then left✝.node k value✝ (right✝.insert key value) else left✝.node key value right✝)β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝: key < k
posBST ((left✝.insert key value).node k value✝ right✝)β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝: ¬key < kBST (if k < key then left✝.node k value✝ (right✝.insert key value) else left✝.node key value right✝)β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝: key < k
posBST ((left✝.insert key value).node k value✝ right✝)Goals accomplished! 🐙β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝: ¬key < k
negBST (if k < key then left✝.node k value✝ (right✝.insert key value) else left✝.node key value right✝)β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝¹: ¬key < k
h✝: k < key
posBST (left✝.node k value✝ (right✝.insert key value))β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝¹: ¬key < k
h✝: ¬k < keyBST (left✝.node key value right✝)β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝¹: ¬key < k
h✝: k < key
posBST (left✝.node k value✝ (right✝.insert key value))Goals accomplished! 🐙β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝¹: ¬key < k
h✝: ¬k < key
negBST (left✝.node key value right✝)β: Type u_1
t: Tree β
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (left✝.insert k value)
ih₂: BST (right✝.insert k value)
h✝¹, h✝: ¬k < k
negBST (left✝.node k value right✝)Goals accomplished! 🐙
Now, we define the type BinTree
using a Subtype
that states that only trees satisfying the BST invariant are BinTree
s.
def BinTree: Type u → Type u
BinTree (β: Type u
β : Type u: Type (u + 1)
Type u) := { t: Tree β
t : Tree: Type u → Type u
Tree β: Type u
β // BST: {β : Type u} → Tree β → Prop
BST t: Tree β
t }
def BinTree.mk: {β : Type u_1} → BinTree β
BinTree.mk : BinTree: Type u_1 → Type u_1
BinTree β: Type u_1
β :=
⟨.leaf: {β : Type u_1} → Tree β
.leaf, .leaf: ∀ {β : Type u_1}, BST Tree.leaf
.leaf⟩
def BinTree.contains: {β : Type u_1} → BinTree β → Nat → Bool
BinTree.contains (b: BinTree β
b : BinTree: Type u_1 → Type u_1
BinTree β: Type u_1
β) (k: Nat
k : Nat: Type
Nat) : Bool: Type
Bool :=
b: BinTree β
b.val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
val.contains: {β : Type u_1} → Tree β → Nat → Bool
contains k: Nat
k
def BinTree.find?: {β : Type u_1} → BinTree β → Nat → Option β
BinTree.find? (b: BinTree β
b : BinTree: Type u_1 → Type u_1
BinTree β: Type u_1
β) (k: Nat
k : Nat: Type
Nat) : Option: Type u_1 → Type u_1
Option β: Type u_1
β :=
b: BinTree β
b.val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
val.find?: {β : Type u_1} → Tree β → Nat → Option β
find? k: Nat
k
def BinTree.insert: {β : Type u_1} → BinTree β → Nat → β → BinTree β
BinTree.insert (b: BinTree β
b : BinTree: Type u_1 → Type u_1
BinTree β: Type u_1
β) (k: Nat
k : Nat: Type
Nat) (v: β
v : β: Type u_1
β) : BinTree: Type u_1 → Type u_1
BinTree β: Type u_1
β :=
⟨b: BinTree β
b.val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
val.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert k: Nat
k v: β
v, b: BinTree β
b.val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
val.bst_insert_of_bst: ∀ {β : Type u_1} {t : Tree β}, BST t → ∀ (key : Nat) (value : β), BST (t.insert key value)
bst_insert_of_bst b: BinTree β
b.property: ∀ {α : Type u_1} {p : α → Prop} (self : Subtype p), p self.val
property k: Nat
k v: β
v⟩
Finally, we prove that BinTree.find?
and BinTree.insert
satisfy the map properties.
attribute [local simp]BinTree.mkBinTree.mk: {β : Type u_1} → BinTree βBinTree.containsBinTree.contains: {β : Type u_1} → BinTree β → Nat → BoolBinTree.find?BinTree.find?: {β : Type u_1} → BinTree β → Nat → Option βBinTree.insertBinTree.insert: {β : Type u_1} → BinTree β → Nat → β → BinTree βTree.find?Tree.find?: {β : Type u_1} → Tree β → Nat → Option βTree.containsTree.contains: {β : Type u_1} → Tree β → Nat → BoolTree.insert theoremTree.insert: {β : Type u_1} → Tree β → Nat → β → Tree βBinTree.find_mk (BinTree.find_mk: ∀ {β : Type u_1} (k : Nat), mk.find? k = nonek :k: NatNat) :Nat: TypeBinTree.mk.BinTree.mk: {β : Type u_1} → BinTree βfind?find?: {β : Type u_1} → BinTree β → Nat → Option βk = (k: Natnone :none: {α : Type u_1} → Option αOptionOption: Type u_1 → Type u_1β) :=β: Type u_1Goals accomplished! 🐙theoremGoals accomplished! 🐙BinTree.find_insert (BinTree.find_insert: ∀ {β : Type u_1} (b : BinTree β) (k : Nat) (v : β), (b.insert k v).find? k = some vb :b: BinTree βBinTreeBinTree: Type u_1 → Type u_1β) (β: Type u_1k :k: NatNat) (Nat: Typev :v: ββ) : (β: Type u_1b.b: BinTree βinsertinsert: {β : Type u_1} → BinTree β → Nat → β → BinTree βkk: Natv).v: βfind?find?: {β : Type u_1} → BinTree β → Nat → Option βk =k: Natsomesome: {α : Type u_1} → α → Option αv :=v: βGoals accomplished! 🐙;β: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST t(insert ⟨t, h⟩ k v).find? k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST t(t.insert k v).find? k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST t(t.insert k v).find? k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h: BST (left.node key value right)
node(if k < key then (left.insert k v).node key value right else if key < k then left.node key value (right.insert k v) else left.node k v right).find? k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h: BST (left.node key value right)
node(if k < key then (left.insert k v).node key value right else if key < k then left.node key value (right.insert k v) else left.node k v right).find? k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h: BST (left.node key value right)
h✝: k < key
pos(left.insert k v).find? k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h: BST (left.node key value right)
h✝: ¬k < key(if key < k then left.node key value (right.insert k v) else left.node k v right).find? k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h: BST (left.node key value right)
h✝: k < key
pos(left.insert k v).find? k = some v;β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h✝: k < key
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right
pos.node(left.insert k v).find? k = some v;β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h✝: k < key
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right
pos.nodeBST leftGoals accomplished! 🐙β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h: BST (left.node key value right)
h✝: ¬k < key
neg(if key < k then left.node key value (right.insert k v) else left.node k v right).find? k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h: BST (left.node key value right)
h✝¹: ¬k < key
h✝: key < k
pos(right.insert k v).find? k = some v;β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h✝¹: ¬k < key
h✝: key < k
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right
pos.node(right.insert k v).find? k = some v;β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h✝¹: ¬k < key
h✝: key < k
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right
pos.nodeBST righttheoremGoals accomplished! 🐙BinTree.find_insert_of_ne (BinTree.find_insert_of_ne: ∀ {β : Type u_1} {k k' : Nat} (b : BinTree β), k ≠ k' → ∀ (v : β), (b.insert k v).find? k' = b.find? k'b :b: BinTree βBinTreeBinTree: Type u_1 → Type u_1β) (β: Type u_1ne :ne: k ≠ k'k ≠k: Natk') (k': Natv :v: ββ) : (β: Type u_1b.b: BinTree βinsertinsert: {β : Type u_1} → BinTree β → Nat → β → BinTree βkk: Natv).v: βfind?find?: {β : Type u_1} → BinTree β → Nat → Option βk' =k': Natb.b: BinTree βfind?find?: {β : Type u_1} → BinTree β → Nat → Option βk' :=k': NatGoals accomplished! 🐙;β: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
t: Tree β
h: BST t(insert ⟨t, h⟩ k v).find? k' = find? ⟨t, h⟩ k'β: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
t: Tree β
h: BST t(t.insert k v).find? k' = t.find? k'β: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
t: Tree β
h: BST t(t.insert k v).find? k' = t.find? k'β: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k' = left.find? k'
ihr: BST right → (right.insert k v).find? k' = right.find? k'
h: BST (left.node key value right)
node(if k < key then (left.insert k v).node key value right else if key < k then left.node key value (right.insert k v) else left.node k v right).find? k' = if k' < key then left.find? k' else if key < k' then right.find? k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
h: BST Tree.leaf
leafk ≤ k' → k < k'β: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
h: BST Tree.leaf
le: k ≤ k'
leafk < k'Goals accomplished! 🐙β: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k' = left.find? k'
ihr: BST right → (right.insert k v).find? k' = right.find? k'
h: BST (left.node key value right)
node(if k < key then (left.insert k v).node key value right else if key < k then left.node key value (right.insert k v) else left.node k v right).find? k' = if k' < key then left.find? k' else if key < k' then right.find? k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k' = left.find? k'
ihr: BST right → (right.insert k v).find? k' = right.find? k'
h: BST (left.node key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
node(if k < key then (left.insert k v).node key value right else if key < k then left.node key value (right.insert k v) else left.node k v right).find? k' = if k' < key then left.find? k' else if key < k' then right.find? k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihr: BST right → (right.insert k v).find? k' = right.find? k'
h: BST (left.node key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
ihl: (left.insert k v).find? k' = left.find? k'
node(if k < key then (left.insert k v).node key value right else if key < k then left.node key value (right.insert k v) else left.node k v right).find? k' = if k' < key then left.find? k' else if key < k' then right.find? k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (left.node key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
ihl: (left.insert k v).find? k' = left.find? k'
ihr: (right.insert k v).find? k' = right.find? k'
node(if k < key then (left.insert k v).node key value right else if key < k then left.node key value (right.insert k v) else left.node k v right).find? k' = if k' < key then left.find? k' else if key < k' then right.find? k' else some value;β: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (left.node key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
ihl: (left.insert k v).find? k' = left.find? k'
ihr: (right.insert k v).find? k' = right.find? k'
h✝: ¬k < key
neg(if key < k then left.node key value (right.insert k v) else left.node k v right).find? k' = if k' < key then left.find? k' else if key < k' then right.find? k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (left.node key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
ihl: (left.insert k v).find? k' = left.find? k'
ihr: (right.insert k v).find? k' = right.find? k'
h✝¹: ¬k < key
h✝: ¬key < k
neg(if k' < k then left.find? k' else if k < k' then right.find? k' else some v) = if k' < key then left.find? k' else if key < k' then right.find? k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ihl: (left.insert k v).find? k' = left.find? k'
ihr: (right.insert k v).find? k' = right.find? k'
h: BST (left.node k value right)
hl: ForallTree (fun k_1 v => k_1 < k) left
hr: ForallTree (fun k_1 v => k < k_1) right
h✝¹, h✝: ¬k < k
neg(if k' < k then left.find? k' else if k < k' then right.find? k' else some v) = if k' < k then left.find? k' else if k < k' then right.find? k' else some value;β: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ihl: (left.insert k v).find? k' = left.find? k'
ihr: (right.insert k v).find? k' = right.find? k'
h: BST (left.node k value right)
hl: ForallTree (fun k_1 v => k_1 < k) left
hr: ForallTree (fun k_1 v => k < k_1) right
h✝², h✝¹: ¬k < k
h✝: ¬k' < k
neg(if k < k' then right.find? k' else some v) = if k < k' then right.find? k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ihl: (left.insert k v).find? k' = left.find? k'
ihr: (right.insert k v).find? k' = right.find? k'
h: BST (left.node k value right)
hl: ForallTree (fun k_1 v => k_1 < k) left
hr: ForallTree (fun k_1 v => k < k_1) right
h✝³, h✝²: ¬k < k
h✝¹: ¬k' < k
h✝: ¬k < k'
negv = valueβ: Type u_1
k': Nat
b: BinTree β
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ne: k' ≠ k'
ihl: (left.insert k' v).find? k' = left.find? k'
ihr: (right.insert k' v).find? k' = right.find? k'
h: BST (left.node k' value right)
hl: ForallTree (fun k v => k < k') left
hr: ForallTree (fun k v => k' < k) right
h✝³, h✝², h✝¹, h✝: ¬k' < k'
negv = valueGoals accomplished! 🐙