chore: Update Lean to v4.33.1

.github/workflows/update.yml

@@ -0,0 +1,55 @@
+name: Update Lean toolchain and pinned deps
+
+on:
+  schedule:
+    # Daily at 00:00 UTC
+    - cron: "0 0 * * *"
+  workflow_dispatch:
+
+permissions:
+  contents: write
+  pull-requests: write
+
+jobs:
+  update:
+    runs-on: ubuntu-latest
+    steps:
+      # create-pull-request takes its base from the checked-out branch, and the
+      # action passes no `base` of its own, so this is what points the update PR
+      # at `dev`. `dev` is already the default branch; naming it keeps the PR
+      # off `master`, which only mirrors digama0/lean4lean (see repo-sync.yml)
+      # and would discard the commit on its next force-sync.
+      - uses: actions/checkout@v7
+        with:
+          ref: dev
+
+      # Mint a token from the GitHub App so the opened PR triggers CI; pushes
+      # made with GITHUB_TOKEN do not. Same App as repo-sync.yml.
+      - uses: actions/create-github-app-token@v3
+        id: app-token
+        with:
+          client-id: ${{ secrets.TOKEN_APP_ID }}
+          private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}
+
+      # `dev` carries the fork's bump_mode/release_channel support; `main` only
+      # mirrors upstream, which silently ignores these inputs. `pinned-tags`
+      # suits this package: batteries is pinned to a Lean version tag rather
+      # than tracking a branch, so its `rev` moves with the toolchain; a
+      # dependency pinned to a commit hash is reported and left alone. A PR is
+      # opened on an update/lean-{release} branch whether or not the build
+      # passes, so an incompatible release shows up as a failing PR to review --
+      # expected here, where a toolchain bump can break the kernel internals
+      # this package mirrors.
+      #
+      # Only the Lean half is automated. flake.nix resolves the toolchain from
+      # `lean-toolchain` through lean4-nix's vendored release table, so nix.yml
+      # fails at evaluation on a release that table has not recorded yet. Those
+      # hashes arrive through lean4-nix's own lean-update PR, which will not
+      # have merged by the time this job runs, so bumping the `lean4-nix` flake
+      # input here would only add unrelated churn. It stays a manual follow-up
+      # on the update PR once lean4-nix has landed the release.
+      - uses: argumentcomputer/lean-update@dev
+        with:
+          bump_mode: pinned-tags
+          on_update_fails: pr
+          token: ${{ steps.app-token.outputs.token }}

Lean4Lean/Audit/SorryFrontier.lean

@@ -58,7 +58,6 @@ import Lean4Lean.Verify.Environment.Normalization
 import Lean4Lean.Verify.Environment.NormalizationMatrix
 import Lean4Lean.Verify.Environment.SingletonParityMatrix
 import Lean4Lean.Verify.Environment.SingletonParityReplay
-import Lean4Lean.Verify.EquivManager
 import Lean4Lean.Verify.Expr
 import Lean4Lean.Verify.Level
 import Lean4Lean.Verify.LocalContext

Lean4Lean/FuelConfig.lean

@@ -28,4 +28,8 @@ structure FuelConfig where
   recDepth    : Nat := 10000
   /-- Shared fuel for the structural loops in `Inductive/Add.lean`. -/
   inductiveFuel : Nat := 1000
+  /-- Upper bound, in bytes, on the `Nat` numerals the kernel will accept or compute while
+  reducing `Nat` literals. Bounds the memory and time a single reduction can consume. The
+  native kernel spells this bound `LEAN_NAT_MAX_SIZE` and defaults it to the same 128 MB. -/
+  natMaxSize : Nat := 134217728 -- 128 MB; a literal so `simp` cannot renormalize it
   deriving Repr, Inhabited, Lean.FromJson, Lean.ToJson

Lean4Lean/Inductive/Add.lean

@@ -107,6 +107,11 @@ instance : MonadLCtx M where
 @[inline] def withEnv (env : Environment) (x : M α) : M α :=
   withReader (fun c => { c with env }) x
 
+/-- Run an action under a different universe parameter list. The recursors are checked under
+their own parameters, which carry the extra eliminator level the declaration itself lacks. -/
+@[inline] def withLParams (lparams : List Name) (x : M α) : M α :=
+  withReader (fun c => { c with lparams }) x
+
 /-- Run a closed-metadata action without inheriting validation-local
 declarations.  All other reader fields, including the staged environment and
 fuel, are preserved exactly. -/
