Lean 99: Ninety-Nine Lean Problems

Lean is a theorem prover, but it is also a programming language. Moreover, it is the best functional language ever! Let's learn functional programming with Lean. 😎

These are Lean translations of Ninety-Nine Haskell Problems, which are themselves translations of Ninety-Nine Lisp Problems.

How to Play

  • Every Lean code block in this book has a button to jump to the Lean web playground. Replace the sorry with your own code so that the test code passes.

  • You can see an answer by clicking on the button in the top right-hand corner of each page.

Good luck! 👍

Problem 1

(Easy 🌟) Find the last element of a list.

variable {α : Type}

def myLast (l : List α) : Option α :=
  sorry

-- The following codes are for test and you should not edit these.

example : myLast [1, 2, 3, 4] = some 4 := by rfl

example : myLast ([] : List α) = none := by rfl

example : myLast [1] = some 1 := by rfl

example : myLast ['x', 'y', 'z'] = some 'z' := by rfl

Problem 2

(Easy 🌟) Find the last-but-one (or second-last) element of a list.

variable {α : Type}

def myButLast (l : List α) : Option α :=
  sorry

-- The following codes are for test and you should not edit these.

example : myButLast [1, 2, 3, 4] = some 3 := rfl

example : myButLast ['x', 'y', 'z'] = some 'y' := rfl

example : myButLast ([] : List α) = none := rfl

example : myButLast [1] = none := rfl

Problem 3

(Easy 🌟) Find the K'th element of a list.

variable {α : Type}

def elementAt (l : List α) (k : Nat) : Option α :=
  sorry

-- The following codes are for test and you should not edit these.

example : elementAt ['a', 'b', 'c', 'd', 'e'] 3 = some 'c' := by rfl

example : elementAt ['a', 'b', 'c', 'd', 'e'] 6 = none := by rfl

example : elementAt ['a', 'b', 'c', 'd', 'e'] 0 = none := by rfl

example : elementAt ([] : List α) 0 = none := by rfl

example : elementAt [1, 2, 3] 2 = some 2 := by rfl

Problem 4

(Easy 🌟) Find the number of elements in a list.

variable {α : Type}

def myLength (l : List α) : Nat :=
  sorry

-- The following codes are for test and you should not edit these.

example : myLength [123, 456, 789] = 3 := by rfl

example : myLength ['L', 'e', 'a', 'n', '4'] = 5 := by rfl

example : myLength [False, True, True] = 3 := by rfl

example : myLength ([] : List α) = 0 := by rfl

Problem 5

(Easy 🌟) Reverse a list.

variable {α : Type}

def myReverse (l : List α) : List α :=
  sorry

-- The following codes are for test and you should not edit these.

example : myReverse [1, 2, 3, 4] = [4, 3, 2, 1] := rfl

example : myReverse ["man", "plan", "canal", "panama"]
  = ["panama", "canal", "plan", "man"] := rfl

Problem 6

(Easy 🌟) Find out whether a list is a palindrome.

Hint: A palindrome can be read forward or backward; e.g. (x a m a x).

variable {α : Type}

-- Assume that the terms in `α` can be compared
-- to determine whether they are identical.
variable [BEq α]

-- you can use `List.reverse`
#check List.reverse

def isPalindrome (l : List α) : Bool :=
  sorry

-- The following codes are for test and you should not edit these.

example : isPalindrome [1, 2, 3] = false := rfl

example : isPalindrome [1, 2, 4, 8, 16, 8, 4, 2, 1] = true := rfl

example : isPalindrome ["a", "b", "a"] = true := rfl

example : isPalindrome ([] : List α) = true := rfl

example : isPalindrome ['x'] = true := rfl

Problem 7

(Intermediate 🌟🌟) Flatten a nested list structure.

variable {α : Type}

-- We have to define a new data type, because lists in Lean are homogeneous.
inductive NestedList (α : Type) where
  | elem : α → NestedList α
  | list : List (NestedList α) → NestedList α

/-- convert NestedList to String. -/
partial def NestedList.toString [ToString α] : NestedList α → String
  | NestedList.elem x => ToString.toString x
  | NestedList.list xs => "[" ++ String.intercalate ", " (xs.map toString) ++ "]"

/-- Display `NestedList` in a readable manner when you run `#eval`. -/
instance [ToString α] : ToString (NestedList (α : Type)) where
  toString nl := NestedList.toString nl

/-- flatten the list structure -/
def flatten (nl : NestedList α) : List α :=
  sorry

-- The following codes are for test and you should not edit these.

open NestedList

def sample : NestedList Nat :=
  list [elem 1, list [elem 2, elem 3], elem 4]

#eval sample

def empty : NestedList String := list []

#eval empty

example : flatten (.elem 5) = [5] := by
  delta flatten
  rfl

example : flatten sample = [1, 2, 3, 4] := by
  delta flatten
  rfl

