From 94d75d2fd2e1df57b1084fc4b4eadb6e9f3545a8 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 3 Sep 2025 10:41:45 +0200 Subject: [PATCH 01/16] start --- HumanEvalLean/HumanEval106.lean | 31 ++++++++++++++++++++++++++++--- 1 file changed, 28 insertions(+), 3 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index b369858..1dd17e8 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -1,5 +1,30 @@ -def f : Unit := - () +def f (n : Nat) : List Nat := Id.run do + let mut ret : List Nat := [] + for i in 1...=n do + if i % 2 = 0 then + let mut x := 1 + for j in 1...=i do x := x * j + ret := x :: ret + else + let mut x := 0 + for j in 1...=i do x := x + j + ret := x :: ret + return ret.reverse + +/-! +## Tests +-/ + +example : f 5 = [1, 2, 6, 24, 15] := by native_decide +example : f 7 = [1, 2, 6, 24, 15, 720, 28] := by native_decide +example : f 1 = [1] := by native_decide +example : f 3 = [1, 2, 6] := by native_decide + +/-! +## Verification + +TODO +-/ /-! ## Prompt @@ -43,4 +68,4 @@ def check(candidate): assert candidate(1) == [1] assert candidate(3) == [1, 2, 6] ``` --/ \ No newline at end of file +-/ From 1c5305bbb1e7dc1784629a1727d26a1c247f6106 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 3 Sep 2025 16:20:19 +0200 Subject: [PATCH 02/16] wip --- HumanEvalLean/HumanEval106.lean | 164 +++++++++++++++++++++++++++++++- lakefile.toml | 3 + 2 files changed, 165 insertions(+), 2 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index 1dd17e8..8a349e9 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -1,3 +1,12 @@ +module + +import Std.Tactic.Do +-- Sadly, it's apparently impossible to easily prove the size of a +-- `Nat` range without unfolding internal stuff. +import all Init.Data.Iterators.Consumers.Loop + +open Std.Do + def f (n : Nat) : List Nat := Id.run do let mut ret : List Nat := [] for i in 1...=n do @@ -22,10 +31,161 @@ example : f 3 = [1, 2, 6] := by native_decide /-! ## Verification - -TODO -/ +def factorial : Nat → Nat + | 0 => 1 + | n + 1 => factorial n * (n + 1) + +example : factorial 1 = 1 := by decide +example : factorial 3 = 6 := by decide + +@[simp] +theorem Std.PRange.length_toList_eq_size [UpwardEnumerable α] [LawfulUpwardEnumerable α] + [SupportsLowerBound sl α] [SupportsUpperBound su α] [BoundedUpwardEnumerable sl α] + [HasFiniteRanges su α] [RangeSize su α] [LawfulRangeSize su α] + {r : PRange ⟨sl, su⟩ α} : + r.toList.length = r.size := by + simp [PRange.toList, PRange.size] + +@[simp] +theorem Nat.size_Rco {a b : Nat} : + (a...b).size = b - a := by + simp [Std.PRange.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size, + Std.PRange.Internal.iter, Std.Iterators.Iter.toIterM, Std.PRange.RangeSize.size] + +@[simp] +theorem Nat.size_Rcc {a b : Nat} : + (a...=b).size = b + 1- a := by + simp [Std.PRange.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size, + Std.PRange.Internal.iter, Std.Iterators.Iter.toIterM, Std.PRange.RangeSize.size] + +theorem Std.PRange.getElem?_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] + [SupportsUpperBound su α] + [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α] + {r : PRange ⟨.closed, su⟩ α} {i} : + r.toList[i]? = (UpwardEnumerable.succMany? i r.lower).filter (SupportsUpperBound.IsSatisfied r.upper) := by + sorry + +theorem Std.PRange.succMany?_isSome_of_lt_length_toList [LE α] [UpwardEnumerable α] + [LawfulUpwardEnumerable α] [SupportsUpperBound su α] + [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α] + {r : PRange ⟨.closed, su⟩ α} {i} (h : i < r.toList.length) : + (UpwardEnumerable.succMany? i r.lower).isSome := by + sorry + +theorem Std.PRange.getElem_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] + [SupportsUpperBound su α] + [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α] + {r : PRange ⟨.closed, su⟩ α} {i h} : + r.toList[i]'h = (UpwardEnumerable.succMany? i r.lower).get + (succMany?_isSome_of_lt_length_toList h) := by + simp [List.getElem_eq_getElem?_get, getElem?_Rcx_eq] + +theorem length_f {n : Nat} : + (f n).length = n := by + generalize hwp : f n = w + apply Std.Do.Id.of_wp_run_eq hwp + mvcgen + all_goals try infer_instance + case inv1 => + exact ⇓⟨cur, xs⟩ => ⌜xs.length = cur.prefix.length⌝ + case inv2 => + -- factorial loop + exact ⇓⟨cur, xs⟩ => ⌜True⌝ + case inv3 => + -- sum loop + exact ⇓⟨cur, xs⟩ => ⌜True⌝ + all_goals simp_all -- relies on `Nat.size_Rcc` + +abbrev SVal' (σs : List (Type u)) (α : Type u) : Type u := match σs with + | [] => α + | σ :: σs => σ → SVal σs α + +abbrev SPred' (σs : List (Type u)) : Type u := SVal σs (ULift Prop) + +def pure {σs : List (Type u)} (P : Prop) : SPred' σs := match σs with + | [] => ULift.up P + | _ :: _ => fun _ => pure P + +-- open Std PRange in +-- @[spec] +-- theorem Spec.forIn'_prange {α β : Type u} +-- [Monad m] [WPMonad m ps] +-- [UpwardEnumerable α] +-- [SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α] +-- [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α] +-- [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α] +-- {xs : PRange ⟨sl, su⟩ α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} +-- (inv : Invariant xs.toList β ps) +-- (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b, +-- Triple +-- (f cur (by simp [←mem_toList_iff_mem, h]) b) +-- (inv.1 (⟨pref, cur::suff, h.symm⟩, b)) +-- (fun r => match r with +-- | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') +-- | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)) : +-- Triple (forIn' xs init f) (inv.1 (⟨[], xs.toList, rfl⟩, init)) (fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2) := by +-- simp only [forIn'_eq_forIn'_toList] +-- apply Spec.forIn'_list inv step + +theorem f_eq_fac {n : Nat} {k : Nat} (hlt : k < n) (hmod : k % 2 = 1) : + (f n)[k]'(by grind [length_f]) = factorial (k + 1) := by + rw [List.getElem_eq_iff] + generalize hwp : f n = w + apply Std.Do.Id.of_wp_run_eq hwp + mvcgen + all_goals try infer_instance + case inv1 => + exact ⇓⟨cur, xs⟩ => ⌜xs.length = cur.prefix.length ∧ ((_ : k < xs.length) → xs[xs.length - 1 - k] = factorial (k + 1))⌝ + case inv2 => + -- factorial loop + exact ⇓⟨cur, x⟩ => ⌜x = factorial cur.prefix.length⌝ + case inv3 => + -- sum loop => irrelevant + exact ⇓⟨cur, xs⟩ => ⌜True⌝ + case vc3 => + simp_all [factorial] + rename_i cur _ _ _ _ pref' cur' suff' h' _ _ _ + have : cur' = (1...=cur).toList[pref'.length]'(by simp [h']) := by simp [h'] + rw [this, Std.PRange.getElem_Rcx_eq] + simp only [Std.PRange.UpwardEnumerable.succMany?, Option.get_some] + grind + case vc4 => simp [factorial] + case vc5 => + simp_all + intro h + rename_i pref cur suff _ _ _ _ _ _ h' _ + have : cur = pref.length + 1 := sorry + obtain ⟨h', h''⟩ := h' + simp_all + rw [List.getElem_cons] + split + · simp_all + grind + · simp_all + refine Eq.trans ?_ (h'' ?_) + · grind + · grind only -- `grind` fails, see #10233 + case vc7 => simp + case vc8 => simp + case vc9 => + simp_all + intro h + rename_i pref cur suff _ _ _ _ _ h'' + have : cur = pref.length + 1 := sorry + refine Eq.trans ?_ (h''.2 ?_) + simp_all + rw [List.getElem_cons] + · rw [dif_neg (by grind only)] + grind + · grind + case vc10 => simp + case vc11 => + rename_i h + obtain ⟨h, h'⟩ := h + simp_all + /-! ## Prompt diff --git a/lakefile.toml b/lakefile.toml index 88f3f54..d420aff 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -2,6 +2,9 @@ name = "human-eval-lean" version = "0.1.0" defaultTargets = ["HumanEvalLean", "create-scaffold"] +[leanOptions] +experimental.module = true + [[lean_lib]] name = "HumanEvalLean" globs = ["HumanEvalLean.*"] From 135f84b9c2d3e5810b8511e86d323f2bec6d0721 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 3 Sep 2025 18:27:27 +0200 Subject: [PATCH 03/16] technically, done --- HumanEvalLean/HumanEval106.lean | 46 +++++++++++++++++++++++++++------ 1 file changed, 38 insertions(+), 8 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index 8a349e9..eb7f0d9 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -61,21 +61,45 @@ theorem Nat.size_Rcc {a b : Nat} : Std.PRange.Internal.iter, Std.Iterators.Iter.toIterM, Std.PRange.RangeSize.size] theorem Std.PRange.getElem?_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] - [SupportsUpperBound su α] + [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α] [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α] {r : PRange ⟨.closed, su⟩ α} {i} : r.toList[i]? = (UpwardEnumerable.succMany? i r.lower).filter (SupportsUpperBound.IsSatisfied r.upper) := by - sorry + induction i generalizing r + · rw [PRange.toList_eq_match, UpwardEnumerable.succMany?_zero] + simp only [Option.filter_some, decide_eq_true_eq] + split <;> simp + · rename_i n ih + rw [PRange.toList_eq_match] + simp + split + · simp [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?] + cases hs : UpwardEnumerable.succ? r.lower + · rw [PRange.toList_eq_match] + simp [BoundedUpwardEnumerable.init?, hs] + · rw [toList_open_eq_toList_closed_of_isSome_succ? (by grind)] + rw [ih] + simp [hs] + · simp [*] + cases hs : UpwardEnumerable.succMany? (n + 1) r.lower + · grind + · rename_i hl a + simp [Option.filter_some] + have : UpwardEnumerable.LE r.lower a := ⟨n + 1, hs⟩ + intro ha + exact hl.elim <| LawfulUpwardEnumerableUpperBound.isSatisfied_of_le r.upper _ _ ha this (α := α) theorem Std.PRange.succMany?_isSome_of_lt_length_toList [LE α] [UpwardEnumerable α] - [LawfulUpwardEnumerable α] [SupportsUpperBound su α] + [LawfulUpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α] [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α] {r : PRange ⟨.closed, su⟩ α} {i} (h : i < r.toList.length) : (UpwardEnumerable.succMany? i r.lower).isSome := by - sorry + have : r.toList[i]?.isSome := by grind + simp only [getElem?_Rcx_eq, Option.isSome_filter] at this + exact Option.isSome_of_any this theorem Std.PRange.getElem_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] - [SupportsUpperBound su α] + [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α] [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α] {r : PRange ⟨.closed, su⟩ α} {i h} : r.toList[i]'h = (UpwardEnumerable.succMany? i r.lower).get @@ -156,7 +180,10 @@ theorem f_eq_fac {n : Nat} {k : Nat} (hlt : k < n) (hmod : k % 2 = 1) : simp_all intro h rename_i pref cur suff _ _ _ _ _ _ h' _ - have : cur = pref.length + 1 := sorry + have : cur = pref.length + 1 := by + have : cur = (1...=n).toList[pref.length]'(by simp [*]) := by simp [*] + simp [this, Std.PRange.getElem_Rcx_eq, Std.PRange.UpwardEnumerable.succMany?] + grind obtain ⟨h', h''⟩ := h' simp_all rw [List.getElem_cons] @@ -166,14 +193,17 @@ theorem f_eq_fac {n : Nat} {k : Nat} (hlt : k < n) (hmod : k % 2 = 1) : · simp_all refine Eq.trans ?_ (h'' ?_) · grind - · grind only -- `grind` fails, see #10233 + · grind only -- `grind` without `only` fails, see #10233 case vc7 => simp case vc8 => simp case vc9 => simp_all intro h rename_i pref cur suff _ _ _ _ _ h'' - have : cur = pref.length + 1 := sorry + have : cur = pref.length + 1 := by + have : cur = (1...=n).toList[pref.length]'(by simp [*]) := by simp [*] + simp [this, Std.PRange.getElem_Rcx_eq, Std.PRange.UpwardEnumerable.succMany?] + grind refine Eq.trans ?_ (h''.2 ?_) simp_all rw [List.getElem_cons] From 92d7d89b3645d955ccff3cdeb9a13526b6146333 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 3 Sep 2025 19:39:32 +0200 Subject: [PATCH 04/16] cleanup --- HumanEvalLean/HumanEval106.lean | 175 +++++++++++++++----------------- 1 file changed, 80 insertions(+), 95 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index eb7f0d9..971d5a1 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -1,8 +1,8 @@ module import Std.Tactic.Do --- Sadly, it's apparently impossible to easily prove the size of a --- `Nat` range without unfolding internal stuff. +-- Sadly, it's apparently currently impossible to easily prove the size of a +-- `Nat` range without unfolding internal stuff. This should be fixed in the standard library. import all Init.Data.Iterators.Consumers.Loop open Std.Do @@ -30,15 +30,10 @@ example : f 1 = [1] := by native_decide example : f 3 = [1, 2, 6] := by native_decide /-! -## Verification --/ - -def factorial : Nat → Nat - | 0 => 1 - | n + 1 => factorial n * (n + 1) +## Standard library wishlist -example : factorial 1 = 1 := by decide -example : factorial 3 = 6 := by decide +The following lemmas halp with the verification and would be nice to have in the standard library. +-/ @[simp] theorem Std.PRange.length_toList_eq_size [UpwardEnumerable α] [LawfulUpwardEnumerable α] @@ -89,7 +84,7 @@ theorem Std.PRange.getElem?_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEn intro ha exact hl.elim <| LawfulUpwardEnumerableUpperBound.isSatisfied_of_le r.upper _ _ ha this (α := α) -theorem Std.PRange.succMany?_isSome_of_lt_length_toList [LE α] [UpwardEnumerable α] +theorem Std.PRange.isSome_succMany?_of_lt_length_toList [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α] [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α] {r : PRange ⟨.closed, su⟩ α} {i} (h : i < r.toList.length) : @@ -103,9 +98,36 @@ theorem Std.PRange.getElem_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnu [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α] {r : PRange ⟨.closed, su⟩ α} {i h} : r.toList[i]'h = (UpwardEnumerable.succMany? i r.lower).get - (succMany?_isSome_of_lt_length_toList h) := by + (isSome_succMany?_of_lt_length_toList h) := by simp [List.getElem_eq_getElem?_get, getElem?_Rcx_eq] +theorem Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons [LE α] + [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] + [SupportsUpperBound su α] [HasFiniteRanges su α] [LawfulUpwardEnumerableUpperBound su α] + {r : PRange ⟨.closed, su⟩ α} {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff) : + cur = (UpwardEnumerable.succMany? pref.length r.lower).get + (isSome_succMany?_of_lt_length_toList (by grind)) := by + have : cur = (pref ++ cur :: suff)[pref.length] := by grind + simp only [← h] at this + simp [this, getElem_Rcx_eq] + +/-! +## Verification +-/ + +def factorial : Nat → Nat + | 0 => 1 + | n + 1 => factorial n * (n + 1) + +def triangle : Nat → Nat + | 0 => 0 + | n + 1 => triangle n + (n + 1) + +example : factorial 1 = 1 := by decide +example : factorial 4 = 24 := by decide +example : triangle 1 = 1 := by decide +example : triangle 4 = 10 := by decide + theorem length_f {n : Nat} : (f n).length = n := by generalize hwp : f n = w @@ -122,99 +144,62 @@ theorem length_f {n : Nat} : exact ⇓⟨cur, xs⟩ => ⌜True⌝ all_goals simp_all -- relies on `Nat.size_Rcc` -abbrev SVal' (σs : List (Type u)) (α : Type u) : Type u := match σs with - | [] => α - | σ :: σs => σ → SVal σs α - -abbrev SPred' (σs : List (Type u)) : Type u := SVal σs (ULift Prop) - -def pure {σs : List (Type u)} (P : Prop) : SPred' σs := match σs with - | [] => ULift.up P - | _ :: _ => fun _ => pure P - --- open Std PRange in --- @[spec] --- theorem Spec.forIn'_prange {α β : Type u} --- [Monad m] [WPMonad m ps] --- [UpwardEnumerable α] --- [SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α] --- [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α] --- [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α] --- {xs : PRange ⟨sl, su⟩ α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} --- (inv : Invariant xs.toList β ps) --- (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b, --- Triple --- (f cur (by simp [←mem_toList_iff_mem, h]) b) --- (inv.1 (⟨pref, cur::suff, h.symm⟩, b)) --- (fun r => match r with --- | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') --- | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)) : --- Triple (forIn' xs init f) (inv.1 (⟨[], xs.toList, rfl⟩, init)) (fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2) := by --- simp only [forIn'_eq_forIn'_toList] --- apply Spec.forIn'_list inv step - -theorem f_eq_fac {n : Nat} {k : Nat} (hlt : k < n) (hmod : k % 2 = 1) : - (f n)[k]'(by grind [length_f]) = factorial (k + 1) := by +theorem f_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : + (f n)[k]'(by grind [length_f]) = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1) := by rw [List.getElem_eq_iff] generalize hwp : f n = w apply Std.Do.Id.of_wp_run_eq hwp mvcgen all_goals try infer_instance + + -- OUTER LOOP case inv1 => - exact ⇓⟨cur, xs⟩ => ⌜xs.length = cur.prefix.length ∧ ((_ : k < xs.length) → xs[xs.length - 1 - k] = factorial (k + 1))⌝ - case inv2 => - -- factorial loop - exact ⇓⟨cur, x⟩ => ⌜x = factorial cur.prefix.length⌝ - case inv3 => - -- sum loop => irrelevant - exact ⇓⟨cur, xs⟩ => ⌜True⌝ - case vc3 => - simp_all [factorial] - rename_i cur _ _ _ _ pref' cur' suff' h' _ _ _ - have : cur' = (1...=cur).toList[pref'.length]'(by simp [h']) := by simp [h'] - rw [this, Std.PRange.getElem_Rcx_eq] - simp only [Std.PRange.UpwardEnumerable.succMany?, Option.get_some] - grind - case vc4 => simp [factorial] - case vc5 => - simp_all - intro h - rename_i pref cur suff _ _ _ _ _ _ h' _ - have : cur = pref.length + 1 := by - have : cur = (1...=n).toList[pref.length]'(by simp [*]) := by simp [*] - simp [this, Std.PRange.getElem_Rcx_eq, Std.PRange.UpwardEnumerable.succMany?] - grind - obtain ⟨h', h''⟩ := h' + exact ⇓⟨cur, xs⟩ => ⌜xs.length = cur.prefix.length ∧ + ((_ : k < xs.length) → xs[xs.length - 1 - k] = + if k % 2 = 0 then triangle (k + 1) else factorial (k + 1))⌝ + case vc10 => simp -- base case + case vc11 => -- postcondition + rename_i h + obtain ⟨h, h'⟩ := h simp_all - rw [List.getElem_cons] + + -- FACTORIAL LOOP + case inv2 => exact ⇓⟨cur, x⟩ => ⌜x = factorial cur.prefix.length⌝ + case vc4 => simp [factorial] -- base case + case vc5 => -- postcondition + simp_all only [Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_›, + Std.PRange.UpwardEnumerable.succMany?, SPred.down_pure, + Std.PRange.length_toList_eq_size, Nat.size_Rcc, List.length_cons, + List.length_append, List.length_nil, true_and, List.getElem_cons] split - · simp_all - grind - · simp_all - refine Eq.trans ?_ (h'' ?_) - · grind - · grind only -- `grind` without `only` fails, see #10233 - case vc7 => simp - case vc8 => simp - case vc9 => - simp_all - intro h - rename_i pref cur suff _ _ _ _ _ h'' - have : cur = pref.length + 1 := by - have : cur = (1...=n).toList[pref.length]'(by simp [*]) := by simp [*] - simp [this, Std.PRange.getElem_Rcx_eq, Std.PRange.UpwardEnumerable.succMany?] + · simp_all only [SPred.down_pure, Std.PRange.length_toList_eq_size, Nat.size_Rcc] grind - refine Eq.trans ?_ (h''.2 ?_) - simp_all - rw [List.getElem_cons] - · rw [dif_neg (by grind only)] + · rename_i h' _ _ + refine fun _ => + Eq.trans ?_ (h'.2 ?_) <;> grind only -- `grind` without `only` fails, see #10233 + case vc3.step => -- step + have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› + simp_all [Std.PRange.UpwardEnumerable.succMany?, Option.get_some, factorial] + grind [factorial] + + -- SUM LOOP + case inv3 => exact ⇓⟨cur, x⟩ => ⌜x = triangle cur.prefix.length⌝ + case vc8 => simp [triangle] -- base case + case vc9 => -- postcondition + simp_all only [Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_›, + Std.PRange.UpwardEnumerable.succMany?, SPred.down_pure, + Std.PRange.length_toList_eq_size, Nat.size_Rcc, List.length_cons, + List.length_append, List.length_nil, true_and, List.getElem_cons] + split + · simp_all only [SPred.down_pure, Std.PRange.length_toList_eq_size, Nat.size_Rcc] grind - · grind - case vc10 => simp - case vc11 => - rename_i h - obtain ⟨h, h'⟩ := h - simp_all + · rename_i h' _ _ + refine fun _ => + Eq.trans ?_ (h'.2 ?_) <;> grind only -- `grind` without `only` fails, see #10233 + case vc7.step => -- step + have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› + simp_all [Std.PRange.UpwardEnumerable.succMany?, Option.get_some, factorial] + grind [triangle] /-! ## Prompt From e7f5e8470c503b7c8e0f3e5e948d0b2ae11bf050 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Thu, 4 Sep 2025 08:53:54 +0200 Subject: [PATCH 05/16] squash nonterminal simps --- HumanEvalLean/HumanEval106.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index 971d5a1..893f40a 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -79,7 +79,7 @@ theorem Std.PRange.getElem?_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEn cases hs : UpwardEnumerable.succMany? (n + 1) r.lower · grind · rename_i hl a - simp [Option.filter_some] + simp only [Option.filter_some, decide_eq_true_eq, right_eq_ite_iff] have : UpwardEnumerable.LE r.lower a := ⟨n + 1, hs⟩ intro ha exact hl.elim <| LawfulUpwardEnumerableUpperBound.isSatisfied_of_le r.upper _ _ ha this (α := α) @@ -179,7 +179,8 @@ theorem f_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : Eq.trans ?_ (h'.2 ?_) <;> grind only -- `grind` without `only` fails, see #10233 case vc3.step => -- step have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› - simp_all [Std.PRange.UpwardEnumerable.succMany?, Option.get_some, factorial] + simp_all only [factorial, SPred.down_pure, Std.PRange.UpwardEnumerable.succMany?, + Option.get_some] grind [factorial] -- SUM LOOP @@ -198,7 +199,8 @@ theorem f_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : Eq.trans ?_ (h'.2 ?_) <;> grind only -- `grind` without `only` fails, see #10233 case vc7.step => -- step have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› - simp_all [Std.PRange.UpwardEnumerable.succMany?, Option.get_some, factorial] + simp_all only [factorial, SPred.down_pure, Std.PRange.UpwardEnumerable.succMany?, + Option.get_some] grind [triangle] /-! From a36a3ce812357ed8a069494ddf7dd171064ec4bd Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Thu, 4 Sep 2025 08:55:58 +0200 Subject: [PATCH 06/16] squash nonterminal simps --- HumanEvalLean/HumanEval106.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index 893f40a..2c17cce 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -66,7 +66,7 @@ theorem Std.PRange.getElem?_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEn split <;> simp · rename_i n ih rw [PRange.toList_eq_match] - simp + simp only split · simp [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?] cases hs : UpwardEnumerable.succ? r.lower @@ -75,7 +75,7 @@ theorem Std.PRange.getElem?_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEn · rw [toList_open_eq_toList_closed_of_isSome_succ? (by grind)] rw [ih] simp [hs] - · simp [*] + · simp only [List.length_nil, Nat.not_lt_zero, not_false_eq_true, getElem?_neg] cases hs : UpwardEnumerable.succMany? (n + 1) r.lower · grind · rename_i hl a From 4010907e28bea3933ae765606a1a60e9677a79d1 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 5 Sep 2025 13:22:23 +0200 Subject: [PATCH 07/16] efficient impl --- HumanEvalLean/HumanEval106.lean | 193 ++++++++++++++++++++++++++++---- 1 file changed, 171 insertions(+), 22 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index 2c17cce..22c4ff8 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -5,29 +5,11 @@ import Std.Tactic.Do -- `Nat` range without unfolding internal stuff. This should be fixed in the standard library. import all Init.Data.Iterators.Consumers.Loop -open Std.Do - -def f (n : Nat) : List Nat := Id.run do - let mut ret : List Nat := [] - for i in 1...=n do - if i % 2 = 0 then - let mut x := 1 - for j in 1...=i do x := x * j - ret := x :: ret - else - let mut x := 0 - for j in 1...=i do x := x + j - ret := x :: ret - return ret.reverse - /-! -## Tests +This file provides two solutions for problem 106: a naïve one and an efficient one. -/ -example : f 5 = [1, 2, 6, 24, 15] := by native_decide -example : f 7 = [1, 2, 6, 24, 15, 720, 28] := by native_decide -example : f 1 = [1] := by native_decide -example : f 3 = [1, 2, 6] := by native_decide +open Std.Do /-! ## Standard library wishlist @@ -51,7 +33,7 @@ theorem Nat.size_Rco {a b : Nat} : @[simp] theorem Nat.size_Rcc {a b : Nat} : - (a...=b).size = b + 1- a := by + (a...=b).size = b + 1 - a := by simp [Std.PRange.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size, Std.PRange.Internal.iter, Std.Iterators.Iter.toIterM, Std.PRange.RangeSize.size] @@ -111,8 +93,36 @@ theorem Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons [LE α] simp only [← h] at this simp [this, getElem_Rcx_eq] +section NaiveImpl + +/-! +## A naïve implementation +-/ + +def f (n : Nat) : List Nat := Id.run do + let mut ret : List Nat := [] + for i in 1...=n do + if i % 2 = 0 then + let mut x := 1 + for j in 1...=i do x := x * j + ret := x :: ret + else + let mut x := 0 + for j in 1...=i do x := x + j + ret := x :: ret + return ret.reverse + +/-! +### Tests +-/ + +example : f 5 = [1, 2, 6, 24, 15] := by native_decide +example : f 7 = [1, 2, 6, 24, 15, 720, 28] := by native_decide +example : f 1 = [1] := by native_decide +example : f 3 = [1, 2, 6] := by native_decide + /-! -## Verification +### Verification -/ def factorial : Nat → Nat @@ -203,6 +213,145 @@ theorem f_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : Option.get_some] grind [triangle] +end NaiveImpl + +section EfficientImpl + +/-! +## An efficient implementation +-/ + +def f' (n : Nat) : Array Nat := Id.run do + if n ≤ 2 then + return #[1, 2].take n + let mut ret : Array Nat := .emptyWithCapacity n + ret := ret.push 1 -- 1st entry should be `triangle 1` + ret := ret.push 2 -- 2nd entry should be `factorial 2` + for i in 2... exact ⇓⟨cur, xs⟩ => ⌜xs.size = cur.prefix.length + 2⌝ + all_goals try simp_all; done -- relies on `Nat.size_Rcc` + simp_all only [Nat.not_le, Std.PRange.length_toList_eq_size, Nat.size_Rco, SPred.down_pure] + grind + +theorem f'_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : + (f' n)[k]'(by grind [size_f']) = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1) := by + rw [Array.getElem_eq_iff] + generalize hwp : f' n = w + apply Std.Do.Id.of_wp_run_eq hwp + mvcgen + all_goals try infer_instance + case inv1 => + exact ⇓⟨cur, xs⟩ => ⌜xs.size = cur.prefix.length + 2 ∧ ∀ j : Nat, (_ : j < xs.size) → + (j % 2 = 1 → xs[j] = factorial (j + 1)) ∧ (j % 2 = 0 → xs[j] = triangle (j + 1))⌝ + case vc1 => + simp_all only [Array.take_eq_extract, List.extract_toArray, List.extract_eq_drop_take, + Nat.sub_zero, List.drop_zero, List.size_toArray, List.length_take, List.length_cons, + List.length_nil, Nat.zero_add, Nat.reduceAdd, Nat.min_eq_left, getElem?_pos, + List.getElem_toArray, List.getElem_take, Option.some.injEq] + match k with + | 0 => simp [triangle] + | 1 => simp [factorial] + | n + 2 => grind + case vc5 => + simp_all + intro k hk + match k with + | 0 => simp [triangle] + | 1 => simp [factorial] + | n + 2 => grind + case vc3 => + simp_all + intro j _ + apply And.intro + · intro _ + have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› + simp [Std.PRange.UpwardEnumerable.succMany?] at this + rw [getElem!_pos] + · rename_i b h _ _ _ _ _ + simp at h + simp_all + rw [Array.getElem_push] + split + · exact (h.2 j (by grind)).1 (by grind) + · have : j = b.size := by grind + cases this + rw [h.1] + grind [factorial] + · simp_all + · intro _ + have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› + simp [Std.PRange.UpwardEnumerable.succMany?] at this + rw [getElem!_pos] + · rename_i b h _ _ _ _ _ + simp at h + simp_all + rw [Array.getElem_push] + split + · exact (h.2 j (by grind)).2 (by grind) + · grind + · simp_all + case vc4 => + simp_all + intro j _ + apply And.intro + · intro _ + have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› + simp [Std.PRange.UpwardEnumerable.succMany?] at this + rw [getElem!_pos] + · rename_i b h _ _ _ _ _ + simp at h + simp_all + rw [Array.getElem_push] + split + · exact (h.2 j (by grind)).1 (by grind) + · grind + · simp_all + · intro _ + have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› + simp [Std.PRange.UpwardEnumerable.succMany?] at this + rw [getElem!_pos] + · rename_i b h _ _ _ _ _ + simp at h + simp_all + rw [Array.getElem_push] + split + · exact (h.2 j (by grind)).2 (by grind) + · have : j = b.size := by grind + cases this + rw [h.1] + grind [triangle] + · simp_all + case vc6 => + simp_all + grind + +end EfficientImpl + /-! ## Prompt From 749bc0614281a35fe4a8fedf3e83f8d968d8a483 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 5 Sep 2025 14:02:18 +0200 Subject: [PATCH 08/16] cleanup --- HumanEvalLean/HumanEval106.lean | 87 ++++++++------------------------- 1 file changed, 21 insertions(+), 66 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index 22c4ff8..095d5d3 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -229,6 +229,8 @@ def f' (n : Nat) : Array Nat := Id.run do ret := ret.push 2 -- 2nd entry should be `factorial 2` for i in 2... exact ⇓⟨cur, xs⟩ => ⌜xs.size = cur.prefix.length + 2 ∧ ∀ j : Nat, (_ : j < xs.size) → (j % 2 = 1 → xs[j] = factorial (j + 1)) ∧ (j % 2 = 0 → xs[j] = triangle (j + 1))⌝ - case vc1 => + case vc1 => -- verification of the early return simp_all only [Array.take_eq_extract, List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, List.size_toArray, List.length_take, List.length_cons, List.length_nil, Nat.zero_add, Nat.reduceAdd, Nat.min_eq_left, getElem?_pos, @@ -277,76 +279,29 @@ theorem f'_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : | 0 => simp [triangle] | 1 => simp [factorial] | n + 2 => grind - case vc5 => - simp_all + case vc5 => -- base case of the loop + mleave + simp_all only [Nat.not_le, Array.emptyWithCapacity_eq, List.push_toArray, List.nil_append, + List.cons_append, List.size_toArray, List.length_cons, List.length_nil, Nat.zero_add, + Nat.reduceAdd, List.getElem_toArray, true_and] intro k hk match k with | 0 => simp [triangle] | 1 => simp [factorial] | n + 2 => grind - case vc3 => - simp_all - intro j _ - apply And.intro - · intro _ - have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› - simp [Std.PRange.UpwardEnumerable.succMany?] at this - rw [getElem!_pos] - · rename_i b h _ _ _ _ _ - simp at h - simp_all - rw [Array.getElem_push] - split - · exact (h.2 j (by grind)).1 (by grind) - · have : j = b.size := by grind - cases this - rw [h.1] - grind [factorial] - · simp_all - · intro _ - have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› - simp [Std.PRange.UpwardEnumerable.succMany?] at this - rw [getElem!_pos] - · rename_i b h _ _ _ _ _ - simp at h - simp_all - rw [Array.getElem_push] - split - · exact (h.2 j (by grind)).2 (by grind) - · grind - · simp_all - case vc4 => - simp_all - intro j _ - apply And.intro - · intro _ - have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› - simp [Std.PRange.UpwardEnumerable.succMany?] at this - rw [getElem!_pos] - · rename_i b h _ _ _ _ _ - simp at h - simp_all - rw [Array.getElem_push] - split - · exact (h.2 j (by grind)).1 (by grind) - · grind - · simp_all - · intro _ - have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› - simp [Std.PRange.UpwardEnumerable.succMany?] at this - rw [getElem!_pos] - · rename_i b h _ _ _ _ _ - simp at h - simp_all - rw [Array.getElem_push] - split - · exact (h.2 j (by grind)).2 (by grind) - · have : j = b.size := by grind - cases this - rw [h.1] - grind [triangle] - · simp_all - case vc6 => + case vc3 hmod h => -- `then` branch + mleave + have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› + simp only [Std.PRange.UpwardEnumerable.succMany?, Option.get_some] at this + simp only [Array.size_push, List.length_append, List.length_cons, List.length_nil, Nat.zero_add] + grind [factorial] + case vc4 => -- `else` branch + mleave + have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› + simp only [Std.PRange.UpwardEnumerable.succMany?, Option.get_some] at this + simp only [Array.size_push, List.length_append, List.length_cons, List.length_nil, Nat.zero_add] + grind [triangle] + case vc6 => -- postcondition simp_all grind From 4a12f0b6fe0b5ffea4ca8d4775ab794e4dbc6d24 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 5 Sep 2025 14:10:19 +0200 Subject: [PATCH 09/16] squash simps --- HumanEvalLean/HumanEval106.lean | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index 095d5d3..e7bf5ff 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -271,19 +271,16 @@ theorem f'_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : exact ⇓⟨cur, xs⟩ => ⌜xs.size = cur.prefix.length + 2 ∧ ∀ j : Nat, (_ : j < xs.size) → (j % 2 = 1 → xs[j] = factorial (j + 1)) ∧ (j % 2 = 0 → xs[j] = triangle (j + 1))⌝ case vc1 => -- verification of the early return - simp_all only [Array.take_eq_extract, List.extract_toArray, List.extract_eq_drop_take, - Nat.sub_zero, List.drop_zero, List.size_toArray, List.length_take, List.length_cons, - List.length_nil, Nat.zero_add, Nat.reduceAdd, Nat.min_eq_left, getElem?_pos, - List.getElem_toArray, List.getElem_take, Option.some.injEq] + simp_all only [List.extract_toArray, Nat.sub_zero, List.drop_zero, List.size_toArray, + List.length_take, List.length_cons, List.length_nil, Nat.min_eq_left, getElem?_pos] match k with | 0 => simp [triangle] | 1 => simp [factorial] | n + 2 => grind case vc5 => -- base case of the loop mleave - simp_all only [Nat.not_le, Array.emptyWithCapacity_eq, List.push_toArray, List.nil_append, - List.cons_append, List.size_toArray, List.length_cons, List.length_nil, Nat.zero_add, - Nat.reduceAdd, List.getElem_toArray, true_and] + simp only [Array.emptyWithCapacity_eq, List.push_toArray, List.nil_append, List.cons_append, + List.size_toArray, List.length_cons, true_and] intro k hk match k with | 0 => simp [triangle] @@ -302,7 +299,7 @@ theorem f'_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : simp only [Array.size_push, List.length_append, List.length_cons, List.length_nil, Nat.zero_add] grind [triangle] case vc6 => -- postcondition - simp_all + simp only [Nat.not_le, Std.PRange.length_toList_eq_size, Nat.size_Rco, SPred.down_pure] at * grind end EfficientImpl From 7a68c5d9816e649d2a367bcedac038032b16cfa8 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 5 Sep 2025 14:14:41 +0200 Subject: [PATCH 10/16] simp_all -> simp --- HumanEvalLean/HumanEval106.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index e7bf5ff..3641b93 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -270,9 +270,10 @@ theorem f'_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : case inv1 => exact ⇓⟨cur, xs⟩ => ⌜xs.size = cur.prefix.length + 2 ∧ ∀ j : Nat, (_ : j < xs.size) → (j % 2 = 1 → xs[j] = factorial (j + 1)) ∧ (j % 2 = 0 → xs[j] = triangle (j + 1))⌝ - case vc1 => -- verification of the early return - simp_all only [List.extract_toArray, Nat.sub_zero, List.drop_zero, List.size_toArray, - List.length_take, List.length_cons, List.length_nil, Nat.min_eq_left, getElem?_pos] + case vc1 hn => -- verification of the early return + simp only [List.extract_toArray, Nat.sub_zero, + List.drop_zero, List.size_toArray, List.length_take, List.length_cons, List.length_nil, + Nat.min_eq_left, getElem?_pos, Option.some.injEq, hn, hlt] match k with | 0 => simp [triangle] | 1 => simp [factorial] From 731823ef317a556912e782f09eb50d72970757ef Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 5 Sep 2025 14:20:10 +0200 Subject: [PATCH 11/16] fix after rebasing --- HumanEvalLean/HumanEval106.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index 3641b93..989c8b3 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -28,8 +28,9 @@ theorem Std.PRange.length_toList_eq_size [UpwardEnumerable α] [LawfulUpwardEnum @[simp] theorem Nat.size_Rco {a b : Nat} : (a...b).size = b - a := by - simp [Std.PRange.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size, - Std.PRange.Internal.iter, Std.Iterators.Iter.toIterM, Std.PRange.RangeSize.size] + simp only [Std.PRange.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size, + Std.Iterators.Iter.toIterM, Std.PRange.Internal.iter, Std.PRange.RangeSize.size, Id.run_pure] + grind @[simp] theorem Nat.size_Rcc {a b : Nat} : From e0f8cef9781dd803d7752b0ad23314807b3b62a7 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 2 Dec 2025 09:33:25 +0100 Subject: [PATCH 12/16] port so that it uses the new range lemmas --- HumanEvalLean/HumanEval106.lean | 197 ++++++-------------------------- 1 file changed, 35 insertions(+), 162 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index 989c8b3..c9465fe 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -11,89 +11,6 @@ This file provides two solutions for problem 106: a naïve one and an efficient open Std.Do -/-! -## Standard library wishlist - -The following lemmas halp with the verification and would be nice to have in the standard library. --/ - -@[simp] -theorem Std.PRange.length_toList_eq_size [UpwardEnumerable α] [LawfulUpwardEnumerable α] - [SupportsLowerBound sl α] [SupportsUpperBound su α] [BoundedUpwardEnumerable sl α] - [HasFiniteRanges su α] [RangeSize su α] [LawfulRangeSize su α] - {r : PRange ⟨sl, su⟩ α} : - r.toList.length = r.size := by - simp [PRange.toList, PRange.size] - -@[simp] -theorem Nat.size_Rco {a b : Nat} : - (a...b).size = b - a := by - simp only [Std.PRange.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size, - Std.Iterators.Iter.toIterM, Std.PRange.Internal.iter, Std.PRange.RangeSize.size, Id.run_pure] - grind - -@[simp] -theorem Nat.size_Rcc {a b : Nat} : - (a...=b).size = b + 1 - a := by - simp [Std.PRange.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size, - Std.PRange.Internal.iter, Std.Iterators.Iter.toIterM, Std.PRange.RangeSize.size] - -theorem Std.PRange.getElem?_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] - [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α] - [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α] - {r : PRange ⟨.closed, su⟩ α} {i} : - r.toList[i]? = (UpwardEnumerable.succMany? i r.lower).filter (SupportsUpperBound.IsSatisfied r.upper) := by - induction i generalizing r - · rw [PRange.toList_eq_match, UpwardEnumerable.succMany?_zero] - simp only [Option.filter_some, decide_eq_true_eq] - split <;> simp - · rename_i n ih - rw [PRange.toList_eq_match] - simp only - split - · simp [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?] - cases hs : UpwardEnumerable.succ? r.lower - · rw [PRange.toList_eq_match] - simp [BoundedUpwardEnumerable.init?, hs] - · rw [toList_open_eq_toList_closed_of_isSome_succ? (by grind)] - rw [ih] - simp [hs] - · simp only [List.length_nil, Nat.not_lt_zero, not_false_eq_true, getElem?_neg] - cases hs : UpwardEnumerable.succMany? (n + 1) r.lower - · grind - · rename_i hl a - simp only [Option.filter_some, decide_eq_true_eq, right_eq_ite_iff] - have : UpwardEnumerable.LE r.lower a := ⟨n + 1, hs⟩ - intro ha - exact hl.elim <| LawfulUpwardEnumerableUpperBound.isSatisfied_of_le r.upper _ _ ha this (α := α) - -theorem Std.PRange.isSome_succMany?_of_lt_length_toList [LE α] [UpwardEnumerable α] - [LawfulUpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α] - [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α] - {r : PRange ⟨.closed, su⟩ α} {i} (h : i < r.toList.length) : - (UpwardEnumerable.succMany? i r.lower).isSome := by - have : r.toList[i]?.isSome := by grind - simp only [getElem?_Rcx_eq, Option.isSome_filter] at this - exact Option.isSome_of_any this - -theorem Std.PRange.getElem_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] - [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α] - [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α] - {r : PRange ⟨.closed, su⟩ α} {i h} : - r.toList[i]'h = (UpwardEnumerable.succMany? i r.lower).get - (isSome_succMany?_of_lt_length_toList h) := by - simp [List.getElem_eq_getElem?_get, getElem?_Rcx_eq] - -theorem Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons [LE α] - [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] - [SupportsUpperBound su α] [HasFiniteRanges su α] [LawfulUpwardEnumerableUpperBound su α] - {r : PRange ⟨.closed, su⟩ α} {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff) : - cur = (UpwardEnumerable.succMany? pref.length r.lower).get - (isSome_succMany?_of_lt_length_toList (by grind)) := by - have : cur = (pref ++ cur :: suff)[pref.length] := by grind - simp only [← h] at this - simp [this, getElem_Rcx_eq] - section NaiveImpl /-! @@ -145,15 +62,10 @@ theorem length_f {n : Nat} : apply Std.Do.Id.of_wp_run_eq hwp mvcgen all_goals try infer_instance - case inv1 => - exact ⇓⟨cur, xs⟩ => ⌜xs.length = cur.prefix.length⌝ - case inv2 => - -- factorial loop - exact ⇓⟨cur, xs⟩ => ⌜True⌝ - case inv3 => - -- sum loop - exact ⇓⟨cur, xs⟩ => ⌜True⌝ - all_goals simp_all -- relies on `Nat.size_Rcc` + case inv1 => exact ⇓⟨cur, xs⟩ => ⌜xs.length = cur.prefix.length⌝ + case inv2 => exact ⇓⟨cur, xs⟩ => ⌜True⌝ -- factorial loop + case inv3 => exact ⇓⟨cur, xs⟩ => ⌜True⌝ -- sum loop + all_goals simp_all -- relies on `Nat.length_toList_rcc` theorem f_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : (f n)[k]'(by grind [length_f]) = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1) := by @@ -168,51 +80,27 @@ theorem f_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : exact ⇓⟨cur, xs⟩ => ⌜xs.length = cur.prefix.length ∧ ((_ : k < xs.length) → xs[xs.length - 1 - k] = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1))⌝ - case vc10 => simp -- base case - case vc11 => -- postcondition - rename_i h - obtain ⟨h, h'⟩ := h - simp_all + case vc7 => simp -- base case + case vc8 => grind [Nat.length_toList_rcc] -- postcondition -- FACTORIAL LOOP case inv2 => exact ⇓⟨cur, x⟩ => ⌜x = factorial cur.prefix.length⌝ - case vc4 => simp [factorial] -- base case - case vc5 => -- postcondition - simp_all only [Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_›, - Std.PRange.UpwardEnumerable.succMany?, SPred.down_pure, - Std.PRange.length_toList_eq_size, Nat.size_Rcc, List.length_cons, - List.length_append, List.length_nil, true_and, List.getElem_cons] - split - · simp_all only [SPred.down_pure, Std.PRange.length_toList_eq_size, Nat.size_Rcc] - grind - · rename_i h' _ _ - refine fun _ => - Eq.trans ?_ (h'.2 ?_) <;> grind only -- `grind` without `only` fails, see #10233 - case vc3.step => -- step - have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› - simp_all only [factorial, SPred.down_pure, Std.PRange.UpwardEnumerable.succMany?, - Option.get_some] - grind [factorial] - + case vc2 => simp [factorial] -- base case + case vc3 => -- step + simp_all only [Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›, Std.PRange.succMany?, + Nat.length_toList_rcc] + grind + case vc1 => -- postcondition + simp_all [Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›, factorial, Nat.add_comm 1] -- SUM LOOP case inv3 => exact ⇓⟨cur, x⟩ => ⌜x = triangle cur.prefix.length⌝ - case vc8 => simp [triangle] -- base case - case vc9 => -- postcondition - simp_all only [Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_›, - Std.PRange.UpwardEnumerable.succMany?, SPred.down_pure, - Std.PRange.length_toList_eq_size, Nat.size_Rcc, List.length_cons, - List.length_append, List.length_nil, true_and, List.getElem_cons] - split - · simp_all only [SPred.down_pure, Std.PRange.length_toList_eq_size, Nat.size_Rcc] - grind - · rename_i h' _ _ - refine fun _ => - Eq.trans ?_ (h'.2 ?_) <;> grind only -- `grind` without `only` fails, see #10233 - case vc7.step => -- step - have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› - simp_all only [factorial, SPred.down_pure, Std.PRange.UpwardEnumerable.succMany?, - Option.get_some] - grind [triangle] + case vc5 => simp [triangle] -- base case + case vc6 => -- step + simp_all only [Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›, Std.PRange.succMany?, + Nat.length_toList_rcc] + grind + case vc4 => -- postcondition + simp_all [Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›, triangle, Nat.add_comm 1] end NaiveImpl @@ -257,9 +145,8 @@ theorem size_f' {n : Nat} : mvcgen all_goals try infer_instance case inv1 => exact ⇓⟨cur, xs⟩ => ⌜xs.size = cur.prefix.length + 2⌝ - all_goals try simp_all; done -- relies on `Nat.size_Rcc` - simp_all only [Nat.not_le, Std.PRange.length_toList_eq_size, Nat.size_Rco, SPred.down_pure] - grind + all_goals try (simp_all; done) -- relies on `Nat.size_Rcc` + grind [Nat.not_le, Nat.length_toList_rco] theorem f'_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : (f' n)[k]'(by grind [size_f']) = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1) := by @@ -272,37 +159,23 @@ theorem f'_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : exact ⇓⟨cur, xs⟩ => ⌜xs.size = cur.prefix.length + 2 ∧ ∀ j : Nat, (_ : j < xs.size) → (j % 2 = 1 → xs[j] = factorial (j + 1)) ∧ (j % 2 = 0 → xs[j] = triangle (j + 1))⌝ case vc1 hn => -- verification of the early return - simp only [List.extract_toArray, Nat.sub_zero, - List.drop_zero, List.size_toArray, List.length_take, List.length_cons, List.length_nil, - Nat.min_eq_left, getElem?_pos, Option.some.injEq, hn, hlt] + -- the return value is a prefix of `[1, 2]` and `k` is the index that needs to be verified match k with - | 0 => simp [triangle] - | 1 => simp [factorial] + | 0 => grind [triangle] + | 1 => grind [factorial] | n + 2 => grind - case vc5 => -- base case of the loop - mleave - simp only [Array.emptyWithCapacity_eq, List.push_toArray, List.nil_append, List.cons_append, - List.size_toArray, List.length_cons, true_and] - intro k hk - match k with - | 0 => simp [triangle] - | 1 => simp [factorial] - | n + 2 => grind - case vc3 hmod h => -- `then` branch - mleave - have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› - simp only [Std.PRange.UpwardEnumerable.succMany?, Option.get_some] at this - simp only [Array.size_push, List.length_append, List.length_cons, List.length_nil, Nat.zero_add] + case vc4 => -- base case of the loop + grind [triangle, factorial] + case vc2 hmod h => -- `then` branch + have := Std.Rco.eq_succMany?_of_toList_eq_append_cons ‹_› + simp only [Std.PRange.UpwardEnumerable.succMany?] at this grind [factorial] - case vc4 => -- `else` branch - mleave - have := Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons ‹_› - simp only [Std.PRange.UpwardEnumerable.succMany?, Option.get_some] at this - simp only [Array.size_push, List.length_append, List.length_cons, List.length_nil, Nat.zero_add] + case vc3 => -- `else` branch + have := Std.Rco.eq_succMany?_of_toList_eq_append_cons ‹_› + simp only [Std.PRange.UpwardEnumerable.succMany?] at this grind [triangle] - case vc6 => -- postcondition - simp only [Nat.not_le, Std.PRange.length_toList_eq_size, Nat.size_Rco, SPred.down_pure] at * - grind + case vc5 => -- postcondition + grind [Nat.not_le, Nat.length_toList_rco] end EfficientImpl From 4514ed351653ef5a74d35ea36cdf48ea7a3b0cc8 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Thu, 18 Dec 2025 00:29:59 +0100 Subject: [PATCH 13/16] disable mvcgen warning --- HumanEvalLean/HumanEval106.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index c9465fe..ddafdac 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -9,6 +9,8 @@ import all Init.Data.Iterators.Consumers.Loop This file provides two solutions for problem 106: a naïve one and an efficient one. -/ +set_option mvcgen.warning false + open Std.Do section NaiveImpl From 83c7c78602622ddd36cc62b2c98369d36899e945 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 21 Jan 2026 11:10:47 +0100 Subject: [PATCH 14/16] more efficient solution --- HumanEvalLean/HumanEval106.lean | 110 ++++++++++++++++++++++++++++++++ 1 file changed, 110 insertions(+) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index ddafdac..ba85293 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -1,5 +1,7 @@ module +import Lean.LibrarySuggestions.Default + import Std.Tactic.Do -- Sadly, it's apparently currently impossible to easily prove the size of a -- `Nat` range without unfolding internal stuff. This should be fixed in the standard library. @@ -181,6 +183,114 @@ theorem f'_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : end EfficientImpl +section MoreEfficientImpl + +/-! +## An efficient implementation avoiding `[·]!` +-/ + +def f'' (n : Nat) : Array Nat := Id.run do + if n ≤ 2 then + return #[1, 2].take n + let mut ret : Array Nat := .emptyWithCapacity n + ret := ret.push 1 -- 1st entry should be `triangle 1` + ret := ret.push 2 -- 2nd entry should be `factorial 2` + let mut even := 1 + let mut odd := 2 + for i in 2... exact ⇓⟨cur, _, _, xs⟩ => ⌜xs.size = cur.prefix.length + 2⌝ + all_goals grind [Nat.length_toList_rco] + +def lastFactorial (n : Nat) := factorial (n / 2 * 2) +def lastTriangle (n : Nat) := triangle ((n - 1) / 2 * 2 + 1) + +@[grind =] theorem lastTriangle_two : lastTriangle 2 = 1 := by decide +@[grind =] theorem lastFactorial_two : lastFactorial 2 = 2 := by decide + +theorem lastTriangle_add_one (h : n % 2 = 1) : + lastTriangle (n + 1) = lastTriangle n := by + grind [lastTriangle] + +@[grind =] +theorem lastFactorial_add_one_of_odd (h : n % 2 = 1) : + lastFactorial (n + 1) = lastFactorial n * n * (n + 1) := by + have : (n + 1) / 2 * 2 = n / 2 * 2 + 2 := by grind + grind [lastFactorial, factorial] + +@[grind =] +theorem lastTriangle_add_one_of_odd (h : n % 2 = 1) : + lastTriangle (n + 1) = lastTriangle n := by + grind [lastTriangle] + +@[grind =] +theorem lastTriangle_add_one_of_even (h : n % 2 = 0) (h' : 0 < n) : + lastTriangle (n + 1) = lastTriangle n + 2 * n + 1 := by + have : n / 2 * 2 = (n - 1) / 2 * 2 + 2 := by grind + grind [lastTriangle, triangle] + +@[grind =] +theorem lastFactorial_add_one_of_even (h : n % 2 = 0) : + lastFactorial (n + 1) = lastFactorial n := by + grind [lastFactorial] + +attribute [grind =] Std.PRange.Nat.succMany?_eq + +theorem f''_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : + (f'' n)[k]'(by grind [size_f'']) = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1) := by + rw [Array.getElem_eq_iff] + generalize hwp : f'' n = w + apply Std.Do.Id.of_wp_run_eq hwp + mvcgen + all_goals try infer_instance + case inv1 => + exact ⇓⟨cur, even, odd, xs⟩ => ⌜xs.size = cur.prefix.length + 2 ∧ odd = lastFactorial xs.size ∧ even = lastTriangle xs.size ∧ ∀ j : Nat, (_ : j < xs.size) → + (j % 2 = 1 → xs[j] = factorial (j + 1)) ∧ (j % 2 = 0 → xs[j] = triangle (j + 1))⌝ + case vc1 hn => -- verification of the early return + -- the return value is a prefix of `[1, 2]` and `k` is the index that needs to be verified + match k with + | 0 => grind [triangle] + | 1 => grind [factorial] + | n + 2 => grind + case vc4 => -- base case of the loop + grind [triangle, factorial] + case vc2 hmod h => -- `then` branch + have := Std.Rco.eq_succMany?_of_toList_eq_append_cons ‹_› + grind [lastFactorial, factorial] + case vc3 => -- `else` branch + have := Std.Rco.eq_succMany?_of_toList_eq_append_cons ‹_› + grind [triangle] + case vc5 => -- postcondition + grind [Nat.not_le, Nat.length_toList_rco] + +end MoreEfficientImpl + /-! ## Prompt From 89de69f58c15484bee59532440717b82fb72168d Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 21 Jan 2026 11:34:46 +0100 Subject: [PATCH 15/16] cleanups --- HumanEvalLean/HumanEval106.lean | 68 ++++++++++++++++++--------------- 1 file changed, 38 insertions(+), 30 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index ba85293..fae2356 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -3,18 +3,18 @@ module import Lean.LibrarySuggestions.Default import Std.Tactic.Do --- Sadly, it's apparently currently impossible to easily prove the size of a --- `Nat` range without unfolding internal stuff. This should be fixed in the standard library. -import all Init.Data.Iterators.Consumers.Loop /-! -This file provides two solutions for problem 106: a naïve one and an efficient one. +This file provides three solutions for problem 106, progressing from most simple to most efficient. -/ set_option mvcgen.warning false open Std.Do +-- missing grind annotations +attribute [grind =] Nat.length_toList_rco Std.PRange.Nat.succMany?_eq Nat.not_le + section NaiveImpl /-! @@ -47,10 +47,12 @@ example : f 3 = [1, 2, 6] := by native_decide ### Verification -/ +@[grind =] def factorial : Nat → Nat | 0 => 1 | n + 1 => factorial n * (n + 1) +@[grind =] def triangle : Nat → Nat | 0 => 0 | n + 1 => triangle n + (n + 1) @@ -71,7 +73,7 @@ theorem length_f {n : Nat} : case inv3 => exact ⇓⟨cur, xs⟩ => ⌜True⌝ -- sum loop all_goals simp_all -- relies on `Nat.length_toList_rcc` -theorem f_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : +theorem getElem_f {n : Nat} {k : Nat} (hlt : k < n) : (f n)[k]'(by grind [length_f]) = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1) := by rw [List.getElem_eq_iff] generalize hwp : f n = w @@ -150,9 +152,9 @@ theorem size_f' {n : Nat} : all_goals try infer_instance case inv1 => exact ⇓⟨cur, xs⟩ => ⌜xs.size = cur.prefix.length + 2⌝ all_goals try (simp_all; done) -- relies on `Nat.size_Rcc` - grind [Nat.not_le, Nat.length_toList_rco] + grind -theorem f'_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : +theorem getElem_f' {n : Nat} {k : Nat} (hlt : k < n) : (f' n)[k]'(by grind [size_f']) = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1) := by rw [Array.getElem_eq_iff] generalize hwp : f' n = w @@ -165,21 +167,21 @@ theorem f'_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : case vc1 hn => -- verification of the early return -- the return value is a prefix of `[1, 2]` and `k` is the index that needs to be verified match k with - | 0 => grind [triangle] - | 1 => grind [factorial] + | 0 => grind + | 1 => grind | n + 2 => grind case vc4 => -- base case of the loop - grind [triangle, factorial] + grind case vc2 hmod h => -- `then` branch have := Std.Rco.eq_succMany?_of_toList_eq_append_cons ‹_› simp only [Std.PRange.UpwardEnumerable.succMany?] at this - grind [factorial] + grind case vc3 => -- `else` branch have := Std.Rco.eq_succMany?_of_toList_eq_append_cons ‹_› simp only [Std.PRange.UpwardEnumerable.succMany?] at this - grind [triangle] + grind case vc5 => -- postcondition - grind [Nat.not_le, Nat.length_toList_rco] + grind end EfficientImpl @@ -195,15 +197,15 @@ def f'' (n : Nat) : Array Nat := Id.run do let mut ret : Array Nat := .emptyWithCapacity n ret := ret.push 1 -- 1st entry should be `triangle 1` ret := ret.push 2 -- 2nd entry should be `factorial 2` - let mut even := 1 - let mut odd := 2 + let mut even := 1 -- `triangle 1 = 1` + let mut odd := 2 -- `factorial 2 = 2` for i in 2... exact ⇓⟨cur, _, _, xs⟩ => ⌜xs.size = cur.prefix.length + 2⌝ - all_goals grind [Nat.length_toList_rco] + all_goals grind def lastFactorial (n : Nat) := factorial (n / 2 * 2) def lastTriangle (n : Nat) := triangle ((n - 1) / 2 * 2 + 1) @@ -234,6 +236,14 @@ def lastTriangle (n : Nat) := triangle ((n - 1) / 2 * 2 + 1) @[grind =] theorem lastTriangle_two : lastTriangle 2 = 1 := by decide @[grind =] theorem lastFactorial_two : lastFactorial 2 = 2 := by decide +@[grind →] +theorem lastTriangle_of_odd (h : n % 2 = 1) : lastTriangle n = triangle n := by + grind [lastTriangle] + +@[grind →] +theorem lastFactorial_of_even (h : n % 2 = 0) : lastFactorial n = factorial n := by + grind [lastFactorial] + theorem lastTriangle_add_one (h : n % 2 = 1) : lastTriangle (n + 1) = lastTriangle n := by grind [lastTriangle] @@ -242,7 +252,7 @@ theorem lastTriangle_add_one (h : n % 2 = 1) : theorem lastFactorial_add_one_of_odd (h : n % 2 = 1) : lastFactorial (n + 1) = lastFactorial n * n * (n + 1) := by have : (n + 1) / 2 * 2 = n / 2 * 2 + 2 := by grind - grind [lastFactorial, factorial] + grind [lastFactorial] @[grind =] theorem lastTriangle_add_one_of_odd (h : n % 2 = 1) : @@ -253,16 +263,14 @@ theorem lastTriangle_add_one_of_odd (h : n % 2 = 1) : theorem lastTriangle_add_one_of_even (h : n % 2 = 0) (h' : 0 < n) : lastTriangle (n + 1) = lastTriangle n + 2 * n + 1 := by have : n / 2 * 2 = (n - 1) / 2 * 2 + 2 := by grind - grind [lastTriangle, triangle] + grind [lastTriangle] @[grind =] theorem lastFactorial_add_one_of_even (h : n % 2 = 0) : lastFactorial (n + 1) = lastFactorial n := by grind [lastFactorial] -attribute [grind =] Std.PRange.Nat.succMany?_eq - -theorem f''_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : +theorem getElem_f'' {n : Nat} {k : Nat} (hlt : k < n) : (f'' n)[k]'(by grind [size_f'']) = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1) := by rw [Array.getElem_eq_iff] generalize hwp : f'' n = w @@ -275,19 +283,19 @@ theorem f''_eq_fac {n : Nat} {k : Nat} (hlt : k < n) : case vc1 hn => -- verification of the early return -- the return value is a prefix of `[1, 2]` and `k` is the index that needs to be verified match k with - | 0 => grind [triangle] - | 1 => grind [factorial] + | 0 => grind + | 1 => grind | n + 2 => grind case vc4 => -- base case of the loop - grind [triangle, factorial] + grind case vc2 hmod h => -- `then` branch have := Std.Rco.eq_succMany?_of_toList_eq_append_cons ‹_› - grind [lastFactorial, factorial] + grind case vc3 => -- `else` branch have := Std.Rco.eq_succMany?_of_toList_eq_append_cons ‹_› - grind [triangle] + grind case vc5 => -- postcondition - grind [Nat.not_le, Nat.length_toList_rco] + grind end MoreEfficientImpl From a4bf1f7bbdcfdd087078dfe0d1e05252ca0be58d Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 21 Jan 2026 12:22:44 +0100 Subject: [PATCH 16/16] final cleanups --- HumanEvalLean/HumanEval106.lean | 96 +++++++++++++++------------------ 1 file changed, 44 insertions(+), 52 deletions(-) diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean index fae2356..ada1b2b 100644 --- a/HumanEvalLean/HumanEval106.lean +++ b/HumanEvalLean/HumanEval106.lean @@ -13,7 +13,7 @@ set_option mvcgen.warning false open Std.Do -- missing grind annotations -attribute [grind =] Nat.length_toList_rco Std.PRange.Nat.succMany?_eq Nat.not_le +attribute [grind =] Nat.length_toList_rco Nat.length_toList_rcc Std.PRange.Nat.succMany?_eq Nat.not_le section NaiveImpl @@ -67,11 +67,11 @@ theorem length_f {n : Nat} : generalize hwp : f n = w apply Std.Do.Id.of_wp_run_eq hwp mvcgen - all_goals try infer_instance - case inv1 => exact ⇓⟨cur, xs⟩ => ⌜xs.length = cur.prefix.length⌝ - case inv2 => exact ⇓⟨cur, xs⟩ => ⌜True⌝ -- factorial loop - case inv3 => exact ⇓⟨cur, xs⟩ => ⌜True⌝ -- sum loop - all_goals simp_all -- relies on `Nat.length_toList_rcc` + invariants + | inv1 => ⇓⟨cur, xs⟩ => ⌜xs.length = cur.prefix.length⌝ + | inv2 => ⇓⟨cur, xs⟩ => ⌜True⌝ -- factorial loop + | inv3 => ⇓⟨cur, xs⟩ => ⌜True⌝ -- sum loop + with grind theorem getElem_f {n : Nat} {k : Nat} (hlt : k < n) : (f n)[k]'(by grind [length_f]) = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1) := by @@ -79,31 +79,30 @@ theorem getElem_f {n : Nat} {k : Nat} (hlt : k < n) : generalize hwp : f n = w apply Std.Do.Id.of_wp_run_eq hwp mvcgen - all_goals try infer_instance - - -- OUTER LOOP - case inv1 => - exact ⇓⟨cur, xs⟩ => ⌜xs.length = cur.prefix.length ∧ + invariants + -- outer loop + | inv1 => ⇓⟨cur, xs⟩ => ⌜xs.length = cur.prefix.length ∧ ((_ : k < xs.length) → xs[xs.length - 1 - k] = if k % 2 = 0 then triangle (k + 1) else factorial (k + 1))⌝ + -- factorial loop + | inv2 => ⇓⟨cur, x⟩ => ⌜x = factorial cur.prefix.length⌝ + -- sum loop + | inv3 => ⇓⟨cur, x⟩ => ⌜x = triangle cur.prefix.length⌝ + + -- OUTER LOOP case vc7 => simp -- base case - case vc8 => grind [Nat.length_toList_rcc] -- postcondition + case vc8 => grind -- postcondition -- FACTORIAL LOOP - case inv2 => exact ⇓⟨cur, x⟩ => ⌜x = factorial cur.prefix.length⌝ - case vc2 => simp [factorial] -- base case case vc3 => -- step - simp_all only [Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›, Std.PRange.succMany?, - Nat.length_toList_rcc] + have := Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_› grind case vc1 => -- postcondition simp_all [Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›, factorial, Nat.add_comm 1] + -- SUM LOOP - case inv3 => exact ⇓⟨cur, x⟩ => ⌜x = triangle cur.prefix.length⌝ - case vc5 => simp [triangle] -- base case case vc6 => -- step - simp_all only [Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›, Std.PRange.succMany?, - Nat.length_toList_rcc] + have := Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_› grind case vc4 => -- postcondition simp_all [Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_›, triangle, Nat.add_comm 1] @@ -122,13 +121,13 @@ def f' (n : Nat) : Array Nat := Id.run do let mut ret : Array Nat := .emptyWithCapacity n ret := ret.push 1 -- 1st entry should be `triangle 1` ret := ret.push 2 -- 2nd entry should be `factorial 2` - for i in 2... - exact ⇓⟨cur, xs⟩ => ⌜xs.size = cur.prefix.length + 2 ∧ ∀ j : Nat, (_ : j < xs.size) → + invariants + | inv1 => ⇓⟨cur, xs⟩ => ⌜xs.size = cur.prefix.length + 2 ∧ ∀ j : Nat, (_ : j < xs.size) → (j % 2 = 1 → xs[j] = factorial (j + 1)) ∧ (j % 2 = 0 → xs[j] = triangle (j + 1))⌝ case vc1 hn => -- verification of the early return - -- the return value is a prefix of `[1, 2]` and `k` is the index that needs to be verified - match k with - | 0 => grind - | 1 => grind - | n + 2 => grind + grind case vc4 => -- base case of the loop grind case vc2 hmod h => -- `then` branch - have := Std.Rco.eq_succMany?_of_toList_eq_append_cons ‹_› - simp only [Std.PRange.UpwardEnumerable.succMany?] at this + have := Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_› grind case vc3 => -- `else` branch - have := Std.Rco.eq_succMany?_of_toList_eq_append_cons ‹_› - simp only [Std.PRange.UpwardEnumerable.succMany?] at this + have := Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_› grind case vc5 => -- postcondition grind @@ -197,15 +189,15 @@ def f'' (n : Nat) : Array Nat := Id.run do let mut ret : Array Nat := .emptyWithCapacity n ret := ret.push 1 -- 1st entry should be `triangle 1` ret := ret.push 2 -- 2nd entry should be `factorial 2` - let mut even := 1 -- `triangle 1 = 1` - let mut odd := 2 -- `factorial 2 = 2` - for i in 2... exact ⇓⟨cur, _, _, xs⟩ => ⌜xs.size = cur.prefix.length + 2⌝ - all_goals grind + invariants + | inv1 => ⇓⟨cur, _, _, xs⟩ => ⌜xs.size = cur.prefix.length + 2⌝ + with grind def lastFactorial (n : Nat) := factorial (n / 2 * 2) def lastTriangle (n : Nat) := triangle ((n - 1) / 2 * 2 + 1) @@ -276,9 +268,9 @@ theorem getElem_f'' {n : Nat} {k : Nat} (hlt : k < n) : generalize hwp : f'' n = w apply Std.Do.Id.of_wp_run_eq hwp mvcgen - all_goals try infer_instance - case inv1 => - exact ⇓⟨cur, even, odd, xs⟩ => ⌜xs.size = cur.prefix.length + 2 ∧ odd = lastFactorial xs.size ∧ even = lastTriangle xs.size ∧ ∀ j : Nat, (_ : j < xs.size) → + invariants + | inv1 => + ⇓⟨cur, even, odd, xs⟩ => ⌜xs.size = cur.prefix.length + 2 ∧ even = lastFactorial xs.size ∧ odd = lastTriangle xs.size ∧ ∀ j : Nat, (_ : j < xs.size) → (j % 2 = 1 → xs[j] = factorial (j + 1)) ∧ (j % 2 = 0 → xs[j] = triangle (j + 1))⌝ case vc1 hn => -- verification of the early return -- the return value is a prefix of `[1, 2]` and `k` is the index that needs to be verified @@ -289,10 +281,10 @@ theorem getElem_f'' {n : Nat} {k : Nat} (hlt : k < n) : case vc4 => -- base case of the loop grind case vc2 hmod h => -- `then` branch - have := Std.Rco.eq_succMany?_of_toList_eq_append_cons ‹_› + have := Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_› grind case vc3 => -- `else` branch - have := Std.Rco.eq_succMany?_of_toList_eq_append_cons ‹_› + have := Std.Rcc.eq_succMany?_of_toList_eq_append_cons ‹_› grind case vc5 => -- postcondition grind