many fixes

- removed warnings from deprecated functions
- make main get the file as argument
- make `makeTree` over a alpha Type

Author: arademaker

Fad/Assignment01.lean

@@ -116,7 +116,7 @@ def product (ns : List Nat) : Nat :=
   | [] => 1
   | n :: ns => n * product ns
 
-#eval product [2, 3, 4] -- should be 24
+-- #eval product [2, 3, 4] -- should be 24
 
 
 end Assignment01

Fad/Chapter3.lean

@@ -277,7 +277,7 @@ theorem length_sl_eq_length (xs : List a)
 
 
 theorem length_tail_lt_length (sl : SymList a) (h : sl ≠ nil)
- : lengthSL sl ≥ lengthSL (tailSL sl) := by
+ : lengthSL sl > lengthSL (tailSL sl) := by
   have ⟨lsl, rsl, ok⟩ := sl
   unfold lengthSL tailSL
   simp

Fad/Chapter4.lean

@@ -8,25 +8,24 @@ namespace Chapter4
 namespace D1
 
 def search₀ (f : Nat → Nat) (t : Nat) : List Nat :=
- List.foldl (fun xs x => if t = f x then x :: xs else xs) []
-  (List.range <| t + 1)
+ (List.range $ t + 1).filter (t = f ·)
 
+-- #eval search₀ (fun _ => 3) 3
 
 def search₁ (f : Nat → Nat) (t : Nat) : List Nat :=
   seek (0, t)
  where
-  acc xs x := if t = f x then x :: xs else xs
   seek : (Nat × Nat) → List Nat
-  | (a, b) => List.foldl acc [] <| List.range' a (b - a + 1)
+  | (a, b) => List.range' a (b - a + 1) |>.filter (t = f ·)
 
 
 def search₂ (f : Nat → Nat) (t : Nat) : List Nat :=
  let rec seek (a b : Nat) : List Nat :=
   let m := (a + b) / 2
   let v := f m
-  if      h₁ : a = b   then
+  if      h₁ : a = b then
    if t = v then [m] else []
-  else if h₉ : a > b   then []
+  else if h₉ : a > b then []
   else if h₂ : t = v then [m]
   else if h₃ : t < v then
     seek a (m - 1)
@@ -35,15 +34,15 @@ def search₂ (f : Nat → Nat) (t : Nat) : List Nat :=
  termination_by (b - a) -- see https://tinyurl.com/57szywn5
  seek 0 t
 
--- #eval search₂ (λ a => dbg_trace "f {a}"; a * a) 100000000
+-- #eval search₂ (λ a => dbg_trace "f {a}"; a * a) 1024
 
 def bound (f : Nat → Nat) (t : Nat) : (Nat × Nat) :=
   if t ≤ f 0 then (0, 0) else (b / 2, b)
  where
   b := Chapter1.until' done (· * 2) 1
   done b := t ≤ f b
 
--- #eval bound (fun x => dbg_trace "fun {x}"; x + 10) 20
+-- #eval bound (fun x => dbg_trace "fun {x}"; x + 10) 10
 
 def smallest (f : Nat → Nat) (t : Nat) (p : Nat × Nat) : Nat :=
  match p with
@@ -54,7 +53,7 @@ def smallest (f : Nat → Nat) (t : Nat) (p : Nat × Nat) : Nat :=
    else if h₁ : a > b then b
    else if h₃ : t = v then m
    else if h₂ : t < v then
-    smallest f t (a, m - 1)
+    smallest f t (a, m)
    else
     smallest f t (m + 1, b)
  termination_by (p.2 - p.1)
@@ -111,6 +110,8 @@ where
 -- #eval search₁ (λ (x, y) => x^2 + 3^y) 20259
 
 
+-- BUG #eval helper 12 (λ (x, y) => x^2 + 3^y) (0, 12) (12,0)
+
 partial def helper (t : Nat) (f : Nat × Nat → Nat)
  : (Nat × Nat) → (Nat × Nat) → List (Nat × Nat)
  | (x₁, y₁), (x₂, y₂) =>
@@ -139,14 +140,11 @@ partial def helper (t : Nat) (f : Nat × Nat → Nat)
      helper t f (x₁, y₁) (c - 1, y) ++ helper t f (c + 1, y - 1) (x₂, y₂)
 
 partial def search₂ (f : Nat × Nat → Nat) (t : Nat) : List (Nat × Nat) :=