example : flatten (empty) = [] := by
  delta flatten
  rfl

Problem 8

(Intermediate 🌟🌟) Eliminate consecutive duplicates of list elements.

variable {α : Type} [BEq α]

def compress (l : List α) : List α :=
  sorry

-- The following codes are for test and you should not edit these.

example : compress [1, 1, 2, 2, 1, 2, 2] = [1, 2, 1, 2] := by rfl

example : compress ([] : List α) = [] := by rfl

example : compress ['C', 'o', 'o', 'o', 'p', 'y', 'y'] = ['C', 'o', 'p', 'y'] := by rfl

Problem 9

(Intermediate 🌟🌟) Pack consecutive duplicates of list elements into sublists.

variable {α : Type} [BEq α]

partial def pack (l : List α) : List (List α) :=
  sorry

-- The following codes are for test and you should not edit these.

def _root_.List.unpack (l : List (List α)) : List α :=
  match l with
  | [] => []
  | x :: xs => x ++ unpack xs

def runTest [ToString α] (l : List α) : IO Unit := do
  let result := pack l
  let check := result.unpack == l
  if check then
    IO.println "ok!"
  else
    throw <| .userError s!"failed: pack {l} = {result}"

#eval runTest ([] : List Nat)

#eval runTest [1]

#eval runTest [0, 0, 1, 0]

#eval runTest ['a', 'a', 'a', 'a', 'b', 'c', 'c', 'a', 'a', 'd', 'e', 'e', 'e', 'e']

Problem 10

(Easy 🌟) Use the result of Problem 9 to implement the so-called run-length encoding data compression method. Consecutive duplicates of elements are encoded as lists (N, E) where N is the number of duplicates of the element E.

variable {α : Type} [BEq α] [Inhabited α]

def pack (l : List α) : List (List α) :=
  sorry

def encode (l : List α) : List (Nat × α) :=
  sorry

-- The following codes are for test and you should not edit these.

example : encode [1, 1, 2, 2, 2, 3, 4, 4, 4, 4] = [(2, 1), (3, 2), (1, 3), (4, 4)] := rfl

example : encode ['a', 'a', 'b', 'c', 'c'] = [(2, 'a'), (1, 'b'), (2, 'c')] := rfl

example : encode [1, 1] = [(2, 1)] := rfl

example : encode ([] : List α) = [] := rfl

Problem 11

(Easy 🌟) Modify the result of Problem 10 in such a way that if an element has no duplicates it is simply copied into the result list. Only elements with duplicates are transferred as (N E) lists.

variable {α : Type} [BEq α]

inductive Data (α : Type) where
  | multiple : Nat → α → Data α
  | single : α → Data α
deriving Repr, DecidableEq

open Data

partial def encodeModified (l : List α) : List (Data α) :=
  sorry

-- The following codes are for test and you should not edit these.

example : encodeModified ['a', 'a', 'b', 'c'] =
  [multiple 2 'a', single 'b', single 'c'] := by native_decide

example : encodeModified ([] : List Nat) = [] := by native_decide

example : encodeModified ['a', 'b', 'b', 'b', 'c', 'b', 'b'] =
  [single 'a', multiple 3 'b', single 'c', multiple 2 'b'] := by native_decide

Problem 12

(Intermediate 🌟🌟) Given a run-length code list generated as specified in problem 11. Construct its uncompressed version.

variable {α : Type} [BEq α]

inductive Data (α : Type) where
  | multiple : Nat → α → Data α
  | single : α → Data α
deriving Repr

open Data

def decodeModified (l : List (Data α)) : List α :=
  sorry

-- The following codes are for test and you should not edit these.

example : decodeModified [multiple 2 'a', single 'b', multiple 2 'c'] = ['a', 'a', 'b', 'c', 'c'] := rfl

example : decodeModified [single 'a', single 'b', single 'c'] = ['a', 'b', 'c'] := rfl

example : decodeModified [multiple 3 '2', multiple 2 '1', single '9'] = ['2', '2', '2', '1', '1', '9'] := rfl

Problem 13

(Intermediate 🌟🌟) Implement the so-called run-length encoding data compression method directly. I.e. don't explicitly create the sublists containing the duplicates, as in Problem 9, but only count them. As in Problem 11, simplify the result list by replacing the singleton lists (1 X) by X.

variable {α : Type} [BEq α] [Inhabited α]

inductive Data (α : Type) where
  | multiple : Nat → α → Data α
  | single : α → Data α
deriving Repr

open Data

def encodeDirect (l : List α) : List (Data α) :=
  sorry

-- The following codes are for test and you should not edit these.

example : encodeDirect ['a', 'a', 'b', 'c'] =
  [multiple 2 'a', single 'b', single 'c'] := by rfl

example : encodeDirect ([] : List α) = [] := by rfl