@@ -2652,6 +2657,39 @@ def mkRecRules (indTypes : Array InductiveType) (elimLevel : Level) (stats : Ind
     rules := rules.push rule
   return rules.toList
 
+/-- Defensively type-checks the generated recursors.
+
+`run` installs a recursor and its computation rules without re-checking them. This verifies that
+(1) each recursor's type is well typed, and (2) each computation rule is type-preserving: reducing
+the recursor applied to a constructor yields a term whose type is the recursor's declared result
+type. This catches a recursor whose minor-premise type and reduction rule disagree; checking only
+that a rule's right-hand side has *some* type is insufficient, because an under-applied minor
+premise is still a well-typed (function) term. -/
+def checkRecursors (indTypes : Array InductiveType) (elimLevel : Level)
+    (stats : InductiveStats) (motives minors : Array Expr) : M Unit := do
+  let {lparams, ..} ← read
+  let lvls := getRecLevels elimLevel stats.levels
+  withLParams (getRecLevelParams elimLevel lparams) do
+  for h : dIdx in [:indTypes.size] do
+    let indType := indTypes[dIdx]
+    let recName := mkRecName indType.name
+    let recCi ← (← read).env.get recName
+    -- (1) The recursor type must be well typed.
+    _ ← (TypeChecker.checkType recCi.type : TypeChecker.M Expr)
+    let recPre := mkAppN (mkAppN (mkAppN (.const recName lvls) stats.params) motives) minors
+    -- (2) Each computation rule must preserve types.
+    for ctor in indType.ctors do
+      mkRecInfos.loopCtorArgs stats ctor.type fun t bu _ => do
+        let (_, itIndices) := getIIndices stats t
+        let introApp := mkAppN (mkAppN (.const ctor.name stats.levels) stats.params) bu
+        let lhs := (mkAppN recPre itIndices).app introApp
+        let expected ← inferType lhs
+        let reduct ← whnf lhs
+        let actual ← inferType reduct
+        unless ← isDefEq actual expected do
+          throw <| .other s!"generated recursor computation rule for '{ctor.name
+            }' is not type-preserving"
+
 def run (nparams : Nat) (types : List InductiveType) (numNested : Nat) : M Environment := do
   let isUnsafe := (← read).safety != .safe
   let indTypes := types.toArray
@@ -2694,6 +2732,7 @@ def run (nparams : Nat) (types : List InductiveType) (numNested : Nat) : M Envir
       numIndices := stats.nindices[dIdx]!
       name, all, numMotives, numMinors, rules, k, isUnsafe
     }
+  withEnv env <| checkRecursors indTypes elimLevel stats motives minors
   pure env
 
 end AddInductive
@@ -2939,6 +2978,61 @@ def checkNoNestedAux (n : Name) (e : Expr) : Except Exception Unit := do
       | _ => false).isSome then
     throw <| .other s!"invalid declaration '{n}', it uses the reserved prefix '_nested'"
 
