floor_abs_intCast

formal source

  55    let z : Int := (coeffSign x) * m
  56    (z : ℝ))
  57
  58lemma floor_abs_intCast (z : Int) : Int.floor (|((z : ℝ))|) = |z| := by
  59  have habs : |((z : ℝ))| = ((|z| : Int) : ℝ) := by
  60    simp
  61  rw [habs]
  62  simpa using (Int.floor_intCast (R := ℝ) (z := |z|))
  63
  64lemma cast_lt_zero_iff {z : Int} : ((z : ℝ) < 0) ↔ z < 0 := by
  65  constructor
  66  · intro hz
  67    by_contra h
  68    have : (0 : Int) ≤ z := le_of_not_gt h
  69    have : (0 : ℝ) ≤ (z : ℝ) := by exact_mod_cast this
  70    exact (not_lt_of_ge this) hz
  71  · intro hz
  72    exact_mod_cast hz
  73
  74lemma clampI32_pos_of_ge_one {x : Int} (hx : 1 ≤ x) : 0 < clampI32 x := by
  75  -- From `x ≥ 1`, the negative-saturation branch is impossible; then either we saturate high,
  76  -- or we return `x` itself. In both cases the result is positive.
  77  have hx0 : (0 : Int) ≤ x := le_trans (by decide : (0 : Int) ≤ 1) hx
  78  have hnot : ¬ x ≤ (-i32Bound) := by
  79    have hi : (-i32Bound : Int) < 0 := by
  80      have : (0 : Int) < i32Bound := by decide
  81      linarith
  82    exact not_le_of_gt (lt_of_lt_of_le hi hx0)
  83  -- Convert `hnot` to the numeral form used by definitional unfolding of `i32Bound`.
  84  have hnot' : ¬ x ≤ (-2147483648 : Int) := by simpa using hnot
  85  dsimp [clampI32]
  86  rw [if_neg hnot']
  87  by_cases h₂ : (2147483648 : Int) ≤ x
  88  · rw [if_pos h₂]