example : encodeDirect ['a', 'b', 'b', 'b', 'c', 'b', 'b'] =
  [single 'a', multiple 3 'b', single 'c', multiple 2 'b'] := by rfl

Problem 14

(Easy 🌟) Duplicate the elements of a list.

variable {α : Type}

def dupli (l : List α) : List α :=
  sorry

-- The following codes are for test and you should not edit these.

example : dupli [1, 2, 3] = [1, 1, 2, 2, 3, 3] := by rfl

example : dupli ([] : List α) = [] := by rfl

example : dupli ['a', 'b', 'c', 'c', 'd']
  = ['a', 'a', 'b', 'b', 'c', 'c', 'c', 'c', 'd', 'd'] := by rfl

Problem 15

(Intermediate 🌟🌟) Replicate the elements of a list a given number of times.

variable {α : Type}

def repli (l : List α) (n : Nat) : List α :=
  sorry

-- The following codes are for test and you should not edit these.

example : repli [1, 2, 3] 3 = [1, 1, 1, 2, 2, 2, 3, 3, 3] := by rfl

example : repli [1, 2, 3] 2 = [1, 1, 2, 2, 3, 3] := by rfl

example : repli [1, 2, 3] 1 = [1, 2, 3] := by rfl

example : repli [1, 2, 3] 0 = [] := by rfl

example : repli ([] : List α) 255 = [] := by rfl

Problem 16

(Intermediate 🌟🌟) Drop every N'th element from a list.

variable {α : Type}

def dropEvery (l : List α) (n : Nat) : List α :=
  sorry

-- The following codes are for test and you should not edit these.

example : dropEvery [1, 2, 3] 0 = [1, 2, 3] := by rfl

example : dropEvery ['a', 'b', 'c', 'd'] 2 = ['a', 'c'] := by rfl

example : dropEvery ['a', 'b', '3', 'c', 'd', '6', 'e'] 3
  = ['a', 'b', 'c', 'd', 'e'] := by rfl

Problem 17

(Easy 🌟) Split a list into two parts; the length of the first part is given.

variable {α : Type}

-- Don't use these functions
#check List.take
#check List.drop

def split (l : List α) (n : Nat) : List α × List α :=
  sorry

-- The following codes are for test and you should not edit these.

example : split [1, 2, 3, 4, 5] 2 = ([1, 2], [3, 4, 5]) := rfl

example : split ["a"] 3 = (["a"], []) := rfl

example : split ([] : List α) 1 = ([], []) := rfl

example : split ["a", "b", "c", "d", "e", "f"] 3
  = (["a", "b", "c"], ["d", "e", "f"]) := rfl

Problem 18

(Intermediate 🌟🌟) Given two indices, i and k, the slice is the list containing the elements between the i'th and k'th element of the original list (both limits included). Start counting the elements with 1.

variable {α : Type}

def slice (l : List α) (i k : Nat) : List α :=
  sorry

-- The following codes are for test and you should not edit these.

example : slice [1, 2, 3, 4, 5, 6, 7, 8, 9] 3 7 = [3, 4, 5, 6, 7] := by rfl

example : slice [1, 2, 3, 4, 5] 1 1 = [1] := by rfl

example : slice [1, 2, 3, 4, 5] 2 3 = [2, 3] := by rfl

Problem 19

(Intermediate 🌟🌟) Rotate a list N places to the left.

variable {α : Type}

def rotate (l : List α) (n : Nat) : List α :=
  sorry

-- The following codes are for test and you should not edit these.

example : rotate [1, 2, 3, 4, 5] 2 = [3, 4, 5, 1, 2] := rfl

example : rotate [1, 2, 3] 0 = [1, 2, 3] := rfl

example : rotate [1, 2, 3] 3 = [1, 2, 3] := rfl

example : rotate [1, 2, 3] 1 = [2, 3, 1] := rfl

Problem 20

(Easy 🌟) Remove the K'th element from a list.

variable {α : Type}

def removeAt (l : List α) (n : Nat) : List α :=
  sorry

-- The following codes are for test and you should not edit these.

example : removeAt ['a', 'b', 'c', 'd'] 2 = ['a', 'c', 'd'] := rfl

example : removeAt ['a', 'b', 'c', 'd'] 5 = ['a', 'b', 'c', 'd'] := rfl

example : removeAt ['a', 'b', 'c', 'd'] 0 = ['a', 'b', 'c', 'd'] := rfl

example : removeAt ['a'] 1 = [] := rfl

example : removeAt ([] : List α) 1 = [] := rfl

Problem 21

(Easy 🌟) Insert an element at a given position into a list.

variable {α : Type}

def insertAt (e : α) (l : List α) (i : Nat) : List α :=
  sorry

-- The following codes are for test and you should not edit these.

example : insertAt "X" ["1", "2", "3", "4"] 2 = ["1", "X", "2", "3", "4"] := rfl

example : insertAt "X" ["1", "2", "3", "4"] 1 = ["X", "1", "2", "3", "4"] := rfl

