diff --git a/.gitignore b/.gitignore index 49adac409..dfc99bd2e 100644 --- a/.gitignore +++ b/.gitignore @@ -10,3 +10,6 @@ conformance-failures/*.json .pod/ sessions/ _out/ + +# Accidentally-committed scratch benchmark tree; see PR #9044. +/scratch-mvpoly-bench/ diff --git a/HexBasic.lean b/HexBasic.lean index 0c3610691..b70714eae 100644 --- a/HexBasic.lean +++ b/HexBasic.lean @@ -6,7 +6,10 @@ Authors: Kim Morrison 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 @@ -17,5 +20,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..e65ce4fa0 --- /dev/null +++ b/HexBasic/ArrayDecEq.lean @@ -0,0 +1,75 @@ +/- +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. 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. `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. -/ +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) + | 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. -/ +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 + 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) + +/-- 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/HexBasic/OfFn.lean b/HexBasic/OfFn.lean new file mode 100644 index 000000000..4bd05be64 --- /dev/null +++ b/HexBasic/OfFn.lean @@ -0,0 +1,62 @@ +/- +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. 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 +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' {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 {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/HexBerlekampZassenhaus/BhksCandidates.lean b/HexBerlekampZassenhaus/BhksCandidates.lean index a09d1b225..e376e7829 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 @@ -36,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 8ef6b0c11..a9bef073b 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 @@ -37,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 82350161f..39810e9e0 100644 --- a/HexBerlekampZassenhaus/Certificate.lean +++ b/HexBerlekampZassenhaus/Certificate.lean @@ -21,17 +21,17 @@ 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 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 9de9de765..c2c4fb059 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 @@ -33,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 b58664ea7..5c1c3e3d0 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 @@ -39,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 1ddb85fea..1e140c9cf 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 @@ -40,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 13082bfbe..279e8e44a 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 @@ -36,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 08da61b1f..4cfb4c050 100644 --- a/HexBerlekampZassenhaus/PrimeSelection.lean +++ b/HexBerlekampZassenhaus/PrimeSelection.lean @@ -21,11 +21,11 @@ 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 + +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq public section diff --git a/HexBerlekampZassenhaus/PrimitivityProofs.lean b/HexBerlekampZassenhaus/PrimitivityProofs.lean index 9c2f7a031..361d5bcda 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 @@ -44,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 d8068389d..31f432def 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 @@ -45,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 b4d53061b..17210cf05 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 @@ -43,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 ecaca8143..fd5073c2c 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 @@ -34,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 32c94f66b..4ef930b13 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 @@ -38,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 edbc87b99..5ad1f3fe4 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 @@ -41,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 05ca6eebc..5a0fd2639 100644 --- a/HexBerlekampZassenhaus/Records.lean +++ b/HexBerlekampZassenhaus/Records.lean @@ -21,17 +21,17 @@ 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 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 19357b8d5..f73060f94 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 @@ -42,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 09e8e7d63..491213495 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 @@ -150,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/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..196b9619b 100644 --- a/HexRCF/SeparationTests.lean +++ b/HexRCF/SeparationTests.lean @@ -20,11 +20,15 @@ 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 +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 835b320cb..5b7bd0ad7 100644 --- a/HexRealRoots/Chain.lean +++ b/HexRealRoots/Chain.lean @@ -7,11 +7,11 @@ 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 + +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq public section diff --git a/HexRealRoots/Isolate.lean b/HexRealRoots/Isolate.lean index a38be8a9c..60a7a6270 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 @@ -21,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 8de0b9186..70326c1e5 100644 --- a/HexRealRoots/IsolateDescartes.lean +++ b/HexRealRoots/IsolateDescartes.lean @@ -9,17 +9,15 @@ 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 +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section /-! diff --git a/HexRealRoots/IsolateSturm.lean b/HexRealRoots/IsolateSturm.lean index bba570305..4d48bf6c9 100644 --- a/HexRealRoots/IsolateSturm.lean +++ b/HexRealRoots/IsolateSturm.lean @@ -8,17 +8,15 @@ 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 +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section /-! diff --git a/HexRealRoots/Mobius.lean b/HexRealRoots/Mobius.lean index 4b31d1181..f6ef62686 100644 --- a/HexRealRoots/Mobius.lean +++ b/HexRealRoots/Mobius.lean @@ -7,16 +7,13 @@ 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 +open scoped Hex -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq + public section /-! diff --git a/HexRealRoots/Refine.lean b/HexRealRoots/Refine.lean index f08ffd0af..9cd210985 100644 --- a/HexRealRoots/Refine.lean +++ b/HexRealRoots/Refine.lean @@ -8,18 +8,16 @@ 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 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 2d99389a9..3fd042b45 100644 --- a/HexRealRoots/SimpleRealRoot.lean +++ b/HexRealRoots/SimpleRealRoot.lean @@ -8,18 +8,17 @@ 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 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 c3820c20d..e904016dd 100644 --- a/HexRealRoots/Var.lean +++ b/HexRealRoots/Var.lean @@ -7,15 +7,14 @@ 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 +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 new file mode 100644 index 000000000..c45e050ad --- /dev/null +++ b/progress/2026-07-28T10-40-00Z.md @@ -0,0 +1,39 @@ +# 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. +- `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 + +- 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..baffb4e6c 100644 --- a/progress/lean4-array-decidableeq-module-repro.md +++ b/progress/lean4-array-decidableeq-module-repro.md @@ -49,19 +49,96 @@ 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. + +**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. 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]` +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: + +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