Rewrite proof with fun_induction

Author: jt0202

HumanEvalLean/HumanEval139.lean

@@ -5,20 +5,31 @@ def Nat.factorial : Nat → Nat
 
 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
-
+where
   go (n fact brazilFact curr : Nat) : Nat :=
     if _h: curr >= n
     then brazilFact
     else
       let fact' := (curr + 1) * fact
-      let brazilFact' := brazilFact * fact'
+      let brazilFact' := fact' * brazilFact
       special_factorial.go n fact' brazilFact' (Nat.succ curr)
   termination_by n - curr
 
@@ -31,26 +42,21 @@ theorem special_factorial_func_correct {n : Nat} :
       · 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
+  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 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
-    · ac_rfl
-    · omega
+    simp [this, h₁, h₂, ih]
 
 theorem test1 : special_factorial 4 = 288 := by native_decide
 theorem test2 : special_factorial 5 = 34560 := by native_decide

HumanEvalLean/HumanEval63.lean

@@ -1,5 +1,88 @@
-def fibfib : Unit :=
-  ()
+def fibfib (n : Nat): Nat :=
+  match n with
+  | 0 => 0
+  | 1 => 0
+  | 2 => 1
+  | (n+3) => fibfib (n+2) + fibfib (n+1) + fibfib n
+
+theorem fibfib_of_three_le {n : Nat} (hn : 3 ≤ n) :
+    fibfib n = fibfib (n - 1) + fibfib (n -2) + fibfib (n - 3) := by
+  conv =>
+    lhs
+    unfold fibfib
+  cases n with
+  | zero => simp at hn
+  | succ m =>
+    cases m with
+    | zero => simp at hn
+    | succ n =>
+      cases n with
+      | zero => simp at hn
+      | succ m =>
+        simp
+
+def computeFibfib (n : Nat) : Nat :=
+  match n with
+  | 0 => 0
+  | 1 => 0
+  | 2 => 1
+  | (m + 3) => go (m + 3) 1 0 0 3 where
+
+  go (m prev1 prev2 prev3 curr : Nat) : Nat :=
+    if curr ≥ m
+    then prev1 + prev2 + prev3
+    else go m (prev1 + prev2 + prev3) prev1 prev2 (curr + 1)
+  termination_by m - curr
+
+theorem testCase1 : computeFibfib 2 = 1 := by native_decide
+theorem testCase2 : computeFibfib 1 = 0 := by native_decide
+theorem testCase3 : computeFibfib 5 = 4 := by native_decide
+theorem testCase4 : computeFibfib 8 = 24 := by native_decide
+theorem testCase5 : computeFibfib 10 = 81 := by native_decide
+theorem testCase6 : computeFibfib 12 = 274 := by native_decide
+theorem testCase7 : computeFibfib 14 = 927 := by native_decide
+
+theorem computeFibfib_correct (n : Nat) : computeFibfib n = fibfib n := by
+  unfold computeFibfib
+  unfold fibfib
+  cases n with
+  | zero => simp[fibfib]
+  | succ m =>
+    cases m with
+    | zero => simp[fibfib]
+    | succ n =>
+      cases n with
+      | zero => simp[fibfib]
+      | succ m =>
+        simp only
+        suffices ∀ (m curr prev1 prev2 prev3 : Nat), 3 ≤ curr → curr ≤ m → prev1 = fibfib (curr - 1) →
+          prev2 = fibfib (curr - 2) → prev3 = fibfib (curr - 3) →
+            computeFibfib.go m prev1 prev2 prev3 curr = fibfib (m - 1) + fibfib (m - 2) + fibfib (m-3) by
+          apply this
+          · omega
+          · omega
+          · simp [fibfib]
+          · simp [fibfib]
+          · simp [fibfib]
+        intro m curr
+        induction h : m - curr generalizing curr with
+        | zero =>
+          simp [Nat.sub_eq_zero_iff_le] at h
+          intro prev1 prev2 prev3 hcurr1 hcurr2 hprev1 hprev2 hprev3
+          have : curr = m := by omega
+          simp [computeFibfib.go, this, hprev1, hprev2, hprev3]
+        | succ n ih =>
+          intro prev1 prev2 prev3 hcurr1 hcurr2 hprev1 hprev2 hprev3
+          unfold computeFibfib.go
+          have : ¬ curr ≥ m := by omega
+          simp only [ge_iff_le, this, ↓reduceIte]
+          apply ih
+          · omega
+          · omega
+          · omega
+          · simp [fibfib_of_three_le, hcurr1, hprev1, hprev2, hprev3]
+          · simp [hprev1]
+          · simp [hprev2]
 
 /-!
 ## Prompt
@@ -53,4 +136,4 @@ def check(candidate):
     assert candidate(14) == 927
 
 ```
--/
+-/