Lean 99: Ninety-Nine Lean Probelms
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 Probelms.
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 α
section
/-!
## Pretty printing of NestedList
Display `NestedList` in a readable manner when you run `#eval`.
When solving this problem, **do not mind** the contents of this section.
The following code was provided by Mario Carneiro.
-/
open Std in
partial def NestedList.repr [Repr α] (a : NestedList α) (n : Nat) : Format :=
let _ : ToFormat (NestedList α) := ⟨(NestedList.repr · 0)⟩
match a, n with
| elem x, _ => reprPrec x n
| list as, _ => Format.bracket "[" (Format.joinSep as ("," ++ Format.line)) "]"
instance [Repr α] : Repr (NestedList α) where
reprPrec := NestedList.repr
end
/-- 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] := rfl
example : flatten sample = [1, 2, 3, 4] := rfl
example : flatten (empty) = [] := 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 List.isPerm [BEq α] : List α → List α → Bool
| [], l₂ => l₂.isEmpty
| a :: l₁, l₂ => l₂.contains a && l₁.isPerm (l₂.erase a)
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 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