From 178d0d4e309ecaba6258d1bb043e2bc1d2dfdde6 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 28 Jul 2026 08:22:05 +0000 Subject: [PATCH 1/3] fix: centralise the module-system Array/Vector kernel-reduction workarounds This PR replaces the per-module `import all Init.Data.Array.DecidableEq` workaround with two shared shims in `HexBasic`, and records the full upstream picture so the eventual removal is mechanical. `HexBasic.ArrayDecEq` supplies higher-priority `DecidableEq` instances for `Array` and `Vector` that route through the fully exposed `List` equality, so `decide` and `rfl` over them reduce in the kernel under the module system. Twenty-six modules across `HexBerlekampZassenhaus`, `HexRealRoots`, `HexRCF`, and `HexBerlekampZassenhausMathlib` now import it instead of carrying their own copy of the workaround and its four-line explanation. `HexPoly.Dense` keeps its local instance, since `hex-poly` has no dependencies and cannot import `HexBasic`; its comment now says so. `HexBasic.OfFn` supplies `Array.ofFn'` and `Vector.ofFn'`, which go through `List.ofFn` and reduce, with `ofFn'_eq_ofFn` proving them equal to the core versions. The core `Array.ofFn` delegates to an unexposed `ofFn.go`, and `Vector.ofFn` inherits that, so neither reduces downstream. Chasing the `Vector` case turned up two further instances of the same defect beyond the known `Array.instDecidableEqImpl` one: every `deriving DecidableEq` instance is opaque across a module boundary, which is how `Vector` gets its instance and which has no consumer-side workaround, and `Array.ofFn` delegates to an unexposed auxiliary. All three are fixed upstream by https://github.com/leanprover/lean4/pull/14270. `progress/lean4-array-decidableeq-module-repro.md` now records all three with minimal repros and carries the cleanup checklist for when that lands. Progress file: progress/2026-07-28T10-40-00Z.md Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_0188fgvPvjbcXhvTYVSATLhv --- HexBasic.lean | 6 +- HexBasic/ArrayDecEq.lean | 59 ++++++++++++++ HexBasic/OfFn.lean | 49 ++++++++++++ HexBerlekampZassenhaus/BhksCandidates.lean | 8 +- HexBerlekampZassenhaus/BhksRecover.lean | 8 +- HexBerlekampZassenhaus/Certificate.lean | 8 +- HexBerlekampZassenhaus/ChoosePrimeData.lean | 8 +- HexBerlekampZassenhaus/FactorEntryPoints.lean | 8 +- HexBerlekampZassenhaus/IrreducibleCore.lean | 8 +- HexBerlekampZassenhaus/Lattice.lean | 8 +- HexBerlekampZassenhaus/PrimeSelection.lean | 8 +- HexBerlekampZassenhaus/PrimitivityProofs.lean | 8 +- HexBerlekampZassenhaus/ProductProofs.lean | 8 +- .../QuadraticRootProofs.lean | 8 +- HexBerlekampZassenhaus/ReassemblyProofs.lean | 8 +- HexBerlekampZassenhaus/Recombination.lean | 8 +- HexBerlekampZassenhaus/RecombineProofs.lean | 8 +- HexBerlekampZassenhaus/Records.lean | 8 +- HexBerlekampZassenhaus/TrialProofs.lean | 8 +- .../FactorPolyTests.lean | 4 +- HexPoly/Dense.lean | 8 +- HexRCF/SeparationTests.lean | 4 +- HexRealRoots/Chain.lean | 8 +- HexRealRoots/Isolate.lean | 9 +-- HexRealRoots/IsolateDescartes.lean | 10 +-- HexRealRoots/IsolateSturm.lean | 10 +-- HexRealRoots/Mobius.lean | 11 +-- HexRealRoots/Refine.lean | 10 +-- HexRealRoots/SimpleRealRoot.lean | 9 +-- HexRealRoots/Var.lean | 9 +-- progress/2026-07-28T10-40-00Z.md | 37 +++++++++ .../lean4-array-decidableeq-module-repro.md | 77 +++++++++++++++++-- scratch-mvpoly-bench/MV.lean | 66 ++++++++++++++++ scratch-mvpoly-bench/T_A_6.lean | 4 + scratch-mvpoly-bench/T_B_6.lean | 4 + scratch-mvpoly-bench/lake-manifest.json | 6 ++ scratch-mvpoly-bench/lakefile.toml | 4 + scratch-mvpoly-bench/lean-toolchain | 1 + scratch-mvpoly-bench/mk.sh | 7 ++ 39 files changed, 395 insertions(+), 145 deletions(-) create mode 100644 HexBasic/ArrayDecEq.lean create mode 100644 HexBasic/OfFn.lean create mode 100644 progress/2026-07-28T10-40-00Z.md create mode 100644 scratch-mvpoly-bench/MV.lean create mode 100644 scratch-mvpoly-bench/T_A_6.lean create mode 100644 scratch-mvpoly-bench/T_B_6.lean create mode 100644 scratch-mvpoly-bench/lake-manifest.json create mode 100644 scratch-mvpoly-bench/lakefile.toml create mode 100644 scratch-mvpoly-bench/lean-toolchain create mode 100755 scratch-mvpoly-bench/mk.sh diff --git a/HexBasic.lean b/HexBasic.lean index 0c3610691..1429cf716 100644 --- a/HexBasic.lean +++ b/HexBasic.lean @@ -6,7 +6,9 @@ Authors: Kim Morrison module +public import HexBasic.ArrayDecEq public import HexBasic.Fold +public import HexBasic.OfFn public import HexBasic.ListShim public import HexBasic.Vector.Modify @@ -17,5 +19,7 @@ public section general-purpose helpers that clearly belong in the standard library and are reproduced here only until they migrate up to lean4. It provides the shared `List.foldl` algebra (`HexBasic.Fold`), the `Batteries` list lemmas reproduced -in `HexBasic.ListShim`, and the `Vector.modify` update helper. +in `HexBasic.ListShim`, the `Vector.modify` update helper, and +kernel-reducible `Array`/`Vector` equality (`HexBasic.ArrayDecEq`) and +`ofFn` (`HexBasic.OfFn`). -/ diff --git a/HexBasic/ArrayDecEq.lean b/HexBasic/ArrayDecEq.lean new file mode 100644 index 000000000..719bc5d4d --- /dev/null +++ b/HexBasic/ArrayDecEq.lean @@ -0,0 +1,59 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +module + +public import Std + +public section + +/-! +Kernel-reducible `DecidableEq` for `Array` and `Vector`. + +Three exposure gaps in core stop `decide` / `rfl` reducing over these types +across a module boundary. In each case an exposed definition delegates to a +plain `def` whose body is unavailable downstream, so reduction stalls: + +* `Array.instDecidableEq` delegates its nonempty/nonempty case to + `Array.instDecidableEqImpl`; +* every `deriving DecidableEq` instance delegates to a generated `decEq`, + which is how `Vector` gets its instance; +* `Array.ofFn` delegates to its `ofFn.go` auxiliary. + +The instances below route through `List` equality, which is fully exposed, and +take priority over the core ones. + +**Delete this file** once +[leanprover/lean4#14270](https://github.com/leanprover/lean4/pull/14270) lands +and the toolchain is bumped past it. The `Array.ofFn` gap is fixed there too, +and has no workaround here: a definition built with `Array.ofFn` or +`Vector.ofFn` still will not reduce, so kernel-facing code must build its arrays +another way until then. +-/ + +namespace Hex + +/-- `DecidableEq (Array α)` that reduces in the kernel under the module system, +routing through the fully exposed `List` equality. -/ +instance (priority := 1100) instDecidableEqArray + {α : Type u} [DecidableEq α] : DecidableEq (Array α) := fun a b => + match h : decEq a.toList b.toList with + | isTrue ht => isTrue (by cases a; cases b; exact congrArg Array.mk ht) + | isFalse hf => isFalse (by intro hab; exact hf (congrArg Array.toList hab)) + +/-- `DecidableEq (Vector α n)` that reduces in the kernel under the module +system. `Vector`'s core instance is derived, and derived instances are opaque +across a module boundary. -/ +instance (priority := 1100) instDecidableEqVector + {α : Type u} {n : Nat} [DecidableEq α] : DecidableEq (Vector α n) := fun a b => + match h : decEq a.toArray.toList b.toArray.toList with + | isTrue ht => isTrue (by + cases a with | mk ba ha => cases b with | mk bb hb => + have hba : ba = bb := by cases ba; cases bb; exact congrArg Array.mk ht + subst hba; rfl) + | isFalse hf => isFalse (by intro hab; subst hab; exact hf rfl) + +end Hex diff --git a/HexBasic/OfFn.lean b/HexBasic/OfFn.lean new file mode 100644 index 000000000..c1b15c68c --- /dev/null +++ b/HexBasic/OfFn.lean @@ -0,0 +1,49 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +module + +public import Std + +public section + +/-! +Kernel-reducible `ofFn` for `Array` and `Vector`. + +`Array.ofFn` delegates to its `ofFn.go` auxiliary, which is not exposed, so +under the module system its body is unavailable downstream and +`(Array.ofFn f)` does not reduce in the kernel. `Vector.ofFn` is itself +`@[expose]` but calls `Array.ofFn`, so it inherits the stall. + +`List.ofFn` is fully exposed and reduces, so the definitions below go through +it. They are otherwise defeq to the core versions. + +**Delete this file** once +[leanprover/lean4#14270](https://github.com/leanprover/lean4/pull/14270) lands +and the toolchain is bumped past it, replacing uses with `Array.ofFn` and +`Vector.ofFn`. See `progress/lean4-array-decidableeq-module-repro.md` for the +full cleanup checklist. +-/ + +namespace Hex + +/-- `Array.ofFn` that reduces in the kernel under the module system. -/ +@[expose] def Array.ofFn' {α : Type u} {n : Nat} (f : Fin n → α) : Array α := + (List.ofFn f).toArray + +/-- `Vector.ofFn` that reduces in the kernel under the module system. -/ +@[expose] def Vector.ofFn' {α : Type u} {n : Nat} (f : Fin n → α) : Vector α n := + ⟨(List.ofFn f).toArray, by simp⟩ + +@[simp] theorem Array.ofFn'_eq_ofFn {α : Type u} {n : Nat} (f : Fin n → α) : + Array.ofFn' f = Array.ofFn f := by + simp [Array.ofFn'] + +@[simp] theorem Vector.ofFn'_eq_ofFn {α : Type u} {n : Nat} (f : Fin n → α) : + Vector.ofFn' f = Vector.ofFn f := by + simp [Vector.ofFn', _root_.Vector.ofFn] + +end Hex diff --git a/HexBerlekampZassenhaus/BhksCandidates.lean b/HexBerlekampZassenhaus/BhksCandidates.lean index a09d1b225..09991c292 100644 --- a/HexBerlekampZassenhaus/BhksCandidates.lean +++ b/HexBerlekampZassenhaus/BhksCandidates.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.Lattice public meta import HexBerlekampZassenhaus.Lattice diff --git a/HexBerlekampZassenhaus/BhksRecover.lean b/HexBerlekampZassenhaus/BhksRecover.lean index 8ef6b0c11..4c10b9ed7 100644 --- a/HexBerlekampZassenhaus/BhksRecover.lean +++ b/HexBerlekampZassenhaus/BhksRecover.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.BhksCandidates public meta import HexBerlekampZassenhaus.BhksCandidates diff --git a/HexBerlekampZassenhaus/Certificate.lean b/HexBerlekampZassenhaus/Certificate.lean index 82350161f..07ac29a96 100644 --- a/HexBerlekampZassenhaus/Certificate.lean +++ b/HexBerlekampZassenhaus/Certificate.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.Records public meta import HexBerlekampZassenhaus.Records diff --git a/HexBerlekampZassenhaus/ChoosePrimeData.lean b/HexBerlekampZassenhaus/ChoosePrimeData.lean index 9de9de765..fd7d47fc9 100644 --- a/HexBerlekampZassenhaus/ChoosePrimeData.lean +++ b/HexBerlekampZassenhaus/ChoosePrimeData.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.Certificate public meta import HexBerlekampZassenhaus.Certificate diff --git a/HexBerlekampZassenhaus/FactorEntryPoints.lean b/HexBerlekampZassenhaus/FactorEntryPoints.lean index b58664ea7..4857e810f 100644 --- a/HexBerlekampZassenhaus/FactorEntryPoints.lean +++ b/HexBerlekampZassenhaus/FactorEntryPoints.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.Recombination public meta import HexBerlekampZassenhaus.Recombination diff --git a/HexBerlekampZassenhaus/IrreducibleCore.lean b/HexBerlekampZassenhaus/IrreducibleCore.lean index 1ddb85fea..72e29819d 100644 --- a/HexBerlekampZassenhaus/IrreducibleCore.lean +++ b/HexBerlekampZassenhaus/IrreducibleCore.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.FactorEntryPoints public meta import HexBerlekampZassenhaus.FactorEntryPoints diff --git a/HexBerlekampZassenhaus/Lattice.lean b/HexBerlekampZassenhaus/Lattice.lean index 13082bfbe..718c9a220 100644 --- a/HexBerlekampZassenhaus/Lattice.lean +++ b/HexBerlekampZassenhaus/Lattice.lean @@ -22,11 +22,9 @@ public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic public import HexBerlekampZassenhaus.WordCld --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.ReassemblyProofs public meta import HexBerlekampZassenhaus.ReassemblyProofs diff --git a/HexBerlekampZassenhaus/PrimeSelection.lean b/HexBerlekampZassenhaus/PrimeSelection.lean index 08da61b1f..ae73d9b59 100644 --- a/HexBerlekampZassenhaus/PrimeSelection.lean +++ b/HexBerlekampZassenhaus/PrimeSelection.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public section diff --git a/HexBerlekampZassenhaus/PrimitivityProofs.lean b/HexBerlekampZassenhaus/PrimitivityProofs.lean index 9c2f7a031..39783d1d6 100644 --- a/HexBerlekampZassenhaus/PrimitivityProofs.lean +++ b/HexBerlekampZassenhaus/PrimitivityProofs.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.QuadraticRootProofs public meta import HexBerlekampZassenhaus.QuadraticRootProofs diff --git a/HexBerlekampZassenhaus/ProductProofs.lean b/HexBerlekampZassenhaus/ProductProofs.lean index d8068389d..ebe62a9aa 100644 --- a/HexBerlekampZassenhaus/ProductProofs.lean +++ b/HexBerlekampZassenhaus/ProductProofs.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.PrimitivityProofs public meta import HexBerlekampZassenhaus.PrimitivityProofs diff --git a/HexBerlekampZassenhaus/QuadraticRootProofs.lean b/HexBerlekampZassenhaus/QuadraticRootProofs.lean index b4d53061b..e29099d17 100644 --- a/HexBerlekampZassenhaus/QuadraticRootProofs.lean +++ b/HexBerlekampZassenhaus/QuadraticRootProofs.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.TrialProofs public meta import HexBerlekampZassenhaus.TrialProofs diff --git a/HexBerlekampZassenhaus/ReassemblyProofs.lean b/HexBerlekampZassenhaus/ReassemblyProofs.lean index ecaca8143..3dea70591 100644 --- a/HexBerlekampZassenhaus/ReassemblyProofs.lean +++ b/HexBerlekampZassenhaus/ReassemblyProofs.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.ChoosePrimeData public meta import HexBerlekampZassenhaus.ChoosePrimeData diff --git a/HexBerlekampZassenhaus/Recombination.lean b/HexBerlekampZassenhaus/Recombination.lean index 32c94f66b..7397d9f3e 100644 --- a/HexBerlekampZassenhaus/Recombination.lean +++ b/HexBerlekampZassenhaus/Recombination.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.BhksRecover public meta import HexBerlekampZassenhaus.BhksRecover diff --git a/HexBerlekampZassenhaus/RecombineProofs.lean b/HexBerlekampZassenhaus/RecombineProofs.lean index edbc87b99..65922e17c 100644 --- a/HexBerlekampZassenhaus/RecombineProofs.lean +++ b/HexBerlekampZassenhaus/RecombineProofs.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.IrreducibleCore public meta import HexBerlekampZassenhaus.IrreducibleCore diff --git a/HexBerlekampZassenhaus/Records.lean b/HexBerlekampZassenhaus/Records.lean index 05ca6eebc..74fa2fd1d 100644 --- a/HexBerlekampZassenhaus/Records.lean +++ b/HexBerlekampZassenhaus/Records.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.PrimeSelection public import HexBerlekampZassenhaus.SquareFreeModularCert diff --git a/HexBerlekampZassenhaus/TrialProofs.lean b/HexBerlekampZassenhaus/TrialProofs.lean index 19357b8d5..390c1129b 100644 --- a/HexBerlekampZassenhaus/TrialProofs.lean +++ b/HexBerlekampZassenhaus/TrialProofs.lean @@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility public import HexHensel.Multifactor public import HexHensel.QuadraticMultifactor public import HexLLL.Basic --- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the --- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public import HexBerlekampZassenhaus.RecombineProofs public meta import HexBerlekampZassenhaus.RecombineProofs diff --git a/HexBerlekampZassenhausMathlib/FactorPolyTests.lean b/HexBerlekampZassenhausMathlib/FactorPolyTests.lean index 09e8e7d63..6e5ec5511 100644 --- a/HexBerlekampZassenhausMathlib/FactorPolyTests.lean +++ b/HexBerlekampZassenhausMathlib/FactorPolyTests.lean @@ -141,7 +141,9 @@ import all HexBasic.Fold import all HexBasic.ListShim import all HexBasic.Vector.Modify import all Init.Data.Array.Basic -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq import all Init.Data.Fin.Fold import all Init.Data.Fin.Basic import all Init.Data.Fin.Iterate diff --git a/HexPoly/Dense.lean b/HexPoly/Dense.lean index ce512967b..4e1d89781 100644 --- a/HexPoly/Dense.lean +++ b/HexPoly/Dense.lean @@ -41,8 +41,12 @@ variable {R : Type u} [Zero R] [DecidableEq R] `Array.instDecidableEq` delegates its nonempty case to the non-`@[expose]` `Array.instDecidableEqImpl`, whose body is unavailable downstream under the module system, so `decide`/`rfl` on `DensePoly` equalities would get stuck -(see `progress/lean4-array-decidableeq-module-repro.md`). `List` equality is -fully exposed and kernel-reduces. -/ +(see `progress/lean4-array-decidableeq-module-repro.md`, fixed upstream by +leanprover/lean4#14270). `List` equality is fully exposed and kernel-reduces. + +`HexBasic.ArrayDecEq` carries the same workaround as a reusable instance, but +`hex-poly` has no dependencies and so cannot import it; this instance stays +local until either that dependency is added or the upstream fix lands. -/ instance : DecidableEq (DensePoly R) := fun a b => match decEq a.coeffs.toList b.coeffs.toList with | isTrue h => diff --git a/HexRCF/SeparationTests.lean b/HexRCF/SeparationTests.lean index 99fb85920..a416edb70 100644 --- a/HexRCF/SeparationTests.lean +++ b/HexRCF/SeparationTests.lean @@ -20,7 +20,9 @@ public meta import HexPolyZ.Mignotte import all HexRCF.Separation import all HexRCF.SeparationCheck import all HexRCF.SturmBuilder -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq import all HexRealRoots.Basic import all HexRealRoots.Chain import all HexRealRoots.Var diff --git a/HexRealRoots/Chain.lean b/HexRealRoots/Chain.lean index 835b320cb..6197b247c 100644 --- a/HexRealRoots/Chain.lean +++ b/HexRealRoots/Chain.lean @@ -7,11 +7,9 @@ Authors: Kim Morrison module public import HexRealRoots.Basic --- Needed so `decide` over `DensePoly`/`Array` equality reduces in the kernel: --- the core `Array.instDecidableEq` delegates its nonempty case to the --- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under --- the module system. Drop once that impl is exposed upstream (lean4). -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq public section diff --git a/HexRealRoots/Isolate.lean b/HexRealRoots/Isolate.lean index a38be8a9c..32ac32dfe 100644 --- a/HexRealRoots/Isolate.lean +++ b/HexRealRoots/Isolate.lean @@ -8,12 +8,9 @@ module public import HexRealRoots.IsolateSturm public import HexRealRoots.IsolateDescartes --- `import all` on the engine modules so `decide` reduces the sanity checks --- below in the kernel: the non-`@[expose]` engine bodies (`isolateSturm?`, --- `isolateDescartes?`, the chain/evaluation helpers they call) are opaque --- across the module boundary otherwise, so a `decide` unfolding them would --- get stuck. Same workaround as Var.lean and Refine.lean. -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq import all HexRealRoots.Basic import all HexRealRoots.Chain import all HexRealRoots.Var diff --git a/HexRealRoots/IsolateDescartes.lean b/HexRealRoots/IsolateDescartes.lean index 8de0b9186..74d664b51 100644 --- a/HexRealRoots/IsolateDescartes.lean +++ b/HexRealRoots/IsolateDescartes.lean @@ -9,13 +9,9 @@ module public import HexRealRoots.Prec public import HexRealRoots.Var public import HexRealRoots.Mobius --- `import all` on the source modules so `decide` reduces the zero and --- constant sanity checks below in the kernel: plain (non-`@[expose]`) defs --- like `sturmChain`, `evalDyadic`, `dyadicSign`, and `sturmVarAt` have opaque --- bodies across the module boundary, so a `decide` that unfolds the driver --- would get stuck without these. The Array-equality `import all` is the same --- workaround as `IsolateSturm.lean`. -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq import all HexRealRoots.Basic import all HexRealRoots.Chain import all HexRealRoots.Var diff --git a/HexRealRoots/IsolateSturm.lean b/HexRealRoots/IsolateSturm.lean index bba570305..44d7f2f1b 100644 --- a/HexRealRoots/IsolateSturm.lean +++ b/HexRealRoots/IsolateSturm.lean @@ -8,13 +8,9 @@ module public import HexRealRoots.Prec public import HexRealRoots.Var --- `import all` on the source modules so `decide` reduces the sanity checks --- below in the kernel: plain (non-`@[expose]`) defs like `sturmChain`, --- `evalDyadic`, `dyadicSign`, and `sturmVarAt` have opaque bodies across the --- module boundary, so a `decide` that unfolds the engine would get stuck --- without these. The Array-equality `import all` is the same workaround as --- Var.lean. -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq import all HexRealRoots.Basic import all HexRealRoots.Chain import all HexRealRoots.Var diff --git a/HexRealRoots/Mobius.lean b/HexRealRoots/Mobius.lean index 4b31d1181..9721bc120 100644 --- a/HexRealRoots/Mobius.lean +++ b/HexRealRoots/Mobius.lean @@ -7,14 +7,9 @@ Authors: Kim Morrison module public import HexRealRoots.Var --- `import all` so `decide` reduces the sanity checks below in the kernel. --- `signVar` (in `Var.lean`) is a plain, non-`@[expose]` def, so its body is --- opaque across the module boundary; `import all` exposes it. The Möbius --- pipeline itself only calls `@[expose]` `DensePoly`/`ZPoly` operations, whose --- bodies are already visible. The `Array`-equality `import all` is the same --- kernel-`decide` workaround as `Chain.lean`/`Var.lean`, needed because the --- array-literal assertions compare `ZPoly` (hence `Array Int`) values. -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq import all HexRealRoots.Var public section diff --git a/HexRealRoots/Refine.lean b/HexRealRoots/Refine.lean index f08ffd0af..d8954fa3e 100644 --- a/HexRealRoots/Refine.lean +++ b/HexRealRoots/Refine.lean @@ -8,13 +8,9 @@ module public import HexRealRoots.Var public import HexRealRoots.Prec --- `import all` on the source modules so `decide` reduces the sanity checks --- below in the kernel: plain (non-`@[expose]`) defs like `sturmChain`, --- `evalDyadic`, `dyadicSign`, `sturmVarAt`, and `twoPow` have opaque bodies --- across the module boundary, so a `decide` that unfolds them here would get --- stuck without these. The Array-equality `import all` is the same workaround --- as Chain.lean and Var.lean. -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq import all HexRealRoots.Basic import all HexRealRoots.Chain import all HexRealRoots.Var diff --git a/HexRealRoots/SimpleRealRoot.lean b/HexRealRoots/SimpleRealRoot.lean index 2d99389a9..7290f35a0 100644 --- a/HexRealRoots/SimpleRealRoot.lean +++ b/HexRealRoots/SimpleRealRoot.lean @@ -8,12 +8,9 @@ module public import HexRealRoots.Refine public import HexRealRoots.Prec --- `import all` on the source modules so `decide` reduces the sanity checks --- below in the kernel: the non-`@[expose]` bodies (`sturmChain`, `evalDyadic`, --- `sturmVarAt`, `sepPrec`, `twoPow`, and the dyadic comparison behind --- `Overlaps`) are opaque across the module boundary otherwise. Same workaround --- as Var.lean and Refine.lean. -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq import all HexRealRoots.Basic import all HexRealRoots.Chain import all HexRealRoots.Var diff --git a/HexRealRoots/Var.lean b/HexRealRoots/Var.lean index c3820c20d..27e51c48a 100644 --- a/HexRealRoots/Var.lean +++ b/HexRealRoots/Var.lean @@ -7,12 +7,9 @@ Authors: Kim Morrison module public import HexRealRoots.Chain --- `import all` on the two source modules so `decide` reduces the sanity --- checks below in the kernel: plain (non-`@[expose]`) defs like `sturmChain`, --- `evalDyadic`, and `dyadicSign` have opaque bodies across the module --- boundary, so a `decide` that unfolds them here would get stuck without --- these. The Array-equality `import all` is the same workaround as Chain.lean. -import all Init.Data.Array.DecidableEq +-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`. +-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. +public import HexBasic.ArrayDecEq import all HexRealRoots.Basic import all HexRealRoots.Chain diff --git a/progress/2026-07-28T10-40-00Z.md b/progress/2026-07-28T10-40-00Z.md new file mode 100644 index 000000000..7f2a75e63 --- /dev/null +++ b/progress/2026-07-28T10-40-00Z.md @@ -0,0 +1,37 @@ +# Centralise the `Array`/`Vector` kernel-equality workaround + +## Accomplished + +- Added `HexBasic/ArrayDecEq.lean`: higher-priority `DecidableEq` instances for + `Array` and `Vector` that route through the fully exposed `List` equality, so + `decide` / `rfl` over them reduces in the kernel under the module system. +- Replaced the per-module `import all Init.Data.Array.DecidableEq` workaround + with `public import HexBasic.ArrayDecEq` in 26 modules across + `HexBerlekampZassenhaus`, `HexRealRoots`, `HexRCF`, and + `HexBerlekampZassenhausMathlib`. +- `HexPoly.Dense` keeps its local hand-written instance: `hex-poly` has no + dependencies, so it cannot import `HexBasic`. Its comment now says so. +- Extended `progress/lean4-array-decidableeq-module-repro.md` to record two + further instances of the same defect found while chasing `Vector`: every + `deriving DecidableEq` instance is opaque across a module boundary, and + `Array.ofFn` does not reduce. Added the cleanup checklist for when the + upstream fix lands. +- Upstream: reopened and extended + [leanprover/lean4#14270](https://github.com/leanprover/lean4/pull/14270), + rebased onto `nightly-with-mathlib`, now covering all three exposure gaps. + +## Current frontier + +- `HexBasic.ArrayDecEq` is a shim with a scheduled death. The cleanup steps are + written down in the repro note. +- The `Array.ofFn` gap has no consumer-side workaround, so kernel-facing code + still cannot build arrays that way. + +## Next step + +- When the toolchain moves past #14270, run the cleanup checklist in + `progress/lean4-array-decidableeq-module-repro.md`. + +## Blockers + +- None. diff --git a/progress/lean4-array-decidableeq-module-repro.md b/progress/lean4-array-decidableeq-module-repro.md index a84cee6d2..e28217084 100644 --- a/progress/lean4-array-decidableeq-module-repro.md +++ b/progress/lean4-array-decidableeq-module-repro.md @@ -49,19 +49,80 @@ system a public non-`@[expose]` `def` exports only its signature, so `instDecida body is unavailable to the kernel downstream — `#print Array.instDecidableEqImpl` reports `` — and reduction stalls for every pair of nonempty arrays. -## Proposed fix +## Two further instances of the same defect -Add `@[expose]` to `Array.instDecidableEqImpl` (and verify its reduction closure, -`Array.isEqv` / `Array.isEqvAux`, is likewise exposed). That restores kernel reduction of -`decide`/`rfl` over `Array` equality under `module`. +Chasing the `Vector` case turned up two more, both with the same shape and neither +fixable from the consumer side. + +**Every `deriving DecidableEq` instance.** `Lean.Elab.Deriving.DecEq.mkAuxFunction` +emits the generated `decEq` as a plain `def`, so its body is opaque across a module +boundary. This is not specific to any type: + +```lean +-- A.lean +module +public section +structure P where + x : Nat +deriving DecidableEq + +-- B.lean +module +public import A +example : (⟨1⟩ : P) ≠ ⟨2⟩ := by decide -- stuck at instDecidableEqP.decEq +``` + +`Vector`'s instance is derived, which is why `Vector` equality stalls even once +`Array` is fixed. There is no workaround: `@[expose]` cannot be attached to a +structure, and `attribute [expose] …` after the fact is rejected ("can only be +added when declaring a `def`"). + +**`Array.ofFn`.** Delegates to its `ofFn.go` auxiliary, so +`(Array.ofFn f).size = n` does not reduce. `Vector.ofFn` is already `@[expose]` +but calls `Array.ofFn`, so it inherits the stall. Marking `Array.ofFn` itself +`@[expose]` is sufficient, because exposure extends to a definition's `where` +bindings; `@[expose]` directly on the `where` binding is rejected. + +## Fix + +All three are fixed by +[leanprover/lean4#14270](https://github.com/leanprover/lean4/pull/14270): +`@[expose]` on `Array.instDecidableEqImpl` (plus `isEqv` / `isEqvAux`), on the +`decEq` emitted by the deriving handler, and on `Array.ofFn`. ## Consumer-side workarounds (no toolchain change) -- `import all Init.Data.Array.DecidableEq` in the module performing the `decide` — pulls the - impl body in and reduces (verified). +- `HexBasic.ArrayDecEq` provides higher-priority `DecidableEq` instances for + `Array` and `Vector` that route through the fully exposed `List` equality. + This is what the tree uses now; `public import HexBasic.ArrayDecEq` in any + module that needs to `decide` such an equality. +- `import all Init.Data.Array.DecidableEq` also works for the `Array` case, and + was what the tree used previously. - Route a wrapper type's `DecidableEq` through `List` instead of `Array`, e.g. - `decidable_of_iff (a.toList = b.toList) …`; `List.instDecidableEq` is fully exposed. - (This is what `HexPoly.Dense`'s `DecidableEq (DensePoly R)` now does.) + `decidable_of_iff (a.toList = b.toList) …`. This is what `HexPoly.Dense`'s + `DecidableEq (DensePoly R)` does, and it has to stay local there because + `hex-poly` has no dependencies and therefore cannot import `HexBasic`. +- `HexBasic.OfFn` provides `Hex.Array.ofFn'` and `Hex.Vector.ofFn'`, which go + through the fully exposed `List.ofFn` and do reduce. They are proved equal to + the core versions (`ofFn'_eq_ofFn`), so the swap back is a rewrite. + +## Cleanup once #14270 lands + +After the toolchain is bumped past the fix: + +1. Delete `HexBasic/ArrayDecEq.lean` and `HexBasic/OfFn.lean`, and their entries + in `HexBasic.lean`. +2. Remove the `public import HexBasic.ArrayDecEq` line and its two-line comment + from every module that carries it (`grep -rl HexBasic.ArrayDecEq`), and + replace every `Array.ofFn'` / `Vector.ofFn'` use with the core version + (`grep -rl "ofFn'"`); `ofFn'_eq_ofFn` makes that a rewrite. +3. Replace `HexPoly.Dense`'s hand-written `DecidableEq (DensePoly R)` with the + ordinary `Array`-based comparison, and drop the explanatory comment. +4. Reconsider `HexPoly.Euclid.leadingCoeff`, which avoids `Array.back?` for the + related reason below, and any code that avoids `Array.ofFn` for kernel + reasons. +5. Re-run the kernel-facing conformance and bench targets, since the point of + all of this is reduction behaviour rather than elaboration. ## Related diff --git a/scratch-mvpoly-bench/MV.lean b/scratch-mvpoly-bench/MV.lean new file mode 100644 index 000000000..2fc174c9a --- /dev/null +++ b/scratch-mvpoly-bench/MV.lean @@ -0,0 +1,66 @@ +import Std +open Std + +abbrev Mono := Array Nat + +def monoCmp (a b : Mono) : Ordering := compare a b + +def monoCmpOld (a b : Mono) : Ordering := Id.run do + for i in [0:a.size] do + let x := a[i]!; let y := b[i]! + if x < y then return .lt + if y < x then return .gt + return .eq + +def monoAdd (a b : Mono) : Mono := a.zipWith (· + ·) b + +/-! ## Rep A: ExtTreeMap-backed -/ +abbrev PA := ExtTreeMap Mono Int compare + +def PA.addTerm (p : PA) (m : Mono) (c : Int) : PA := + p.alter m fun + | none => if c == 0 then none else some c + | some d => if d + c == 0 then none else some (d + c) + +def PA.add (p q : PA) : PA := q.foldl (fun acc m c => acc.addTerm m c) p +def PA.mul (p q : PA) : PA := + p.foldl (fun acc m c => q.foldl (fun acc m' c' => acc.addTerm (monoAdd m m') (c * c')) acc) ∅ + +/-! ## Rep B: sorted-list backed (Karatarakis / WuProver shape) -/ +abbrev PB := List (Mono × Int) + +def PB.addTerm : PB → Mono → Int → PB + | [], m, c => if c == 0 then [] else [(m, c)] + | (m', c') :: t, m, c => + match compare m m' with + | .lt => (m', c') :: PB.addTerm t m c + | .gt => if c == 0 then (m', c') :: t else (m, c) :: (m', c') :: t + | .eq => if c' + c == 0 then t else (m', c' + c) :: t + +def PB.add (p q : PB) : PB := q.foldl (fun acc (m, c) => PB.addTerm acc m c) p +def PB.mul (p q : PB) : PB := + p.foldl (fun acc (m, c) => q.foldl (fun acc (m', c') => PB.addTerm acc (monoAdd m m') (c * c')) acc) [] + +/-! ## Workload: (1 + x0 + ... + x_{n-1})^k, two ways -/ +def genA (n : Nat) : PA := + (List.range n).foldl (fun p i => p.addTerm (Array.ofFn (fun j : Fin n => if j.val = i then 1 else 0)) 1) + (PA.addTerm ∅ (Array.replicate n 0) 1) +def genB (n : Nat) : PB := + (List.range n).foldl (fun p i => PB.addTerm p (Array.ofFn (fun j : Fin n => if j.val = i then 1 else 0)) 1) + (PB.addTerm [] (Array.replicate n 0) 1) + +def powA (p : PA) : Nat → PA + | 0 => PA.addTerm ∅ (Array.replicate 3 0) 1 + | k+1 => PA.mul p (powA p k) +def powB (p : PB) : Nat → PB + | 0 => PB.addTerm [] (Array.replicate 3 0) 1 + | k+1 => PB.mul p (powB p k) + +def sizeA (n k : Nat) : Nat := (powA (genA n) k).toList.length +def sizeB (n k : Nat) : Nat := (powB (genB n) k).length + +#eval (sizeA 3 5, sizeB 3 5) +#eval (sizeA 3 8, sizeB 3 8) + +def PA.toListX (p : PA) : List (Mono × Int) := p.toList +def PB.toListX (p : PB) : List (Mono × Int) := p diff --git a/scratch-mvpoly-bench/T_A_6.lean b/scratch-mvpoly-bench/T_A_6.lean new file mode 100644 index 000000000..713c8bde4 --- /dev/null +++ b/scratch-mvpoly-bench/T_A_6.lean @@ -0,0 +1,4 @@ +import MV +set_option maxRecDepth 100000 in +example : ((powA (genA 3) 6).toListX == (PA.mul (powA (genA 3) 3) (powA (genA 3) 3)).toListX) = true := by + decide +kernel diff --git a/scratch-mvpoly-bench/T_B_6.lean b/scratch-mvpoly-bench/T_B_6.lean new file mode 100644 index 000000000..7171ca95c --- /dev/null +++ b/scratch-mvpoly-bench/T_B_6.lean @@ -0,0 +1,4 @@ +import MV +set_option maxRecDepth 100000 in +example : ((powB (genB 3) 6).toListX == (PB.mul (powB (genB 3) 3) (powB (genB 3) 3)).toListX) = true := by + decide +kernel diff --git a/scratch-mvpoly-bench/lake-manifest.json b/scratch-mvpoly-bench/lake-manifest.json new file mode 100644 index 000000000..5df5305ca --- /dev/null +++ b/scratch-mvpoly-bench/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "mvbench", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/scratch-mvpoly-bench/lakefile.toml b/scratch-mvpoly-bench/lakefile.toml new file mode 100644 index 000000000..80c0c548a --- /dev/null +++ b/scratch-mvpoly-bench/lakefile.toml @@ -0,0 +1,4 @@ +name = "mvbench" +defaultTargets = ["MV"] +[[lean_lib]] +name = "MV" diff --git a/scratch-mvpoly-bench/lean-toolchain b/scratch-mvpoly-bench/lean-toolchain new file mode 100644 index 000000000..2694eb767 --- /dev/null +++ b/scratch-mvpoly-bench/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.32.0-rc1 diff --git a/scratch-mvpoly-bench/mk.sh b/scratch-mvpoly-bench/mk.sh new file mode 100755 index 000000000..51643ad3c --- /dev/null +++ b/scratch-mvpoly-bench/mk.sh @@ -0,0 +1,7 @@ +rep=$1; k=$2 +cat > T_${rep}_${k}.lean < Date: Tue, 28 Jul 2026 08:24:46 +0000 Subject: [PATCH 2/3] fix: compile `ofFn'` to the core implementation via `@[csimp]` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `(List.ofFn f).toArray` is the shape the kernel can reduce, and the wrong shape for compiled code, which wants to fill an array of known capacity rather than build a linked list and convert. A `@[csimp]` redirect back to `Array.ofFn` / `Vector.ofFn` means the `List` route is paid only in the kernel. `@[csimp]` requires a literal `@f = @g`, so `Vector.ofFn'` takes its implicits in core's order (`{n} {α}`, which is the opposite of `Array.ofFn`'s `{α} {n}`). Also drops `scratch-mvpoly-bench/` from the branch, which `git add -A` had swept in, and ignores `scratch-*/` so it cannot recur. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_0188fgvPvjbcXhvTYVSATLhv --- .gitignore | 3 ++ HexBasic/OfFn.lean | 19 +++++-- scratch-mvpoly-bench/MV.lean | 66 ------------------------- scratch-mvpoly-bench/T_A_6.lean | 4 -- scratch-mvpoly-bench/T_B_6.lean | 4 -- scratch-mvpoly-bench/lake-manifest.json | 6 --- scratch-mvpoly-bench/lakefile.toml | 4 -- scratch-mvpoly-bench/lean-toolchain | 1 - scratch-mvpoly-bench/mk.sh | 7 --- 9 files changed, 19 insertions(+), 95 deletions(-) delete mode 100644 scratch-mvpoly-bench/MV.lean delete mode 100644 scratch-mvpoly-bench/T_A_6.lean delete mode 100644 scratch-mvpoly-bench/T_B_6.lean delete mode 100644 scratch-mvpoly-bench/lake-manifest.json delete mode 100644 scratch-mvpoly-bench/lakefile.toml delete mode 100644 scratch-mvpoly-bench/lean-toolchain delete mode 100755 scratch-mvpoly-bench/mk.sh diff --git a/.gitignore b/.gitignore index 49adac409..e39aa08df 100644 --- a/.gitignore +++ b/.gitignore @@ -10,3 +10,6 @@ conformance-failures/*.json .pod/ sessions/ _out/ + +# Scratch experiments kept out of the tree. +scratch-*/ diff --git a/HexBasic/OfFn.lean b/HexBasic/OfFn.lean index c1b15c68c..4bd05be64 100644 --- a/HexBasic/OfFn.lean +++ b/HexBasic/OfFn.lean @@ -19,7 +19,10 @@ under the module system its body is unavailable downstream and `@[expose]` but calls `Array.ofFn`, so it inherits the stall. `List.ofFn` is fully exposed and reduces, so the definitions below go through -it. They are otherwise defeq to the core versions. +it. That is the wrong shape for compiled code, which wants to push into an +array of known capacity rather than build a linked list and convert, so each +carries a `@[csimp]` lemma redirecting the compiler back to the core version. +The `List` route is then paid only in the kernel, which is where it is needed. **Delete this file** once [leanprover/lean4#14270](https://github.com/leanprover/lean4/pull/14270) lands @@ -35,15 +38,25 @@ namespace Hex (List.ofFn f).toArray /-- `Vector.ofFn` that reduces in the kernel under the module system. -/ -@[expose] def Vector.ofFn' {α : Type u} {n : Nat} (f : Fin n → α) : Vector α n := +@[expose] def Vector.ofFn' {n : Nat} {α : Type u} (f : Fin n → α) : Vector α n := ⟨(List.ofFn f).toArray, by simp⟩ @[simp] theorem Array.ofFn'_eq_ofFn {α : Type u} {n : Nat} (f : Fin n → α) : Array.ofFn' f = Array.ofFn f := by simp [Array.ofFn'] -@[simp] theorem Vector.ofFn'_eq_ofFn {α : Type u} {n : Nat} (f : Fin n → α) : +@[simp] theorem Vector.ofFn'_eq_ofFn {n : Nat} {α : Type u} (f : Fin n → α) : Vector.ofFn' f = Vector.ofFn f := by simp [Vector.ofFn', _root_.Vector.ofFn] +/-- Compiled code uses the core `Array.ofFn`, which fills an array of known +capacity instead of building a `List` first. The `List` route exists only so +that the kernel can reduce it. -/ +@[csimp] theorem Array.ofFn'_eq_ofFn' : @Array.ofFn' = @_root_.Array.ofFn := by + funext α n f; exact Array.ofFn'_eq_ofFn f + +/-- As `Array.ofFn'_eq_ofFn'`. -/ +@[csimp] theorem Vector.ofFn'_eq_ofFn' : @Vector.ofFn' = @_root_.Vector.ofFn := by + funext n α f; exact Vector.ofFn'_eq_ofFn f + end Hex diff --git a/scratch-mvpoly-bench/MV.lean b/scratch-mvpoly-bench/MV.lean deleted file mode 100644 index 2fc174c9a..000000000 --- a/scratch-mvpoly-bench/MV.lean +++ /dev/null @@ -1,66 +0,0 @@ -import Std -open Std - -abbrev Mono := Array Nat - -def monoCmp (a b : Mono) : Ordering := compare a b - -def monoCmpOld (a b : Mono) : Ordering := Id.run do - for i in [0:a.size] do - let x := a[i]!; let y := b[i]! - if x < y then return .lt - if y < x then return .gt - return .eq - -def monoAdd (a b : Mono) : Mono := a.zipWith (· + ·) b - -/-! ## Rep A: ExtTreeMap-backed -/ -abbrev PA := ExtTreeMap Mono Int compare - -def PA.addTerm (p : PA) (m : Mono) (c : Int) : PA := - p.alter m fun - | none => if c == 0 then none else some c - | some d => if d + c == 0 then none else some (d + c) - -def PA.add (p q : PA) : PA := q.foldl (fun acc m c => acc.addTerm m c) p -def PA.mul (p q : PA) : PA := - p.foldl (fun acc m c => q.foldl (fun acc m' c' => acc.addTerm (monoAdd m m') (c * c')) acc) ∅ - -/-! ## Rep B: sorted-list backed (Karatarakis / WuProver shape) -/ -abbrev PB := List (Mono × Int) - -def PB.addTerm : PB → Mono → Int → PB - | [], m, c => if c == 0 then [] else [(m, c)] - | (m', c') :: t, m, c => - match compare m m' with - | .lt => (m', c') :: PB.addTerm t m c - | .gt => if c == 0 then (m', c') :: t else (m, c) :: (m', c') :: t - | .eq => if c' + c == 0 then t else (m', c' + c) :: t - -def PB.add (p q : PB) : PB := q.foldl (fun acc (m, c) => PB.addTerm acc m c) p -def PB.mul (p q : PB) : PB := - p.foldl (fun acc (m, c) => q.foldl (fun acc (m', c') => PB.addTerm acc (monoAdd m m') (c * c')) acc) [] - -/-! ## Workload: (1 + x0 + ... + x_{n-1})^k, two ways -/ -def genA (n : Nat) : PA := - (List.range n).foldl (fun p i => p.addTerm (Array.ofFn (fun j : Fin n => if j.val = i then 1 else 0)) 1) - (PA.addTerm ∅ (Array.replicate n 0) 1) -def genB (n : Nat) : PB := - (List.range n).foldl (fun p i => PB.addTerm p (Array.ofFn (fun j : Fin n => if j.val = i then 1 else 0)) 1) - (PB.addTerm [] (Array.replicate n 0) 1) - -def powA (p : PA) : Nat → PA - | 0 => PA.addTerm ∅ (Array.replicate 3 0) 1 - | k+1 => PA.mul p (powA p k) -def powB (p : PB) : Nat → PB - | 0 => PB.addTerm [] (Array.replicate 3 0) 1 - | k+1 => PB.mul p (powB p k) - -def sizeA (n k : Nat) : Nat := (powA (genA n) k).toList.length -def sizeB (n k : Nat) : Nat := (powB (genB n) k).length - -#eval (sizeA 3 5, sizeB 3 5) -#eval (sizeA 3 8, sizeB 3 8) - -def PA.toListX (p : PA) : List (Mono × Int) := p.toList -def PB.toListX (p : PB) : List (Mono × Int) := p diff --git a/scratch-mvpoly-bench/T_A_6.lean b/scratch-mvpoly-bench/T_A_6.lean deleted file mode 100644 index 713c8bde4..000000000 --- a/scratch-mvpoly-bench/T_A_6.lean +++ /dev/null @@ -1,4 +0,0 @@ -import MV -set_option maxRecDepth 100000 in -example : ((powA (genA 3) 6).toListX == (PA.mul (powA (genA 3) 3) (powA (genA 3) 3)).toListX) = true := by - decide +kernel diff --git a/scratch-mvpoly-bench/T_B_6.lean b/scratch-mvpoly-bench/T_B_6.lean deleted file mode 100644 index 7171ca95c..000000000 --- a/scratch-mvpoly-bench/T_B_6.lean +++ /dev/null @@ -1,4 +0,0 @@ -import MV -set_option maxRecDepth 100000 in -example : ((powB (genB 3) 6).toListX == (PB.mul (powB (genB 3) 3) (powB (genB 3) 3)).toListX) = true := by - decide +kernel diff --git a/scratch-mvpoly-bench/lake-manifest.json b/scratch-mvpoly-bench/lake-manifest.json deleted file mode 100644 index 5df5305ca..000000000 --- a/scratch-mvpoly-bench/lake-manifest.json +++ /dev/null @@ -1,6 +0,0 @@ -{"version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": [], - "name": "mvbench", - "lakeDir": ".lake", - "fixedToolchain": false} diff --git a/scratch-mvpoly-bench/lakefile.toml b/scratch-mvpoly-bench/lakefile.toml deleted file mode 100644 index 80c0c548a..000000000 --- a/scratch-mvpoly-bench/lakefile.toml +++ /dev/null @@ -1,4 +0,0 @@ -name = "mvbench" -defaultTargets = ["MV"] -[[lean_lib]] -name = "MV" diff --git a/scratch-mvpoly-bench/lean-toolchain b/scratch-mvpoly-bench/lean-toolchain deleted file mode 100644 index 2694eb767..000000000 --- a/scratch-mvpoly-bench/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.32.0-rc1 diff --git a/scratch-mvpoly-bench/mk.sh b/scratch-mvpoly-bench/mk.sh deleted file mode 100755 index 51643ad3c..000000000 --- a/scratch-mvpoly-bench/mk.sh +++ /dev/null @@ -1,7 +0,0 @@ -rep=$1; k=$2 -cat > T_${rep}_${k}.lean < Date: Tue, 28 Jul 2026 09:00:33 +0000 Subject: [PATCH 3/3] fix: scope the shim instances, redirect compiled equality, add boundary tests Follow-up to review of the shim. The `DecidableEq` instances are now `scoped`, so they apply only inside `namespace Hex` or after `open scoped Hex`. As global instances they overrode core's for every downstream consumer, including consumers of the released libraries that depend on `hex-basic`, which is far too much reach for a workaround that exists to be deleted. A module that forgets to activate them now gets a stuck `decide`, which is loud. Compiled equality regressed the same way `ofFn'` did: routing through `List` means an `O(n)` conversion that allocates both lists in full before comparison starts and loses early exit. Both instances now carry a `@[csimp]` redirect back to the core deciders, proved by `Subsingleton.elim`, so the `List` route is paid only in the kernel. `HexBasic/ModuleBoundaryTests.lean` exercises all three gaps from a separate module, which is the only place they are observable: the defect is that a callee's body is unavailable across a module boundary, so a same-module test passes whether or not the workaround is present. The removal checklist in the repro note was self-contradictory (claiming `ofFn` had no workaround while providing one) and unordered. It now runs call sites before deletions, uses `rg` assertions that must return nothing, names the exact `DensePoly` replacement, and drops `Array.back?`, which is a related exposure gap that #14270 does not fix. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_0188fgvPvjbcXhvTYVSATLhv --- .gitignore | 4 +- HexBasic.lean | 1 + HexBasic/ArrayDecEq.lean | 30 +++++++-- HexBasic/ModuleBoundaryTests.lean | 67 +++++++++++++++++++ HexBerlekampZassenhaus/BhksCandidates.lean | 2 + HexBerlekampZassenhaus/BhksRecover.lean | 2 + HexBerlekampZassenhaus/Certificate.lean | 2 + HexBerlekampZassenhaus/ChoosePrimeData.lean | 2 + HexBerlekampZassenhaus/FactorEntryPoints.lean | 2 + HexBerlekampZassenhaus/IrreducibleCore.lean | 2 + HexBerlekampZassenhaus/Lattice.lean | 2 + HexBerlekampZassenhaus/PrimeSelection.lean | 2 + HexBerlekampZassenhaus/PrimitivityProofs.lean | 2 + HexBerlekampZassenhaus/ProductProofs.lean | 2 + .../QuadraticRootProofs.lean | 2 + HexBerlekampZassenhaus/ReassemblyProofs.lean | 2 + HexBerlekampZassenhaus/Recombination.lean | 2 + HexBerlekampZassenhaus/RecombineProofs.lean | 2 + HexBerlekampZassenhaus/Records.lean | 2 + HexBerlekampZassenhaus/TrialProofs.lean | 2 + .../FactorPolyTests.lean | 2 + HexRCF/SeparationTests.lean | 2 + HexRealRoots/Chain.lean | 2 + HexRealRoots/Isolate.lean | 2 + HexRealRoots/IsolateDescartes.lean | 2 + HexRealRoots/IsolateSturm.lean | 2 + HexRealRoots/Mobius.lean | 2 + HexRealRoots/Refine.lean | 2 + HexRealRoots/SimpleRealRoot.lean | 2 + HexRealRoots/Var.lean | 2 + progress/2026-07-28T10-40-00Z.md | 6 +- .../lean4-array-decidableeq-module-repro.md | 52 +++++++++----- 32 files changed, 183 insertions(+), 29 deletions(-) create mode 100644 HexBasic/ModuleBoundaryTests.lean diff --git a/.gitignore b/.gitignore index e39aa08df..dfc99bd2e 100644 --- a/.gitignore +++ b/.gitignore @@ -11,5 +11,5 @@ conformance-failures/*.json sessions/ _out/ -# Scratch experiments kept out of the tree. -scratch-*/ +# Accidentally-committed scratch benchmark tree; see PR #9044. +/scratch-mvpoly-bench/ diff --git a/HexBasic.lean b/HexBasic.lean index 1429cf716..b70714eae 100644 --- a/HexBasic.lean +++ b/HexBasic.lean @@ -8,6 +8,7 @@ module public import HexBasic.ArrayDecEq public import HexBasic.Fold +public import HexBasic.ModuleBoundaryTests public import HexBasic.OfFn public import HexBasic.ListShim public import HexBasic.Vector.Modify diff --git a/HexBasic/ArrayDecEq.lean b/HexBasic/ArrayDecEq.lean index 719bc5d4d..e65ce4fa0 100644 --- a/HexBasic/ArrayDecEq.lean +++ b/HexBasic/ArrayDecEq.lean @@ -24,21 +24,25 @@ plain `def` whose body is unavailable downstream, so reduction stalls: * `Array.ofFn` delegates to its `ofFn.go` auxiliary. The instances below route through `List` equality, which is fully exposed, and -take priority over the core ones. +take priority over the core ones. They are `scoped`, so they apply only inside +`namespace Hex` or after `open scoped Hex`, and never leak into the released +libraries that depend on `hex-basic` or into their consumers. A module that +forgets to activate them gets a stuck `decide`, which is loud. `List` is the wrong shape for compiled code, +where `Array.toList` is an `O(n)` conversion that allocates both lists in full +before comparison begins and gives up early exit, so each carries a `@[csimp]` +redirect back to the core instance. The `List` route is then paid only in the +kernel, which is where it is needed. **Delete this file** once [leanprover/lean4#14270](https://github.com/leanprover/lean4/pull/14270) lands -and the toolchain is bumped past it. The `Array.ofFn` gap is fixed there too, -and has no workaround here: a definition built with `Array.ofFn` or -`Vector.ofFn` still will not reduce, so kernel-facing code must build its arrays -another way until then. +and the toolchain is bumped past it. `HexBasic.OfFn` covers the third gap. -/ namespace Hex /-- `DecidableEq (Array α)` that reduces in the kernel under the module system, routing through the fully exposed `List` equality. -/ -instance (priority := 1100) instDecidableEqArray +scoped instance (priority := 1100) instDecidableEqArray {α : Type u} [DecidableEq α] : DecidableEq (Array α) := fun a b => match h : decEq a.toList b.toList with | isTrue ht => isTrue (by cases a; cases b; exact congrArg Array.mk ht) @@ -47,7 +51,7 @@ instance (priority := 1100) instDecidableEqArray /-- `DecidableEq (Vector α n)` that reduces in the kernel under the module system. `Vector`'s core instance is derived, and derived instances are opaque across a module boundary. -/ -instance (priority := 1100) instDecidableEqVector +scoped instance (priority := 1100) instDecidableEqVector {α : Type u} {n : Nat} [DecidableEq α] : DecidableEq (Vector α n) := fun a b => match h : decEq a.toArray.toList b.toArray.toList with | isTrue ht => isTrue (by @@ -56,4 +60,16 @@ instance (priority := 1100) instDecidableEqVector subst hba; rfl) | isFalse hf => isFalse (by intro hab; subst hab; exact hf rfl) +/-- Compiled code uses the core `Array` decider, which compares in place. The +`List` route exists only so that the kernel can reduce it. `DecidableEq` is a +subsingleton, so the two agree. -/ +@[csimp] theorem instDecidableEqArray_eq : + @instDecidableEqArray = @_root_.Array.instDecidableEq := by + funext α _ a b; exact Subsingleton.elim _ _ + +/-- As `instDecidableEqArray_eq`. -/ +@[csimp] theorem instDecidableEqVector_eq : + @instDecidableEqVector = @_root_.instDecidableEqVector := by + funext α n _ a b; exact Subsingleton.elim _ _ + end Hex diff --git a/HexBasic/ModuleBoundaryTests.lean b/HexBasic/ModuleBoundaryTests.lean new file mode 100644 index 000000000..0ac14291b --- /dev/null +++ b/HexBasic/ModuleBoundaryTests.lean @@ -0,0 +1,67 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +module + +public import HexBasic.ArrayDecEq +public import HexBasic.OfFn + +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + +public section + +/-! +Regression tests for the three module-system exposure gaps worked around by +`HexBasic.ArrayDecEq` and `HexBasic.OfFn`. + +These have to live in a *separate module* from the definitions they exercise: +the defect is that a callee's body is unavailable across a module boundary, so +a same-module test passes whether or not the workaround is present and proves +nothing. Every example below fails against core's `Array.instDecidableEq`, +`Vector`'s derived instance, or `Array.ofFn`. + +Delete alongside the workarounds once +[leanprover/lean4#14270](https://github.com/leanprover/lean4/pull/14270) lands, +after first re-pointing them at the core definitions and confirming they still +pass. That is the check that the upstream fix actually works. +-/ + +namespace Hex.ModuleBoundaryTests + +/-! ## `Array` equality, both sides nonempty -/ + +example : (#[0, 1] : Array Nat) ≠ #[1] := by decide +example : (#[2, 3] : Array Nat) = #[2, 3] := by decide +example : (#[1, 2, 3] : Array Nat) ≠ #[1, 2, 4] := by decide +kernel +example : decide ((#[0, 1] : Array Nat) = #[0, 1]) = true := by rfl + +/-! Cases that reduced even before the workaround, kept so a regression in the +empty/nonempty branches is caught too. -/ + +example : (#[] : Array Nat) = #[] := by decide +example : (#[] : Array Nat) ≠ #[1] := by decide + +/-! ## `Vector` equality, whose core instance is derived -/ + +example : (#v[0, 1, 2] : Vector Nat 3) ≠ #v[0, 0, 0] := by decide +example : (#v[0, 1, 2] : Vector Nat 3) = #v[0, 1, 2] := by decide +kernel + +/-! ## `ofFn` -/ + +example : (Array.ofFn' (n := 3) (fun i => i.val)).size = 3 := by decide +example : Array.ofFn' (n := 3) (fun i => i.val) = #[0, 1, 2] := by decide +example : Vector.ofFn' (n := 4) (fun i => i.val * 2) = #v[0, 2, 4, 6] := by + decide +kernel + +/-! ## The combination, which is the shape `hex-mv-poly` will use: an exponent +vector built with `ofFn'` and compared for equality. -/ + +example : + (Vector.ofFn' (n := 3) (fun j => if j = 1 then 1 else 0) : Vector Nat 3) + ≠ Vector.ofFn' (fun j => if j = 2 then 1 else 0) := by + decide +kernel + +end Hex.ModuleBoundaryTests diff --git a/HexBerlekampZassenhaus/BhksCandidates.lean b/HexBerlekampZassenhaus/BhksCandidates.lean index 09991c292..e376e7829 100644 --- a/HexBerlekampZassenhaus/BhksCandidates.lean +++ b/HexBerlekampZassenhaus/BhksCandidates.lean @@ -34,6 +34,8 @@ import all HexBerlekampZassenhaus.ChoosePrimeData import all HexBerlekampZassenhaus.ReassemblyProofs import all HexBerlekampZassenhaus.Lattice +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/BhksRecover.lean b/HexBerlekampZassenhaus/BhksRecover.lean index 4c10b9ed7..a9bef073b 100644 --- a/HexBerlekampZassenhaus/BhksRecover.lean +++ b/HexBerlekampZassenhaus/BhksRecover.lean @@ -35,6 +35,8 @@ import all HexBerlekampZassenhaus.ReassemblyProofs import all HexBerlekampZassenhaus.Lattice import all HexBerlekampZassenhaus.BhksCandidates +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/Certificate.lean b/HexBerlekampZassenhaus/Certificate.lean index 07ac29a96..39810e9e0 100644 --- a/HexBerlekampZassenhaus/Certificate.lean +++ b/HexBerlekampZassenhaus/Certificate.lean @@ -30,6 +30,8 @@ public meta import HexBerlekampZassenhaus.Records import all HexBerlekampZassenhaus.PrimeSelection import all HexBerlekampZassenhaus.Records +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/ChoosePrimeData.lean b/HexBerlekampZassenhaus/ChoosePrimeData.lean index fd7d47fc9..c2c4fb059 100644 --- a/HexBerlekampZassenhaus/ChoosePrimeData.lean +++ b/HexBerlekampZassenhaus/ChoosePrimeData.lean @@ -31,6 +31,8 @@ import all HexBerlekampZassenhaus.PrimeSelection import all HexBerlekampZassenhaus.Records import all HexBerlekampZassenhaus.Certificate +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/FactorEntryPoints.lean b/HexBerlekampZassenhaus/FactorEntryPoints.lean index 4857e810f..5c1c3e3d0 100644 --- a/HexBerlekampZassenhaus/FactorEntryPoints.lean +++ b/HexBerlekampZassenhaus/FactorEntryPoints.lean @@ -37,6 +37,8 @@ import all HexBerlekampZassenhaus.BhksCandidates import all HexBerlekampZassenhaus.BhksRecover import all HexBerlekampZassenhaus.Recombination +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/IrreducibleCore.lean b/HexBerlekampZassenhaus/IrreducibleCore.lean index 72e29819d..1e140c9cf 100644 --- a/HexBerlekampZassenhaus/IrreducibleCore.lean +++ b/HexBerlekampZassenhaus/IrreducibleCore.lean @@ -38,6 +38,8 @@ import all HexBerlekampZassenhaus.BhksRecover import all HexBerlekampZassenhaus.Recombination import all HexBerlekampZassenhaus.FactorEntryPoints +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/Lattice.lean b/HexBerlekampZassenhaus/Lattice.lean index 718c9a220..279e8e44a 100644 --- a/HexBerlekampZassenhaus/Lattice.lean +++ b/HexBerlekampZassenhaus/Lattice.lean @@ -34,6 +34,8 @@ import all HexBerlekampZassenhaus.Certificate import all HexBerlekampZassenhaus.ChoosePrimeData import all HexBerlekampZassenhaus.ReassemblyProofs +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/PrimeSelection.lean b/HexBerlekampZassenhaus/PrimeSelection.lean index ae73d9b59..4cfb4c050 100644 --- a/HexBerlekampZassenhaus/PrimeSelection.lean +++ b/HexBerlekampZassenhaus/PrimeSelection.lean @@ -25,6 +25,8 @@ public import HexLLL.Basic -- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. public import HexBasic.ArrayDecEq +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/PrimitivityProofs.lean b/HexBerlekampZassenhaus/PrimitivityProofs.lean index 39783d1d6..361d5bcda 100644 --- a/HexBerlekampZassenhaus/PrimitivityProofs.lean +++ b/HexBerlekampZassenhaus/PrimitivityProofs.lean @@ -42,6 +42,8 @@ import all HexBerlekampZassenhaus.RecombineProofs import all HexBerlekampZassenhaus.TrialProofs import all HexBerlekampZassenhaus.QuadraticRootProofs +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/ProductProofs.lean b/HexBerlekampZassenhaus/ProductProofs.lean index ebe62a9aa..31f432def 100644 --- a/HexBerlekampZassenhaus/ProductProofs.lean +++ b/HexBerlekampZassenhaus/ProductProofs.lean @@ -43,6 +43,8 @@ import all HexBerlekampZassenhaus.TrialProofs import all HexBerlekampZassenhaus.QuadraticRootProofs import all HexBerlekampZassenhaus.PrimitivityProofs +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/QuadraticRootProofs.lean b/HexBerlekampZassenhaus/QuadraticRootProofs.lean index e29099d17..17210cf05 100644 --- a/HexBerlekampZassenhaus/QuadraticRootProofs.lean +++ b/HexBerlekampZassenhaus/QuadraticRootProofs.lean @@ -41,6 +41,8 @@ import all HexBerlekampZassenhaus.IrreducibleCore import all HexBerlekampZassenhaus.RecombineProofs import all HexBerlekampZassenhaus.TrialProofs +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/ReassemblyProofs.lean b/HexBerlekampZassenhaus/ReassemblyProofs.lean index 3dea70591..fd5073c2c 100644 --- a/HexBerlekampZassenhaus/ReassemblyProofs.lean +++ b/HexBerlekampZassenhaus/ReassemblyProofs.lean @@ -32,6 +32,8 @@ import all HexBerlekampZassenhaus.Records import all HexBerlekampZassenhaus.Certificate import all HexBerlekampZassenhaus.ChoosePrimeData +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/Recombination.lean b/HexBerlekampZassenhaus/Recombination.lean index 7397d9f3e..4ef930b13 100644 --- a/HexBerlekampZassenhaus/Recombination.lean +++ b/HexBerlekampZassenhaus/Recombination.lean @@ -36,6 +36,8 @@ import all HexBerlekampZassenhaus.Lattice import all HexBerlekampZassenhaus.BhksCandidates import all HexBerlekampZassenhaus.BhksRecover +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/RecombineProofs.lean b/HexBerlekampZassenhaus/RecombineProofs.lean index 65922e17c..5ad1f3fe4 100644 --- a/HexBerlekampZassenhaus/RecombineProofs.lean +++ b/HexBerlekampZassenhaus/RecombineProofs.lean @@ -39,6 +39,8 @@ import all HexBerlekampZassenhaus.Recombination import all HexBerlekampZassenhaus.FactorEntryPoints import all HexBerlekampZassenhaus.IrreducibleCore +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/Records.lean b/HexBerlekampZassenhaus/Records.lean index 74fa2fd1d..5a0fd2639 100644 --- a/HexBerlekampZassenhaus/Records.lean +++ b/HexBerlekampZassenhaus/Records.lean @@ -30,6 +30,8 @@ public import HexBerlekampZassenhaus.SquareFreeModularCert public meta import HexBerlekampZassenhaus.PrimeSelection import all HexBerlekampZassenhaus.PrimeSelection +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhaus/TrialProofs.lean b/HexBerlekampZassenhaus/TrialProofs.lean index 390c1129b..f73060f94 100644 --- a/HexBerlekampZassenhaus/TrialProofs.lean +++ b/HexBerlekampZassenhaus/TrialProofs.lean @@ -40,6 +40,8 @@ import all HexBerlekampZassenhaus.FactorEntryPoints import all HexBerlekampZassenhaus.IrreducibleCore import all HexBerlekampZassenhaus.RecombineProofs +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section set_option backward.proofsInPublic true diff --git a/HexBerlekampZassenhausMathlib/FactorPolyTests.lean b/HexBerlekampZassenhausMathlib/FactorPolyTests.lean index 6e5ec5511..491213495 100644 --- a/HexBerlekampZassenhausMathlib/FactorPolyTests.lean +++ b/HexBerlekampZassenhausMathlib/FactorPolyTests.lean @@ -152,6 +152,8 @@ import all Init.Data.List.Range import all Init.Data.Nat.Fold import all Init.Data.Range.Basic +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section /-! diff --git a/HexRCF/SeparationTests.lean b/HexRCF/SeparationTests.lean index a416edb70..196b9619b 100644 --- a/HexRCF/SeparationTests.lean +++ b/HexRCF/SeparationTests.lean @@ -27,6 +27,8 @@ import all HexRealRoots.Basic import all HexRealRoots.Chain import all HexRealRoots.Var +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section /-! Regression tests for strict separation and exact endpoint comparison. -/ diff --git a/HexRealRoots/Chain.lean b/HexRealRoots/Chain.lean index 6197b247c..5b7bd0ad7 100644 --- a/HexRealRoots/Chain.lean +++ b/HexRealRoots/Chain.lean @@ -11,6 +11,8 @@ public import HexRealRoots.Basic -- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it. public import HexBasic.ArrayDecEq +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section /-! diff --git a/HexRealRoots/Isolate.lean b/HexRealRoots/Isolate.lean index 32ac32dfe..60a7a6270 100644 --- a/HexRealRoots/Isolate.lean +++ b/HexRealRoots/Isolate.lean @@ -18,6 +18,8 @@ import all HexRealRoots.Prec import all HexRealRoots.IsolateSturm import all HexRealRoots.IsolateDescartes +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section /-! diff --git a/HexRealRoots/IsolateDescartes.lean b/HexRealRoots/IsolateDescartes.lean index 74d664b51..70326c1e5 100644 --- a/HexRealRoots/IsolateDescartes.lean +++ b/HexRealRoots/IsolateDescartes.lean @@ -16,6 +16,8 @@ import all HexRealRoots.Basic import all HexRealRoots.Chain import all HexRealRoots.Var +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section /-! diff --git a/HexRealRoots/IsolateSturm.lean b/HexRealRoots/IsolateSturm.lean index 44d7f2f1b..4d48bf6c9 100644 --- a/HexRealRoots/IsolateSturm.lean +++ b/HexRealRoots/IsolateSturm.lean @@ -15,6 +15,8 @@ import all HexRealRoots.Basic import all HexRealRoots.Chain import all HexRealRoots.Var +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section /-! diff --git a/HexRealRoots/Mobius.lean b/HexRealRoots/Mobius.lean index 9721bc120..f6ef62686 100644 --- a/HexRealRoots/Mobius.lean +++ b/HexRealRoots/Mobius.lean @@ -12,6 +12,8 @@ public import HexRealRoots.Var public import HexBasic.ArrayDecEq import all HexRealRoots.Var +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section /-! diff --git a/HexRealRoots/Refine.lean b/HexRealRoots/Refine.lean index d8954fa3e..9cd210985 100644 --- a/HexRealRoots/Refine.lean +++ b/HexRealRoots/Refine.lean @@ -16,6 +16,8 @@ import all HexRealRoots.Chain import all HexRealRoots.Var import all HexRealRoots.Prec +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section /-! diff --git a/HexRealRoots/SimpleRealRoot.lean b/HexRealRoots/SimpleRealRoot.lean index 7290f35a0..3fd042b45 100644 --- a/HexRealRoots/SimpleRealRoot.lean +++ b/HexRealRoots/SimpleRealRoot.lean @@ -17,6 +17,8 @@ import all HexRealRoots.Var import all HexRealRoots.Prec import all HexRealRoots.Refine +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section /-! diff --git a/HexRealRoots/Var.lean b/HexRealRoots/Var.lean index 27e51c48a..e904016dd 100644 --- a/HexRealRoots/Var.lean +++ b/HexRealRoots/Var.lean @@ -13,6 +13,8 @@ public import HexBasic.ArrayDecEq import all HexRealRoots.Basic import all HexRealRoots.Chain +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section /-! diff --git a/progress/2026-07-28T10-40-00Z.md b/progress/2026-07-28T10-40-00Z.md index 7f2a75e63..c45e050ad 100644 --- a/progress/2026-07-28T10-40-00Z.md +++ b/progress/2026-07-28T10-40-00Z.md @@ -24,8 +24,10 @@ - `HexBasic.ArrayDecEq` is a shim with a scheduled death. The cleanup steps are written down in the repro note. -- The `Array.ofFn` gap has no consumer-side workaround, so kernel-facing code - still cannot build arrays that way. +- `HexBasic.OfFn` covers the `Array.ofFn` gap, but nothing in the tree uses it + yet; roughly 42 exposed definitions still call core `Array.ofFn` / + `Vector.ofFn` and should be audited for whether they need to reduce + downstream. ## Next step diff --git a/progress/lean4-array-decidableeq-module-repro.md b/progress/lean4-array-decidableeq-module-repro.md index e28217084..baffb4e6c 100644 --- a/progress/lean4-array-decidableeq-module-repro.md +++ b/progress/lean4-array-decidableeq-module-repro.md @@ -51,8 +51,7 @@ body is unavailable to the kernel downstream — `#print Array.instDecidableEqIm ## Two further instances of the same defect -Chasing the `Vector` case turned up two more, both with the same shape and neither -fixable from the consumer side. +Chasing the `Vector` case turned up two more, both with the same shape. **Every `deriving DecidableEq` instance.** `Lean.Elab.Deriving.DecEq.mkAuxFunction` emits the generated `decEq` as a plain `def`, so its body is opaque across a module @@ -73,9 +72,11 @@ example : (⟨1⟩ : P) ≠ ⟨2⟩ := by decide -- stuck at instDecidableEqP. ``` `Vector`'s instance is derived, which is why `Vector` equality stalls even once -`Array` is fixed. There is no workaround: `@[expose]` cannot be attached to a -structure, and `attribute [expose] …` after the fact is rejected ("can only be -added when declaring a `def`"). +`Array` is fixed. The generated `decEq` cannot be exposed retrospectively: +`@[expose]` cannot be attached to a structure, and `attribute [expose] …` after +the fact is rejected ("can only be added when declaring a `def`"). A consumer +can still supply a replacement instance, which is what `HexBasic.ArrayDecEq` +does. **`Array.ofFn`.** Delegates to its `ofFn.go` auxiliary, so `(Array.ofFn f).size = n` does not reduce. `Vector.ofFn` is already `@[expose]` @@ -110,19 +111,34 @@ All three are fixed by After the toolchain is bumped past the fix: -1. Delete `HexBasic/ArrayDecEq.lean` and `HexBasic/OfFn.lean`, and their entries - in `HexBasic.lean`. -2. Remove the `public import HexBasic.ArrayDecEq` line and its two-line comment - from every module that carries it (`grep -rl HexBasic.ArrayDecEq`), and - replace every `Array.ofFn'` / `Vector.ofFn'` use with the core version - (`grep -rl "ofFn'"`); `ofFn'_eq_ofFn` makes that a rewrite. -3. Replace `HexPoly.Dense`'s hand-written `DecidableEq (DensePoly R)` with the - ordinary `Array`-based comparison, and drop the explanatory comment. -4. Reconsider `HexPoly.Euclid.leadingCoeff`, which avoids `Array.back?` for the - related reason below, and any code that avoids `Array.ofFn` for kernel - reasons. -5. Re-run the kernel-facing conformance and bench targets, since the point of - all of this is reduction behaviour rather than elaboration. +Record the first toolchain containing the fix, then, **in this order** (call +sites before deletions, so nothing is briefly unbuildable): + +1. Re-point `HexBasic/ModuleBoundaryTests.lean` at the core definitions + (`Array.ofFn`, `Vector.ofFn`, and core equality) and confirm it still + passes. This is the check that the upstream fix actually landed; do not + skip it. +2. Replace Lean call sites: + `rg -l "ofFn'" --glob '*.lean'` and rewrite each to the core version; + `ofFn'_eq_ofFn` makes that a rewrite rather than a reproof. +3. Remove the `public import HexBasic.ArrayDecEq` line and its two-line + comment from every module carrying it: + `rg -l "HexBasic.ArrayDecEq" --glob '*.lean'`. +4. Replace `HexPoly.Dense`'s hand-written `DecidableEq (DensePoly R)` with + `fun a b => decEq a.coeffs b.coeffs` lifted through proof irrelevance on the + `normalized` field, and drop its explanatory comment. Update the + `beqCoeffs` docstring, which describes the pre-workaround behaviour. +5. Delete `HexBasic/ArrayDecEq.lean`, `HexBasic/OfFn.lean`, and + `HexBasic/ModuleBoundaryTests.lean`, and their entries in `HexBasic.lean`. +6. Assert the cleanup is complete: `rg "ofFn'|HexBasic.ArrayDecEq" --glob + '*.lean'` must return nothing. +7. Run a full `lake build` plus the kernel-facing conformance and bench + targets, since the point of all of this is reduction behaviour rather than + elaboration. + +`HexPoly.Euclid.leadingCoeff` avoids `Array.back?`, which is a related +exposure gap but is **not** fixed by #14270. Leave it alone; it needs its own +upstream change. ## Related