example : insertAt "X" [] 1 = ["X"] := rfl

Problem 22

(Easy 🌟) Create a list containing all integers within a given range.

def range (m n : Int) : List Int :=
  sorry

-- The following codes are for test and you should not edit these.

example : range 4 9 = [4, 5, 6, 7, 8, 9] := by rfl

example : range (-1) 2 = [-1, 0, 1, 2] := by rfl

example : range (-2) (-1) = [-2, -1] := by rfl

Problem 23

(Intermediate 🌟🌟) Extract a given number of randomly selected elements from a list.

import Lean

variable {α : Type} [Inhabited α]

def rndSelect (l : List α) (n : Nat) : IO (List α) := do
  sorry

-- The following codes are for test and you should not edit these.

def runTest [BEq α] [ToString α] (l : List α) (n : Nat) : IO Unit := do
  let result ← rndSelect l n
  let check := result.length == n
    |> (· && result.all l.contains)
  if check then
    IO.println s!"ok!"
  else
    throw <| .userError s!"failed: rndSelect {l} {n} = {result}"

#eval runTest [1, 2, 3] 0

#eval runTest ['a', 'b'] 1

#eval runTest [1, 2, 3, 4, 5] 2

#eval runTest [1, 1, 1] 2

#eval runTest [2, 2, 2] 12

#eval runTest (List.range 5200) 1897

Problem 24

(Easy 🌟) Lotto: Draw N different random numbers from the set 1..M.

import Lean

/-- List of natural numbers from `1` to `n` -/
def List.nrange (n : Nat) : List Nat :=
  match n with
  | 0 => []
  | 1 => [1]
  | n + 1 => nrange n ++ [n + 1]

example : List.nrange 5 = [1, 2, 3, 4, 5] := rfl

-- You can use this function
#check List.nrange

def diffSelect (count range : Nat) : IO (List Nat) := do
  sorry

-- The following codes are for test and you should not edit these.

def runTest (count range : Nat) : IO Unit := do
  let result ← diffSelect count range
  let check := result.eraseDups.length == count
    |> (· && result.all (List.nrange range).contains)
  if check then
    IO.println "ok!"
  else
    throw <| .userError s!"failed: diffSelect {count} {range} = {result}"

#eval runTest 3 3

#eval runTest 1 1

#eval runTest 2 2

#eval runTest 6 49

#eval runTest 1998 1999

#eval runTest 5668 5998

Problem 25

(Easy 🌟) Generate a random permutation of the elements of a list.

variable {α : Type} [Inhabited α] [BEq α]

/-- Randomly removes one element from the given list
and returns the removed element and the remaining pairs of elements in the List. -/
def List.extractOne (univ : List α) : IO (Option α × List α) := do
  if univ == [] then
    return (none, [])

  let index ← IO.rand 0 (univ.length - 1)
  let element := univ.get! index
  let rest := univ.take index ++ univ.drop (index + 1)
  return (element, rest)

partial def rndPermu (l : List α) : IO (List α) := do
  sorry

-- The following codes are for test and you should not edit these.

def runTest [ToString α] (l : List α) : IO Unit := do
  let result ← rndPermu l
  let check := result.isPerm l

  if l.length >= 30 then
    let result' ← rndPermu l
    if result == result' then
      throw <| .userError "failed: Your function is not random."

  if check then
    IO.println "ok!"
  else
    throw <| .userError s!"failed: rndPermu {l} = {result}"

#eval runTest [1, 2, 3]

#eval runTest ['a', 'a', 'a']

#eval runTest ([] : List Nat)

#eval runTest (List.range 35)

Problem 26

(Intermediate 🌟🌟) Generate combinations of K distinct objects chosen from the N elements of a list.

variable {α : Type}

def List.combinations (k : Nat) (l : List α) : List (List α) :=
  sorry

-- The following codes are for test and you should not edit these.

example : [1, 2, 3, 4].combinations 2
  = [[1, 2], [1, 3], [1, 4], [2, 3], [2, 4], [3, 4]] := rfl

example : [1, 2, 3, 4].combinations 3
  = [[1, 2, 3], [1, 2, 4], [1, 3, 4], [2, 3, 4]] := rfl

example : ['a', 'b', 'c'].combinations 1
  = [['a'], ['b'], ['c']] := rfl

Problem 27

(Intermediate 🌟🌟) Group the elements of a set into disjoint subsets.

Write a function that generates all the possibilities and returns them in a list.

Note: Originally there were two questions, (a) and (b), but I omitted (a) because it is a special case of (b).

universe u
variable {α : Type}

/-- `List` is a Monad.
Since Lean does not use lazy evaluation, no Monad instance of List is defined in the Lean standard library for performance reasons. -/
instance : Monad List.{u} where
  pure := @List.pure
  bind := @List.bind
  map := @List.map

