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
sorrywith 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}
-- You can use this!
#check List.mergeSort
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}
-- You can use this!
#check List.mergeSort
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 41
(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.
warning
A completely balanced binary tree is not the same as a (hight) balanced binary tree.
inductive BinTree (α : Type) where
| empty : BinTree α
| node : α → BinTree α → BinTree α → BinTree α
deriving Repr
def leaf {α : Type} (a : α) : BinTree α := .node a .empty .empty
def BinTree.nodes {α : Type} : BinTree α → Nat
| .empty => 0
| .node _ l r => 1 + l.nodes + r.nodes
def BinTree.isCBalanced {α : Type} : BinTree α → Bool
| .empty => true
| .node _ l r =>
Int.natAbs ((l.nodes : Int) - (r.nodes : Int)) ≤ 1 && l.isCBalanced && r.isCBalanced
/-- monad instance of `List` -/
instance : Monad List where
pure := @List.pure
bind := @List.bind
map := @List.map
/-- construct all completely 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.isCBalanced |>.and
#eval (cbalTree 4)|>.map BinTree.isCBalanced |>.and
#eval (cbalTree 4).length = 4
#eval (cbalTree 5)|>.map BinTree.isCBalanced |>.and
#eval (cbalTree 6)|>.map BinTree.isCBalanced |>.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 <| [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}
section
/- pretty print of binary tree -/
variable [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⟩
end
#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