correcao do assignment 4

- implementacao do BST insert2 que recebe funcao `key`
- implementacao parcial do Bucketsort

Author: arademaker

Fad/Assignment04.lean

@@ -92,7 +92,7 @@ end
 
 section
 open Chapter5.Quicksort (qsort₂)
-open Chapter4.BST2 (search mkTree mkTree₁)
+open Chapter4.BST2 (search mkTree mkTree₁ mkTree₂)
 
 structure Book where
   title : String
@@ -108,15 +108,23 @@ instance : LT Book where
 instance : DecidableRel (fun (a b : Book) => a < b) :=
   fun a b => Float.decLt a.price b.price
 
-def books := List.range 12 |>.map (λ n => Book.mk s!"{n}" n.toFloat)
-
-#eval mkTree₁ books |>.toFormat
+def books := List.range 12
+  |>.map (λ n => Book.mk s!"{n}" n.toFloat)
 
 /- Both `search` and `mkTree₁` need to use the same field for
    insertion and lookup.-/
 
--- #eval mkTree₁ books
-#eval search (fun x => x.title) "10" (mkTree₁ books)
+instance : Ord Float where
+  compare a b :=
+    if      a < b then Ordering.lt
+    else if a > b then Ordering.gt
+    else Ordering.eq
+
+/-
+#eval
+  let tb := mkTree₂ (·.price) books
+  search (·.price) 10 tb
+-/
 
 end
 

Fad/Chapter1.lean

@@ -16,20 +16,17 @@ def map (f : a → b) : List a → List b
 | [] => []
 | (x :: xs) => f x :: map f xs
 
--- #eval map (· + 10) [1,2,3]
-
-example : map (· * 10) [1,2,3] = [10,20,30] := rfl
-
+example : map (· * 10) [1,2,3] = [10,20,30] :=
+  rfl
 
-theorem map_equal (a : List α) (f : α → β): map f a = List.map f a := by
+theorem map_equal {α β} (a : List α) (f : α → β)
+ : map f a = List.map f a := by
  induction a with
  | nil => rfl
  | cons a as ih =>
    simp [List.map, map]
    rw [ih]
 
-
-
 def makeInc (n : Nat) : (Nat → Nat) :=
   fun x => x + n
 

Fad/Chapter4.lean

@@ -238,7 +238,6 @@ inductive Tree (a : Type) : Type
 | node : Nat → (Tree a) → a → (Tree a) → Tree a
 deriving Nonempty, Inhabited
 
-/-
 open Std.Format in
 
 def Tree.toFormat [ToString a] : (t : Tree a) → Std.Format
@@ -249,7 +248,7 @@ def Tree.toFormat [ToString a] : (t : Tree a) → Std.Format
 
 instance [ToString a] : Repr (Tree a) where
  reprPrec e _ := e.toFormat
--/
+
 
 def Tree.height : Tree a → Nat
  | .null => 0
@@ -305,7 +304,6 @@ def insert : (x : a) -> Tree a -> Tree a
    if x < y then balance (insert x l) y r else
    if x > y then balance l y (insert x r) else .node h l y r
 
-
 def mkTree : (xs : List a) → Tree a :=
  List.foldr insert (.null : Tree a)
 
@@ -346,6 +344,34 @@ def insert₁ : (x : a) -> Tree a -> Tree a
 def mkTree₁ : List a → Tree a :=
   List.foldr insert₁ Tree.null
 
+def insert₂ {b : Type} [Ord b] (key: a → b)
+ : (x : a) -> Tree a -> Tree a
+ | x, .null         => node .null x .null
+ | x, .node h l y r =>
+     match compare (key x) (key y) with
+   | .lt => gbalance (insert₂ key x l) y r
+   | .gt => gbalance l y (insert₂ key x r)
+   | .eq => .node h l y r
+
+def mkTree₂ {b : Type} [Ord b] (key: a → b)
+  : List a → Tree a :=
+  List.foldr (insert₂ key) Tree.null
+
+
+/- how to deal with list with duplicated elements -/
+
+instance : Ord (Nat × Nat) where
+  compare a b :=
+   match compare a.1 b.1 with
+   | .eq => compare a.2 b.2
+   | x   => x
+
+/-
+#eval
+  (λ xs => mkTree₂ id xs.zipIdx |> Tree.flatten |>.map (·.1))
+  [1,3,2,1,2]
+-/
+
 def sort : List a → List a :=
   Tree.flatten ∘ mkTree₁
 

Fad/Chapter5.lean

@@ -3,6 +3,8 @@ import Fad.«Chapter1-Ex»
 
 namespace Chapter5
 