- let p := D1.smallest (λ y => f (0, y)) t (-1, t)
- let q := D1.smallest (λ x => f (x, 0)) t (-1, t)
+ let p := D1.smallest (λ y => f (0, y)) t (0, t)
+ let q := D1.smallest (λ x => f (x, 0)) t (0, t)
  helper t f (0, p) (q, 0)
 
 
--- BUG #eval helper 12 (λ (x, y) => x^2 + 3^y) (0, 12) (12,0)
-
-
 /- https://kmill.github.io/informalization/ucsc_cse_talk.pdf -/
 
 def scale (a : Array Int) (c : Int) : Array Int := Id.run do
@@ -174,6 +172,8 @@ end D2
 
 namespace BST1
 
+variable {α : Type}
+
 inductive Tree (α : Type) : Type
 | null : Tree α
 | node : (Tree α) → α → (Tree α) → Tree α
@@ -187,20 +187,19 @@ def Tree.toFormat [ToString α] : (t : Tree α) → Std.Format
   bracket "(" (f!"{x}" ++
    line ++ nest 2 t₁.toFormat ++ line ++ nest 2 t₂.toFormat) ")"
 
-instance [ToString a] : Repr (Tree a) where
- reprPrec e _ := Tree.toFormat e
+instance [ToString α] : Repr (Tree α) where
+ reprPrec e _ := e.toFormat
 
-def Tree.size : Tree a → Nat
+def Tree.size : Tree α → Nat
 | null => 0
 | node t₁ _ t₂ => 1 + t₁.size + t₂.size
 
-def Tree.flatten : Tree a → List a
+def Tree.flatten : Tree α → List α
 | null => []
 | node l x r => l.flatten ++ [x] ++ r.flatten
 
-
 def search (f : Nat → Nat) : Nat → Tree Nat → Option Nat
-| _, Tree.null => none
+| _, Tree.null       => none
 | k, Tree.node l x r =>
   if f x < k then
    search f k r
@@ -210,12 +209,13 @@ def search (f : Nat → Nat) : Nat → Tree Nat → Option Nat
    else
     search f k l
 
-def Tree.height : Tree a → Nat
+def Tree.height : Tree α → Nat
 | null => 0
 | node l _ r => 1 + (max l.height r.height)
 
 
-def mkTree : List Nat → Tree Nat
+def mkTree [LT α] [DecidableRel (α := α) (· < ·)]
+: List α → Tree α
 | [] => Tree.null
 | x :: xs =>
   let p := xs.partition (· < x)
@@ -224,12 +224,17 @@ def mkTree : List Nat → Tree Nat
  decreasing_by
   all_goals
    simp [List.partition_eq_filter_filter,
-         List.length_filter_le, Nat.lt_add_one_of_le]
+         List.length_filter_le,
+         Nat.lt_add_one_of_le]
+
 
 end BST1
 
+
 namespace BST2
 
+variable {α : Type}
+
 inductive Tree (α : Type) : Type
 | null : Tree α
 | node : Nat → (Tree α) → α → (Tree α) → Tree α
@@ -243,14 +248,14 @@ def Tree.toFormat [ToString α] : (t : Tree α) → Std.Format
   bracket "(" (f!"{x}" ++
    line ++ nest 2 t₁.toFormat ++ line ++ nest 2 t₂.toFormat) ")"
 
-instance [ToString a] : Repr (Tree a) where
- reprPrec e _ := Tree.toFormat e
+instance [ToString α] : Repr (Tree α) where
+ reprPrec e _ := e.toFormat
 
-def Tree.height : (a : Tree α) -> Nat
- | Tree.null => 0
- | Tree.node x _ _ _ => x
+def Tree.height : Tree α → Nat
+ | .null => 0
+ | .node x _ _ _ => x
 
-def Tree.flatten : Tree a → List a
+def Tree.flatten : Tree α → List α
 | null => []
 | node _ l x r => l.flatten ++ [x] ++ r.flatten
 

Fad/Chapter5-Ex.lean

@@ -333,7 +333,7 @@ open Function (uncurry) in
 
 def csort (m : Nat) (xs : List Nat) : List Nat :=
   let a := Chapter3.accumArray Nat.add 0 m (xs.map (·, 1))
