Update on Ackerman left inverse

GraphAlgorithms/DataStructures/BinaryTree.lean

@@ -73,22 +73,85 @@ because a binary tree could have q >/< key while being in
 the left/right subtree of key respectively.
 If `contains t q` is true, then `q` is in `t`; but
 the converse need not necessarily hold true. The
-converse is true for a binary search tree.
+converse is true for a binary search tree. Hence the name of it.
 -/
-def contains [LinearOrder α] (t : Tree α) (q : α) : Prop :=
+def BST_contains [LinearOrder α] (t : Tree α) (q : α) : Prop :=
   match t with
   | nil => False
   | l △[key] r =>
     if q < key then
-      l.contains q
+      l.BST_contains q
     else if key < q then
-      r.contains q
+      r.BST_contains q
     else
       True
 
 end CoreDefs
 
 
+/-! ### Membership -/
+section Membership
+
+/-- Inductive membership relation on binary trees, modelled on `List.Mem`. -/
+inductive Mem (a : α) : Tree α → Prop where
+  /-- `a` is the key at the root. -/
+  | here  {l r : Tree α} : Mem a (l △[a] r)
+  /-- `a` lies in the left subtree. -/
+  | left  {k : α} {l r : Tree α} : Mem a l → Mem a (l △[k] r)
+  /-- `a` lies in the right subtree. -/
+  | right {k : α} {l r : Tree α} : Mem a r → Mem a (l △[k] r)
+
+instance : Membership α (Tree α) := ⟨fun t a => Mem a t⟩
+
+@[simp] lemma not_mem_nil (a : α) : a ∉ (nil : Tree α) := nofun
+
+@[simp] lemma mem_node_iff {a k : α} {l r : Tree α} :
+    a ∈ (l △[k] r) ↔ a = k ∨ a ∈ l ∨ a ∈ r := by
+  refine ⟨fun h => ?_, fun h => ?_⟩
+  · cases h with
+    | here    => exact Or.inl rfl
+    | left h  => exact Or.inr (Or.inl h)
+    | right h => exact Or.inr (Or.inr h)
+  · rcases h with rfl | h | h
+    · exact .here
+    · exact .left h
+    · exact .right h
+
+/-- Membership agrees with membership in the in-order key list. -/
+theorem mem_iff_mem_toKeyList {a : α} {t : Tree α} :
+    a ∈ t ↔ a ∈ t.toKeyList := by
+  induction t with
+  | nil => simp
+  | node k l r ihl ihr =>
+    rw [toKeyList_node, mem_node_iff]
+    simp only [List.mem_append, List.mem_singleton, ihl, ihr]
+    tauto
+
+instance decidableMem [DecidableEq α] (a : α) : ∀ t : Tree α, Decidable (a ∈ t)
+  | .nil       => isFalse nofun
+  | l △[k] r =>
+    haveI : Decidable (a ∈ l) := decidableMem a l
+    haveI : Decidable (a ∈ r) := decidableMem a r
+    decidable_of_iff (a = k ∨ a ∈ l ∨ a ∈ r) mem_node_iff.symm
+
+/-- The search-path `contains` implies membership. The converse needs the BST
+invariant. -/
+theorem contains_imp_mem [LinearOrder α] {t : Tree α} {q : α} :
+    t.BST_contains q → q ∈ t := by
+  induction t with
+  | nil => simp [BST_contains]
+  | node k l r ihl ihr =>
+    intro h
+    simp only [BST_contains] at h
+    split_ifs at h with h1 h2
+    · exact .left (ihl h)
+    · exact .right (ihr h)
+    · have hqk : q = k := le_antisymm (not_lt.mp h2) (not_lt.mp h1)
+      exact hqk ▸ .here
+
+end Membership
+
+
 /-! ### Rotations and Mirroring -/
 section Transformations
 
@@ -143,24 +206,24 @@ end Transformations
 section ContainsLemmas
 
 @[simp] lemma not_contains_empty [LinearOrder α] (q : α) :
-    ¬ (nil : Tree α).contains q := nofun
+    ¬ (nil : Tree α).BST_contains q := nofun
 
 @[simp] lemma contains_node_lt [LinearOrder α] {l : Tree α} {k q : α}
     {r : Tree α} (h : q < k) :
