From dee5dbca982ddd3e79871e9792ed25b2ec27c59a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Apr 2022 07:13:46 -0700 Subject: [PATCH] chore: cleanup example --- doc/examples/bintree.lean | 72 +++++++++++++++++++++++---------------- 1 file changed, 43 insertions(+), 29 deletions(-) diff --git a/doc/examples/bintree.lean b/doc/examples/bintree.lean index 85b3d4619a..61bf993713 100644 --- a/doc/examples/bintree.lean +++ b/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