structure Hex.Matrix.Region (N M rows cols : Nat) : Type

A backing-free descriptor for a rows × cols rectangle inside an N × M matrix.

• r0 : Nat

  Row offset in the destination matrix.

• c0 : Nat

  Column offset in the destination matrix.

• rows_le : self.r0 + rows ≤ N

  The described rows lie in the destination.

• cols_le : self.c0 + cols ≤ M

  The described columns lie in the destination.

@[inline]

def Hex.Matrix.Region.row {N M rows cols : Nat} (D : Region N M rows cols) (i : Fin rows) : Fin N

Destination row corresponding to a local region row.

Equations

• D.row i = ⟨D.r0 + ↑i, ⋯⟩

@[inline]

def Hex.Matrix.Region.col {N M rows cols : Nat} (D : Region N M rows cols) (j : Fin cols) : Fin M

Destination column corresponding to a local region column.

Equations

• D.col j = ⟨D.c0 + ↑j, ⋯⟩

@[inline]

def Hex.Matrix.Region.rowStart {N M rows cols : Nat} (D : Region N M rows cols) (i : Fin rows) : Nat

First flat destination index in a local region row.

Equations

• D.rowStart i = (D.r0 + ↑i) * M + D.c0

@[inline]

def Hex.Matrix.Region.index {N M rows cols : Nat} (D : Region N M rows cols) (i : Fin rows) (j : Fin cols) : Fin (N * M)

Flat destination index corresponding to local region coordinates. The row-invariant multiplication is kept in rowStart, outside column loops.

Equations

• D.index i j = ⟨D.rowStart i + ↑j, ⋯⟩

@[inline]

def Hex.Matrix.Region.get {R : Type u} {N M rows cols : Nat} (D : Region N M rows cols) (A : Matrix R N M) (i : Fin rows) (j : Fin cols) : R

Read a matrix entry through a region descriptor.

Equations

• D.get A i j = A[(D.row i, D.col j)]

theorem Hex.Matrix.Region.get_eq_data {R : Type u} {N M rows cols : Nat} (D : Region N M rows cols) (A : Matrix R N M) (i : Fin rows) (j : Fin cols) : D.get A i j = A.data[↑(D.index i j)]

A region read is a read at its flat index.

def Hex.Matrix.Region.toMatrix {R : Type u} {N M rows cols : Nat} (D : Region N M rows cols) (A : Matrix R N M) : Matrix R rows cols

Materialize the entries described by a region. This is a proof-facing operation; the storage-scheduled implementation writes through descriptors without calling it.

Equations

• D.toMatrix A = Hex.Matrix.ofFn fun (i : Fin rows) (j : Fin cols) => D.get A i j

@[simp]

theorem Hex.Matrix.Region.getElem_toMatrix {R : Type u} {N M rows cols : Nat} (D : Region N M rows cols) (A : Matrix R N M) (i : Fin rows) (j : Fin cols) : (D.toMatrix A)[i][j] = D.get A i j

Entry formula for a materialized region.

theorem Hex.Matrix.Region.get_of_toMatrix_eq {R : Type u} {N M rows cols : Nat} (D : Region N M rows cols) (A : Matrix R N M) (B : Matrix R rows cols) (h : D.toMatrix A = B) (i : Fin rows) (j : Fin cols) : D.get A i j = B[(i, j)]

Extract an entry equality from equality of a materialized region and a matrix.

theorem Hex.Matrix.Region.get_eq_of_toMatrix_eq {R : Type u} {N M rows cols : Nat} (D : Region N M rows cols) (A B : Matrix R N M) (h : D.toMatrix A = D.toMatrix B) (i : Fin rows) (j : Fin cols) : D.get A i j = D.get B i j

Equal materialized regions have equal entries.

@[inline]

def Hex.Matrix.Region.full (N M : Nat) : Region N M N M

The descriptor for a whole matrix.

Equations

• Hex.Matrix.Region.full N M = { r0 := 0, c0 := 0, rows_le := ⋯, cols_le := ⋯ }

@[simp]

theorem Hex.Matrix.Region.get_full {R : Type u} {N M : Nat} (A : Matrix R N M) (i : Fin N) (j : Fin M) : (full N M).get A i j = A[(i, j)]

Reading through a whole-matrix descriptor is ordinary matrix access.

@[simp]

theorem Hex.Matrix.Region.toMatrix_full {R : Type u} {N M : Nat} (A : Matrix R N M) : (full N M).toMatrix A = A

Materializing a whole-matrix descriptor returns the matrix.

@[inline]

