chore: correctness of isLawfulLower_Number_getZero_of_underflowNonneg

Fp/Basic.lean

@@ -2271,11 +2271,13 @@ theorem toRatExp_eq_of_isNorm {e s} {pf : PackedFloat e s} (hnorm : pf.isNorm) :
   pf.toRatExp = pf.ex.toNat - bias e := by
   simp [toRatExp, hnorm]
 
--- TODO: Give this definition a better name; It exists
--- to be a nicer version of 'toRat'.
+/-- The rational interpretation of the packed floating point number. -/
 def toRat {e s} (pf : PackedFloat e s) : Rat :=
     pf.sign.toSign * pf.toRatSig * 2 ^ (pf.toRatExp)
 
+/-- Equation lemma for 'toRat'. -/
+theorem toRat_eq {e s} (pf : PackedFloat e s) :
+  pf.toRat = pf.sign.toSign * pf.toRatSig * 2 ^ (pf.toRatExp) := rfl
 
 @[simp]
 theorem toRatExp_neg {pf : PackedFloat e s} :
@@ -2288,6 +2290,7 @@ theorem toRat_neg {e s} (pf : PackedFloat e s) :
   simp [toRat]
   grind only
 
+
 @[simp]
 theorem toRatSig_eq_zero_of_isZero {e s} (pf : PackedFloat e s) (hzero : pf.isZero := by grind) :
   pf.toRatSig = 0 := by
