chore: cleanup example

doc/examples/bintree.lean

@@ -71,7 +71,7 @@ Here's a function that does so with an in-order traversal of the tree.
 def Tree.toList (t : Tree β) : List (Nat × β) :=
   match t with
   | leaf => []
-  | node left key value right => left.toList ++ [(key, value)] ++ right.toList
+  | node l k v r => l.toList ++ [(k, v)] ++ r.toList
 
 #eval Tree.leaf.insert 2 "two" |>.insert 3 "three" |>.insert 1 "one"
 #eval Tree.leaf.insert 2 "two" |>.insert 3 "three" |>.insert 1 "one" |>.toList
@@ -88,7 +88,7 @@ where
   go (t : Tree β) (acc : List (Nat × β)) : List (Nat × β) :=
     match t with
     | leaf => acc
-    | node left key value right => left.go ((key, value) :: right.go acc)
+    | node l k v r => l.go ((k, v) :: r.go acc)
 
 /-|
 We now prove that `t.toList` and `t.toListTR` return the same list.
@@ -98,8 +98,10 @@ to define `Tree.toListTR`, we use an auxiliary theorem here too.
 theorem Tree.toList_eq_toListTR (t : Tree β) : t.toList = t.toListTR := by
   simp [toListTR, go t []]
 where
-  go (t : Tree β) (acc : List (Nat × β)) : toListTR.go t acc = t.toList ++ acc := by
-    induction t generalizing acc <;> simp [toListTR.go, toList, *, List.append_assoc]
+  go (t : Tree β) (acc : List (Nat × β))
+     : toListTR.go t acc = t.toList ++ acc := by
+    induction t generalizing acc <;>
+      simp [toListTR.go, toList, *, List.append_assoc]
 
 /-|
 The `[csimp]` annotation instructs the Lean code generator to replace
@@ -119,8 +121,11 @@ to express that idea that a predicate holds at every node of a tree:
 -/
 inductive ForallTree (p : Nat → β → Prop) : Tree β → Prop
   | leaf : ForallTree p .leaf
-  | node : ForallTree p left → p key value → ForallTree p right → ForallTree p (.node left key value right)
-
+  | node :
+     ForallTree p left →
+     p key value →
+     ForallTree p right →
+     ForallTree p (.node left key value right)
 
 /-|
 Second, we define the BST invariant:
@@ -136,6 +141,15 @@ inductive BST : Tree β → Prop
      BST left → BST right →
      BST (.node left key value right)
 
+local macro "have_eq " lhs:term:max rhs:term:max : tactic =>
+  `((have h : $lhs:term = $rhs:term :=
+       -- TODO: replace with linarith
+       by simp_arith at *; apply Nat.le_antisymm <;> assumption
+     try subst $lhs:term))
+
+local macro "by_cases' " e:term :  tactic =>
+  `(by_cases $e:term <;> simp [*])
+
 /-|
 We now prove that `Tree.insert` preserves the BST invariant using induction and case analysis.
 -/
@@ -146,12 +160,11 @@ theorem Tree.forall_insert_of_forall (h₁ : ForallTree p t) (h₂ : p key value
   | node hl hp hr ihl ihr =>
     rename Nat => k
     simp [insert]
-    by_cases key < k <;> simp [*]
+    by_cases' key < k
     · exact .node ihl hp hr
-    · by_cases k < key <;> simp [*]
+    · by_cases' k < key
       · exact .node hl hp ihr
-      · have heq : key = k := by simp_arith at *; apply Nat.le_antisymm <;> assumption -- TODO: improve with linarith
-        subst key
+      · have_eq key k
         exact .node hl h₂ hr
 
 theorem Tree.bst_insert_of_bst {t : Tree β} (h : BST t) (key : Nat) (value : β) : BST (t.insert key value) := by
@@ -160,12 +173,11 @@ theorem Tree.bst_insert_of_bst {t : Tree β} (h : BST t) (key : Nat) (value : β
   | node h₁ h₂ b₁ b₂ ih₁ ih₂ =>
     rename Nat => k
     simp [insert]
-    by_cases hlt : key < k <;> simp [*]
-    · exact .node (forall_insert_of_forall h₁ hlt) h₂ ih₁ b₂
-    · by_cases hgt : k < key <;> simp [*]
-      · exact .node h₁ (forall_insert_of_forall h₂ hgt) b₁ ih₂
-      · have heq : key = k := by simp_arith at *; apply Nat.le_antisymm <;> assumption -- TODO: improve with linarith
-        subst key
+    by_cases' key < k
+    · exact .node (forall_insert_of_forall h₁ ‹key < k›) h₂ ih₁ b₂
+    · by_cases' k < key
+      · exact .node h₁ (forall_insert_of_forall h₂ ‹k < key›) b₁ ih₂
+      · have_eq key k
         exact .node h₁ h₂ b₁ b₂
 
 /-|
@@ -191,34 +203,36 @@ attribute [local simp] BinTree.mk BinTree.contains BinTree.find? BinTree.insert
 Finally, we prove that `BinTree.find?` and `BinTree.insert` satisfy the map properties.
 -/
 
-theorem BinTree.find_mk {β : Type u} (k : Nat) : (@BinTree.mk β).find? k = none := by
+theorem BinTree.find_mk (k : Nat)
+        : BinTree.mk.find? k = (none : Option β) := by
   simp
 
-theorem BinTree.find_insert (b : BinTree β) (k : Nat) (v : β) : (b.insert k v).find? k = some v := by
+theorem BinTree.find_insert (b : BinTree β) (k : Nat) (v : β)
+        : (b.insert k v).find? k = some v := by
   let ⟨t, h⟩ := b; simp
   induction t with simp
   | node left key value right ihl ihr =>
-    by_cases k < key <;> simp [*]
+    by_cases' k < key
     · cases h; apply ihl; assumption
-    · by_cases key < k <;> simp [*]
+    · by_cases' key < k
       cases h; apply ihr; assumption
 
-theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β) : (b.insert k v).find? k' = b.find? k' := by
+theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β)
+        : (b.insert k v).find? k' = b.find? k' := by
   let ⟨t, h⟩ := b; simp
   induction t with simp
   | leaf =>
     split <;> simp <;> split <;> simp
-    have heq : k = k' := by simp_arith at *; apply Nat.le_antisymm <;> assumption -- TODO: improve with linarith
+    have_eq k k'
     contradiction
   | node left key value right ihl ihr =>
     let .node hl hr bl br := h
     have ihl := ihl bl
     have ihr := ihr br
-    by_cases k < key <;> simp [*]
-    by_cases key < k <;> simp [*]
-    have heq : key = k := by simp_arith at *; apply Nat.le_antisymm <;> assumption -- TODO: improve with linarith
-    subst key
-    by_cases k' < k <;> simp [*]
-    by_cases k  < k' <;> simp [*]
-    have heq : k = k' := by simp_arith at *; apply Nat.le_antisymm <;> assumption -- TODO: improve with linarith
+    by_cases' k < key
+    by_cases' key < k
+    have_eq key k
+    by_cases' k' < k
+    by_cases' k  < k'
+    have_eq k k'
     contradiction