+/-- Checks the occurrence of a datatype being declared at the head of `e`, if there is one.
+Returns `true` when the occurrence was checked and `e`'s subterms need not be revisited. -/
+def checkUniformIndOcc (lvls : List Level) (indNames : List Name) (nparams : Nat)
+    (e : Expr) (offset : Nat) : Except Exception Bool := do
+  let .const c ls := e.getAppFn | return false
+  unless indNames.contains c do return false
+  let args := e.getAppArgs
+  -- Over-applied: descend, so that occurrences in the indices are checked too. The parameter
+  -- application itself is visited as a subterm of `e` and checked then.
+  if args.size > nparams then return false
+  let ok := args.size == nparams && offset ≥ nparams && ls == lvls
+    && (List.range nparams).all fun i => args[i]! == .bvar (offset - 1 - i)
+  unless ok do
+    throw <| .other s!"invalid occurrence of datatype '{c}' being declared: it must be applied \
+      to the parameters and universe levels of the mutual declaration"
+  return true
+
+/-- Checks that every occurrence of a datatype being declared in `e` is applied to the
+declaration's universe levels and to its parameters, which at binder depth `offset` are the bound
+variables `#(offset-1) … #(offset-nparams)`. That those binders really are the parameters is
+established later, by the parameter check in `checkConstructors`. -/
+def checkUniformIndOccsIn (lvls : List Level) (indNames : List Name) (nparams : Nat) :
+    Expr → Nat → Except Exception Unit
+  | e, offset => do
+    if ← checkUniformIndOcc lvls indNames nparams e offset then return
+    match e with
+    | .forallE _ d b _ | .lam _ d b _ =>
+      checkUniformIndOccsIn lvls indNames nparams d offset
+      checkUniformIndOccsIn lvls indNames nparams b (offset + 1)
+    | .letE _ t v b _ =>
+      checkUniformIndOccsIn lvls indNames nparams t offset
+      checkUniformIndOccsIn lvls indNames nparams v offset
+      checkUniformIndOccsIn lvls indNames nparams b (offset + 1)
+    | .app f a =>
+      checkUniformIndOccsIn lvls indNames nparams f offset
+      checkUniformIndOccsIn lvls indNames nparams a offset
+    | .mdata _ b => checkUniformIndOccsIn lvls indNames nparams b offset
+    | .proj _ _ b => checkUniformIndOccsIn lvls indNames nparams b offset
+    | _ => pure ()
+
+/-- Runs `checkUniformIndOccsIn` over every constructor type of the declaration.
+
+Later phases inspect the constructor types modulo `whnf`, which can erase an occurrence (as in
+`(fun _ => Unit) (T Nat)`), and the parametric arguments of a nested occurrence are dropped from
+the auxiliary declaration altogether, so a non-uniform occurrence could escape checking there.
+Reduction never creates an occurrence of a datatype being declared, since those are not yet in the
+environment, so checking the syntactic occurrences here covers all of them. -/
+def checkUniformIndOccs (lparams : List Name) (nparams : Nat) (types : List InductiveType) :
+    Except Exception Unit := do
+  let lvls := lparams.map Level.param
+  let indNames := types.map (·.name)
+  for indType in types do
+    for ctor in indType.ctors do
+      checkUniformIndOccsIn lvls indNames nparams ctor.type 0
+
 def Environment.addInductive (env : Environment) (lparams : List Name) (nparams : Nat)
     (types : List InductiveType) (isUnsafe allowPrimitive : Bool) (fuel : FuelConfig := {}) :
     Except Exception Environment := do
