Paul/58

.gitignore

@@ -1 +1,2 @@
 /.lake
+**/.DS_Store

HumanEvalLean/Common/IsPrime.lean

@@ -78,3 +78,12 @@ public theorem isPrime_eq_true_iff_isPrime {n : Nat} :
     grind
   -- `mem_toList_iff_mem` and `mem_iff` should be simp lemmas
   simp [hn, isPrime_iff_mul_self, Std.Rco.mem_toList_iff_mem, Std.Rco.mem_iff]
+
+public theorem IsPrime.dvd_mul_iff (h : IsPrime d) :
+    d ∣ a * b ↔ d ∣ a ∨ d ∣ b := by
+  constructor
+  · by_cases d ∣ a
+    · grind
+    · have : Nat.Coprime d a := by grind [IsPrime, Nat.gcd_dvd_left, Nat.gcd_dvd_right]
+      exact Or.inr ∘ this.dvd_of_dvd_mul_left
+  · grind

HumanEvalLean/HumanEval58.lean

@@ -1,7 +1,39 @@
 module
 
-def common : Unit :=
-  ()
+public import Std
+open Std
+
+public section
+
+/-! ## Implementation -/
+
+def common (xs ys : List Nat) : List Nat :=
+  let xsSet : TreeSet Nat := .ofList xs
+  let ysSet : TreeSet Nat := .ofList ys
+  ysSet.filter (· ∈ xsSet) |>.toList
+
+/-! ## Tests -/
+
+set_option cbv.warning false
+
+example : common [1, 4, 3, 34, 653, 2, 5] [5, 7, 1, 5, 9, 653, 121] = [1, 5, 653] := by cbv
+example : common [5, 3, 2, 8] [3, 2] = [2, 3] := by cbv
+example : common [4, 3, 2, 8] [3, 2, 4] = [2, 3, 4] := by cbv
+example : common [4, 3, 2, 8] [] = [] := by cbv
+
+/-! ## Verification -/
+
+theorem pairwise_lt_common :
+    (common xs ys).Pairwise (· < ·) := by
+  grind [common, TreeSet.ordered_toList, compare_eq_lt]
+
+theorem distinct_common :
+    (common xs ys).Pairwise (· ≠ ·) := by
+  grind [common, TreeSet.distinct_toList]
+
+theorem mem_common_iff :
+    x ∈ common xs ys ↔ x ∈ xs ∧ x ∈ ys := by
+  grind [common]
 
 /-!
 ## Prompt