-  a.zipWithIndex.toList.flatMap (uncurry replicate)
+  a.zipIdx.toList.flatMap (uncurry replicate)
 
 
 /- # Exercicio 5.19 -/

Fad/Chapter6.lean

@@ -99,7 +99,7 @@ def minmax [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)]
 
 def select₀ [Inhabited a] [LT a] [DecidableRel (α := a) (· < ·)]
  (k : Nat) (xs : List a) : a :=
- (qsort₁ xs).get! (k - 1)
+ (qsort₁ xs)[k - 1]!
 
 
 def median [Inhabited a] [LT a] [DecidableRel (α := a) (· < ·)]
@@ -120,7 +120,7 @@ partial def group [Inhabited a] (n : Nat) (xs : List a) : List (List a) :=
 def medians [Inhabited a] [LT a]
   [DecidableRel (α := a) (· < ·)] [DecidableRel (α := a) (· = ·)]
   : List a → List a :=
-  let middle (xs : List a) := xs.get! (((xs.length + 1) / 2) - 1)
+  let middle (xs : List a) := xs[((xs.length + 1) / 2) - 1]!
   List.map (middle ∘ qsort₁) ∘ group 5
 
 
@@ -152,7 +152,7 @@ partial def select [Inhabited a] [LT a]
     let m := us.length
     let n := vs.length
     if          k ≤ m then select k us
-    else if k ≤ m + n then vs.get! (k - m - 1)
+    else if k ≤ m + n then vs[k - m - 1]!
     else if k > m + n then select (k - m - n) ws
     else panic! "unreachable code"
 

Fad/Chapter7-Ex.lean

@@ -109,11 +109,12 @@ namespace S73
    return the other `minimum`. -/
 
 def mktuples' : List Denom → Nat → List Tuple
-  | [1]  , n   => [[n]]
-  | []   , _   => panic! "mktuples: invalid empty list"
+  | [1]    , n => [[n]]
+  | []     , _ => panic! "mktuples: invalid empty list"
   | d :: ds, n =>
-    let rs := List.iota (n / d + 1) |>.map (· - 1)
-    rs.flatMap (λ c => mktuples₀ ds (n - c * d) |>.map (λ cs => c :: cs))
+    let rs := List.range (n / d + 1)
+    rs.flatMap (λ c => mktuples₀ ds (n - c * d) |>.map
+     (λ cs => c :: cs))
 
 def mkchange' (ds : List Denom) : Nat → Tuple :=
   minWith List.sum ∘ mktuples' ds

Fad/Chapter9-Ex.lean

@@ -9,14 +9,15 @@ def toAdj (g : Graph) : AdjArray :=
 
 def toGraph (adj : AdjArray) : Graph :=
   let vs := List.range adj.size
-  let es : List Edge := adj.toList.enum |>.flatMap
+  let es : List Edge := adj.toList.zipIdx.map (λ (a,b) => (b,a))
+    |>.flatMap
    (λ (v, ps) => ps.map (λ p => (v, p.1, p.2)))
   (vs, es)
 
 def g : Graph :=
  ([0, 1, 2, 3],
   [(0, 1, 1), (1, 2, 5), (1, 3, 10), (2, 3, 2), (3, 0, 4)])
 
-
+-- #eval toAdj g |> toGraph
 
 end Chapter9

Fad/Chapter9.lean

@@ -17,6 +17,4 @@ def weight (e : Edge) : Weight := e.2.2
 abbrev AdjArray := Array (List (Vertex × Weight))
 
 
-
-
 end Chapter9

Main.lean

@@ -1,4 +1,22 @@
 import Fad
 
-def main : IO Unit :=
-  IO.println Chapter0.hello₁
+
+def readFile (filename : String) : IO (List Nat) := do
+  let contents ← IO.FS.readFile filename
+  let lines := contents.splitOn "\n"
+  let mut result := []
+  for line in lines do
+    match line.trim.toNat? with
+    | some n => result := n :: result
+    | none => result := result
+  return result
+
+
+def main (args : List String) : IO Unit := do
+ match args with
+ | [] => println! "Usage: lake fad FILE"
+ | a :: _ =>
+  let r ← readFile a
+  let t := Chapter4.BST1.mkTree r
+  println! t.height
+  println! Chapter4.BST1.search id 678 t