Proof-indexed finite operations

Application lemmas for finite-operation contracts, including acceptance predicates on input and output codes, such as a floating-point result remaining finite.

Finite1, Finite2, and Finite3 state that running a code-level operation on represented finite inputs produces the specified finite scalar result. This module turns those contracts into the forms users normally need: a denotation equation or a new proof-indexed value.

The If families require a proof of the acceptance predicate for the actual input and output codes. Given that proof and the input denotations, the refinement contract determines the output's finite scalar value.

Unconditional finite-operation contracts

theorem FloatLib.Numerics.Operation.Finite1.ofFinite {CodeA : Type u} {ScalarA : Type v} {CodeB : Type w} {ScalarB : Type x} {decodeA : CodeA → ScalarA} {decodeB : CodeB → ScalarB} {run : CodeA → CodeB} {spec : ScalarA → ScalarB} (correct : ∀ (code : CodeA), decodeB (run code) = spec (decodeA code)) : Finite1 (NumericalSystem.ofFinite decodeA) (NumericalSystem.ofFinite decodeB) run spec

Lift a commuting decoder equation to a finite unary-operation refinement.

This is the standard proof principle for formats whose codes all denote ordinary finite values.

theorem FloatLib.Numerics.Operation.Finite1.denote {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → B.Code} {spec : A.Scalar → B.Scalar} (hrefines : Finite1 A B run spec) {code : A.Code} {value : A.Scalar} (hcode : A.Represents code value) : B.denote (run code) = NumericalValue.finite (spec value)

Apply a finite unary refinement to a represented concrete input.

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

Observe a finite unary operation with an independently stated scalar result.

@[inline]

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

Apply a finite unary refinement to a proof-indexed finite value.

theorem FloatLib.Numerics.Operation.Finite2.ofFinite {CodeA : Type u} {ScalarA : Type v} {CodeB : Type w} {ScalarB : Type x} {CodeC : Type y} {ScalarC : Type z} {decodeA : CodeA → ScalarA} {decodeB : CodeB → ScalarB} {decodeC : CodeC → ScalarC} {run : CodeA → CodeB → CodeC} {spec : ScalarA → ScalarB → ScalarC} (correct : ∀ (left : CodeA) (right : CodeB), decodeC (run left right) = spec (decodeA left) (decodeB right)) : Finite2 (NumericalSystem.ofFinite decodeA) (NumericalSystem.ofFinite decodeB) (NumericalSystem.ofFinite decodeC) run spec

Lift a commuting two-input decoder equation to a finite binary-operation refinement.

Input and output code types may differ, so this also covers scale-changing operations.

theorem FloatLib.Numerics.Operation.Finite2.denote {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → C.Code} {spec : A.Scalar → B.Scalar → C.Scalar} (hrefines : Finite2 A B C run spec) {left : A.Code} {right : B.Code} {leftValue : A.Scalar} {rightValue : B.Scalar} (hleft : A.Represents left leftValue) (hright : B.Represents right rightValue) : C.denote (run left right) = NumericalValue.finite (spec leftValue rightValue)

Apply a finite two-input refinement to represented concrete inputs.

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

Observe a finite two-input operation with an independently stated scalar result.

The proof-indexed inputs determine both semantic operands before automation selects the operation contract. This prevents independent metavariables for the operands from drifting across proof search branches.

@[inline]

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

Apply a finite two-input refinement to proof-indexed finite values.

theorem FloatLib.Numerics.Operation.Finite3.ofFinite {CodeA : Type u} {ScalarA : Type v} {CodeB : Type w} {ScalarB : Type x} {CodeC : Type y} {ScalarC : Type z} {CodeD : Type u₁} {ScalarD : Type v₁} {decodeA : CodeA → ScalarA} {decodeB : CodeB → ScalarB} {decodeC : CodeC → ScalarC} {decodeD : CodeD → ScalarD} {run : CodeA → CodeB → CodeC → CodeD} {spec : ScalarA → ScalarB → ScalarC → ScalarD} (correct : ∀ (first : CodeA) (second : CodeB) (third : CodeC), decodeD (run first second third) = spec (decodeA first) (decodeB second) (decodeC third)) : Finite3 (NumericalSystem.ofFinite decodeA) (NumericalSystem.ofFinite decodeB) (NumericalSystem.ofFinite decodeC) (NumericalSystem.ofFinite decodeD) run spec

Lift a commuting three-input decoder equation to a finite ternary-operation refinement.

theorem FloatLib.Numerics.Operation.Finite3.denote {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → D.Code} {spec : A.Scalar → B.Scalar → C.Scalar → D.Scalar} (hrefines : Finite3 A B C D run spec) {first : A.Code} {second : B.Code} {third : C.Code} {firstValue : A.Scalar} {secondValue : B.Scalar} {thirdValue : C.Scalar} (hfirst : A.Represents first firstValue) (hsecond : B.Represents second secondValue) (hthird : C.Represents third thirdValue) : D.denote (run first second third) = NumericalValue.finite (spec firstValue secondValue thirdValue)

Apply a finite three-input refinement to represented concrete inputs.

theorem FloatLib.Numerics.Operation.Finite3.denote_eq {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → D.Code} {spec : A.Scalar → B.Scalar → C.Scalar → D.Scalar} {expected : D.Scalar} (hrefines : Finite3 A B C D run spec) {firstValue : A.Scalar} {secondValue : B.Scalar} {thirdValue : C.Scalar} (first : A.AtFinite firstValue) (second : B.AtFinite secondValue) (third : C.AtFinite thirdValue) (hspec : spec firstValue secondValue thirdValue = expected) : D.denote (run first.val second.val third.val) = NumericalValue.finite expected

Observe a finite three-input operation with an independently stated scalar result.

