internlm/Lean-Github huggingface dataset:
Theorem: iterate'_correct
Proof state before:
case pos
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : rs.val < z2.val
⊢ z2.val ≤ Complex.normSq z'
Tactic:
simp only [Complex.normSq_apply, ←sq, ←hz2, ←hzr2, ←hzi2] at z2n ⊢
Proof state after:
case pos
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
⊢ (z.re.sqr.lo.add z.im.sqr.lo false).val ≤ z'.re ^ 2 + z'.im ^ 2
Theorem: iterate'_correct
Proof state before:
case pos
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
⊢ (z.re.sqr.lo.add z.im.sqr.lo false).val ≤ z'.re ^ 2 + z'.im ^ 2
Tactic:
rcases Floating.ne_nan_of_add z2n with ⟨nr, ni⟩
Proof state after:
case pos.intro
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : z.re.sqr.lo ≠ nan
ni : z.im.sqr.lo ≠ nan
⊢ (z.re.sqr.lo.add z.im.sqr.lo false).val ≤ z'.re ^ 2 + z'.im ^ 2
Theorem: iterate'_correct
Proof state before:
case pos.intro
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : z.re.sqr.lo ≠ nan
ni : z.im.sqr.lo ≠ nan
⊢ (z.re.sqr.lo.add z.im.sqr.lo false).val ≤ z'.re ^ 2 + z'.im ^ 2
Tactic:
simp only [ne_eq, Interval.lo_eq_nan] at nr ni
Proof state after:
case pos.intro
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ (z.re.sqr.lo.add z.im.sqr.lo false).val ≤ z'.re ^ 2 + z'.im ^ 2
Theorem: iterate'_correct
Proof state before:
case pos.intro
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ (z.re.sqr.lo.add z.im.sqr.lo false).val ≤ z'.re ^ 2 + z'.im ^ 2
Tactic:
refine le_trans (Floating.add_le z2n) (add_le_add ?_ ?_)
Proof state after:
case pos.intro.refine_1
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z.re.sqr.lo.val ≤ z'.re ^ 2

case pos.intro.refine_2
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z.im.sqr.lo.val ≤ z'.im ^ 2
Theorem: iterate'_correct
Proof state before:
case pos.intro.refine_1
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z.re.sqr.lo.val ≤ z'.re ^ 2
Tactic:
apply Interval.lo_le nr
Proof state after:
case pos.intro.refine_1
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z'.re ^ 2 ∈ approx z.re.sqr
Theorem: iterate'_correct
Proof state before:
case pos.intro.refine_1
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z'.re ^ 2 ∈ approx z.re.sqr
Tactic:
mono
Proof state after:
no goals
Theorem: iterate'_correct
Proof state before:
case pos.intro.refine_2
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z.im.sqr.lo.val ≤ z'.im ^ 2
Tactic:
apply Interval.lo_le ni
Proof state after:
case pos.intro.refine_2
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z'.im ^ 2 ∈ approx z.im.sqr
Theorem: iterate'_correct
Proof state before:
case pos.intro.refine_2
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z'.im ^ 2 ∈ approx z.im.sqr
Tactic:
mono
Proof state after:
no goals
Theorem: iterate'_correct
Proof state before:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
⊢ k ≤
      (if z2 = nan then { z := z, n := k, exit := Exit.nan }
        else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).n ∧
    (f' 2
              c')^[(if z2 = nan then { z := z, n := k, exit := Exit.nan }
                else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).n -
              k]
          z' ∈
        approx
          (if z2 = nan then { z := z, n := k, exit := Exit.nan }
            else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).z ∧
      ((if z2 = nan then { z := z, n := k, exit := Exit.nan }
            else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).exit =
          Exit.large →
        rs' <
          Complex.abs
              ((f' 2
                    c')^[(if z2 = nan then { z := z, n := k, exit := Exit.nan }
                      else
                        if rs.val < z2.val then { z := z, n := k, exit := Exit.large }
                        else iterate' c w rs (k + 1) n).n -
                    k]
                z') ^
            2)
Tactic:
simp only [rz, ite_false, z2n]
Proof state after:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
⊢ k ≤ (iterate' c w rs (k + 1) n).n ∧
    (f' 2 c')^[(iterate' c w rs (k + 1) n).n - k] z' ∈ approx (iterate' c w rs (k + 1) n).z ∧
      ((iterate' c w rs (k + 1) n).exit = Exit.large →
        rs' < Complex.abs ((f' 2 c')^[(iterate' c w rs (k + 1) n).n - k] z') ^ 2)
Theorem: iterate'_correct
Proof state before:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
⊢ k ≤ (iterate' c w rs (k + 1) n).n ∧
    (f' 2 c')^[(iterate' c w rs (k + 1) n).n - k] z' ∈ approx (iterate' c w rs (k + 1) n).z ∧
      ((iterate' c w rs (k + 1) n).exit = Exit.large →
        rs' < Complex.abs ((f' 2 c')^[(iterate' c w rs (k + 1) n).n - k] z') ^ 2)
Tactic:
generalize hi : iterate' c w rs (k + 1) n = i
Proof state after:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
⊢ k ≤ i.n ∧ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Theorem: iterate'_correct
Proof state before:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
⊢ k ≤ i.n ∧ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Tactic:
specialize h wa (k+1)
Proof state after:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  let i := iterate' c w rs (k + 1) n;
  let w' := (f' 2 c')^[i.n - (k + 1)] w';
  k + 1 ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
⊢ k ≤ i.n ∧ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Theorem: iterate'_correct
Proof state before:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  let i := iterate' c w rs (k + 1) n;
  let w' := (f' 2 c')^[i.n - (k + 1)] w';
  k + 1 ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
⊢ k ≤ i.n ∧ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Tactic:
simp only [hi] at h
Proof state after:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
⊢ k ≤ i.n ∧ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Theorem: iterate'_correct
Proof state before:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
⊢ k ≤ i.n ∧ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Tactic:
refine ⟨by omega, ?_⟩
Proof state after:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
⊢ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Theorem: iterate'_correct
Proof state before:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
⊢ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Tactic:
have ie : i.n - k = (i.n - (k + 1)) + 1 := by omega
Proof state after:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
ie : i.n - k = i.n - (k + 1) + 1
⊢ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)