internlm/Lean-Github huggingface dataset:
Theorem: Interval.mem_approx_quantize
Proof state before:
case neg.intro
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
simp only [n0, not_false_eq_true, n1, true_and]
Proof state after:
case neg.intro
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Theorem: Interval.mem_approx_quantize
Proof state before:
case neg.intro
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
have mn : c.unquantize ≠ nan := by rw [←hl] at n0; exact (Floating.ne_nan_of_sub n0).1
Proof state after:
case neg.intro
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Theorem: Interval.mem_approx_quantize
Proof state before:
case neg.intro
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
by_cases g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
Proof state after:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

case neg
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : ¬(lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val)
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Theorem: Interval.mem_approx_quantize
Proof state before:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : lo = nan ∨ hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
rcases n with n | n
Proof state after:
case pos.inl
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : lo = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

case pos.inr
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Theorem: Interval.mem_approx_quantize
Proof state before:
case pos.inl
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : lo = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

case pos.inr
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
all_goals simp [n]
Proof state after:
no goals
Theorem: Interval.mem_approx_quantize
Proof state before:
case pos.inr
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
simp [n]
Proof state after:
no goals
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
⊢ c.unquantize ≠ nan
Tactic:
rw [←hl] at n0
Proof state after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬hi = nan
⊢ c.unquantize ≠ nan
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬hi = nan
⊢ c.unquantize ≠ nan
Tactic:
exact (Floating.ne_nan_of_sub n0).1
Proof state after:
no goals
Theorem: Interval.mem_approx_quantize
Proof state before:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
have xn : x ≠ nan := by
  contrapose g
  simp only [ne_eq, not_not] at g
  simp only [g, lo_nan, hi_nan, Floating.val_nan_le, and_true, not_le, ←Floating.val_lt_val]
  exact Floating.nan_lt n0
Proof state after:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Theorem: Interval.mem_approx_quantize
Proof state before:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
simp only [g, and_self, ↓reduceIte, approx_some, approx, Rat.cast_div, Rat.cast_ofNat, mem_Icc,
  tsub_le_iff_right, UInt8.color, add_div]
Proof state after:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Theorem: Interval.mem_approx_quantize
Proof state before:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
simp only [approx, lo_eq_nan, xn, ↓reduceIte, mem_Icc] at xm
Proof state after:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Theorem: Interval.mem_approx_quantize
Proof state before:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
have e : half_color_error.lo.val ≤ color_error / 2 := by
  rw [half_color_error]
  apply lo_le (by native_decide)
  have e : (color_error : ℝ) / 2 = (color_error / 2 : ℚ) := by
    simp only [Rat.cast_div, Rat.cast_ofNat]
  rw [e]; mono
Proof state after:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Theorem: Interval.mem_approx_quantize
Proof state before:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
simp only [←hl, ←hh] at n0 n1 mn g
Proof state after:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
g :
  (c.unquantize.sub half_color_error.lo true).val ≤ x.lo.val ∧
    x.hi.val ≤ (c.unquantize.add half_color_error.lo false).val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Theorem: Interval.mem_approx_quantize
Proof state before:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
g :
  (c.unquantize.sub half_color_error.lo true).val ≤ x.lo.val ∧
    x.hi.val ≤ (c.unquantize.add half_color_error.lo false).val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
have le_lo := Floating.le_sub n0
Proof state after:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
g :
  (c.unquantize.sub half_color_error.lo true).val ≤ x.lo.val ∧
    x.hi.val ≤ (c.unquantize.add half_color_error.lo false).val
le_lo : c.unquantize.val - half_color_error.lo.val ≤ (c.unquantize.sub half_color_error.lo true).val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Theorem: Interval.mem_approx_quantize
Proof state before:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
g :
  (c.unquantize.sub half_color_error.lo true).val ≤ x.lo.val ∧
    x.hi.val ≤ (c.unquantize.add half_color_error.lo false).val
le_lo : c.unquantize.val - half_color_error.lo.val ≤ (c.unquantize.sub half_color_error.lo true).val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
have le_hi := Floating.add_le n1
Proof state after:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
g :
  (c.unquantize.sub half_color_error.lo true).val ≤ x.lo.val ∧
    x.hi.val ≤ (c.unquantize.add half_color_error.lo false).val
le_lo : c.unquantize.val - half_color_error.lo.val ≤ (c.unquantize.sub half_color_error.lo true).val
le_hi : (c.unquantize.add half_color_error.lo false).val ≤ c.unquantize.val + half_color_error.lo.val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Theorem: Interval.mem_approx_quantize
Proof state before:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
g :
  (c.unquantize.sub half_color_error.lo true).val ≤ x.lo.val ∧
    x.hi.val ≤ (c.unquantize.add half_color_error.lo false).val
le_lo : c.unquantize.val - half_color_error.lo.val ≤ (c.unquantize.sub half_color_error.lo true).val
le_hi : (c.unquantize.add half_color_error.lo false).val ≤ c.unquantize.val + half_color_error.lo.val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
simp only [UInt8.val_unquantize mn, hl, tsub_le_iff_right, hh, hl, hh] at le_lo le_hi g ⊢
Proof state after:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
le_lo : ↑c.toNat / 256 + 1 / 512 ≤ lo.val + half_color_error.lo.val
le_hi : hi.val ≤ ↑c.toNat / 256 + 1 / 512 + half_color_error.lo.val
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Theorem: Interval.mem_approx_quantize
Proof state before:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
le_lo : ↑c.toNat / 256 + 1 / 512 ≤ lo.val + half_color_error.lo.val
le_hi : hi.val ≤ ↑c.toNat / 256 + 1 / 512 + half_color_error.lo.val
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
exact ⟨by linarith, by linarith⟩
Proof state after:
no goals
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
⊢ x ≠ nan
Tactic:
contrapose g
Proof state after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : ¬x ≠ nan
⊢ ¬(lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val)
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : ¬x ≠ nan
⊢ ¬(lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val)
Tactic:
simp only [ne_eq, not_not] at g
Proof state after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : x = nan
⊢ ¬(lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val)
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : x = nan
⊢ ¬(lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val)
Tactic:
simp only [g, lo_nan, hi_nan, Floating.val_nan_le, and_true, not_le, ←Floating.val_lt_val]
Proof state after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : x = nan
⊢ nan < lo
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : x = nan
⊢ nan < lo
Tactic:
exact Floating.nan_lt n0
Proof state after:
no goals
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ half_color_error.lo.val ≤ ↑color_error / 2
Tactic:
rw [half_color_error]
Proof state after:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ (ofRat (color_error / 2)).lo.val ≤ ↑color_error / 2
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ (ofRat (color_error / 2)).lo.val ≤ ↑color_error / 2
Tactic:
apply lo_le (by native_decide)
Proof state after:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ ↑color_error / 2 ∈ approx (ofRat (color_error / 2))