Task 139

HumanEvalLean/HumanEval139.lean

@@ -1,5 +1,62 @@
-def special_factorial : Unit :=
-  ()
+-- from Mathlib
+def Nat.factorial : Nat → Nat
+  | 0 => 1
+  | .succ n => Nat.succ n * factorial n
+
+notation:10000 n "!" => Nat.factorial n
+
+def Nat.brazilianFactorial : Nat → Nat
+    | .zero => 1
+    | .succ n => (Nat.succ n)! * brazilianFactorial n
+
+def special_factorial (n : Nat) : Nat :=
+    special_factorial.go n 1 1 0
+    where
+
+    go (n fact brazilFact curr : Nat) : Nat :=
+        if _h: curr >= n
+        then brazilFact
+        else
+            let fact' := (curr + 1) * fact
+            let brazilFact' := brazilFact * fact'
+            special_factorial.go n fact' brazilFact' (Nat.succ curr)
+    termination_by n - curr
+
+theorem special_factorial_func_correct {n : Nat} :
+        special_factorial n = n.brazilianFactorial := by
+    simp [special_factorial]
+    suffices ∀ (curr fact brazilFact : Nat), fact = curr ! → brazilFact = curr.brazilianFactorial →
+        curr ≤ n → special_factorial.go n fact brazilFact curr = n.brazilianFactorial by
+        apply this
+        · simp [Nat.factorial]
+        · simp [Nat.brazilianFactorial]
+        · simp
+    intro curr
+    induction h: n - curr generalizing curr with
+    | zero =>
+        intro _ brazil _ hbrazil hcurr
+        rw [Nat.sub_eq_zero_iff_le] at h
+        have : n = curr := by omega
+        simp [special_factorial.go, h, this, hbrazil]
+    | succ m ih =>
+        intro fact brazilFact hfact hbrazil hcurr
+        have : ¬ curr ≥ n := by omega
+        unfold special_factorial.go
+        simp only [ge_iff_le, this, ↓reduceDIte, Nat.succ_eq_add_one]
+        have : n - (curr + 1) = m := by omega
+        specialize ih (curr + 1) this ((curr + 1) * fact) (brazilFact * ((curr + 1) * fact))
+        simp only [hfact, Nat.factorial, Nat.succ_eq_add_one, hbrazil, Nat.brazilianFactorial,
+          forall_const] at ih
+        simp only [hfact, hbrazil]
+        apply ih
+        · -- omega does not work
+          rw [Nat.mul_comm, Nat.mul_assoc]
+        · omega
+
+theorem test1 : special_factorial 4 = 288 := by native_decide
+theorem test2 : special_factorial 5 = 34560 := by native_decide
+theorem test3 : special_factorial 7 = 125411328000 := by native_decide
+theorem test4 : special_factorial 1 = 1 := by native_decide
 
 /-!
 ## Prompt
@@ -45,4 +102,4 @@ def check(candidate):
     assert candidate(1) == 1, "Test 1"
 
 ```
--/
+-/