+-- ## Section 5.1 Quicksort
+
 namespace Quicksort
 
 variable {a : Type} [h₁ : LT a] [h₂ : DecidableRel (α := a) (· < ·)]
@@ -58,9 +60,9 @@ def qsort₂ [Ord a] (f : a → a → Ordering) : List a → List a
 #eval qsort₂ compare ['c','a','b']
 -/
 
-
 end Quicksort
 
+-- ## Section 5.2 MergeSort
 
 namespace Mergesort
 
@@ -189,35 +191,29 @@ def mkPair (n : Nat) (xs : List a) : (Tree a × List a) :=
 def mkTree₁ (as : List a) : Tree a :=
   mkPair as.length as |>.1
 
-
 def msort₂ (xs : List a) : List a :=
   (Tree.flatten ∘ mkTree₁) xs
 
-
 def pairWith (f : a → a → a) : List a → List a
  | []             => []
  | [x]            => [x]
  | (x :: y :: xs) => f x y :: pairWith f xs
 
-
 def mkTree₂ : List a → Tree a
  | []  => .null
  | as  =>
    unwrap (until' single (pairWith .node) (as.map .leaf))
     |>.getD .null
 
-
 def msort₃ (xs : List a) : List a :=
   (Tree.flatten ∘ mkTree₂) xs
 
-
 def msort₄ : List a → List a
  | []   => []
  | as   =>
    unwrap (until' single (pairWith merge) (as.map wrap))
     |>.getD []
 
-
 def msort₅ : List a → List a
   | []  => []
   | xs  =>
@@ -232,36 +228,79 @@ def msort₅ : List a → List a
     let runs := List.foldr op []
   unwrap (until' single (pairWith merge) (runs xs)) |>.getD []
 
-
 end Mergesort
 
 
+-- ## Section 5.3 Heapsort
 
 namespace Heapsort
 
-inductive Tree (α : Type) : Type
- | null : Tree α
- | node : α → Tree α → Tree α → Tree α
- deriving Inhabited
+variable {a : Type} [LE a] [ToString a]
 
+inductive Tree (a : Type) : Type
+ | null : Tree a
+ | node : a → Tree a → Tree a → Tree a
+ deriving Inhabited
 
-def flatten [LE a] [DecidableRel (α := a) (· ≤ ·)] : Tree a → List a
+def flatten [DecidableRel (α := a) (· ≤ ·)] : Tree a → List a
 | Tree.null       => []
 | Tree.node x u v => x :: Mergesort.merge (flatten u) (flatten v)
 
-
 open Std.Format in
 
-def Tree.toFormat [ToString α] : (t: Tree α) → Std.Format
+def Tree.toFormat : (t: Tree a) → Std.Format
 | .null => Std.Format.text "."
 | .node x t₁ t₂ =>
   bracket "(" (f!"{x}" ++
    line ++ nest 2 t₁.toFormat ++ line ++ nest 2 t₂.toFormat) ")"
 
-instance [ToString a] : Repr (Tree a) where
+instance : Repr (Tree a) where
  reprPrec e _ := Tree.toFormat e
 
-
 end Heapsort
 
+
+-- ## Section 5.4 Bucketsort and Radixsort
+
+namespace Bucketsort
+
+variable {α : Type}
+
+inductive Tree (α : Type)
+| leaf : α → Tree α
+| node : List (Tree α) → Tree α
+deriving Repr
+
+
+def Tree.flatten (r : Tree (List α)) : List α :=
+ match r with
+ | .leaf v  => v
+ | .node ts =>
+   List.flatten <| ts.map flatten
+
+def ptn₀ {α β : Type} [BEq β] (rng : List β)
+  (f : α → β) (xs : List α) : List (List α) :=
+  rng.map (λ m => xs.filter (λ x => f x == m))
+
+def mkTree {α β : Type} [BEq β]
+  (rng : List β)
+  (ds : List (α → β)) (xs : List α) : Tree (List α) :=
+  match ds with
+  | []       => .leaf xs
+  | d :: ds' =>
+    .node ((ptn₀ rng d xs).map (mkTree rng ds'))
+
+def bsort₀ {β : Type} [BEq β] (rng : List β)
+  (ds : List (α → β)) (xs : List α) : List α :=
+  Tree.flatten (mkTree rng ds xs)
+
+/-
+#eval bsort₀ "abc".toList
+  [fun s => s.toList[0]!,fun s => s.toList[1]!]
+  ["ba", "ab", "aab", "bba"]
+-/
+
+end Bucketsort
+
+
 end Chapter5