Task 139 (#178)

* Solution

* Fix intendation

* Rewrite proof with fun_induction

* Remove accidently added solution+

* Revert 63 completely

---------

Co-authored-by: Markus Himmel <markus@lean-fro.org>

Author: jt0202

HumanEvalLean/HumanEval139.lean

@@ -1,5 +1,67 @@
-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
+
+@[simp] theorem Nat.factorial_zero : 0! = 1 :=
+  rfl
+
+theorem Nat.factorial_succ (n : Nat) : (n + 1)! = (n + 1) * n ! :=
+  rfl
+
+def Nat.brazilianFactorial : Nat → Nat
+  | .zero => 1
+  | .succ n => (Nat.succ n)! * brazilianFactorial n
+
+@[simp] theorem Nat.brazilianFactorial_zero : brazilianFactorial 0 = 1 :=
+  rfl
+
+theorem Nat.brazilianFactorial_succ (n : Nat) : brazilianFactorial (n + 1) = (n + 1)! * (brazilianFactorial n) :=
+  rfl
+
+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' := fact' * brazilFact
+      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 fact brazil_fact h₁ h₂ h₃
+  fun_induction special_factorial.go with
+  | case1 fact brazil_fact curr h =>
+    rw [h₂]
+    unfold special_factorial.go
+    simp [h]
+    have : curr = n := by omega
+    rw [this]
+  | case2 fact brazilFact curr h fact' brazilFact' ih =>
+    simp only [ge_iff_le, Nat.not_le] at h
+    simp only [h₁, Nat.succ_eq_add_one, Nat.factorial_succ, h₂, Nat.brazilianFactorial_succ,
+      Nat.succ_le_of_lt h, forall_const, fact', brazilFact'] at ih
+    have : ¬ curr >= n := by omega
+    unfold special_factorial.go
+    simp [this, h₁, h₂, ih]
+
+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 +107,4 @@ def check(candidate):
     assert candidate(1) == 1, "Test 1"
 
 ```
--/
+-/