Merge branch 'Aug19'

Src/Problem50.lean

@@ -28,13 +28,13 @@ def insertionSort {α : Type} [Ord α] : List α → List α
 
 /-- Huffman Tree -/
 inductive HuffTree where
-  | Node (left : HuffTree) (right : HuffTree) (weight : Nat)
+  | node (left : HuffTree) (right : HuffTree) (weight : Nat)
   | Leaf (c : Char) (weight : Nat)
 deriving Inhabited, Repr
 
 def HuffTree.weight : HuffTree → Nat
   | Leaf _ w => w
-  | Node _ _ w => w
+  | node _ _ w => w
 
 def HuffTree.compare (s s' : HuffTree) : Ordering :=
   let w := s.weight
@@ -59,7 +59,7 @@ partial def HuffTree.merge (trees : List HuffTree) : List HuffTree :=
   | [] => []
   | [tree] => [tree]
   | t1 :: t2 :: rest =>
-    let t' := HuffTree.Node t1 t2 (t1.weight + t2.weight)
+    let t' := HuffTree.node t1 t2 (t1.weight + t2.weight)
     HuffTree.merge (t' :: rest)
 
 -- This function is not used in the solution
@@ -70,7 +70,7 @@ abbrev Code := String
 --#--
 def HuffTree.encode (c : Char) : HuffTree → Option Code
   | .Leaf c' _ => if c = c' then some "" else none
-  | .Node l r _w =>
+  | .node l r _w =>
     match l.encode c, r.encode c with
     | none, some s => some ("1" ++ s)
     | some s, none => some ("0" ++ s)

Src/Problem55.lean

@@ -7,19 +7,19 @@ Write a function `cbalTree` to construct completely balanced binary trees for a
 -/
 
 inductive BinTree (α : Type) where
-  | Empty : BinTree α
-  | Node : α → BinTree α → BinTree α → BinTree α
+  | empty : BinTree α
+  | node : α → BinTree α → BinTree α → BinTree α
 deriving Repr
 
-def leaf {α : Type} (a : α) : BinTree α := .Node a .Empty .Empty
+def leaf {α : Type} (a : α) : BinTree α := .node a .empty .empty
 
 def BinTree.depth {α : Type} : BinTree α → Nat
-| .Empty => 0
-| .Node _ l r => 1 + max l.depth r.depth
+| .empty => 0
+| .node _ l r => 1 + max l.depth r.depth
 
 def BinTree.isBalanced {α : Type} : BinTree α → Bool
-  | .Empty => true
-  | .Node _ l r =>
+  | .empty => true
+  | .node _ l r =>
     l.isBalanced ∧ r.isBalanced ∧
     Int.natAbs ((l.depth : Int) - (r.depth : Int)) ≤ 1
 
@@ -29,18 +29,19 @@ instance : Monad List where
   bind := @List.bind
   map := @List.map
 
+/-- construct all balanced binary trees which contains `x` elements -/
 partial def cbalTree (x : Nat) : List (BinTree Unit) :=
   -- sorry
   match x with
-  | 0 => [.Empty]
+  | 0 => [.empty]
   | n + 1 => do
     let q := n / 2
     let r := n % 2
     let indices := List.range (q+r+1) |>.drop q
     let i ← indices
     let left ← cbalTree i
     let right ← cbalTree (n - i)
-    pure (BinTree.Node () left right)
+    pure (BinTree.node () left right)
   -- sorry
 
 -- The following codes are for test and you should not edit these.

Src/Problem56.lean

@@ -0,0 +1,49 @@
+/- # Problem 56
+
+Let us call a binary tree symmetric if you can draw a vertical line through the root node and then the right subtree is the mirror image of the left subtree. Write a predicate symmetric/1 to check whether a given binary tree is symmetric. Hint: Write a predicate mirror/2 first to check whether one tree is the mirror image of another. We are only interested in the structure, not in the contents of the nodes.
+-/
+
+inductive BinTree (α : Type) where
+  | empty : BinTree α
+  | node : α → BinTree α → BinTree α → BinTree α
+deriving Repr
+
+def leaf {α : Type} (a : α) : BinTree α := .node a .empty .empty
+
+/-- This is used to display `#check` results -/
+@[app_unexpander BinTree.node]
+def leaf.unexpander : Lean.PrettyPrinter.Unexpander
+  | `($_ $a BinTree.empty BinTree.empty) => `(leaf $a)
+  | _ => throw ()
+
+/-- Use `leaf` to display `#eval` results -/
+def BinTree.toString {α : Type} [ToString α] (t : BinTree α) : String :=
+  match t with
+  | .node v .empty .empty => s!"leaf {v}"
+  | .node v l r => s!"BinTree.node {v} ({toString l}) ({toString r})"
+  | .empty => "empty"
+
+variable {α : Type}
+
+def BinTree.mirror (s t : BinTree α) : Bool :=
+  -- sorry
+  match s, t with
+  | .empty, .empty => true
+  | .node _ a b, .node _ x y => mirror a y && mirror b x
+  | _, _ => false
+  -- sorry
+
+def BinTree.isSymmetric (t : BinTree α) : Bool :=
+  -- sorry
+  match t with
+  | .empty => true
+  | .node _ l r => mirror l r
+  -- sorry
+
+-- The following codes are for test and you should not edit these.
+
+#guard BinTree.isSymmetric (leaf 'x')
+
+#guard ! BinTree.isSymmetric (BinTree.node 'x' (leaf 'x') BinTree.empty)
+
+#guard BinTree.isSymmetric (BinTree.node 'x' (leaf 'x') (leaf 'x'))

Src/Problem57.lean

@@ -0,0 +1,72 @@
+/- # Problem 57
+
+Use the predicate add/3, developed in chapter 4 of the course, to write a predicate to construct a binary search tree from a list of integer numbers.
+-/
+
+inductive BinTree (α : Type) where
+  | empty : BinTree α
+  | node : α → BinTree α → BinTree α → BinTree α
+
+def leaf {α : Type} (a : α) : BinTree α := .node a .empty .empty
+
+/-- This is used to display `#check` results -/
+@[app_unexpander BinTree.node]
+def leaf.unexpander : Lean.PrettyPrinter.Unexpander
+  | `($_ $a BinTree.empty BinTree.empty) => `(leaf $a)
+  | _ => throw ()
+
+/-- Use `leaf` to display `#eval` results -/
+def BinTree.toString {α : Type} [ToString α] (t : BinTree α) : String :=
+  match t with
+  | .node v .empty .empty => s!"leaf {v}"
+  | .node v l r => s!"BinTree.node {v} ({toString l}) ({toString r})"
+  | .empty => "empty"
+
+instance {α : Type} [ToString α] : ToString (BinTree α) := ⟨BinTree.toString⟩
+
+variable {α : Type}
+
+instance [Ord α] : Max α where
+  max x y :=
+    match compare x y with
+    | .lt => y
+    | _ => x
+
+def BinTree.max [Ord α] (t : BinTree α) : Option α :=
+  match t with
+  | .empty => none
+  | .node v l r =>
+    let left_max := (max l).getD v
+    let right_max := (max r).getD v
+    some <| [v, left_max, right_max].foldl Max.max v
+
+def BinTree.searchTree [Ord α] (t : BinTree α) : Bool :=
+  -- sorry
+  match t with
+  | .empty => true
+  | .node v l r =>
+    let left_max := (max l).getD v
+    let right_max := (max r).getD v
+    match compare left_max v, compare v right_max with
+    | _, .gt => false
+    | .gt, _ => false
+    | _, _ => searchTree l && searchTree r
+  -- sorry
+
+def BinTree.searchTreeFromList [Ord α] (xs : List α) : BinTree α :=
+  -- sorry
+  xs.foldl insert BinTree.empty
+where
+  insert : BinTree α → α → BinTree α
+  | .empty, x => leaf x
+  | .node v l r, x =>
+    match compare x v with
+    | .lt => BinTree.node v (insert l x) r
+    | _ => BinTree.node v l (insert r x)
+  -- sorry
+
+-- The following codes are for test and you should not edit these.
+
+#guard BinTree.node 3 (.node 2 (leaf 1) .empty) (.node 5 .empty (leaf 7)) |>.searchTree
+
+#guard BinTree.searchTreeFromList [3, 2, 5, 7, 1] |>.searchTree

Src/Problem58.lean

@@ -0,0 +1,83 @@
+/- # Problem 58
+
+Apply the generate-and-test paradigm to construct all symmetric, completely balanced binary trees with a given number of nodes.
+-/
+
+/-- binary tree -/
+inductive BinTree (α : Type) where
+  | empty : BinTree α
+  | node : α → BinTree α → BinTree α → BinTree α
+
+def leaf {α : Type} (a : α) : BinTree α := .node a .empty .empty
+
+variable {α : Type} [ToString α]
+
+def String.addIndent (s : String) (depth : Nat) : String :=
+  Nat.repeat (fun s => " " ++ s) depth s
+
+def BinTree.toString (tree : BinTree α) : String :=
+  aux tree 2
+where
+  aux (tree : BinTree α) (depth : Nat) : String :=
+    match tree with
+    | .node v .empty .empty => s!"leaf {v}"
+    | .node v l r =>
+      let ls := aux l (depth + 2)
+      let rs := aux r (depth + 2)
+      s!".node {v}\n" ++ s!"{ls}\n".addIndent depth ++ s!"{rs}\n".addIndent depth
+    | .empty => "empty"
+
+instance {α : Type} [ToString α] : ToString (BinTree α) := ⟨BinTree.toString⟩
+
+#eval BinTree.node 3 (.node 2 (leaf 1) .empty) (.node 5 .empty (leaf 7))
+
+#eval BinTree.node 'x' (leaf 'x') (leaf 'x')
+
+#eval BinTree.node 'x' .empty (leaf 'x')
+
+#eval BinTree.node 'x' (leaf 'x') .empty
+
+/-- monad instance of `List` -/
+instance : Monad List where
+  pure := @List.pure
+  bind := @List.bind
+  map := @List.map
+
+/-- construct all balanced binary trees which contains `x` elements -/
+partial def cbalTree (x : Nat) : List (BinTree Unit) :=
+  -- sorry
+  match x with
+  | 0 => [.empty]
+  | n + 1 => do
+    let q := n / 2
+    let r := n % 2
+    let indices := List.range (q+r+1) |>.drop q
+    let i ← indices
+    let left ← cbalTree i
+    let right ← cbalTree (n - i)
+    pure (BinTree.node () left right)
+  -- sorry
+
+def BinTree.mirror (s t : BinTree α) : Bool :=
+  match s, t with
+  | .empty, .empty => true
+  | .node _ a b, .node _ x y => mirror a y && mirror b x
+  | _, _ => false
+
+def BinTree.isSymmetric (t : BinTree α) : Bool :=
+  match t with
+  | .empty => true
+  | .node _ l r => mirror l r
+
+/-- construct all balanced, symmetric binary trees with given number of elements -/
+def symCbalTrees (n : Nat) : List (BinTree Unit) :=
+  -- sorry
+  cbalTree n |>.filter BinTree.isSymmetric
+  -- sorry
+
+-- The following codes are for test and you should not edit these.
+
+#guard (symCbalTrees 5).length = 2
+#guard (symCbalTrees 6).length = 0
+#guard (symCbalTrees 7).length = 1
+#guard (symCbalTrees 8).length = 0

Src/Problem59.lean

@@ -0,0 +1,66 @@
+/- # Problem 59
+
+Construct height-balanced binary trees.
+-/
+
+/-- binary tree -/
+inductive BinTree (α : Type) where
+  | empty : BinTree α
+  | node : α → BinTree α → BinTree α → BinTree α
+
+deriving Repr
+
+def leaf {α : Type} (a : α) : BinTree α := .node a .empty .empty
+
+variable {α : Type} [ToString α]
+
+def BinTree.height (t : BinTree α) : Nat :=
+  match t with
+  | .empty => 0
+  | .node _ l r => 1 + max l.height r.height
+
+/-- monad instance of `List` -/
+instance : Monad List where
+  pure := @List.pure
+  bind := @List.bind
+  map := @List.map
+
+/-- construct all balanced binary trees which contains `x` elements -/
+partial def cbalTree (x : Nat) : List (BinTree Unit) :=
+  -- sorry
+  match x with
+  | 0 => [.empty]
+  | n + 1 => do
+    let q := n / 2
+    let r := n % 2
+    let indices := List.range (q+r+1) |>.drop q
+    let i ← indices
+    let left ← cbalTree i
+    let right ← cbalTree (n - i)
+    pure (BinTree.node () left right)
+  -- sorry
+
+variable {β : Type}
+
+def List.product (as : List α) (bs : List β) : List (α × β) := do
+  let a ← as
+  let b ← bs
+  return (a, b)
+
+/-- construct all balanced binary trees whose hight is `height`. -/
+def hbalTrees (height : Nat) : List (BinTree Unit) :=
+  -- sorry
+  match height with
+  | 0 => [.empty]
+  | 1 => [leaf ()]
+  | h + 2 =>
+    let t1s := hbalTrees (h + 1)
+    let t2s := hbalTrees h
+    let ts := List.product t1s t2s ++ List.product t2s t1s
+    ts.map fun (t1, t2) => BinTree.node () t1 t2
+  -- sorry
+
+-- The following codes are for test and you should not edit these.
+
+#guard (hbalTrees 2 |>.length) = 2
+#guard (hbalTrees 3 |>.length) = 4

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0-rc3
+leanprover/lean4:v4.11.0

md/SUMMARY.md

@@ -65,4 +65,8 @@
 # 54-60: Binary trees
 
 * [54: check binary tree]()
-* [55: list up balanced binary tree](./build/Problem55.md)
+* [55: List up balanced binary tree](./build/Problem55.md)
+* [56: Symmetric binary tree](./build/Problem56.md)
+* [57: Binary search tree](./build/Problem57.md)
+* [58: List up symmetric balanced binary trees](./build/Problem58.md)
+* [59: List up balanced binary trees with given hight](./build/Problem59.md)