Arithmetic refinement equations

The six *_eq_spec theorems rewrite ExecFloat.add, ExecFloat.sub, ExecFloat.mul, ExecFloat.div, ExecFloat.sqrt, and ExecFloat.fma to the format's reference operations. They follow from the selected capability's refinement proof. The four *_notation_eq_spec theorems state the same equations for left + right, left - right, left * right, and left / right. Rewriting, simp, and grind match terms up to reducible unfolding, and notation elaborates to HAdd.hAdd and its siblings rather than to ExecFloat.add, so both forms are registered. 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. For left + right, use add_notation_eq_spec.

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. For left - right, use sub_notation_eq_spec.

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. For left * right, use mul_notation_eq_spec.

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. For left / right, use div_notation_eq_spec.

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

The notation left + right agrees with reference addition.

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

The notation left - right agrees with reference subtraction.

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

The notation left * right agrees with reference multiplication.

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

The notation left / right agrees with reference division.

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.