Proof-indexed total operations

Total1, Total2, and Total3 describe operations whose semantics cover every encoded input, including exceptional numerical values. This file supplies the uniform ways to apply those contracts either to raw codes or to proof-indexed values.

The helpers are intentionally regular across arities. Generic automation can expose a denotation, rewrite it to an independently stated result, or run the same executable function while retaining its semantic index. Format families therefore do not need local copies of these proof bridges.

theorem FloatLib.Numerics.Operation.Total1.denote {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → B.Code} {spec : NumericalValue A.Scalar → NumericalValue B.Scalar} (hrefines : Total1 A B run spec) (code : A.Code) : B.denote (run code) = spec (A.denote code)

Apply a total unary refinement to a concrete input.

theorem FloatLib.Numerics.Operation.Total1.denote_eq {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → B.Code} {spec : NumericalValue A.Scalar → NumericalValue B.Scalar} {expected : NumericalValue B.Scalar} (hrefines : Total1 A B run spec) (code : A.Code) (hspec : spec (A.denote code) = expected) : B.denote (run code) = expected

Apply a total unary refinement while leaving the displayed result independent of the contract's chosen specification. This is the stable shape used by generic automation.

@[inline]

def FloatLib.Numerics.Operation.Total1.applyAt {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → B.Code} {spec : NumericalValue A.Scalar → NumericalValue B.Scalar} (hrefines : Total1 A B run spec) {value : NumericalValue A.Scalar} (code : A.At value) : B.At (spec value)

Apply a total unary refinement to a proof-indexed complete value.

theorem FloatLib.Numerics.Operation.Total2.denote {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → C.Code} {spec : NumericalValue A.Scalar → NumericalValue B.Scalar → NumericalValue C.Scalar} (hrefines : Total2 A B C run spec) (left : A.Code) (right : B.Code) : C.denote (run left right) = spec (A.denote left) (B.denote right)

Apply a total two-input refinement to concrete inputs.

theorem FloatLib.Numerics.Operation.Total2.denote_eq {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → C.Code} {spec : NumericalValue A.Scalar → NumericalValue B.Scalar → NumericalValue C.Scalar} {expected : NumericalValue C.Scalar} (hrefines : Total2 A B C run spec) (left : A.Code) (right : B.Code) (hspec : spec (A.denote left) (B.denote right) = expected) : C.denote (run left right) = expected

Apply a total two-input refinement with an independently stated result.

@[inline]

def FloatLib.Numerics.Operation.Total2.applyAt {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → C.Code} {spec : NumericalValue A.Scalar → NumericalValue B.Scalar → NumericalValue C.Scalar} (hrefines : Total2 A B C run spec) {leftValue : NumericalValue A.Scalar} {rightValue : NumericalValue B.Scalar} (left : A.At leftValue) (right : B.At rightValue) : C.At (spec leftValue rightValue)

Apply a total two-input refinement to proof-indexed complete values.

theorem FloatLib.Numerics.Operation.Total3.denote {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → D.Code} {spec : NumericalValue A.Scalar → NumericalValue B.Scalar → NumericalValue C.Scalar → NumericalValue D.Scalar} (hrefines : Total3 A B C D run spec) (first : A.Code) (second : B.Code) (third : C.Code) : D.denote (run first second third) = spec (A.denote first) (B.denote second) (C.denote third)

Apply a total three-input refinement to concrete inputs.

theorem FloatLib.Numerics.Operation.Total3.denote_eq {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → D.Code} {spec : NumericalValue A.Scalar → NumericalValue B.Scalar → NumericalValue C.Scalar → NumericalValue D.Scalar} {expected : NumericalValue D.Scalar} (hrefines : Total3 A B C D run spec) (first : A.Code) (second : B.Code) (third : C.Code) (hspec : spec (A.denote first) (B.denote second) (C.denote third) = expected) : D.denote (run first second third) = expected

Apply a total three-input refinement with an independently stated result.

@[inline]

def FloatLib.Numerics.Operation.Total3.applyAt {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → D.Code} {spec : NumericalValue A.Scalar → NumericalValue B.Scalar → NumericalValue C.Scalar → NumericalValue D.Scalar} (hrefines : Total3 A B C D run spec) {firstValue : NumericalValue A.Scalar} {secondValue : NumericalValue B.Scalar} {thirdValue : NumericalValue C.Scalar} (first : A.At firstValue) (second : B.At secondValue) (third : C.At thirdValue) : D.At (spec firstValue secondValue thirdValue)

Apply a total three-input refinement to proof-indexed complete values.