44

Author: TwoFX

HumanEvalLean/HumanEval44.lean

@@ -1,7 +1,25 @@
 module
 
-def change_base : Unit :=
-  ()
+def changeBase (x : Nat) (base : Nat) : String :=
+  String.ofList (Nat.toDigits base x)
+
+example : changeBase 8 3 = "22" := by native_decide
+example : changeBase 9 3 = "100" := by native_decide
+example : changeBase 234 2 = "11101010" := by native_decide
+example : changeBase 16 2 = "10000" := by native_decide
+example : changeBase 8 2 = "1000" := by native_decide
+example : changeBase 7 2 = "111" := by native_decide
+
+namespace Nat
+
+theorem ofDigitChars_toDigits' {b n : Nat} (hb' : 1 < b) (hb : b ≤ 10) : ofDigitChars b (toDigits b n) 0 = n := by
+  sorry -- https://github.com/leanprover/lean4/pull/13098
+
+end Nat
+
+theorem ofDigitChars_changeBase {x : Nat} {base : Nat} (hb' : 1 < base) (hb : base ≤ 10) :
+    Nat.ofDigitChars base (changeBase x base).toList 0 = x := by
+  simp [changeBase, Nat.ofDigitChars_toDigits' hb' hb]
 
 /-!
 ## Prompt
@@ -51,4 +69,4 @@ def check(candidate):
         assert candidate(x, x + 1) == str(x)
 
 ```
--/
+-/