@@ -2947,6 +3041,7 @@ def Environment.addInductive (env : Environment) (lparams : List Name) (nparams
     for ctor in indType.ctors do
       env.checkNoMVarNoFVar ctor.name ctor.type
       checkNoNestedAux ctor.name ctor.type
+  checkUniformIndOccs lparams nparams types
   let res ← ElimNestedInductive.run fuel.inductiveFuel nparams types env
     |>.run' { lvls := lparams.map .param, newTypes := types.toArray }
   let numNested := res.aux2nested.size

Lean4Lean/Inductive/Reduce.lean

@@ -9,6 +9,7 @@ open Kernel
 section
 variable [Monad m] (env : Environment)
     (whnf : Expr → m Expr) (inferType : Expr → m Expr) (isDefEq : Expr → Expr → m Bool)
+    (isNeverProp : Expr → m Bool)
 
 def getFirstCtor (dName : Name) : Option Name := do
   let some (.inductInfo info) := env.find? dName | none
@@ -60,8 +61,11 @@ def toCtorWhenStruct (inductName : Name) (e : Expr) : m Expr := do
     return e
   let eType ← whnf (← inferType e)
   if !eType.getAppFn.isConstOf inductName then return e
-  let .sort u ← whnf (← inferType eType) | unreachable!
-  unless u.isNeverZero do return e
+  -- Lean tests `is_prop eType` and declines to expand when it holds; lean4lean instead requires
+  -- the level to be *never* zero, so an uncertain level declines too (see `divergences.md`).
+  -- Either way the level comes from a sort-ensuring check, so a non-sort type raises a kernel
+  -- error rather than reaching an unreachable branch.
+  unless ← isNeverProp eType do return e
   return expandEtaStruct env eType e
 
 def getRecRuleFor (rval : RecursorVal) (major : Expr) : Option RecursorRule := do
@@ -78,7 +82,8 @@ constructor to everything before the indices in the recursor application (its pa
 and minor premises) and then to the fields of the constructor application; any arguments after the
 major premise are re-applied to the result. -/
 def inductiveReduceRec [Monad m] (env : Environment) (e : Expr)
-    (whnf : Expr → m Expr) (inferType : Expr → m Expr) (isDefEq : Expr → Expr → m Bool) :
+    (whnf : Expr → m Expr) (inferType : Expr → m Expr) (isDefEq : Expr → Expr → m Bool)
+    (isNeverProp : Expr → m Bool) :
     m (Option Expr) := do
   let .const recFn ls := e.getAppFn | return none
   let some (.recInfo info) := env.find? recFn | return none
@@ -91,7 +96,7 @@ def inductiveReduceRec [Monad m] (env : Environment) (e : Expr)
   match ← whnf major with
   | .lit (.natVal n) => major := .natLitToConstructor n
   | .lit (.strVal s) => major ← whnf (.strLitToConstructor s)
-  | e => major ← toCtorWhenStruct env whnf inferType info.getMajorInduct e
+  | e => major ← toCtorWhenStruct env whnf inferType isNeverProp info.getMajorInduct e
   let some rule := getRecRuleFor info major | return none
   let majorArgs := major.getAppArgs
   if rule.nfields > majorArgs.size then return none

Lean4Lean/Std/Basic.lean

@@ -1,7 +1,6 @@
 import Batteries.CodeAction
 import Batteries.Data.Array.Lemmas
 import Batteries.Data.HashMap.Basic
-import Batteries.Data.UnionFind.Basic
 import Batteries.Tactic.SeqFocus
 
 open Std
@@ -217,6 +216,12 @@ instance [BEq α] [PartialEquivBEq α] [BEq β] [PartialEquivBEq β] : PartialEq
 instance [BEq α] [EquivBEq α] [BEq β] [EquivBEq β] : EquivBEq (α × β) where
   rfl := by simp [(· == ·)]
 
+instance [BEq α] [Hashable α] [LawfulHashable α] [BEq β] [Hashable β] [LawfulHashable β] :
+    LawfulHashable (α × β) where
+  hash_eq a b h := by
+    simp [(· == ·)] at h
+    simp [hash, LawfulHashable.hash_eq _ _ h.1, LawfulHashable.hash_eq _ _ h.2]
+
 instance [BEq α] [PartialEquivBEq α] : PartialEquivBEq (List α) where
   symm := by
     simp [(· == ·)]; intro a b
@@ -257,27 +262,3 @@ instance : LawfulEqOrd UInt64 where
 
 end UInt64
 
-namespace Batteries.UnionFind
-
-@[simp] theorem size_empty : (∅ : UnionFind).size = 0 := rfl
-
-@[simp] theorem size_push (uf : UnionFind) : uf.push.size = uf.size + 1 := by
-  simp [push, size]
-
-@[simp] theorem size_link (uf : UnionFind) (i j hi) : (uf.link i j hi).size = uf.size := by
-  simp [link, size]
-
-@[simp] theorem size_union (uf : UnionFind) (i j) : (uf.union i j).size = uf.size := by
-  simp [union, size]
-
-theorem Equiv.eq_of_ge_size (h : Equiv uf a b) (h2 : uf.size ≤ a) : a = b := by
-  simp [Equiv, rootD, Nat.not_lt.2 h2] at h; split at h
-  · have := (uf.root ⟨b, ‹_›⟩).2; omega
-  · exact h
-
-theorem Equiv.lt_size (h : Equiv uf a b) : a < uf.size ↔ b < uf.size :=
-  suffices ∀ {a b}, Equiv uf a b → b < uf.size → a < uf.size from ⟨this h.symm, this h⟩
-  fun h h1 => Nat.not_le.1 fun h2 => Nat.not_le.2 h1 <| h.eq_of_ge_size h2 ▸ h2
-
-
-end Batteries.UnionFind

Lean4Lean/Tests.lean

@@ -1,5 +1,6 @@
 import Lean4Lean.Tests.Toolchain
 import Lean4Lean.Tests.Environment
+import Lean4Lean.Tests.UniformIndOccs
 import Lean4Lean.Tests.LevelStd
 import Lean4Lean.Tests.LiteralReadiness
 import Lean4Lean.Tests.NotationPreludeReplay