def List.split (n : Nat) (xs : List α) : List (List α × List α) :=
  sorry

#guard [1, 2].split 1 = [([1], [2]), ([2], [1])]

#guard [1, 2, 3].split 2 = [([1, 2], [3]), ([1, 3], [2]), ([2, 3], [1])]

#guard [1, 2, 3].split 3 = [([1, 2, 3], [])]

#guard [1, 2, 3].split 0 = [([], [1, 2, 3])]

def group (pattern : List Nat) (xs : List α): List <| List <| List α :=
  sorry

#guard group [1, 2] [1, 2, 3] = [[[1], [2, 3]], [[2], [1, 3]], [[3], [1, 2]]]

#guard group [2, 1] [2, 4, 6] = [[[2, 4], [6]], [[2, 6], [4]], [[4, 6], [2]]]

#guard group [1, 1] [1, 2] = [[[1], [2]], [[2], [1]]]

-- The following codes are for test and you should not edit these.

/-- pattern of 2D `List` -/
def List.pattern (xs : List (List α)) : List Nat :=
  xs.map List.length

def Nat.factorial (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * n.factorial

def runTest [ToString α] [BEq α] (pattern : List Nat) (xs : List α) : IO Unit := do
  if pattern.foldl (· + ·) 0 != xs.length then
    throw <| IO.userError s!"invalid test case: the sum of pattern should be equal to the length of the input list."

  let result := group pattern xs
  let pattern_check := result.map List.pattern
    |>.all (· = pattern)
  if not pattern_check then
    throw <| .userError s!"pattern check failed: some elements of result has invalid pattern."

  let distinct_check := result.eraseDups.length = result.length
  if not distinct_check then
    throw <| .userError s!"distinct check failed: the elements of result should be distinct."

  let expected_length := pattern.map Nat.factorial
    |>.foldl (· * ·) 1
    |> (fun x => xs.length.factorial / x)
  let length_check := result.length = expected_length
  if not length_check then
    throw <| .userError s!"length check failed: the length of result should be equal to {expected_length}."

  IO.println "OK!"

#eval runTest [1, 2, 3] <| List.range 6

#eval runTest [2, 2, 4] <| List.range 8

#eval runTest [2, 3, 4] <| List.range 9

Problem 28A

(Intermediate 🌟🌟) Sorting a list of lists according to length of sublists.

variable {α : Type}

def orderedInsert (a : α) (ord : α → Nat) : List α → List α
  | [] => [a]
  | b :: l =>
    if ord a ≤ ord b then a :: b :: l
    else b :: orderedInsert a ord l

/-- insertion sort -/
def insertionSort (ord : α → Nat) : List α → List α
  | [] => []
  | b :: l => orderedInsert b ord <| insertionSort ord l

#guard insertionSort (fun x => x) [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5]
  = [1, 1, 2, 3, 3, 4, 5, 5, 5, 6, 9]

-- You can use this!
#check insertionSort

def lsort (l : List (List α)) : List (List α) :=
  sorry

-- The following codes are for test and you should not edit these.

#guard lsort [["a", "b", "c"], ["a", "b"], ["a"]]
  = [["a"], ["a", "b"], ["a", "b", "c"]]

#guard lsort [[3, 1, 4], [1, 5, 9, 2], [6, 5, 3, 5], [1]]
  = [[1], [3, 1, 4], [1, 5, 9, 2], [6, 5, 3, 5]]

Problem 28B

(Intermediate 🌟🌟) Again, we suppose that a list contains elements that are lists themselves. But this time the objective is to sort the elements of this list according to their length frequency; i.e., in the default, where sorting is done ascendingly, lists with rare lengths are placed first, others with a more frequent length come later.

variable {α : Type}

/-- Insert an element in a way that
does not break the order of the sorted list. -/
def orderedInsert (a : α) (ord : α → Nat) : List α → List α
  | [] => [a]
  | b :: l =>
    if ord a ≤ ord b then a :: b :: l
    else b :: orderedInsert a ord l

/-- insertion sort -/
def insertionSort (ord : α → Nat) : List α → List α
  | [] => []
  | b :: l => orderedInsert b ord <| insertionSort ord l

-- You can use this!
#check insertionSort

def lfsort (l : List (List α)) : List (List α) :=
  sorry

-- The following codes are for test and you should not edit these.

#guard lfsort ([[]] : List (List String)) = [[]]

#guard lfsort [[1, 2], [1], [1, 2]] = [[1], [1, 2], [1, 2]]

#guard lfsort [[1, 2], [1], [2, 3]] = [[1], [1, 2], [2, 3]]

Problem 31

(Intermediate 🌟🌟) Determine whether a given integer number is prime.

def isPrime (n : Nat) : Bool :=
  sorry

-- The following codes are for test and you should not edit these.

example : isPrime 7 = true := rfl

example : isPrime (7 * 43) = false := rfl

example : isPrime 307 = true := rfl

example : isPrime 0 = false := rfl

example : isPrime 1 = false := rfl

Problem 32

(Intermediate 🌟🌟) Determine the greatest common divisor of two positive integer numbers. Use the Euclid's algorithm.

-- don't use this
#check Nat.gcd

/-- Euclidean algorithm -/
partial def gcd (m n : Nat) : Nat :=
  sorry

-- The following codes are for test and you should not edit these.

example : gcd 6 0 = 6 := by native_decide

example : gcd 1 37 = 1 := by native_decide

example : gcd 6 15 = 3 := by native_decide

example : gcd 21 3 = 3 := by native_decide

example : gcd 42998431 120019 = 1 := by native_decide

Problem 33

(Easy 🌟) Determine whether two positive integer numbers are coprime.

-- You can use this
#check Nat.gcd

def coprime (a b : Nat) : Bool :=
  sorry

-- The following codes are for test and you should not edit these.

example : coprime 35 64 = true := rfl

example : coprime 38859 233153 = true := rfl

example : coprime 10284412 24135577 = true := rfl

Problem 34

(Intermediate 🌟🌟) Calculate Euler's totient function φ(m).

Euler's so-called totient function φ(m) is defined as the number of positive integers r (1 <= r < m) that are coprime to m.

Example: m = 10: r = 1, 3, 7, 9; thus φ(m) = 4. Note the special case: φ(1) = 1.

def totient (m : Nat) : Nat :=
  sorry

-- The following codes are for test and you should not edit these.

example : totient 1 = 1 := rfl

example : totient 10 = 4 := rfl

example : totient 7 = 6 := rfl

example : totient 70 = 24 := rfl

Problem 35

(Intermediate 🌟🌟) Determine the prime factors of a given positive integer.

Construct a flat list containing the prime factors in ascending order.

partial def primeFactors (n : Nat) : List Nat :=
  sorry

-- The following codes are for test and you should not edit these.

example : primeFactors 17 = [17] := by native_decide

example : primeFactors 315 = [3, 3, 5, 7] := by native_decide

example : primeFactors 65536 = [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2] := by native_decide

example : primeFactors 20063 = [20063] := by native_decide

example : primeFactors 627537863 = [24137, 25999] := by native_decide

example : primeFactors 10963345907 = [104683, 104729] := by native_decide

Problem 36

(Intermediate 🌟🌟) Determine the prime factors and their multiplicities of a given positive integer.

Construct a list containing each prime factor and its multiplicity.

partial def primeFactorsMult (n : Nat) : List (Nat × Nat) :=
  sorry

-- The following codes are for test and you should not edit these.

#guard primeFactorsMult 0 = []

#guard primeFactorsMult 1 = []

#guard primeFactorsMult 2 = [(2, 1)]

#guard primeFactorsMult 315 = [(3, 2), (5, 1), (7, 1)]

#guard primeFactorsMult 307 = [(307, 1)]

#guard primeFactorsMult 1000 = [(2, 3), (5, 3)]

#guard primeFactorsMult 990801529 = [(31477, 2)]

#guard primeFactorsMult 119883030485877764933
  = [(104623, 1), (104639, 2), (104651, 1)]

Problem 37

(Intermediate 🌟🌟) Calculate Euler's totient function φ(m) (improved).

See Problem 34 for the definition of Euler's totient function. If the list of the prime factors of a number m is known in the form of Problem 36 then the function φ(m) can be efficiently calculated as follows: Let [(p₁, m₁), (p₂, m₂), (p₃, m₃), ...] be the list of prime factors (and their multiplicities) of a given number m. Then φ(m) can be calculated with the following formula:

$$ φ(m) = ∏_{i=1}^{n} (p_i - 1) * p_i^{(m_i - 1)} $$

/-- the list of prime factors and their multiplicities of `n` -/
abbrev PrimeFactor := List (Nat × Nat)

def φ (_n : Nat) (factors : PrimeFactor) : Nat :=
  sorry

-- The following codes are for test and you should not edit these.

#guard φ 10 [(2, 1), (5, 1)] = 4

#guard φ 20 [(2, 2), (5, 1)] = 8

#guard φ 39 [(3, 1), (13, 1)] = 24

Problem 39

(Easy 🌟) Given a range of integers by its lower and upper limit, construct a list of all prime numbers in that range.

/-- eratosthenes sieve -/
def eratosthenes (n : Nat) : Array Bool := Id.run do
  let mut isPrime := Array.mkArray (n + 1) true

  isPrime := isPrime.set! 0 false
  isPrime := isPrime.set! 1 false

  for p in [2 : n + 1] do
    if not isPrime[p]! then
      continue

    if p ^ 2 > n then
      break

    let mut q := p * p
    while q <= n do
      isPrime := isPrime.set! q false
      q := q + p

  return isPrime


def primesR (s t : Nat) : List Nat :=
  sorry

-- The following codes are for test and you should not edit these.

#guard primesR 10 10 = []

#guard primesR 11 11 = [11]

#guard primesR 1 10 = [2, 3, 5, 7]

#guard primesR 30 100 = [31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97]

Problem 40

(Intermediate 🌟🌟) Goldbach's conjecture says that every positive even number greater than 2 is the sum of two prime numbers. Example: 28 = 5 + 23. It is one of the most famous facts in number theory that has not been proved to be correct in the general case. It has been numerically confirmed up to very large numbers (much larger than we can go with our Prolog system). Write a predicate to find the two prime numbers that sum up to a given even integer.

def Nat.isPrime (n : Nat) : Bool := Id.run do
  if n ≤ 2 then
    return false
  for d in [2:n] do
    if n % d = 0 then
      return false
    if d ^ 2 > n then
      break
  return true

-- You can use this!
#check Nat.isPrime

def goldbach (n : Nat) : Nat × Nat := Id.run do
  sorry

-- The following codes are for test and you should not edit these.

def goldbachTest (n : Nat) : IO Unit :=
  let (fst, snd) := goldbach n
  if fst + snd ≠ n then
    throw <| .userError s!"failed: {fst} + {snd} ≠ {n}"
  else if ! fst.isPrime || ! snd.isPrime then
    throw <| .userError s!"failed: {fst} and {snd} must be prime."
  else
    IO.println s!"ok! {n} = {fst} + {snd}"

#eval goldbachTest 14

#eval goldbachTest 308

#eval goldbachTest 308000

#eval goldbachTest 19278020

Problem 40

(Intermediate 🌟🌟) A list of even numbers and their Goldbach compositions in a given range.

def Nat.isPrime (n : Nat) : Bool := Id.run do
  if n ≤ 2 then
    return false
  for d in [2:n] do
    if n % d = 0 then
      return false
    if d ^ 2 > n then
      break
  return true

def goldbach (n : Nat) : Nat × Nat := Id.run do
  for cand in [2:n] do
    if not cand.isPrime then
      continue
    let rest := n - cand
    if not rest.isPrime then
      continue
    return (cand, rest)

  panic! "we've found a counter example of goldbach conjecture!! 🎉"

def goldbachList (lower upper : Nat) (primeLower : Nat := 2) : List (Nat × Nat) :=
  sorry

-- The following codes are for test and you should not edit these.

#guard goldbachList 9 20 == [(3, 7), (5, 7), (3, 11), (3, 13), (5, 13), (3, 17)]

#guard goldbachList 9 20 3 == [(5, 7), (5, 13)]

#guard goldbachList 4 2000 50 == [(73,919),(61,1321),(67,1789),(61,1867)]

Problem 46

(Intermediate 🌟🌟) Truth tables for logical expressions.

def table (p : Bool → Bool → Bool) : List (List Bool) :=
  sorry

-- The following codes are for test and you should not edit these.

#guard table (fun a b => And a (Or a b)) ==
  [
    [true, true, true],
    [true, false, true],
    [false, true, false],
    [false, false, false]
  ]

Problem 47

(Easy 🌟) Truth tables for logical expressions (part 2).

def table (p : Bool → Bool → Bool) : List (List Bool) :=
  sorry

-- The following codes are for test and you should not edit these.

#guard table (fun a b => a && (a || b)) ==
  [
    [true, true, true],
    [true, false, true],
    [false, true, false],
    [false, false, false]
  ]

Problem 48

(Easy 🌟) Truth tables for logical expressions (part 3).

Generalize Problem 47 in such a way that the logical expression may contain any number of logical variables. Define table/2 in a way that table(List,Expr) prints the truth table for the expression Expr, which contains the logical variables enumerated in List.

universe u

/-- monad instance of `List` -/
instance : Monad List.{u} where
  pure := @List.pure
  bind := @List.bind
  map := @List.map

def Arity : (n : Nat) → Type
  | 0 => Bool
  | n + 1 => Bool → Arity n

def tablen (n : Nat) (p : Arity n) : List (List Bool) :=
  sorry

-- The following codes are for test and you should not edit these.

#guard tablen 1 (fun a => a) = [[true, true], [false, false]]

#guard tablen 2 (fun a b => a && b) = [
  [true, true, true],
  [true, false, false],
  [false, true, false],
  [false, false, false]
]

