Binary predicate semantics

All predicates use exact extended-real order on non-NaN inputs and their specified unordered truth value on NaNs. The exception theorems distinguish quiet and signaling comparisons without changing their Boolean answers.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Comparison.quiet_value_of_toEReal? {fmt : FloatFormat} (predicate : Predicate) {x y : Model fmt} {a b : EReal} (hx : x.toEReal? = some a) (hy : y.toEReal? = some b) : (quiet predicate x y).value = Numerics.IEEEComparison.Predicate.accepts predicate (some (Ord.compare a b))

Every quiet predicate agrees with its truth table on exact extended-real order.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Comparison.signaling_value_of_toEReal? {fmt : FloatFormat} (predicate : Predicate) {x y : Model fmt} {a b : EReal} (hx : x.toEReal? = some a) (hy : y.toEReal? = some b) : (signaling predicate x y).value = Numerics.IEEEComparison.Predicate.accepts predicate (some (Ord.compare a b))

Every signaling predicate has the same exact numerical truth table.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Comparison.quiet_value_of_nan {fmt : FloatFormat} (predicate : Predicate) (x y : Model fmt) (h : x.isNaN = true ∨ y.isNaN = true) : (quiet predicate x y).value = Numerics.IEEEComparison.Predicate.accepts predicate none

NaN operands select the predicate's unordered truth value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Comparison.signaling_value_of_nan {fmt : FloatFormat} (predicate : Predicate) (x y : Model fmt) (h : x.isNaN = true ∨ y.isNaN = true) : (signaling predicate x y).value = Numerics.IEEEComparison.Predicate.accepts predicate none

Signaling comparison uses the same unordered truth value as quiet comparison.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Comparison.quiet_value_eq_signaling {fmt : FloatFormat} (predicate : Predicate) (x y : Model fmt) : (quiet predicate x y).value = (signaling predicate x y).value

Quiet and signaling comparisons differ only in their exception behavior.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Comparison.quiet_invalid_iff {fmt : FloatFormat} (predicate : Predicate) (x y : Model fmt) : (quiet predicate x y).status.invalid = true ↔ x.isSNaN = true ∨ y.isSNaN = true

Quiet comparisons raise invalid exactly for signaling NaN operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Comparison.signaling_invalid_iff {fmt : FloatFormat} (predicate : Predicate) (x y : Model fmt) : (signaling predicate x y).status.invalid = true ↔ x.isNaN = true ∨ y.isNaN = true

Signaling comparisons raise invalid exactly for NaN operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Comparison.quiet_status {fmt : FloatFormat} (predicate : Predicate) (x y : Model fmt) : (quiet predicate x y).status = { invalid := x.isSNaN || y.isSNaN }

Quiet comparison raises no range, division, or inexact exception.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Comparison.signaling_status {fmt : FloatFormat} (predicate : Predicate) (x y : Model fmt) : (signaling predicate x y).status = { invalid := x.isNaN || y.isNaN }

Signaling comparison raises no range, division, or inexact exception.