@@ -3293,6 +3296,25 @@ theorem toRat'_neg (uf : UnpackedFloat e s) :
   simp [toRat']
   grind only
 
+/-- `toRat'` is nonnegative when the sign is `false`. -/
+theorem zero_le_toRat'_of_sign_eq_false (x : UnpackedFloat e s) (hsign : x.sign = false) :
+    0 ≤ x.toRat' := by
+  simp [toRat']
+  have : 0 ≤ x.sig.toNat := by grind
+  have : 0 ≤ (2 : Rat) ^ x.toExpInt := by grind
+  simp [hsign]
+  grind only [Rat.mul_nonneg]
+
+/-- `toRat'` is nonpositive when the sign is `true`. -/
+theorem le_zero_toRat'_of_sign_eq_true (x : UnpackedFloat e s) (hsign : x.sign = true) :
+    x.toRat' ≤ 0 := by
+  simp [toRat']
+  have : 0 ≤ x.sig.toNat := by grind
+  have : 0 ≤ (2 : Rat) ^ x.toExpInt := by grind
+  simp [hsign]
+  suffices (0 : Rat) ≤ x.sig.toNat * (2 : Rat) ^ x.toExpInt by grind only
+  grind only [Rat.mul_nonneg]
+
 @[bv_normalize]
 def maxNormal (eout sout : Nat) (e s : Nat) (sign : Bool) :
     UnpackedFloat eout sout :=

Fp/Theorems/LowerUpperRound/Functional.lean

@@ -418,6 +418,7 @@ theorem lsLawfulLower_smtLibLower (e s : Nat) (he : 0 < e) (hs : 0 < s) (r : Ext
   have := IsLawfulLower_lower e s he hs r
   grind only [#de43]
 
+
 /--
 two lawful lowers are equal to each other.
 -/
@@ -740,4 +741,19 @@ info: 'Fp.smtLibUpper_eq_self_of_eq_toExtRat_of_not_isNaN' depends on axioms: [p
 -/
 #guard_msgs in #print axioms smtLibUpper_eq_self_of_eq_toExtRat_of_not_isNaN
 
+
+/-- To show that 'x' is a `IsLawfulLower r`, it suffices to show that it's equal to what `lower` computes. -/
+theorem IsLawfulLower_of_eq_lower
+    (e s : Nat) (r : ExtRat) (x : PackedFloat e s) (he : 0 < e) (hs : 0 < s)
+    (heq : x = lower e s he hs r) : SmtLibSemantics.IsLawfulLower r x := by
+  rw [heq]
+  exact IsLawfulLower_lower e s he hs r
+
+/-- To show that 'x' is a `IsLawfulUpper r`, it suffices to show that it's equal to what `lower` computes. -/
+theorem IsLawfulLower_of_eq_upper
+    (e s : Nat) (r : ExtRat) (x : PackedFloat e s) (he : 0 < e) (hs : 0 < s)
+    (heq : x = upper e s he hs r) : SmtLibSemantics.IsLawfulUpper r x := by
+  rw [heq]
+  exact IsLawfulUpper_upper e s he hs r
+
 end Fp

Fp/Theorems/UnpackedFloat/Round.lean

@@ -505,6 +505,50 @@ theorem UnpackedFloat.normalize_neg_eq_neg_of_normalize_eq (x : UnpackedFloat e
     (-x).normalize = -x := by
   rw [UnpackedFloat.neg_normalize_eq_neg_normalize, hxnorm]
 
+/-# blastIsEvenUpper, blastIsEvenLower -/
+
+theorem blastIsEvenUpper_iff_smtLibIsEven_upper (he : 1 < ep) (hs : 0 < sp) (x : UnpackedFloat e s) :
+  x.blastIsEvenUpper ep sp = true ↔
+    (SmtLibSemantics.smtLibRoundMethod (R := ExtRat) ep sp SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).isEven
+          (SmtLibSemantics.smtLibUpper.upper (ExtRat.Number x.toRat')) = true := by
+  simp [UnpackedFloat.blastIsEvenUpper]
+  simp [SmtLibSemantics.smtLibRoundMethod]
+  sorry
+
+theorem blastIsEvenUpper_eq (he : 1 < ep) (hs : 0 < sp) (x : UnpackedFloat e s) :
+  x.blastIsEvenUpper ep sp = (decide <| (SmtLibSemantics.smtLibRoundMethod (R := ExtRat) ep sp SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).isEven
+          (SmtLibSemantics.smtLibUpper.upper (ExtRat.Number x.toRat'))) := by
+  have := blastIsEvenUpper_iff_smtLibIsEven_upper he hs x
+  grind
+
+theorem blastIsEvenLower_iff_smtLibIsEven_lower (he : 1 < ep) (hs : 0 < sp) (x : UnpackedFloat e s) :
+  x.blastIsEvenLower ep sp = true ↔
+    (SmtLibSemantics.smtLibRoundMethod (R := ExtRat) ep sp SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).isEven
+          (SmtLibSemantics.smtLibLower.lower (ExtRat.Number x.toRat')) = true := by
+  simp [UnpackedFloat.blastIsEvenLower]
+  simp [SmtLibSemantics.smtLibRoundMethod]
+  sorry
+
+theorem blastIsEvenLower_eq (he : 1 < ep) (hs : 0 < sp) (x : UnpackedFloat e s) :
+  x.blastIsEvenLower ep sp = (decide <| (SmtLibSemantics.smtLibRoundMethod (R := ExtRat) ep sp SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).isEven
+          (SmtLibSemantics.smtLibLower.lower (ExtRat.Number x.toRat'))) := by
+  have := blastIsEvenLower_iff_smtLibIsEven_lower he hs x
+  grind
+
+/-# blastIsOverflowNonneg -/
+
+@[simp]
+theorem UnpackedFloat.blastIsEarlyOverflowNonneg_eq_decide  (he : 1 < ep) (hs : 0 < sp)
+    (heu : exponentWidth ep sp ≤ eu)
+    (x : UnpackedFloat eu su) :
+    x.blastIsEarlyOverflowNonneg ep sp = decide (maxNormalExp ep < x.ex.toInt) := by
+  simp [UnpackedFloat.blastIsEarlyOverflowNonneg]
+  rw [BitVec.slt_eq_decide]
+  rw [toInt_ofInt_maxNormalExp_eq_maxNormalExp_of_le (w := eu) he hs]
+  · grind only
+
+
+
 /-# `blastLowerNonneg` matches `lower`
 
 ## Plan
@@ -578,6 +622,32 @@ info: 'Fp.EUnpackedFloat.Rel_smtLibLower_of_witness' depends on axioms: [propext
 -/
 #guard_msgs in #print axioms EUnpackedFloat.Rel_smtLibLower_of_witness
 
+/-# blastIsUnderflowNonneg -/
+
+@[simp]
+theorem UnpackedFloat.blastUnderflowNonneg_eq_decide (he : 1 < ep) (hs : 0 < sp)
+    (heu : exponentWidth ep sp ≤ eu)
+    (x : UnpackedFloat eu su) :
+    x.blastIsUnderflowNonneg ep sp = decide (x.ex.toInt < minSubnormalExp ep sp) := by
+  simp [UnpackedFloat.blastIsUnderflowNonneg]
+  rw [BitVec.slt_eq_decide]
+  rw [toInt_ofInt_minSubnormalExp_eq_minSubnormalExp_of_le (w := eu) he hs]
+  · grind only
+
+/-# blastIsEarlyUnderflowNonneg -/
+
+@[simp]
+theorem UnpackedFloat.blastIsEarlyUnderflowNonneg_eq_decide (he : 1 < ep) (hs : 0 < sp)
+    (heu : exponentWidth ep sp ≤ eu)
+    (x : UnpackedFloat eu su) :
+    x.blastIsEarlyUnderflowNonneg ep sp = decide (x.ex.toInt < minSubnormalExp ep sp - 1) := by
+  simp [UnpackedFloat.blastIsEarlyUnderflowNonneg]
+  rw [BitVec.slt_eq_decide]
+  rw [toInt_ofInt_minSubnormalExp_sub_one_eq_minSubnormalExp_sub_one_of_le (w := eu) he hs]
+  · grind only
+
+
+
 /-! ## Branch (1): underflow
 
 When `x` is positive but smaller in magnitude than the smallest representable
@@ -592,16 +662,67 @@ This is hard: it requires knowing `x.toRat' < (minSubnormal target).toRat`
 and that no negative PF can be `> x`'s value (since `x ≥ 0`).
 -/
 theorem isLawfulLower_Number_getZero_of_underflowNonneg
-    (he : 0 < ep) (hs : 0 < sp)
+    (he : 1 < ep) (hs : 0 < sp)
+    (heu : exponentWidth ep sp ≤ eu)
     (x : UnpackedFloat eu su)
     (hxsign : x.sign = false)
     (hunder : x.blastIsUnderflowNonneg ep sp = true) :
     SmtLibSemantics.IsLawfulLower (ExtRat.Number x.toRat')
       (PackedFloat.getZero ep sp false) := by
-  sorry
+  constructor
+  · -- is a lower bound.
+    simp [hs]
+    rw [PackedFloat.toExtRat'_getZero]
+    simp only [ExtRat.ExtRat.num_le_num_iff, decide_eq_true_eq]
+    -- 0 ≤ x.toRat' because 'x' is nonnegative. (sign = false) and is not nan.
+    apply UnpackedFloat.zero_le_toRat'_of_sign_eq_false
+    · grind only
+  · -- is a greatest lower bound.
+    intros lower' hlower'
+    simp at hlower'
+    apply PackedFloat.le_of_toExtRat'_le_toExtRat'
+    · grind
+    · grind
+    · grind
+    · grind
+    · grind
+    · grind
+    · rw [PackedFloat.toExtRat'_getZero]
+      induction lower' using PackedFloat.classification
+      case nanCase => grind only [= PackedFloat.isNaN_iff_toExtRat'_eq_NaN, = ExtRat.le_NaN]
+      case infCase infsign =>
+        simp [hs, show 0 < ep by grind] at hlower' ⊢
+        grind only
+      case zeroCase zerosign =>
+        simp [hs, show 0 < ep by grind] at hlower' ⊢
+      case numCase y hy =>
+        simp [hs, show 0 < ep by grind] at hlower' ⊢
+        simp [show ¬ y.isNaN by grind]
+        simp [show ¬ y.isZero by grind]
+        apply Classical.byContradiction
+        intros hysign
+        simp at hysign
+        -- y must be zero, since it is strrictly less than y.
+        rw [y.toExtRat'_eq_toRat_of] at hlower'
+        simp at hlower'
+        rw [PackedFloat.toRat_eq] at hlower'
+        simp [hysign] at hlower'
+        rw [UnpackedFloat.blastUnderflowNonneg_eq_decide (he := by grind) (hs := by grind) (heu := by grind)] at hunder
+        simp at hunder
+        rw [UnpackedFloat.toRat'] at hlower'
+        simp [hxsign] at hlower'
+        rw [UnpackedFloat.toExpInt] at hlower'
+        rw [Int.neg_sub] at hlower'
+        rw [Rat.zpow_sub_eq_zpow_mul_zpow] at hlower'
+
+
+
+
 
 theorem UnpackedFloat.blastLowerNonneg_Rel_smtLibLower_underflow
-    (he : 1 < ep) (hs : 0 < sp) (x : UnpackedFloat eu su)
+    (he : 1 < ep) (hs : 0 < sp)
+    (heu : exponentWidth ep sp ≤ eu)
+    (x : UnpackedFloat eu su)
     (hxsign : x.sign = false)
     (hunder : x.blastIsUnderflowNonneg ep sp = true) :
     (EUnpackedFloat.mkNumber (UnpackedFloat.mkZero false) :
@@ -612,7 +733,10 @@ theorem UnpackedFloat.blastLowerNonneg_Rel_smtLibLower_underflow
       (he := by grind) (hs := hs)
   · simp
   · simp; grind only
-  · exact isLawfulLower_Number_getZero_of_underflowNonneg (by grind) hs x hxsign hunder
+  · exact isLawfulLower_Number_getZero_of_underflowNonneg (he := show 1 < ep by grind)
+      (hs := show  0 < sp by grind)
+      (heu := show exponentWidth ep sp ≤ eu by grind)
+      x hxsign hunder
   · -- `(mkZero false).num.toRat' = 0 = (getZero ep sp false).toRat`
     simp only [EUnpackedFloat.num_mkNumber]
     rw [UnpackedFloat.toRat'_mkZero,
@@ -825,7 +949,7 @@ theorem UnpackedFloat.blastLowerNonneg_Rel_smtLibLower (he : 2 < ep) (hsp : 0 <
   unfold UnpackedFloat.blastLowerNonneg
   by_cases hunder : x.blastIsUnderflowNonneg ep sp = true
   · simp [hunder]
-    exact UnpackedFloat.blastLowerNonneg_Rel_smtLibLower_underflow (by grind only) hsp x hxsign hunder
+    exact UnpackedFloat.blastLowerNonneg_Rel_smtLibLower_underflow (he := show 1 < ep by grind) (hs := show 0 < sp by grind) (show exponentWidth ep sp ≤ eu by grind) x hxsign hunder
   · simp only [Bool.not_eq_true] at hunder
     simp [hunder]
     by_cases hover : x.blastIsEarlyOverflowNonneg ep sp = true
@@ -922,72 +1046,6 @@ theorem UnpackedFloat.blastUpper_Rel_smtLibUpper (hep : 2 < ep) (hsp : 0 < sp)
     · grind only
     · simp [hsign]
 
-/-# blastIsEvenUpper, blastIsEvenLower -/
-
-theorem blastIsEvenUpper_iff_smtLibIsEven_upper (he : 1 < ep) (hs : 0 < sp) (x : UnpackedFloat e s) :
-  x.blastIsEvenUpper ep sp = true ↔
-    (SmtLibSemantics.smtLibRoundMethod (R := ExtRat) ep sp SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).isEven
-          (SmtLibSemantics.smtLibUpper.upper (ExtRat.Number x.toRat')) = true := by
-  simp [UnpackedFloat.blastIsEvenUpper]
-  simp [SmtLibSemantics.smtLibRoundMethod]
-  sorry
-
-theorem blastIsEvenUpper_eq (he : 1 < ep) (hs : 0 < sp) (x : UnpackedFloat e s) :
-  x.blastIsEvenUpper ep sp = (decide <| (SmtLibSemantics.smtLibRoundMethod (R := ExtRat) ep sp SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).isEven
-          (SmtLibSemantics.smtLibUpper.upper (ExtRat.Number x.toRat'))) := by
-  have := blastIsEvenUpper_iff_smtLibIsEven_upper he hs x
-  grind
-
-theorem blastIsEvenLower_iff_smtLibIsEven_lower (he : 1 < ep) (hs : 0 < sp) (x : UnpackedFloat e s) :
-  x.blastIsEvenLower ep sp = true ↔
-    (SmtLibSemantics.smtLibRoundMethod (R := ExtRat) ep sp SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).isEven
-          (SmtLibSemantics.smtLibLower.lower (ExtRat.Number x.toRat')) = true := by
-  simp [UnpackedFloat.blastIsEvenLower]
-  simp [SmtLibSemantics.smtLibRoundMethod]
-  sorry
-
-theorem blastIsEvenLower_eq (he : 1 < ep) (hs : 0 < sp) (x : UnpackedFloat e s) :
-  x.blastIsEvenLower ep sp = (decide <| (SmtLibSemantics.smtLibRoundMethod (R := ExtRat) ep sp SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).isEven
-          (SmtLibSemantics.smtLibLower.lower (ExtRat.Number x.toRat'))) := by
-  have := blastIsEvenLower_iff_smtLibIsEven_lower he hs x
-  grind
-
-/-# blastIsOverflowNonneg -/
-
-@[simp]
-theorem UnpackedFloat.blastIsEarlyOverflowNonneg_eq_decide  (he : 1 < ep) (hs : 0 < sp)
-    (heu : exponentWidth ep sp ≤ eu)
-    (x : UnpackedFloat eu su) :
-    x.blastIsEarlyOverflowNonneg ep sp = decide (maxNormalExp ep < x.ex.toInt) := by
-  simp [UnpackedFloat.blastIsEarlyOverflowNonneg]
-  rw [BitVec.slt_eq_decide]
-  rw [toInt_ofInt_maxNormalExp_eq_maxNormalExp_of_le (w := eu) he hs]
-  · grind only
-
-/-# blastIsUnderflowNonneg -/
-
-@[simp]
-theorem UnpackedFloat.blastUnderflowNonneg_eq_decide (he : 1 < ep) (hs : 0 < sp)
-    (heu : exponentWidth ep sp ≤ eu)
-    (x : UnpackedFloat eu su) :
-    x.blastIsUnderflowNonneg ep sp = decide (x.ex.toInt < minSubnormalExp ep sp) := by
-  simp [UnpackedFloat.blastIsUnderflowNonneg]
-  rw [BitVec.slt_eq_decide]
-  rw [toInt_ofInt_minSubnormalExp_eq_minSubnormalExp_of_le (w := eu) he hs]
-  · grind only
-
-/-# blastIsEarlyUnderflowNonneg -/
-
-@[simp]
-theorem UnpackedFloat.blastIsEarlyUnderflowNonneg_eq_decide (he : 1 < ep) (hs : 0 < sp)
-    (heu : exponentWidth ep sp ≤ eu)
-    (x : UnpackedFloat eu su) :
-    x.blastIsEarlyUnderflowNonneg ep sp = decide (x.ex.toInt < minSubnormalExp ep sp - 1) := by
-  simp [UnpackedFloat.blastIsEarlyUnderflowNonneg]
-  rw [BitVec.slt_eq_decide]
-  rw [toInt_ofInt_minSubnormalExp_sub_one_eq_minSubnormalExp_sub_one_of_le (w := eu) he hs]
-  · grind only
-
 /-# blastIsLowerHalf -/
 
 @[simp]

Fp/UnpackedRound.lean

@@ -673,19 +673,19 @@ def UnpackedFloat.blastIsLowerHalf {eu su : Nat} (uf : UnpackedFloat eu su) (tep
     uf.blastIsLowerHalfNonneg tep tsp
 
 @[bv_normalize]
-def UnpackedFloat.blastIsEvenNonneg {eu su : Nat} (uf : UnpackedFloat eu su) (tep tsp : Nat) : Bool :=
+def UnpackedFloat.blastIsEvenLowerNonneg {eu su : Nat} (uf : UnpackedFloat eu su) (tep tsp : Nat) : Bool :=
   uf.blastExtractIsEven tep tsp
 
 @[bv_normalize]
-def UnpackedFloat.blastIsEvenNeg {eu su : Nat} (uf : UnpackedFloat eu su) (tep tsp : Nat) : Bool :=
+def UnpackedFloat.blastIsEvenLowerNeg {eu su : Nat} (uf : UnpackedFloat eu su) (tep tsp : Nat) : Bool :=
   !uf.blastExtractIsEven tep tsp
 
 @[bv_normalize]
-def UnpackedFloat.blastIsEven {eu su : Nat} (uf : UnpackedFloat eu su) (tep tsp : Nat) : Bool :=
+def UnpackedFloat.blastIsEvenLower {eu su : Nat} (uf : UnpackedFloat eu su) (tep tsp : Nat) : Bool :=
   if uf.sign then
-    uf.blastIsEvenNeg tep tsp
+    uf.blastIsEvenLowerNeg tep tsp
   else
-    uf.blastIsEvenNonneg tep tsp
+    uf.blastIsEvenLowerNonneg tep tsp
 
 -- We are in the tie break cast if we are exactly in the middle, *and are also*
 -- in the normal range! If we are outside the normal range, then note that our distance to infinity
@@ -715,14 +715,9 @@ def UnpackedFloat.blastRounderForSign {eu su : Nat} (uf : UnpackedFloat eu su) (
   else
     uf.blastLower tep tsp
 
-
-@[bv_normalize]
-def UnpackedFloat.blastIsEvenLower {eu su : Nat} (uf : UnpackedFloat eu su) (tep tsp : Nat) : Bool :=
-  uf.blastIsEven tep tsp
-
 @[bv_normalize]
 def UnpackedFloat.blastIsEvenUpper {eu su : Nat} (uf : UnpackedFloat eu su) (tep tsp : Nat) : Bool :=
-  !uf.blastIsEven tep tsp
+  !uf.blastIsEvenLower tep tsp
 
 
 @[bv_normalize]