@@ -45,4 +77,4 @@ def check(candidate):
     assert candidate([4, 3, 2, 8], []) == []
 
 ```
--/
+-/

HumanEvalLean/HumanEval59.lean

@@ -1,7 +1,269 @@
 module
 
-def largest_prime_factor : Unit :=
-  ()
+public import Std
+public import HumanEvalLean.Common.IsPrime
+import Init.Data.Nat.Coprime
+open Std Std.Do
+
+set_option mvcgen.warning false
+
+public section
+
+/-! ## Implementation -/
+
+/--
+Given natural numbers `n ≥ 1` and a `d ≥ 2`, returns `n / d ^ i` with the largest possible `i`
+for which `d ^ i ∣ n`.
+-/
+def dividePower (n : { n : Nat // 0 < n }) (d : Nat) (hd : 1 < d) : { n : Nat // 0 < n} :=
+  if hd' : d ∣ n.val then
+    dividePower ⟨n.val / d, by grind [Nat.eq_zero_of_dvd_of_div_eq_zero]⟩ d hd
+  else
+    n
+termination_by n.val
+decreasing_by
+  rwa [Nat.div_lt_iff_lt_mul (by grind), Nat.lt_mul_iff_one_lt_right (by grind)]
+
+/--
+Returns the largest prime factor of a given number by iteratively dividing away the smallest factor.
+
+Other than the Python reference implementation, this one runs in `O(sqrt(n) + log(n))`.
+-/
+def largestPrimeFactor (n : Nat) : Nat := Id.run do
+  if hn : 0 < n then
+    let mut m : { m : Nat // 0 < m } := ⟨n, hn⟩
+    let mut mostRecentFactor := 1
+    for hd : d in 2...=n do
+      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
+
+/-! ## Tests -/
+
+example : largestPrimeFactor 15 = 5 := by native_decide
+example : largestPrimeFactor 27 = 3 := by native_decide
+example : largestPrimeFactor 63 = 7 := by native_decide
+example : largestPrimeFactor 330 = 11 := by native_decide
+example : largestPrimeFactor 13195 = 29 := by native_decide
+
+/-! ## Missing API -/
+
+theorem eq_getElem_append_cons {pref suff : List α} {cur : α} :
+    (pref ++ cur :: suff)[pref.length]? = cur := by
+  simp
+
+grind_pattern eq_getElem_append_cons => pref ++ cur :: suff
+attribute [grind =] Nat.getElem?_toList_rcc
+attribute [grind =] Nat.length_toList_rcc
+
+/-! ## Verification -/
+
+theorem dividePower_dvd :
+    (dividePower n d hd).val ∣ n.val := by
+  fun_induction dividePower n d hd
+  · rename_i n h_dvd ih
+    have : n.val / d ∣ n.val := Nat.div_dvd_of_dvd h_dvd
+    grind [Nat.dvd_trans]
+  · apply Nat.dvd_refl
+
+theorem dividePower_le :
+    (dividePower n d hd).val ≤ n.val :=
+  Nat.le_of_dvd (by grind) dividePower_dvd
+
+theorem dividePower_lt (h : d ∣ n.val) :
+    (dividePower n d hd).val < n.val := by
+  fun_cases dividePower n d hd
+  · exact Nat.lt_of_le_of_lt dividePower_le (Nat.div_lt_self (by grind) (by grind))
+  · grind
+
+theorem not_dvd_dividePower :
+    ¬ d ∣ (dividePower n d hd).val := by
+  fun_induction dividePower n d hd <;> assumption
+
+theorem largestPrimeFactor_dvd :
+    largestPrimeFactor n ∣ n := by
+  generalize hwp : largestPrimeFactor n = wp
+  apply Id.of_wp_run_eq hwp
+  mvcgen
+  invariants
+  · .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 Nat.div_div_eq_div_mul' {a b c : Nat} (h : b ∣ a) (h' : c ∣ b) : a / (b / c) = a / b * c := by
+  by_cases a = 0
+  · simp [*]
+  · have : 0 < b := Nat.pos_of_dvd_of_pos h (by grind)
+    have : 0 < c := Nat.pos_of_dvd_of_pos h' (by grind)
+    rw [Nat.div_eq_iff_eq_mul_left]
+    · rw [Nat.mul_assoc, ← Nat.mul_div_assoc, Nat.mul_div_cancel_left, Nat.div_mul_cancel]
+      all_goals assumption
+    · have : c ≤ b := Nat.le_of_dvd ‹_› ‹_›
+      simp only [Nat.div_pos_iff]
+      grind
+    · refine Nat.dvd_trans ?_ h
+      apply Nat.div_dvd_of_dvd
+      assumption
+
+theorem dvd_or_dvd_of_dvd_self_div_dividePower {e : Nat} (h : m.val ∣ n)
+    (h : e ∣ n / (dividePower m d hd)) (hp : IsPrime e) :
+    e ∣ n / m ∨ e ∣ d := by
+  fun_induction dividePower m d hd
+  · rename_i ih _
+    simp only at ih
+    specialize ih (by grind [Nat.dvd_trans, Nat.div_dvd_of_dvd]) h
+    cases ih
+    · rename_i h'
+      grind [hp.dvd_mul_iff, Nat.div_div_eq_div_mul']
+    · grind
+  · grind
+
+/--
+Main theorem: `largestPrimeFactor n` is prime and maximal.
+Even though the problem description does not require it, we also prove this statement for
+`n` prime.
+
+The loop invariant tracks that `factor` divides `n`, all prime divisors of `m` are ≥ the current
+trial divisor, and `factor` is the largest prime factor found so far among those already divided
+out. -/
+theorem isPrime_largestPrimeFactor (h : 1 < n) :
+    IsPrime (largestPrimeFactor n) ∧ ∀ d : Nat, d ∣ n → IsPrime d → d ≤ (largestPrimeFactor n) := by
+  generalize hwp : largestPrimeFactor n = wp
+  apply Id.of_wp_run_eq hwp
+  mvcgen
+  invariants
+  · .withEarlyReturn
+    (fun cur ⟨m, mostRecentFactor⟩ =>
+      ⌜let i := cur.pos + 2; -- loop variable
+        -- At the beginning of the loop, the `mostRecentFactor` variable is less than the loop variable.
+        mostRecentFactor < i ∧
+        -- The `m` variable is a divisor of `n`.
+        m.val ∣ n ∧
+        -- Except if `m = n`, `mostRecentFactor` is the largest prime factor of `n / m`.
+        (if m.val = n then
+            mostRecentFactor = 1
+          else
+            IsPrime mostRecentFactor ∧ ∀ e : Nat, e ∣ n / m → IsPrime e → e ≤ mostRecentFactor) ∧
+        -- Every nontrivial divisor of `m` is at least as large as the loop variable.
+        ∀ 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.2.1
+      rw [if_neg (by grind)]
+      constructor
+      · rw [IsPrime]
+        constructor
+        · grind
+        · intro d hd
+          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.2.1
+        replace he := dvd_or_dvd_of_dvd_self_div_dividePower (by grind) he hep
+        split at this
+        · have : m = ⟨n, ‹_›⟩ := by grind
+          rw [this] at he
+          simp only [Nat.div_self ‹0 < n›, Nat.dvd_one] at he
+          cases he
+          · grind
+          · exact Nat.le_of_dvd (by grind) ‹_›
+        · replace this := this.2 e
+          cases he
+          · grind
+          · exact Nat.le_of_dvd (by grind) ‹_›
+    · simp only [List.Cursor.pos_mk, reduceCtorEq, false_and, and_false, exists_const, or_false] at *
+      intro e he
+      have : e ≠ cur := by grind [not_dvd_dividePower]
+      replace ih := ih.2.2.2.2 e
+      grind [dividePower_dvd, Nat.dvd_trans]
+  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.2 e
+      grind
+  case vc4 =>
+    simp only [List.Cursor.pos_mk, true_and, reduceCtorEq, false_and, exists_const, or_false]
+    refine ⟨?_, ?_, ?_, ?_⟩
+    · grind
+    · grind [Nat.dvd_refl]
+    · grind
+    · simp at *
+      intro e he
+      have : 0 < e := Nat.pos_of_dvd_of_pos he ‹0 < n›
+      grind
+  case vc5 r _ ih =>
+    simp only [List.Cursor.pos_mk, Rcc.length_toList, Nat.size_rcc, Nat.reduceSubDiff,
+      true_and] at *
+    simp_all only [true_and, reduceCtorEq, false_and, exists_const, or_false]
+    have := ih.2.2.2 _ (Nat.dvd_refl _)
+    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 vc7 => grind
+  -- Early return verification conditions:
+  case vc3 pref cur suff _ _ _ m _ hlt ih =>
+    simp_all only [Nat.not_le, List.Cursor.pos_mk, reduceCtorEq, false_and, and_false, exists_const,
+      or_false, Option.some.injEq, true_and, exists_eq_left', false_or]
+    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
@@ -51,4 +313,4 @@ def check(candidate):
     assert candidate(13195) == 29
 
 ```
--/
+-/