#guard tablen 2 (fun a b => !a || b) = [
  [true, true, true],
  [true, false, false],
  [false, true, true],
  [false, false, true]
]

#guard tablen 3 (fun a b c => a && b && c) = [
  [true, true, true, true],
  [true, true, false, false],
  [true, false, true, false],
  [true, false, false, false],
  [false, true, true, false],
  [false, true, false, false],
  [false, false, true, false],
  [false, false, false, false]
]

Problem 49

(Intermediate 🌟🌟) Gray codes.

An n-bit Gray code is a sequence of n-bit strings constructed according to certain rules. For example,

n = 1: C(1) = ['0','1'].
n = 2: C(2) = ['00','01','11','10'].
n = 3: C(3) = ['000','001','011','010','110','111','101','100'].

Find out the construction rules and write a predicate with the following specification:

% gray(N,C) :- C is the N-bit Gray code

Can you apply the method of "result caching" in order to make the predicate more efficient, when it is to be used repeatedly?

inductive Digit : Type where
  | zero
  | one
deriving DecidableEq

abbrev GrayCode := List Digit

def Digit.toString : Digit → String
  | .zero => "0"
  | .one => "1"

instance : OfNat Digit 0 where
  ofNat := Digit.zero

instance : OfNat Digit 1 where
  ofNat := Digit.one

