NF Proof Utilities #
Small proof utilities shared across NF backend approximation modules.
We keep these helpers in a dedicated file so we don’t re-prove the same list-fold facts in every large operator proof (Conv2D, linalg, etc.).
List folds #
foldl_congr is the workhorse for rewriting a foldl step function when the new step is
pointwise equal to the old one.
theorem
Proofs.RuntimeApprox.NFBackend.foldl_congr
{α β : Type}
(l : List β)
(f g : α → β → α)
(init : α)
(h : ∀ (a : α) (b : β), f a b = g a b)
:
Generic facts about approxT #
These lemmas are backend-independent but heavily used in NF backend developments.
theorem
Proofs.RuntimeApprox.NFBackend.approxT_eps_nonneg
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
{rnd : ℝ → ℤ}
{s : Spec.Shape}
{xS : Spec.SpecTensor s}
{xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s}
{eps : ℝ}
(hx : approxT toSpec xS xR eps)
:
theorem
Proofs.RuntimeApprox.NFBackend.approxT_dim_of_forall
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
{rnd : ℝ → ℤ}
{n : ℕ}
{s : Spec.Shape}
{xS : Spec.SpecTensor (Spec.Shape.dim n s)}
{xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim n s)}
{eps : ℝ}
(hε : 0 ≤ eps)
(h :
∀ (i : Fin n),
approxT toSpec
(match xS with
| Spec.Tensor.dim f => f i)
(match xR with
| Spec.Tensor.dim f => f i)
eps)
: