[GOAL]
C : FloatCfg
e : ℤ
m : ℕ
⊢ Decidable (ValidFinite e m)
[PROOFSTEP]
unfold ValidFinite
[GOAL]
C : FloatCfg
e : ℤ
m : ℕ
⊢ Decidable (emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size m) - ↑prec) emin)
[PROOFSTEP]
infer_instance
[GOAL]
C : FloatCfg
⊢ emin ≤ emin + ↑prec - 1
[PROOFSTEP]
rw [add_sub_assoc]
[GOAL]
C : FloatCfg
⊢ emin ≤ emin + (↑prec - 1)
[PROOFSTEP]
apply le_add_of_nonneg_right
[GOAL]
case h
C : FloatCfg
⊢ 0 ≤ ↑prec - 1
[PROOFSTEP]
apply sub_nonneg_of_le
[GOAL]
case h.a
C : FloatCfg
⊢ 1 ≤ ↑prec
[PROOFSTEP]
apply Int.ofNat_le_ofNat_of_le
[GOAL]
case h.a.a
C : FloatCfg
⊢ 1 ≤ prec
[PROOFSTEP]
exact C.precPos
[GOAL]
C : FloatCfg
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
C : FloatCfg
this : prec ≤ 2 * emax
⊢ emin + ↑prec - 1 ≤ ↑emax
[PROOFSTEP]
rw [← Int.ofNat_le] at this 
[GOAL]
C : FloatCfg
this : ↑prec ≤ ↑(2 * emax)
⊢ emin + ↑prec - 1 ≤ ↑emax
[PROOFSTEP]
rw [← sub_nonneg] at *
[GOAL]
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * emax)
this : 0 ≤ ↑(2 * emax) - ↑prec
⊢ 0 ≤ ↑emax - (emin + ↑prec - 1)
[PROOFSTEP]
simp only [emin, emax] at *
[GOAL]
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * FloatCfg.emax)
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ ↑FloatCfg.emax - (1 - ↑FloatCfg.emax + ↑prec - 1)
[PROOFSTEP]
ring_nf
[GOAL]
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * FloatCfg.emax)
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ ↑FloatCfg.emax * 2 - ↑prec
[PROOFSTEP]
rw [mul_comm]
[GOAL]
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * FloatCfg.emax)
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ 2 * ↑FloatCfg.emax - ↑prec
[PROOFSTEP]
assumption
[GOAL]
C : FloatCfg
⊢ emin = max (emin + ↑(Nat.size 0) - ↑prec) emin
[PROOFSTEP]
rw [max_eq_right]
[GOAL]
C : FloatCfg
⊢ emin + ↑(Nat.size 0) - ↑prec ≤ emin
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
C : FloatCfg
n d : ℕ+
⊢ Float × Bool
[PROOFSTEP]
let e₁ : ℤ := n.1.size - d.1.size - prec
[GOAL]
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
⊢ Float × Bool
[PROOFSTEP]
cases' h₁ : Int.shift2 d.1 n.1 (e₁ + prec) with d₁ n₁
[GOAL]
case mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
⊢ Float × Bool
[PROOFSTEP]
let e₂ := if n₁ < d₁ then e₁ - 1 else e₁
[GOAL]
case mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
⊢ Float × Bool
[PROOFSTEP]
let e₃ := max e₂ emin
[GOAL]
case mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
⊢ Float × Bool
[PROOFSTEP]
cases' h₂ : Int.shift2 d.1 n.1 (e₃ + prec) with d₂ n₂
[GOAL]
case mk.mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
h₂ : Int.shift2 (↑d) (↑n) (e₃ + ↑prec) = (d₂, n₂)
⊢ Float × Bool
[PROOFSTEP]
let r := mkRat n₂ d₂
[GOAL]
case mk.mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
h₂ : Int.shift2 (↑d) (↑n) (e₃ + ↑prec) = (d₂, n₂)
r : ℚ := mkRat (↑n₂) d₂
⊢ Float × Bool
[PROOFSTEP]
let m := r.floor
[GOAL]
case mk.mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
h₂ : Int.shift2 (↑d) (↑n) (e₃ + ↑prec) = (d₂, n₂)
r : ℚ := mkRat (↑n₂) d₂
m : ℤ := Rat.floor r
⊢ Float × Bool
[PROOFSTEP]
refine' (Float.finite Bool.false e₃ (Int.toNat m) _, r.den = 1)
[GOAL]
case mk.mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
h₂ : Int.shift2 (↑d) (↑n) (e₃ + ↑prec) = (d₂, n₂)
r : ℚ := mkRat (↑n₂) d₂
m : ℤ := Rat.floor r
⊢ ValidFinite e₃ (Int.toNat m)
[PROOFSTEP]
exact lcProof
[GOAL]
C : FloatCfg
e : ℤ
m : ℕ
v : ValidFinite e m
m' : ℕ := Nat.succ m
ss : Nat.size m' = Nat.size m
⊢ ValidFinite e m'
[PROOFSTEP]
unfold ValidFinite at *
[GOAL]
C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size m) - ↑prec) emin
m' : ℕ := Nat.succ m
ss : Nat.size m' = Nat.size m
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size m') - ↑prec) emin
[PROOFSTEP]
rw [ss]
[GOAL]
C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size m) - ↑prec) emin
m' : ℕ := Nat.succ m
ss : Nat.size m' = Nat.size m
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size m) - ↑prec) emin
[PROOFSTEP]
exact v
[GOAL]
C : FloatCfg
e : ℤ
m m' : ℕ
v : ValidFinite e (Nat.succ m')
ss : Nat.size m' = Nat.size (Nat.succ m')
⊢ ValidFinite e m'
[PROOFSTEP]
unfold ValidFinite at *
[GOAL]
C : FloatCfg
e : ℤ
m m' : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size (Nat.succ m')) - ↑prec) emin
ss : Nat.size m' = Nat.size (Nat.succ m')
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size m') - ↑prec) emin
[PROOFSTEP]
rw [ss]
[GOAL]
C : FloatCfg
e : ℤ
m m' : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size (Nat.succ m')) - ↑prec) emin
ss : Nat.size m' = Nat.size (Nat.succ m')
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size (Nat.succ m')) - ↑prec) emin
[PROOFSTEP]
exact v
