chore: bump to nightly-2026-03-22

HumanEvalLean/Common/Brackets.lean

@@ -262,7 +262,7 @@ theorem isBalanced_eq_true_iff {openBracket closeBracket : Char} {s : String} (h
   generalize hwp : isBalanced openBracket closeBracket s = w
   apply Std.Do.Id.of_wp_run_eq hwp
   mvcgen
-  case inv =>
+  case inv1 =>
     exact Std.Do.StringInvariant.withEarlyReturn
       (fun pos depth => ⌜∀ t₁ t₂, pos.Splits t₁ t₂ → minBalance (parens openBracket closeBracket t₁) = 0 ∧ depth = balance (parens openBracket closeBracket t₁)⌝)
       (fun res depth => ⌜res = false ∧ ¬ IsBalanced (parens openBracket closeBracket s)⌝)

HumanEvalLean/HumanEval1.lean

@@ -53,7 +53,7 @@ theorem goal {s : String} {hbal : IsBalanced (parens '(' ')' s)} :
   generalize hwp : separateParenGroups s = w
   apply Std.Do.Id.of_wp_run_eq hwp
   mvcgen
-  case vc1.inv => exact ⇓⟨pos, ⟨curr, depth, result⟩⟩ =>
+  case inv1 => exact ⇓⟨pos, ⟨curr, depth, result⟩⟩ =>
     ⌜∀ t₁ t₂, pos.Splits t₁ t₂ →
       result.toList.flatMap (parens '(' ')') ++ (parens '(' ')' curr) = parens '(' ')' t₁ ∧
       result.toList.flatMap String.toList ++ curr.toList = t₁.toList.filter (fun c => c = '(' ∨ c = ')') ∧

HumanEvalLean/HumanEval119.lean

@@ -41,7 +41,7 @@ theorem computeBalance_eq {s : String.Slice} :
   generalize hwp : computeBalance s = w
   apply Std.Do.Id.of_wp_run_eq hwp
   mvcgen
-  case inv => exact (⇓(pos, ⟨bal, minBal⟩) => ⌜∀ (t₁ t₂ : String), pos.Splits t₁ t₂ →
+  case inv1 => exact (⇓(pos, ⟨bal, minBal⟩) => ⌜∀ (t₁ t₂ : String), pos.Splits t₁ t₂ →
     bal = balance (parens '(' ')' t₁) ∧ minBal = minBalance (parens '(' ')' t₁)⌝)
   next pos _ hp bal minBal h newBal newMinBal ih =>
     simp only [↓Char.isValue, SPred.down_pure] at ⊢ ih

HumanEvalLean/HumanEval128.lean

@@ -41,12 +41,7 @@ theorem List.product_eq_zero_iff {xs : List Int} :
 
 theorem Option.of_wp {α} {prog : Option α} (P : Option α → Prop) :
     (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (some a)⌝, fun _ => ⌜P none⌝⟩) → P prog := by
-  intro hspec
-  simp only [wp, PredTrans.apply_pushOption, PredTrans.apply_Pure_pure, SPred.entails_nil,
-    SPred.down_pure, forall_const] at hspec
-  split at hspec
-  case h_1 a s' heq => rw [← heq] at hspec; exact hspec
-  case h_2 s' heq => rw [← heq] at hspec; exact hspec
+  cases prog <;> simp [wp, Option.instWP._aux_1, OptionT.run]
 
 theorem Option.of_wp_eq {α : Type} {x : Option α} {prog : Option α} (h : prog = x) (P : Option α → Prop) :
     (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (some a)⌝, fun _ => ⌜P none⌝⟩) → P x := by

HumanEvalLean/HumanEval129.lean

@@ -2,6 +2,7 @@ module
 
 import Std
 import all Init.Data.Range.Polymorphic.RangeIterator
+public meta import Std.Tactic.Do.Syntax
 open Std Std.Do
 
 set_option mvcgen.warning false

HumanEvalLean/HumanEval6.lean

@@ -30,7 +30,7 @@ theorem computeMaxDepth_eq {s : String.Slice} :
   generalize hwp : computeMaxDepth s = w
   apply Std.Do.Id.of_wp_run_eq hwp
   mvcgen
-  case inv => exact (⇓(pos, ⟨bal, maxBal⟩) => ⌜∀ (t₁ t₂ : String), pos.Splits t₁ t₂ →
+  case inv1 => exact (⇓(pos, ⟨bal, maxBal⟩) => ⌜∀ (t₁ t₂ : String), pos.Splits t₁ t₂ →
     bal = balance (parens '(' ')' t₁) ∧ maxBal = maxBalance (parens '(' ')' t₁)⌝)
   next pos _ hp bal minBal h newBal newMinBal ih =>
     simp only [↓Char.isValue, SPred.down_pure] at ⊢ ih

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-03-09
+leanprover/lean4:nightly-2026-03-22