def Hex.Matrix.Region.toBlocks₁₁ {N M h w : Nat} (D : Region N M (h + h) (w + w)) : Region N M h w

Top-left quadrant of an evenly split region.

Equations

• D.toBlocks₁₁ = { r0 := D.r0, c0 := D.c0, rows_le := ⋯, cols_le := ⋯ }

@[inline]

def Hex.Matrix.Region.toBlocks₁₂ {N M h w : Nat} (D : Region N M (h + h) (w + w)) : Region N M h w

Top-right quadrant of an evenly split region.

Equations

• D.toBlocks₁₂ = { r0 := D.r0, c0 := D.c0 + w, rows_le := ⋯, cols_le := ⋯ }

@[inline]

def Hex.Matrix.Region.toBlocks₂₁ {N M h w : Nat} (D : Region N M (h + h) (w + w)) : Region N M h w

Bottom-left quadrant of an evenly split region.

Equations

• D.toBlocks₂₁ = { r0 := D.r0 + h, c0 := D.c0, rows_le := ⋯, cols_le := ⋯ }

@[inline]

def Hex.Matrix.Region.toBlocks₂₂ {N M h w : Nat} (D : Region N M (h + h) (w + w)) : Region N M h w

Bottom-right quadrant of an evenly split region.

Equations

• D.toBlocks₂₂ = { r0 := D.r0 + h, c0 := D.c0 + w, rows_le := ⋯, cols_le := ⋯ }

def Hex.Matrix.Region.Disjoint {N M rows cols rows' cols' : Nat} (D : Region N M rows cols) (E : Region N M rows' cols') : Prop

Two region descriptors have disjoint rectangles.

Equations

• D.Disjoint E = (D.r0 + rows ≤ E.r0 ∨ E.r0 + rows' ≤ D.r0 ∨ D.c0 + cols ≤ E.c0 ∨ E.c0 + cols' ≤ D.c0)

theorem Hex.Matrix.Region.disjoint₁₁₁₂ {N M h w : Nat} (D : Region N M (h + h) (w + w)) : D.toBlocks₁₁.Disjoint D.toBlocks₁₂

The left and right quadrants in the top row are disjoint.

theorem Hex.Matrix.Region.disjoint₁₁₂₁ {N M h w : Nat} (D : Region N M (h + h) (w + w)) : D.toBlocks₁₁.Disjoint D.toBlocks₂₁

The top-left and bottom-left quadrants are disjoint.

theorem Hex.Matrix.Region.disjoint₁₁₂₂ {N M h w : Nat} (D : Region N M (h + h) (w + w)) : D.toBlocks₁₁.Disjoint D.toBlocks₂₂

The top-left and bottom-right quadrants are disjoint.

theorem Hex.Matrix.Region.disjoint₁₂₂₁ {N M h w : Nat} (D : Region N M (h + h) (w + w)) : D.toBlocks₁₂.Disjoint D.toBlocks₂₁

The top-right and bottom-left quadrants are disjoint.

theorem Hex.Matrix.Region.disjoint₁₂₂₂ {N M h w : Nat} (D : Region N M (h + h) (w + w)) : D.toBlocks₁₂.Disjoint D.toBlocks₂₂

The top-right and bottom-right quadrants are disjoint.

theorem Hex.Matrix.Region.disjoint₂₁₂₂ {N M h w : Nat} (D : Region N M (h + h) (w + w)) : D.toBlocks₂₁.Disjoint D.toBlocks₂₂

The left and right quadrants in the bottom row are disjoint.

theorem Hex.Matrix.Region.disjoint_toBlocks₁₁ {N M rows cols h w : Nat} (D : Region N M (h + h) (w + w)) (E : Region N M rows cols) (hDE : D.Disjoint E) : D.toBlocks₁₁.Disjoint E

A region disjoint from a parent is disjoint from its top-left quadrant.

theorem Hex.Matrix.Region.disjoint_toBlocks₁₂ {N M rows cols h w : Nat} (D : Region N M (h + h) (w + w)) (E : Region N M rows cols) (hDE : D.Disjoint E) : D.toBlocks₁₂.Disjoint E

A region disjoint from a parent is disjoint from its top-right quadrant.

theorem Hex.Matrix.Region.disjoint_toBlocks₂₁ {N M rows cols h w : Nat} (D : Region N M (h + h) (w + w)) (E : Region N M rows cols) (hDE : D.Disjoint E) : D.toBlocks₂₁.Disjoint E

A region disjoint from a parent is disjoint from its bottom-left quadrant.