-    (l △[k] r).contains q ↔ l.contains q := by
-  simp [contains, h]
+    (l △[k] r).BST_contains q ↔ l.BST_contains q := by
+  simp [BST_contains, h]
 
 @[simp] lemma contains_node_gt [LinearOrder α] {l : Tree α} {k q : α}
     {r : Tree α} (h : k < q) :
-    (l △[k] r).contains q ↔ r.contains q := by
-  simp [contains, h, not_lt_of_gt h]
+    (l △[k] r).BST_contains q ↔ r.BST_contains q := by
+  simp [BST_contains, h, not_lt_of_gt h]
 
 @[simp] lemma contains_node_not_eq_not_lt [LinearOrder α]
     {l : Tree α} {k q : α} {r : Tree α}
     (h1 : ¬ q = k) (h2 : ¬ q < k) :
-    (l △[k] r).contains q ↔ r.contains q := by
+    (l △[k] r).BST_contains q ↔ r.BST_contains q := by
   have hgt : k < q := lt_of_le_of_ne (Std.not_lt.mp h2) (Ne.symm (Ne.intro h1))
-  simp [contains, hgt, not_lt_of_gt hgt]
+  simp [BST_contains, hgt, not_lt_of_gt hgt]
 
 end ContainsLemmas
 
@@ -204,22 +267,62 @@ section IsBSTAccessors
 
 end IsBSTAccessors
 
-end Tree
-
-
-/-! ### BST Structure -/
-section BSTStructure
 
-structure BST (α : Type) [LinearOrder α] where
-  tree : Tree α
-  hBST : Tree.IsBST tree
+/-! ### BST Membership -/
+section BSTMembership
+
+/-- In a BST subtree with upper bound `some ub`, every member is `< ub`. -/
+private lemma IsBSTAux.lt_of_mem_ub [LinearOrder α] {t : Tree α} {q ub : α}
+    {lb : Option α} (h : IsBSTAux t lb (some ub)) (hmem : q ∈ t) : q < ub := by
+  induction t generalizing lb ub with
+  | nil => simp at hmem
+  | node k l r ihl ihr =>
+    obtain ⟨_, hub, hl, hr⟩ := (IsBSTAux_node l k r lb (some ub)).mp h
+    rcases mem_node_iff.mp hmem with rfl | hml | hmr
+    · exact hub
+    · exact lt_trans (ihl hl hml) hub
+    · exact ihr hr hmr
+
+/-- In a BST subtree with lower bound `some lb`, every member is `> lb`. -/
+private lemma IsBSTAux.gt_of_mem_lb [LinearOrder α] {t : Tree α} {q lb : α}
+    {ub : Option α} (h : IsBSTAux t (some lb) ub) (hmem : q ∈ t) : lb < q := by
+  induction t generalizing lb ub with
+  | nil => simp at hmem
+  | node k l r ihl ihr =>
+    obtain ⟨hlb, _, hl, hr⟩ := (IsBSTAux_node l k r (some lb) ub).mp h
+    rcases mem_node_iff.mp hmem with rfl | hml | hmr
+    · exact hlb
+    · exact ihl hl hml
+    · exact lt_trans hlb (ihr hr hmr)
+
+/-- Membership implies the BST search path finds the key, for any bound
+configuration. -/
+private theorem IsBSTAux.mem_imp_contains [LinearOrder α] {t : Tree α} {q : α}
+    {lb ub : Option α} (h : IsBSTAux t lb ub) (hmem : q ∈ t) : t.BST_contains q := by
+  induction t generalizing lb ub with
+  | nil => simp at hmem
+  | node k l r ihl ihr =>
+    obtain ⟨_, _, hl, hr⟩ := (IsBSTAux_node l k r lb ub).mp h
+    rcases mem_node_iff.mp hmem with rfl | hml | hmr
+    · simp [BST_contains]
+    · have hlt : q < k := IsBSTAux.lt_of_mem_ub hl hml
+      simp only [BST_contains, if_pos hlt]
+      exact ihl hl hml
+    · have hgt : k < q := IsBSTAux.gt_of_mem_lb hr hmr
+      simp only [BST_contains, if_neg (not_lt.mpr hgt.le), if_pos hgt]
+      exact ihr hr hmr
+
+/-- Converse of `contains_imp_mem` for BSTs: membership implies the search-path
+`contains` succeeds. -/
+theorem mem_imp_contains [LinearOrder α] {t : Tree α} (hbst : IsBST t)
+    {q : α} (hmem : q ∈ t) : t.BST_contains q :=
+  IsBSTAux.mem_imp_contains hbst hmem
+
+/-- For BSTs, the search-path `contains` coincides with membership. -/
+theorem contains_iff_mem [LinearOrder α] {t : Tree α} (hbst : IsBST t) {q : α} :
+    t.BST_contains q ↔ q ∈ t :=
+  ⟨contains_imp_mem, mem_imp_contains hbst⟩
+
+end BSTMembership
 
