Arithmetic refinement equations

The six *_eq_spec theorems rewrite +, -, *, /, ExecFloat.sqrt, and ExecFloat.fma to the format's reference operations. They apply directly to notation and follow from the selected capability's refinement proof. The equations hold for built-in and user-defined formats under any supported planning policy.

theorem FloatLib.Floats.ExecFloat.Proof.add_eq_spec {F : Type u} [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Add F] (left right : ExecFloat F) : left.add right = Spec.add left right

Executable addition agrees with reference addition; the theorem also applies to left + right.

theorem FloatLib.Floats.ExecFloat.Proof.sub_eq_spec {F : Type u} [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Sub F] (left right : ExecFloat F) : left.sub right = Spec.sub left right

Executable subtraction agrees with reference subtraction; the theorem also applies to left - right.

theorem FloatLib.Floats.ExecFloat.Proof.mul_eq_spec {F : Type u} [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Mul F] (left right : ExecFloat F) : left.mul right = Spec.mul left right

Executable multiplication agrees with reference multiplication; the theorem also applies to left * right.

theorem FloatLib.Floats.ExecFloat.Proof.div_eq_spec {F : Type u} [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Div F] (left right : ExecFloat F) : left.div right = Spec.div left right

Executable division agrees with reference division; the theorem also applies to left / right.

theorem FloatLib.Floats.ExecFloat.Proof.sqrt_eq_spec {F : Type u} [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Sqrt F] (value : ExecFloat F) : value.sqrt = Spec.sqrt value

Executable square root agrees with the format's reference square root.

theorem FloatLib.Floats.ExecFloat.Proof.fma_eq_spec {F : Type u} [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Fma F] (left right addend : ExecFloat F) : left.fma right addend = Spec.fma left right addend

Executable fused multiply-add agrees with the reference operation supplied by its capability.