theorem Hex.Matrix.Region.disjoint_toBlocks₂₂ {N M rows cols h w : Nat} (D : Region N M (h + h) (w + w)) (E : Region N M rows cols) (hDE : D.Disjoint E) : D.toBlocks₂₂.Disjoint E

A region disjoint from a parent is disjoint from its bottom-right quadrant.

theorem Hex.Matrix.Region.toMatrix_toBlocks₁₁ {R : Type u} {N M h w : Nat} (D : Region N M (h + h) (w + w)) (A : Matrix R N M) : D.toBlocks₁₁.toMatrix A = (D.toMatrix A).toBlocks₁₁

Materializing a descriptor's top-left quadrant is matrix block extraction.

theorem Hex.Matrix.Region.toMatrix_toBlocks₁₂ {R : Type u} {N M h w : Nat} (D : Region N M (h + h) (w + w)) (A : Matrix R N M) : D.toBlocks₁₂.toMatrix A = (D.toMatrix A).toBlocks₁₂

Materializing a descriptor's top-right quadrant is matrix block extraction.

theorem Hex.Matrix.Region.toMatrix_toBlocks₂₁ {R : Type u} {N M h w : Nat} (D : Region N M (h + h) (w + w)) (A : Matrix R N M) : D.toBlocks₂₁.toMatrix A = (D.toMatrix A).toBlocks₂₁

Materializing a descriptor's bottom-left quadrant is matrix block extraction.

theorem Hex.Matrix.Region.toMatrix_toBlocks₂₂ {R : Type u} {N M h w : Nat} (D : Region N M (h + h) (w + w)) (A : Matrix R N M) : D.toBlocks₂₂.toMatrix A = (D.toMatrix A).toBlocks₂₂

Materializing a descriptor's bottom-right quadrant is matrix block extraction.

theorem Hex.Matrix.Region.disjoint_comm {N M rows cols rows' cols' : Nat} {D : Region N M rows cols} {E : Region N M rows' cols'} : D.Disjoint E ↔ E.Disjoint D

Disjointness of region descriptors is symmetric.

@[inline]

def Hex.Matrix.Region.overwrite {R : Type u} {N M rows cols : Nat} (D : Region N M rows cols) (A : Matrix R N M) (f : Fin rows → Fin cols → R) : Matrix R N M

Fill a destination region from an entry function, threading the destination array directly through its writes.

Equations

• D.overwrite { data := d } f = { data := Fin.foldl rows (fun (d : Vector R (N * M)) (i : Fin rows) => Hex.Matrix.Region.setRowWith✝ D d i (f i)) d }

theorem Hex.Matrix.Region.get_overwrite {R : Type u} {N M rows cols : Nat} (D : Region N M rows cols) (A : Matrix R N M) (f : Fin rows → Fin cols → R) (i : Fin rows) (j : Fin cols) : D.get (D.overwrite A f) i j = f i j

Reading inside an overwritten region returns the supplied entry.

theorem Hex.Matrix.Region.get_overwrite_disjoint {R : Type u} {N M rows cols rows' cols' : Nat} (D : Region N M rows cols) (E : Region N M rows' cols') (h : D.Disjoint E) (A : Matrix R N M) (f : Fin rows → Fin cols → R) (i : Fin rows') (j : Fin cols') : E.get (D.overwrite A f) i j = E.get A i j

Overwriting one region preserves every disjoint region.

@[inline]

def Hex.Matrix.Region.accumulateWith {R : Type u} {N M rows cols : Nat} (D : Region N M rows cols) (A : Matrix R N M) (f : Fin rows → Fin cols → R) (op : R → R → R) : Matrix R N M

Combine a destination region with entries supplied by a read-only function, modifying each destination entry directly.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Hex.Matrix.Region.accumulateExternal {R : Type u} {N M rows cols : Nat} (D : Region N M rows cols) (A : Matrix R N M) (B : Matrix R rows cols) (op : R → R → R) : Matrix R N M

Combine a destination region entrywise with a separate matrix, modifying each destination entry directly.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.Matrix.Region.get_accumulateWith {R : Type u} {N M rows cols : Nat} (D : Region N M rows cols) (A : Matrix R N M) (f : Fin rows → Fin cols → R) (op : R → R → R) (i : Fin rows) (j : Fin cols) : D.get (D.accumulateWith A f op) i j = op (D.get A i j) (f i j)

Reading a region after accumulation with a function returns the entrywise combination.