instance : ToString Digit where
  toString := Digit.toString

def gray (n : Nat) : List GrayCode :=
  sorry

-- The following codes are for test and you should not edit these.

#guard gray 1 = [[0], [1]]

#guard gray 2 = [[0, 0], [0, 1], [1, 1], [1, 0]]

#guard gray 3 = [
  [0, 0, 0],
  [0, 0, 1],
  [0, 1, 1],
  [0, 1, 0],
  [1, 1, 0],
  [1, 1, 1],
  [1, 0, 1],
  [1, 0, 0]
]

Problem 50

(Hard 🌟🌟🌟) Huffman codes.

We suppose a set of symbols with their frequencies, given as a list of fr(S,F) terms.

Example: [fr(a,45), fr(b,13), fr(c,12), fr(d,16), fr(e,9), fr(f,5)].

Our objective is to construct a list hc(S,C) terms, where C is the Huffman code word for the symbol S.

/-- Insert an element in a way that
does not break the order of the sorted list. -/
def orderedInsert {α : Type} [Ord α] (a : α) : List α → List α
  | [] => [a]
  | b :: l =>
    match compare a b with
    | .lt => a :: b :: l
    | _ => b :: orderedInsert a l

/-- insertion sort -/
def insertionSort {α : Type} [Ord α] : List α → List α
  | [] => []
  | b :: l => orderedInsert b (insertionSort l)

