early return

Author: datokrat

HumanEvalLean/HumanEval59.lean

@@ -32,9 +32,12 @@ def largestPrimeFactor (n : Nat) : Nat := Id.run do
     let mut m : { m : Nat // 0 < m } := ⟨n, hn⟩
     let mut mostRecentFactor := 1
     for hd : d in 2...=n do
-      if d ∣ m.val then
-        mostRecentFactor := d
-        m := dividePower m d (by grind [Rcc.mem_iff])
+      if d * d ≤ m then
+        if d ∣ m.val then
+          mostRecentFactor := d
+          m := dividePower m d (by grind [Rcc.mem_iff])
+      else
+        return max mostRecentFactor m
     return mostRecentFactor
   else
     return 1
@@ -87,7 +90,7 @@ theorem largestPrimeFactor_dvd :
   apply Id.of_wp_run_eq hwp
   mvcgen
   invariants
-  · ⇓⟨cur, m, factor⟩ => ⌜factor ∣ n ∧ m.val ∣ n⌝
+  · .withEarlyReturn (fun cur ⟨m, factor⟩ => ⌜factor ∣ n ∧ m.val ∣ n⌝) (fun ret ⟨m, factor⟩ => ⌜ret ∣ n⌝)
   with grind [dividePower_dvd, Nat.dvd_trans, Nat.dvd_refl]
 
 theorem dvd_or_dvd_of_dvd_self_div_dividePower {e : Nat} (h : m.val ∣ n)
@@ -123,30 +126,34 @@ theorem isPrime_largestPrimeFactor (h : 1 < n) :
   apply Id.of_wp_run_eq hwp
   mvcgen
   invariants
-  · ⇓⟨cur, m, factor⟩ =>
+  · .withEarlyReturn
+    (fun cur ⟨m, factor⟩ =>
       ⌜let i := cur.pos + 2;
         factor < i ∧
           m.val ∣ n ∧
           (if m.val = n then factor = 1 else IsPrime factor ∧ ∀ e : Nat, e ∣ n / m → IsPrime e → e ≤ factor) ∧
-          ∀ e : Nat, e ∣ m → e = 1 ∨ i ≤ e⌝
-  case vc1 pref cur suf _ _ m _ _ ih =>
-    refine ⟨?_, ?_, ?_, ?_⟩
+          ∀ e : Nat, e ∣ m → e = 1 ∨ i ≤ e⌝)
+    (fun ret ⟨m, factor⟩ => ⌜IsPrime ret ∧ ∀ d : Nat, d ∣ n → IsPrime d → d ≤ ret⌝)
+  case vc1 pref cur suf _ _ _ m _ _ _ ih =>
+    simp only [reduceCtorEq, false_and, exists_false, or_false]
+    refine ⟨?_, ?_, ?_, ?_, ?_⟩
+    · grind
     · grind
     · grind [dividePower_dvd, Nat.dvd_trans]
     · simp at *
       have : (dividePower m cur (by grind)).val < m.val := dividePower_lt (by grind)
-      have : m.val ≤ n := Nat.le_of_dvd ‹0 < n› ih.2.1
+      have : m.val ≤ n := Nat.le_of_dvd ‹0 < n› ih.2.2.1
       rw [if_neg (by grind)]
       constructor
       · rw [IsPrime]
         constructor
         · grind
         · intro d hd
-          have := ih.2.2.2 d (by grind [Nat.dvd_trans])
+          have := ih.2.2.2.2 d (by grind [Nat.dvd_trans])
           have : d ≤ cur := Nat.le_of_dvd (by grind) hd
           grind
       · intro e he hep
-        have := ih.2.2.1
+        have := ih.2.2.2.1
         replace he := dvd_or_dvd_of_dvd_self_div_dividePower (by grind) he hep
         split at this
         · have : m = ⟨n, ‹_›⟩ := by grind
@@ -159,20 +166,24 @@ theorem isPrime_largestPrimeFactor (h : 1 < n) :
           cases he
           · grind
           · exact Nat.le_of_dvd (by grind) ‹_›
-    · intro e he
+    · simp at *
+      intro e he
       have : e ≠ cur := by grind [not_dvd_dividePower]
-      replace ih := ih.2.2.2 e
+      replace ih := ih.2.2.2.2 e
       grind [dividePower_dvd, Nat.dvd_trans]
-  case vc2 pref cur suf _ _ _ _ _ ih =>
+  case vc2 pref cur suf _ _ _ _ _ _ _ ih =>
+    simp only [List.Cursor.pos_mk, true_and, reduceCtorEq, false_and, exists_const, or_false]
+    simp only [List.Cursor.pos_mk, reduceCtorEq, false_and, and_false, exists_const, or_false] at ih
     refine ⟨?_, ?_, ?_, ?_⟩
     · grind
     · grind
     · grind
     · intro e he
       have : e ≠ cur := by grind
-      replace ih := ih.2.2.2 e
+      replace ih := ih.2.2.2.2 e
       grind
-  case vc3 =>
+  case vc4 =>
+    simp only [List.Cursor.pos_mk, true_and, reduceCtorEq, false_and, exists_const, or_false]
     refine ⟨?_, ?_, ?_, ?_⟩
     · grind
     · grind [Nat.dvd_refl]
@@ -181,15 +192,58 @@ theorem isPrime_largestPrimeFactor (h : 1 < n) :
       intro e he
       have : 0 < e := Nat.pos_of_dvd_of_pos he ‹0 < n›
       grind
-  case vc4 r ih =>
+  case vc5 r _ ih =>
     simp at *
+    simp_all
     have := ih.2.2.2 _ (Nat.dvd_refl _)
-    have : r.fst.val ≤ n := Nat.le_of_dvd ‹0 < n› ih.2.1
-    have : r.fst.val = 1 := by grind
+    have : r.2.1.val ≤ n := Nat.le_of_dvd ‹0 < n› ih.2.1
+    have : r.2.1.val = 1 := by grind
     have := ih.2.2.1
     rw [if_neg (by grind)] at this
     simpa [*] using this
-  case vc5 => grind
+  case vc7 => grind
+  -- Early return verification conditions:
+  case vc3 pref cur suff _ _ _ m _ hlt ih =>
+    simp_all
+    rw [max_eq_if]
+    split
+    · constructor
+      · grind
+      · intro d hd hdp
+        rw [if_neg (by grind)] at ih
+        rw [← show n / m.val * m.val = n from Nat.div_mul_cancel (by grind)] at hd
+        rw [hdp.dvd_mul_iff] at hd
+        cases hd
+        · grind
+        · have := ih.2.2.2.2 d ‹_›
+          cases this
+          · grind
+          · have : cur ≤ d := by grind
+            have : m.val / d ∣ m.val := Nat.div_dvd_of_dvd ‹_›
+            have : m.val / d < cur := by
+              rw [Nat.div_lt_iff_lt_mul (by grind)]
+              exact Nat.lt_of_lt_of_le hlt (Nat.mul_le_mul_left cur ‹_›)
+            have := ih.2.2.2.2 (m.val / d) ‹_›
+            cases this
+            · rename_i h
+              rw [Nat.div_eq_iff_eq_mul_left (by grind) (by grind)] at h
+              grind
+            · grind
+    · constructor
+      · rw [isPrime_iff_mul_self]
+        constructor
+        · grind [IsPrime]
+        · intro e he he'
+          refine Nat.lt_of_lt_of_le hlt ?_
+          have := ih.2.2.2.2 e he'
+          exact Nat.mul_self_le_mul_self (by grind)
+      · intro d hd hdp
+        rw [← show n / m.val * m.val = n from Nat.div_mul_cancel (by grind)] at hd
+        rw [hdp.dvd_mul_iff] at hd
+        cases hd
+        · grind [Nat.div_self, Nat.dvd_one]
+        · exact Nat.le_of_dvd (by grind) ‹_›
+  case vc6 => grind
 
 /-!
 ## Prompt