Reference · Non-negative rationals

rainbow.math.rational.nnrat.minmax

Non-negative rationalssrc/rainbow/math/rational/nnrat/minmax.clj2 definitions, 6 theorems

General exact-rational min/max with UNIVERSAL (forall-quantified) order guarantees. Unlike the worked-instance selection proofs in the AHoF catalog (which fix concrete operands), these theorems hold for ALL nonnegative-rational operands: min a b = if (a <= b) then a else b max a b = if (a <= b) then b else a Proved for all a, b: min-lower-left : min a b <= a min-lower-right : min a b <= b max-upper-left : a <= max a b max-upper-right : b <= max a b at-most-min : lo <= x -> lo <= y -> lo <= min x y (greatest-lower-bound step) at-most-max : x <= hi -> y <= hi -> max x y <= hi (least-upper-bound step) The proofs case-split on the decidable order via data/Bool.rec with an equality motive, discharging the true branch by nnrat/decide-at-most-true-sound and the false branch by nnrat/decide-at-most-false-reverse -- the standard Rainbow decide case-split. Native and axiom-free.

minmax/min :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

minmax/max :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

minmax/min-lower-left :
  (a b : ℚ≥0)
  → minmax/min a b ≤ a

minmax/min-lower-right :
  (a b : ℚ≥0)
  → minmax/min a b ≤ b

minmax/max-upper-left :
  (a b : ℚ≥0)
  → a ≤ minmax/max a b

minmax/max-upper-right :
  (a b : ℚ≥0)
  → b ≤ minmax/max a b

minmax/at-most-min :
  (lo x y : ℚ≥0)
  (lo-x : lo ≤ x)
  (lo-y : lo ≤ y)
  → lo ≤ minmax/min x y

minmax/at-most-max :
  (x y hi : ℚ≥0)
  (x-hi : x ≤ hi)
  (y-hi : y ≤ hi)
  → minmax/max x y ≤ hi