theorem Hex.Matrix.Region.get_accumulateWith_disjoint {R : Type u} {N M rows cols rows' cols' : Nat} (D : Region N M rows cols) (E : Region N M rows' cols') (h : D.Disjoint E) (A : Matrix R N M) (f : Fin rows → Fin cols → R) (op : R → R → R) (i : Fin rows') (j : Fin cols') : E.get (D.accumulateWith A f op) i j = E.get A i j

Accumulation with a read-only function preserves every disjoint region.

theorem Hex.Matrix.Region.get_accumulateExternal {R : Type u} {N M rows cols : Nat} (D : Region N M rows cols) (A : Matrix R N M) (B : Matrix R rows cols) (op : R → R → R) (i : Fin rows) (j : Fin cols) : D.get (D.accumulateExternal A B op) i j = op (D.get A i j) B[(i, j)]

Reading a region after an external accumulation returns the entrywise combination.

theorem Hex.Matrix.Region.get_accumulateExternal_disjoint {R : Type u} {N M rows cols rows' cols' : Nat} (D : Region N M rows cols) (E : Region N M rows' cols') (h : D.Disjoint E) (A : Matrix R N M) (B : Matrix R rows cols) (op : R → R → R) (i : Fin rows') (j : Fin cols') : E.get (D.accumulateExternal A B op) i j = E.get A i j

Accumulating into one region preserves every disjoint region.

@[inline]

def Hex.Matrix.Region.accumulate {R : Type u} {N M rows cols : Nat} (D S : Region N M rows cols) (_h : D.Disjoint S) (A : Matrix R N M) (op : R → R → R) : Matrix R N M

Combine two disjoint regions of the owned output matrix, writing the first and threading the backing array directly through every entry update.

Equations

• D.accumulate S _h { data := d } op = { data := Fin.foldl rows (fun (d : Vector R (N * M)) (i : Fin rows) => Hex.Matrix.Region.combineRowWith✝ D S d i op) d }

theorem Hex.Matrix.Region.get_accumulate {R : Type u} {N M rows cols : Nat} (D S : Region N M rows cols) (h : D.Disjoint S) (A : Matrix R N M) (op : R → R → R) (i : Fin rows) (j : Fin cols) : D.get (D.accumulate S h A op) i j = op (D.get A i j) (S.get A i j)

Reading the destination of an in-buffer accumulation returns the requested entrywise combination.

theorem Hex.Matrix.Region.get_accumulate_disjoint {R : Type u} {N M rows cols rows' cols' : Nat} (D S : Region N M rows cols) (hDS : D.Disjoint S) (E : Region N M rows' cols') (hDE : D.Disjoint E) (A : Matrix R N M) (op : R → R → R) (i : Fin rows') (j : Fin cols') : E.get (D.accumulate S hDS A op) i j = E.get A i j

In-buffer accumulation writes only its destination region.

theorem Hex.Matrix.Region.toMatrix_overwrite_disjoint {R : Type u} {N M rows cols rows' cols' : Nat} (D : Region N M rows cols) (E : Region N M rows' cols') (h : D.Disjoint E) (A : Matrix R N M) (f : Fin rows → Fin cols → R) : E.toMatrix (D.overwrite A f) = E.toMatrix A

Matrix-level form of get_overwrite_disjoint.

theorem Hex.Matrix.Region.toMatrix_accumulateWith_disjoint {R : Type u} {N M rows cols rows' cols' : Nat} (D : Region N M rows cols) (E : Region N M rows' cols') (h : D.Disjoint E) (A : Matrix R N M) (f : Fin rows → Fin cols → R) (op : R → R → R) : E.toMatrix (D.accumulateWith A f op) = E.toMatrix A

Matrix-level form of get_accumulateWith_disjoint.

theorem Hex.Matrix.Region.toMatrix_accumulateExternal_disjoint {R : Type u} {N M rows cols rows' cols' : Nat} (D : Region N M rows cols) (E : Region N M rows' cols') (h : D.Disjoint E) (A : Matrix R N M) (B : Matrix R rows cols) (op : R → R → R) : E.toMatrix (D.accumulateExternal A B op) = E.toMatrix A

Matrix-level form of get_accumulateExternal_disjoint.

theorem Hex.Matrix.Region.toMatrix_accumulate_disjoint {R : Type u} {N M rows cols rows' cols' : Nat} (D S : Region N M rows cols) (hDS : D.Disjoint S) (E : Region N M rows' cols') (hDE : D.Disjoint E) (A : Matrix R N M) (op : R → R → R) : E.toMatrix (D.accumulate S hDS A op) = E.toMatrix A

Matrix-level form of get_accumulate_disjoint.