1.2. Kernel-reducible containers🔗

Hex certificate checking runs decide +kernel over concrete arrays and vectors, so the kernel has to reduce both array construction and array equality. Under Lean's module system it does not, for four separate reasons. Array.ofFn delegates to an unexposed ofFn.go; Array.map delegates to an unexposed implementation loop, and Vector.map inherits that through it; core's Array.instDecidableEq delegates to an unexposed Array.instDecidableEqImpl; and Vector gets its equality from deriving DecidableEq, whose generated decEq is likewise unexposed. In each case the callee's body is unavailable downstream, so reduction stalls on a term the kernel can see but cannot unfold.

The workaround is the same in every case. Route through List, which is fully exposed and does reduce, and attach a @[csimp] lemma sending compiled code back to the core definition. The list detour is then paid only in the kernel, which is the one place it buys anything: Array.toList is an O(n) conversion that allocates in full and gives up early exit, so it is the wrong shape for compiled code.

def

Hex.Array.ofFn'.{u} {α : Type u} {n : Nat} (f : Fin n → α) : Array α
Hex.Array.ofFn'.{u} {α : Type u} {n : Nat}
  (f : Fin n → α) : Array α

An Array.ofFn equivalent that reduces in the kernel under the module system.

def

Hex.Vector.ofFn'.{u} {n : Nat} {α : Type u} (f : Fin n → α) : Vector α n
Hex.Vector.ofFn'.{u} {n : Nat}
  {α : Type u} (f : Fin n → α) :
  Vector α n

A Vector.ofFn equivalent that reduces in the kernel under the module system.

def

Hex.Array.map'.{u, v} {α : Type u} {β : Type v} (f : α → β)
  (a : Array α) : Array β
Hex.Array.map'.{u, v} {α : Type u}
  {β : Type v} (f : α → β) (a : Array α) :
  Array β

An Array.map equivalent that reduces in the kernel under the module system: core Array.map's implementation loop is not exposed, so (a.map f) stalls downstream exactly like Array.ofFn. Remove this shim and migrate its callers to core Array.map when the pinned toolchain reaches Lean v4.35.0-rc1, which includes <https://github.com/leanprover/lean4/pull/14996>.

def

Hex.Vector.map'.{u, v} {α : Type u} {β : Type v} {n : Nat} (f : α → β)
  (v : Vector α n) : Vector β n
Hex.Vector.map'.{u, v} {α : Type u}
  {β : Type v} {n : Nat} (f : α → β)
  (v : Vector α n) : Vector β n

A Vector.map equivalent that reduces in the kernel under the module system: core Vector.map delegates to Array.map, whose implementation loop is not exposed, so (v.map f) stalls downstream. Remove this shim and migrate its callers to core Vector.map when the pinned toolchain reaches Lean v4.35.0-rc1, alongside Hex.Array.map'.

The accompanying simplification lemmas identify the primed constructors with their standard counterparts, so ordinary container lemmas remain available. Hex.Vector.map' is what makes the Leibniz determinant reduce in the kernel: Hex.Matrix.permutationVectors builds its enumeration by mapping over the shorter permutations, so a stalled Vector.map stalls the whole determinant.

def

Hex.instDecidableEqArray.{u} {α : Type u} [DecidableEq α] :
  DecidableEq (Array α)
Hex.instDecidableEqArray.{u} {α : Type u}
  [DecidableEq α] : DecidableEq (Array α)

DecidableEq (Array α) that reduces in the kernel under the module system, routing through the fully exposed List equality.

def

Hex.instDecidableEqVector.{u} {α : Type u} {n : Nat} [DecidableEq α] :
  DecidableEq (Vector α n)
Hex.instDecidableEqVector.{u} {α : Type u}
  {n : Nat} [DecidableEq α] :
  DecidableEq (Vector α n)

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.

Both instances are scoped, so they take effect under open scoped Hex and nowhere else, and never leak into a consumer that has not asked for them. A module that forgets to open the scope gets a stuck decide, which is a loud failure rather than a silent change of meaning.

These definitions are shims, not API this library wants to own, and they retire on different upstream fixes rather than all at once. ofFn and the two equality instances wait on leanprover/lean4#14270; the map shims wait on leanprover/lean4#14996, which ships in Lean v4.35.0-rc1. Once the toolchain moves past the relevant one, core's own operation reduces in the kernel, that shim goes away, and callers move back to the standard name. Retire them one at a time, and re-check that the downstream reduction still works before removing each: the stall these work around is only visible across a module boundary. HexBasic.ModuleBoundaryTests is what makes that checkable: it sits in a separate module from the definitions it exercises, because a same-module test passes whether or not the workaround is present and so proves nothing.

HexBasic also supplies an entrywise vector update with the pointwise read law its callers reason with.

def

Vector.modify.{u_1} {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat)
  (f : α → α) : Vector α n
Vector.modify.{u_1} {α : Type u_1}
  {n : Nat} (xs : Vector α n) (i : Nat)
  (f : α → α) : Vector α n

In-place update of the element at index i via f, wrapping Array.modify so the underlying swap-with-placeholder ownership transfer survives codegen. Calling xs.set i (f xs[i]) forces a lean_inc on the borrowed entry and loses uniqueness on nested-array shapes (e.g. matrix rows); modify avoids that copy when xs is uniquely owned.

theorem

Vector.getElem_modify.{u_1} {α : Type u_1} {n : Nat} {xs : Vector α n}
  {i : Nat} {f : α → α} {j : Nat} (hj : j < n) :
  (xs.modify i f)[j] = if i = j then f xs[j] else xs[j]
Vector.getElem_modify.{u_1} {α : Type u_1}
  {n : Nat} {xs : Vector α n} {i : Nat}
  {f : α → α} {j : Nat} (hj : j < n) :
  (xs.modify i f)[j] =
    if i = j then f xs[j] else xs[j]

Entrywise read of modify: the modified index gets f applied, every other index is unchanged.