From a0ae97cba86ef726f216ff0dce29d143ce16eb76 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Thu, 28 Mar 2024 01:22:15 +0900
Subject: [PATCH] add P25

---
 Src/Problem25.lean | 58 ++++++++++++++++++++++++++++++++++++++++++++++
 md/SUMMARY.md      |  1 +
 2 files changed, 59 insertions(+)
 create mode 100644 Src/Problem25.lean

diff --git a/Src/Problem25.lean b/Src/Problem25.lean
new file mode 100644
index 0000000..aa7293e
--- /dev/null
+++ b/Src/Problem25.lean
@@ -0,0 +1,58 @@
+/-
+# Problem 25
+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)
+
+def rndPermu (l : List α) : IO (List α) := do
+  -- sorry
+  let (element, rest) ← l.extractOne
+  match element with
+  | none => return []
+  | some e =>
+    return e :: (← rndPermu rest)
+  -- sorry
+
+  -- Avoid proving that the function terminates as a recursive function.
+  -- You don't have to fill in the `sorry` here.
+  decreasing_by 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 mut check := true
+  check := 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)
diff --git a/md/SUMMARY.md b/md/SUMMARY.md
index 559a832..632e414 100644
--- a/md/SUMMARY.md
+++ b/md/SUMMARY.md
@@ -34,6 +34,7 @@
 * [22: Integers within a range](./build/Problem22.md)
 * [23: Random selection](./build/Problem23.md)
 * [24: Draw N diffrent random numbers](./build/Problem24.md)
+* [25: Random permutation](./build/Problem25.md)
 
 # 31-40: Arithmetic