feat: Rounding Proof: Galois Connection [3/?]

Foo.lean

@@ -0,0 +1,39 @@
+theorem concat_truncate_zero_eq_mul_pow2
+    {n : Nat} (x : BitVec n) (tz : Nat) (htz : tz ≤ n) :
+    ((x.truncate (n - tz)) ++ (0#tz) |>.cast (by omega)) = x * (1#n <<< tz) := by
+  ext i
+  simp
+  rw [BitVec.getElem_append]
+  have : 1#n <<< tz = BitVec.twoPow _ tz := by
+    ext i
+    simp
+    by_cases hi : i < tz <;> simp [hi] <;> omega
+  rw [this]
+  rw [← BitVec.shiftLeft_eq_mul_twoPow]
+  rw [BitVec.getElem_shiftLeft]
+  by_cases hi : i < tz 
+  · simp [hi]
+  · simp [hi]
+    rw [BitVec.getLsbD_eq_getElem]
+
+
+/--
+appending 'tz' trailing zeroes to the truncated 'x' is equal to
+multiplying 'x' by 2^tz.
+-/
+theorem extractLsb'_append_zero_eq_mul_shiftLeft {n : Nat}
+    (x : BitVec n) (tz : Nat) (htz : tz ≤ n) :
+    ((x.extractLsb' 0 (n - tz) ++ (0#tz)).cast (by omega))
+      = x * (1#n <<< tz) := by
+  ext i
+  simp only [BitVec.getElem_cast]
+  rw [BitVec.getElem_append]
+  have : 1#n <<< tz = BitVec.twoPow _ tz := by 
+    ext i
+    simp only [BitVec.getElem_shiftLeft, BitVec.getElem_one, BitVec.getElem_twoPow]
+    by_cases hi : i < tz <;> simp [hi] <;> omega
+  rw [this, ← BitVec.shiftLeft_eq_mul_twoPow, BitVec.getElem_shiftLeft]
+  by_cases hi : i < tz
+  · simp [hi]
+  · simp [hi]
+    rw [BitVec.getLsbD_eq_getElem]

Fp/Basic.lean

@@ -59,7 +59,6 @@ instance : Repr (PackedFloat exWidth sigWidth) where
   reprPrec x _prec :=
     f!"\{ sign := {if x.sign then "-" else "+"}, ex := {x.ex}, sig := {x.sig} }"
 
-
 /--
 A fixed point number with specified exponent offset.
 -/
@@ -1091,6 +1090,7 @@ instance : LE ExtRat where
   le a b := le a b
 
 
+
 @[simp]
 theorem le_def {a b : ExtRat} : a.le b = (a ≤ b) := rfl
 
@@ -1403,6 +1403,26 @@ theorem mul_comm (x y : ExtRat) : x * y = y * x := by
 
 end InfinityBehaviour
 
+theorem le_refl (x : ExtRat) : x ≤ x := by
+  rw [← ExtRat.le_def]
+  unfold ExtRat.le
+  grind
+
+theorem le_trans {x y z : ExtRat} (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by
+  rw [← ExtRat.le_def] at hxy hyz ⊢
+  unfold ExtRat.le at hxy hyz ⊢
+  grind
+
+theorem le_antisymm {x y : ExtRat} (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by
+  rw [← ExtRat.le_def] at hxy hyx
+  unfold ExtRat.le at hxy hyx
+  grind
+
+instance : Std.IsPartialOrder ExtRat where
+  le_refl := le_refl
+  le_trans := by grind [le_trans]
+  le_antisymm := by grind [le_antisymm]
+
 
 def isNaN (r : ExtRat) : Bool :=
   r = .NaN
@@ -1428,9 +1448,22 @@ def bias (e : Nat) : Nat :=
 
 namespace PackedFloat
 
+-- | TODO: delete one of mkNaN or getNaN
 def mkNaN (sign := false) (sig := BitVec.intMin s) : PackedFloat e s :=
   { sign, ex := BitVec.allOnes e, sig }
 
+@[simp, grind =]
+theorem sign_mkNaN (sign : Bool) (sig : BitVec s) :
+  (mkNaN sign sig : PackedFloat e s).sign = sign := rfl
+
+@[simp, grind =]
+theorem ex_mkNaN (sign : Bool) (sig : BitVec s) :
+  (mkNaN sign sig : PackedFloat e s).ex = BitVec.allOnes e := rfl
+
+@[simp]
+theorem sig_mkNaN {s e} (sign : Bool) (sig : BitVec s) :
+  (mkNaN sign sig : PackedFloat e s).sig = sig := rfl
+
 def toExtDyadic (pf : PackedFloat e s) : ExtDyadic :=
   bif pf.isNaN then
     .NaN
@@ -1461,6 +1494,48 @@ theorem toExtDyadic_eq_Infinity_of_isInfinite (pf : PackedFloat e s) (hp : pf.is
 def toExtRat (pf : PackedFloat e s) : ExtRat :=
   pf.toExtDyadic.toExtRat
 
+
+/--
+'An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic',
+definition from the model of floating point.
+-/
+def le (x y : PackedFloat e s) : Prop :=
+    (x.isNaN ∧ y.isNaN) ∨
+    (¬ x.isNaN ∧ ¬ y.isNaN ∧
+      (x.sign = true ∧ y.sign = false) ∨ -- x negative, y positive.
+      (x.sign = false ∧ y.sign = false ∧ x.ex.toInt < y.ex.toInt) ∨ -- both +ve, x smaller ex.
+      (x.sign = false ∧ y.sign = false ∧ x.ex = y.ex ∧ x.sig.toNat ≤ y.sig.toNat) ∨ -- both +ve, x smaller sig.
+      (x.sign = true ∧ y.sign = true ∧ y.ex.toInt < x.ex.toInt) ∨ -- both -ve, y smaller ex.
+      (x.sign = true ∧ y.sign = true ∧ x.ex = y.ex ∧ y.sig.toNat ≤ x.sig.toNat)
+    )
+
+instance {x y : PackedFloat e s} : Decidable (le x y) := by
+  simp [le]; infer_instance
+
+instance : LE (PackedFloat exWidth sigWidth) where
+  le x y := le x y
+
+@[simp]
+theorem le_def (x y : PackedFloat e s) :
+  x.le y = (x ≤ y) := rfl
+
+@[simp]
+theorem minus_zero_le_plus_zero {e s} :
+    (PackedFloat.getZero e s true ≤ PackedFloat.getZero e s false) =
+    (e = 0 → s = 0 ∨ ¬s = 0) := by
+  simp [getZero, ← PackedFloat.le_def, PackedFloat.le, PackedFloat.isNaN]
+
+@[simp]
+theorem plus_zero_not_le_minus_zero :
+    (PackedFloat.getZero e s false ≤ PackedFloat.getZero e s true) =
+    (e = 0 ∧ s = 0) := by
+  simp [getZero, ← PackedFloat.le_def, PackedFloat.le, PackedFloat.isNaN]
+
+
+instance {x y : PackedFloat e s} : Decidable (x ≤ y) := by
+    simp only [← PackedFloat.le_def]
+    infer_instance
+
 def toExtRat' (pf : PackedFloat e s) : ExtRat :=
   bif pf.isNaN then
     .NaN
@@ -1474,6 +1549,8 @@ def toExtRat' (pf : PackedFloat e s) : ExtRat :=
     -- `-(bias e - 1)` is slightly different from SMT-LIB standard `1 - bias e` to allow `e = 1`.
     .Number (pf.sign.toSign * (0 + pf.sig.toNat / 2 ^ s) * 2 ^ (-(bias e - 1 : Nat) : Int))
 
+
+
 @[simp]
 theorem toExtRat'_eq_zero_of_isZero (pf : PackedFloat e s) (hp : pf.isZero) :
     pf.toExtRat' = .Number 0 := by
@@ -1562,21 +1639,125 @@ theorem toExtRat'_eq_Number_of_isNormOrNonzeroSubnorm {pf : PackedFloat e s} (hp
   simp [toExtRat', hnan, hinf, hzero, toNumberRat]
   grind
 
-@[simp]
-theorem toExtRat'_mkInfinity (sign : Bool) (hs : 0 < s := by grind) :
+@[simp, grind! .]
+theorem toExtRat'_getInfinity (sign : Bool) (hs : 0 < s := by grind) :
     (PackedFloat.getInfinity e s sign).toExtRat' = .Infinity sign := by
   have : (PackedFloat.getInfinity e s sign).isInfinite = true := by
     grind
   simp [hs]
 
+@[simp, grind! .]
+theorem isNaN_mkNaN : (PackedFloat.mkNaN : PackedFloat e s).isNaN = true := by
+  simp [mkNaN, isNaN]
+  grind
+
 @[simp]
+theorem toExtRat'_mkNaN :
+    (PackedFloat.mkNaN : PackedFloat e s).toExtRat' = .NaN := by
+  rw [toExtRat']
+  simp
+
+@[simp, grind! .]
 axiom toExtRat'_getZero (sign : Bool) (hs : 0 < s := by grind) :
     (PackedFloat.getZero e s sign).toExtRat' = .Number 0 -- := by
   -- have : (PackedFloat.getZero e s sign).isZero = true := by
     -- sorry
   -- simp [this]
     -- grind
 
+/--
+Case splitting on the different values a packed float
+can have: it can be nan, infinity, zero, or a nonzero normal/subnormal.+
+-/
+@[elab_as_elim]
+theorem classification {P : PackedFloat e s → Prop}
+    (x : PackedFloat e s)
+    (nanCase : ∀ (n : PackedFloat e s), n.isNaN → P n)
+    (infCase : ∀ sign, P (PackedFloat.getInfinity e s sign))
+    (zeroCase : ∀ sign, P (PackedFloat.getZero e s sign))
+    (numCase : ∀ (n : PackedFloat e s), n.isNormOrNonzeroSubnorm → P n) :
+    P x := by
+  have := x.classification_exhaustive
+  simp at this
+  by_cases h1 : x.isNaN
+  · grind
+  · by_cases h2 : x.isInfinite
+    · grind
+    · by_cases h3 : x.isZero
+      · grind
+      · by_cases h4 : x.isNonzeroSubnorm
+        · grind
+        · by_cases h5 : x.isNorm
+          · grind
+          · grind
+
+@[simp, grind .]
+theorem PackedFloat.le_refl (x : PackedFloat e s) : x ≤ x := by simp [← PackedFloat.le_def, PackedFloat.le]
+
+theorem PackedFloat.le_NaN (x : PackedFloat e s) (he : 0 < e) (hs : 0 < s):
+    x ≤ PackedFloat.mkNaN ↔ x.isNaN := by
+  -- simp only [← PackedFloat.le_def, PackedFloat.le]
+  -- simp
+  by_cases hx : x.isNaN
+  · simp only [hx, iff_true]
+    simp only [← PackedFloat.le_def, PackedFloat.le, hx]
+    simp only [isNaN_mkNaN, and_self, not_true_eq_false, false_and, false_or, true_or]
+  · simp [hx]
+    simp only [← PackedFloat.le_def, PackedFloat.le]
+    simp [hx]
+    simp [PackedFloat.isNaN] at hx
+    by_cases hs : x.sign
+    · simp [hs]
+    · simp [hs]
+      simp [he]
+      sorry
+
+theorem PackedFloat.NaN_le (x : PackedFloat e s)
+    (he : 0 < e) (hs : 0 < s) : PackedFloat.mkNaN ≤ x ↔ x.isNaN := by
+  simp only [← PackedFloat.le_def, PackedFloat.le, PackedFloat.isNaN]
+  simp only [ex_mkNaN, BEq.rfl, sig_mkNaN, BitVec.zero_eq, Bool.true_and, Bool.or_eq_true,
+    beq_iff_eq, bne_iff_ne, ne_eq, Bool.and_eq_true, not_or,
+    Decidable.not_not, not_and_self, not_and, sign_mkNaN, Bool.false_eq_true, false_and, and_false,
+    and_self, Int.reduceNeg, true_and, BitVec.toNat_intMin, or_self, or_false,
+    false_or]
+  simp [show ¬ s = 0 by grind]
+  by_cases hsign : x.sign
+  · simp [hsign]
+  · simp [hsign]
+    simp [he]
+    intros h
+    sorry
+
+@[simp]
+theorem le_iff_toExtRat_le_toExtRat_of_not_isZero (x y : PackedFloat e s) (hx : ¬ x.isZero) (hy : ¬ y.isZero) :
+  x ≤ y ↔ x.toExtRat ≤ y.toExtRat := sorry
+
+-- recall that -0 ≤ +0. So if x has sign = false, then y also needs sign = false
+@[simp]
+theorem le_iff_sign_eq_of_isZero (x y : PackedFloat e s)
+  (hx : x.isZero) (hy : y.isZero) : x ≤ y ↔ (x.sign = false → y.sign = false) := by
+  sorry
+
+theorem PackedFloat.le_antisymm (he : 0 < e) (hs : 0 < s) {x y : PackedFloat e s}
+  (hxy : x ≤ y) (hyx : y ≤ x) :
+    x = y := by
+  sorry
+  -- grind (splits := 10) [PackedFloat]
+
+theorem PackedFloat.le_trans
+    {x y z : PackedFloat e s} (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by
+  sorry
+
+@[simp]
+theorem le_zero_iff_sign_eq_true {x : PackedFloat e s} :
+    (x ≤ PackedFloat.getZero e s true) ↔ (x.sign = true) := by
+  simp only [PackedFloat.getZero, ← PackedFloat.le_def, PackedFloat.le]
+  sorry
+
+@[simp]
+theorem zero_le_iff_sign_eq_false {x : PackedFloat e s} :
+  (PackedFloat.getZero e s false ≤ x) ↔ (x.sign = false) := by sorry
+
 
 end PackedFloat