-- You can use this!
#check insertionSort


/-- Huffman Tree -/
inductive HuffTree where
  | 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

def HuffTree.compare (s s' : HuffTree) : Ordering :=
  let w := s.weight
  let w' := s'.weight
  Ord.compare w w'

instance : Ord HuffTree where
  compare := HuffTree.compare

def HuffTree.sort (trees : List HuffTree) : List HuffTree := insertionSort trees

abbrev Code := String

def huffman (input : List (Char × Nat)) : List (Char × Code) :=
  sorry

-- The following codes are for test and you should not edit these.

#guard huffman [('a', 45),('b', 13),('c', 12),('d', 16),('e', 9),('f', 5)] =
  [('a', "0"),('b', "101"),('c', "100"),('d', "111"),('e', "1101"),('f', "1100")]

#guard huffman [('B', 7),('C', 6),('A', 3),('D', 1),('E', 1),] =
  [('B', "0"), ('C', "11"), ('A', "101"), ('D', "1001"), ('E', "1000")]

Problem 55

(Intermediate 🌟🌟) Construct completely balanced binary trees.

In a completely balanced binary tree, the following property holds for every node: The number of nodes in its left subtree and the number of nodes in its right subtree are almost equal, which means their difference is not greater than one.

Write a function cbalTree to construct completely balanced binary trees for a given number of nodes. The predicate should generate all solutions via backtracking.

inductive BinTree (α : Type) where
  | empty : BinTree α
  | node : α → BinTree α → BinTree α → BinTree α
deriving Repr

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

def BinTree.isBalanced {α : Type} : BinTree α → Bool
  | .empty => true
  | .node _ l r =>
    l.isBalanced ∧ r.isBalanced ∧
    Int.natAbs ((l.depth : Int) - (r.depth : Int)) ≤ 1

/-- 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

-- The following codes are for test and you should not edit these.

#eval (cbalTree 3).length = 1
#eval (cbalTree 3)|>.map BinTree.isBalanced |>.and
#eval (cbalTree 4)|>.map BinTree.isBalanced |>.and
#eval (cbalTree 4).length = 4
#eval (cbalTree 5)|>.map BinTree.isBalanced |>.and
#eval (cbalTree 6)|>.map BinTree.isBalanced |>.and
#eval (cbalTree 7).length = 1

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

def BinTree.isSymmetric (t : BinTree α) : Bool :=
  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'))

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

def BinTree.searchTreeFromList [Ord α] (xs : List α) : BinTree α :=
  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

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

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

-- 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

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

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

-- The following codes are for test and you should not edit these.

#guard (hbalTrees 2 |>.length) = 2
#guard (hbalTrees 3 |>.length) = 4