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 three separate reasons. Array.ofFn delegates to an unexposed ofFn.go; 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 all three cases. 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.

The accompanying simplification lemmas identify the primed constructors with their standard counterparts, so ordinary container lemmas remain available.

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 four definitions are shims, not API this library wants to own. When leanprover/lean4#14270 lands and the toolchain moves past it, core's own ofFn and equality reduce in the kernel, the primed constructors and the priority instances go away, and callers move back to the standard names. HexBasic.ModuleBoundaryTests is what makes that removal 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.