Any

Bridge lemmas between the proved typed context (TList) and the runtime tape representation (Runtime.AnyTensor stored in Arrays).

This is part of the explicit trust boundary: the runtime engine operates on erased tensors, while the proved model keeps shapes at the type level.

def Proofs.Autograd.Algebra.TList.toAnyList {α : Type} {ss : List Spec.Shape} : TList α ss → List (Runtime.AnyTensor α)

Convert a typed context (TList) into a runtime list of erased tensors (AnyTensor).

This is part of the “trust boundary” between the proved model (typed shapes) and the runtime engine (erased shape/value pairs).

def Proofs.Autograd.Algebra.TList.toAnyArray {α : Type} {ss : List Spec.Shape} (ts : TList α ss) : Array (Runtime.AnyTensor α)

toAnyList but as an Array (the container used by the runtime tape).

def Proofs.Autograd.Algebra.TList.toIndexedAnyList {α : Type} {ss : List Spec.Shape} : TList α ss → ℕ → List (ℕ × Runtime.AnyTensor α)

Like toAnyList, but tags each element with the absolute runtime node id it should correspond to, starting from start.

theorem Proofs.Autograd.Algebra.TList.mem_toIndexedAnyList_lt {α : Type} {ss : List Spec.Shape} (ts : TList α ss) (start : ℕ) {pid : ℕ} {pg : Runtime.AnyTensor α} : (pid, pg) ∈ ts.toIndexedAnyList start → pid < start + ss.length

Every (pid, tensor) produced by toIndexedAnyList ts start satisfies pid < start + ss.length.

This is bookkeeping used to prove runtime backward only references earlier nodes.

@[simp]

theorem Proofs.Autograd.Algebra.TList.toAnyList_cast {α : Type} {ss₁ ss₂ : List Spec.Shape} (h : ss₁ = ss₂) (xs : TList α ss₁) : (cast h xs).toAnyList = xs.toAnyList

toAnyList ignores type-level casts of the shape list.

This is a convenience lemma for rewriting across reassociation/cast steps in proofs.

@[simp]

theorem Proofs.Autograd.Algebra.TList.toAnyArray_cast {α : Type} {ss₁ ss₂ : List Spec.Shape} (h : ss₁ = ss₂) (xs : TList α ss₁) : (cast h xs).toAnyArray = xs.toAnyArray

toAnyArray ignores type-level casts of the shape list.

This is a direct corollary of toAnyList_cast.

@[simp]

theorem Proofs.Autograd.Algebra.TList.length_toAnyList {α : Type} {ss : List Spec.Shape} (xs : TList α ss) : xs.toAnyList.length = ss.length

toAnyList has the same length as the underlying shape list.

@[simp]

theorem Proofs.Autograd.Algebra.TList.size_toAnyArray {α : Type} {ss : List Spec.Shape} (xs : TList α ss) : xs.toAnyArray.size = ss.length

toAnyArray has the same size as the underlying shape list.

Shape-erasing conversions

The lemmas in this section show that these conversions preserve length/order and interact well with TList.snoc and TList.get. They’re used later to relate runtime node ids to positions in the typed proof context Γ ++ ss.

theorem Proofs.Autograd.Algebra.TList.toAnyList_snoc {α : Type} {ss : List Spec.Shape} {τ : Spec.Shape} (xs : TList α ss) (t : Spec.Tensor α τ) : (xs.snoc t).toAnyList = xs.toAnyList ++ [Runtime.Autograd.AnyTensor.mk t]

toAnyList commutes with appending a value: converting snoc xs t is toAnyList xs ++ [t].

@[simp]

theorem Proofs.Autograd.Algebra.TList.toAnyArray_snoc {α : Type} {ss : List Spec.Shape} {τ : Spec.Shape} (xs : TList α ss) (t : Spec.Tensor α τ) : (xs.snoc t).toAnyArray = xs.toAnyArray.push (Runtime.Autograd.AnyTensor.mk t)

Array-form version of toAnyList_snoc.

theorem Proofs.Autograd.Algebra.TList.toAnyArray_cons {α : Type} {s : Spec.Shape} {ss : List Spec.Shape} (x : Spec.Tensor α s) (xs : TList α ss) : (cons x xs).toAnyArray = #[Runtime.Autograd.AnyTensor.mk x] ++ xs.toAnyArray

toAnyArray of a cons context is array cons/append of the head element.

theorem Proofs.Autograd.Algebra.TList.get_toAnyArray {α : Type} {ss : List Spec.Shape} (xs : TList α ss) (i : Fin ss.length) : let arr := xs.toAnyArray; arr[↑i] = Runtime.Autograd.AnyTensor.mk (xs.get i)

Array lookup through toAnyArray corresponds to TList.get (up to the AnyTensor wrapper).

This is the key lemma that lets us connect runtime indexing (arr[i]) to proof indexing (get xs i).