@[inline]

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

Apply a finite three-input refinement to proof-indexed finite values.

Finite-operation contracts with a code-level acceptance condition

theorem FloatLib.Numerics.Operation.Finite1If.denote {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → B.Code} {spec : A.Scalar → B.Scalar} {accept : A.Code → B.Code → Prop} (hrefines : Finite1If A B run spec accept) {code : A.Code} {value : A.Scalar} (hcode : A.Represents code value) (haccept : accept code (run code)) : B.denote (run code) = NumericalValue.finite (spec value)

Apply a condition-aware finite unary refinement to a represented concrete input.

theorem FloatLib.Numerics.Operation.Finite1If.denote_eq {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → B.Code} {spec : A.Scalar → B.Scalar} {accept : A.Code → B.Code → Prop} {expected : B.Scalar} (hrefines : Finite1If A B run spec accept) {value : A.Scalar} (code : A.AtFinite value) (haccept : accept code.val (run code.val)) (hspec : spec value = expected) : B.denote (run code.val) = NumericalValue.finite expected

Observe a condition-aware finite unary operation with an independently stated result.

@[inline]

def FloatLib.Numerics.Operation.Finite1If.applyAt {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → B.Code} {spec : A.Scalar → B.Scalar} {accept : A.Code → B.Code → Prop} (hrefines : Finite1If A B run spec accept) {value : A.Scalar} (code : A.AtFinite value) (haccept : accept code.val (run code.val)) : B.AtFinite (spec value)

Apply a condition-aware finite unary refinement to a proof-indexed value.

theorem FloatLib.Numerics.Operation.Finite2If.denote {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → C.Code} {spec : A.Scalar → B.Scalar → C.Scalar} {accept : A.Code → B.Code → C.Code → Prop} (hrefines : Finite2If A B C run spec accept) {left : A.Code} {right : B.Code} {leftValue : A.Scalar} {rightValue : B.Scalar} (hleft : A.Represents left leftValue) (hright : B.Represents right rightValue) (haccept : accept left right (run left right)) : C.denote (run left right) = NumericalValue.finite (spec leftValue rightValue)

Apply a condition-aware finite two-input refinement to represented concrete inputs.

theorem FloatLib.Numerics.Operation.Finite2If.denote_eq {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → C.Code} {spec : A.Scalar → B.Scalar → C.Scalar} {accept : A.Code → B.Code → C.Code → Prop} {expected : C.Scalar} (hrefines : Finite2If A B C run spec accept) {leftValue : A.Scalar} {rightValue : B.Scalar} (left : A.AtFinite leftValue) (right : B.AtFinite rightValue) (haccept : accept left.val right.val (run left.val right.val)) (hspec : spec leftValue rightValue = expected) : C.denote (run left.val right.val) = NumericalValue.finite expected

Observe a condition-aware finite two-input operation with an independently stated result.

@[inline]

def FloatLib.Numerics.Operation.Finite2If.applyAt {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → C.Code} {spec : A.Scalar → B.Scalar → C.Scalar} {accept : A.Code → B.Code → C.Code → Prop} (hrefines : Finite2If A B C run spec accept) {leftValue : A.Scalar} {rightValue : B.Scalar} (left : A.AtFinite leftValue) (right : B.AtFinite rightValue) (haccept : accept left.val right.val (run left.val right.val)) : C.AtFinite (spec leftValue rightValue)

Apply a condition-aware finite two-input refinement to proof-indexed values.

theorem FloatLib.Numerics.Operation.Finite3If.denote {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → D.Code} {spec : A.Scalar → B.Scalar → C.Scalar → D.Scalar} {accept : A.Code → B.Code → C.Code → D.Code → Prop} (hrefines : Finite3If A B C D run spec accept) {first : A.Code} {second : B.Code} {third : C.Code} {firstValue : A.Scalar} {secondValue : B.Scalar} {thirdValue : C.Scalar} (hfirst : A.Represents first firstValue) (hsecond : B.Represents second secondValue) (hthird : C.Represents third thirdValue) (haccept : accept first second third (run first second third)) : D.denote (run first second third) = NumericalValue.finite (spec firstValue secondValue thirdValue)

Apply a condition-aware finite three-input refinement to represented concrete inputs.

theorem FloatLib.Numerics.Operation.Finite3If.denote_eq {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → D.Code} {spec : A.Scalar → B.Scalar → C.Scalar → D.Scalar} {accept : A.Code → B.Code → C.Code → D.Code → Prop} {expected : D.Scalar} (hrefines : Finite3If A B C D run spec accept) {firstValue : A.Scalar} {secondValue : B.Scalar} {thirdValue : C.Scalar} (first : A.AtFinite firstValue) (second : B.AtFinite secondValue) (third : C.AtFinite thirdValue) (haccept : accept first.val second.val third.val (run first.val second.val third.val)) (hspec : spec firstValue secondValue thirdValue = expected) : D.denote (run first.val second.val third.val) = NumericalValue.finite expected

Observe a condition-aware finite three-input operation with an independent result.

@[inline]

def FloatLib.Numerics.Operation.Finite3If.applyAt {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → D.Code} {spec : A.Scalar → B.Scalar → C.Scalar → D.Scalar} {accept : A.Code → B.Code → C.Code → D.Code → Prop} (hrefines : Finite3If A B C D run spec accept) {firstValue : A.Scalar} {secondValue : B.Scalar} {thirdValue : C.Scalar} (first : A.AtFinite firstValue) (second : B.AtFinite secondValue) (third : C.AtFinite thirdValue) (haccept : accept first.val second.val third.val (run first.val second.val third.val)) : D.AtFinite (spec firstValue secondValue thirdValue)

Apply a condition-aware finite three-input refinement to proof-indexed values.