-namespace BST
-
-/-- Checks if the BST contains a given key by delegating to the underlying tree. -/
-def contains [LinearOrder α] (t : BST α) (q : α) : Prop :=
-  t.tree.contains q
-
-end BST
-
-end BSTStructure
+end Tree

GraphAlgorithms/DataStructures/SplayTree/Correctness.lean

@@ -175,12 +175,12 @@ section RootOfContainedKey
 /-- If `t.contains q`, the subtree reached by `descend` is a node whose key
 equals `q`. Mirrors how `descend` and `Tree.contains` follow the same
 comparison path. -/
-theorem descend_contains [LinearOrder α] (t : Tree α) (q : α) (h : t.contains q) :
+theorem descend_contains [LinearOrder α] (t : Tree α) (q : α) (h : t.BST_contains q) :
     ∃ l r, (descend t q).1 = l △[q] r := by
   induction t with
-  | nil => simp [contains] at h
+  | nil => simp [BST_contains] at h
   | node k lt rt ihl ihr =>
-    simp only [contains] at h
+    simp only [BST_contains] at h
     by_cases hlt : q < k
     · simp only [hlt, ite_true] at h
       obtain ⟨l', r', hd⟩ := ihl h
@@ -193,6 +193,12 @@ theorem descend_contains [LinearOrder α] (t : Tree α) (q : α) (h : t.contains
       · have hqk : q = k := le_antisymm (not_lt.mp hgt) (not_lt.mp hlt)
         subst hqk; exact ⟨lt, rt, by rw [descend_node_eq]⟩
 
+/-- Membership-style variant of `descend_contains`: in a BST, if `q ∈ t` then
+`descend` reaches the node with key `q`. -/
+theorem descend_contains' [LinearOrder α] (t : Tree α) (q : α) (hbst : IsBST t)
+    (h : q ∈ t) : ∃ l r, (descend t q).1 = l △[q] r :=
+  descend_contains t q (mem_imp_contains hbst h)
+
 /-- Splaying a node `c = l △[k] r` upward along any path yields a tree
 whose root key is still `k`. Each rotation step brings `c` one level higher
 without changing its root key. -/
@@ -218,14 +224,20 @@ theorem splayUp_root_key_of_node :
 
 /-- If `t.contains q`, the bottom-up splay of `t` at `q` has `q` at the root. -/
 theorem splay_root_of_contains [LinearOrder α] (t : Tree α) (q : α)
-    (hc : t.contains q) : ∃ l r, splay t q = l △[q] r := by
+    (hc : t.BST_contains q) : ∃ l r, splay t q = l △[q] r := by
   obtain ⟨lr, rr, hd⟩ := descend_contains t q hc
   unfold splay
   rcases hdecomp : descend t q with ⟨reached, path⟩
   rw [hdecomp] at hd
   subst hd
   exact splayUp_root_key_of_node path lr q rr
 
+/-- Membership-style variant of `splay_root_of_contains`: in a BST, if `q ∈ t`
+then splaying brings `q` to the root. -/
+theorem splay_root_of_contains' [LinearOrder α] (t : Tree α) (q : α)
+    (hbst : IsBST t) (h : q ∈ t) : ∃ l r, splay t q = l △[q] r :=
+  splay_root_of_contains t q (mem_imp_contains hbst h)
+
 end RootOfContainedKey
 
 end SplayTree