Theorem: Image.get!_parallel_colors' (Ray/Render/Image.lean)

State before:
f : ℕ → Color UInt8
n o chunk k : ℕ
lt : k < n * 4
⊢ (parallel_colors' f n o chunk).get! k = (f (o + k / 4))[↑k]
Tactic:
have four : ((4 : ℕ) : Fin 4) = 0 := by decide
State after:
f : ℕ → Color UInt8
n o chunk k : ℕ
lt : k < n * 4
four : ↑4 = 0
⊢ (parallel_colors' f n o chunk).get! k = (f (o + k / 4))[↑k]

State before:
f : ℕ → Color UInt8
n o chunk k : ℕ
lt : k < n * 4
four : ↑4 = 0
⊢ (parallel_colors' f n o chunk).get! k = (f (o + k / 4))[↑k]
Tactic:
induction' n using Nat.strong_induction_on with n i generalizing o k
State after:
case h
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
⊢ (parallel_colors' f n o chunk).get! k = (f (o + k / 4))[↑k]

State before:
case h
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
⊢ (parallel_colors' f n o chunk).get! k = (f (o + k / 4))[↑k]
Tactic:
rw [parallel_colors']
State after:
case h
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
        else
          let n0 := n / 2;
          let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
          let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
          t0.get ++ t1.get).get!
      k =
    (f (o + k / 4))[↑k]

State before:
case h
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
        else
          let n0 := n / 2;
          let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
          let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
          t0.get ++ t1.get).get!
      k =
    (f (o + k / 4))[↑k]
Tactic:
by_cases h : n ≤ max 1 chunk
State after:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
        else
          let n0 := n / 2;
          let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
          let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
          t0.get ++ t1.get).get!
      k =
    (f (o + k / 4))[↑k]

case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : ¬n ≤ max 1 chunk
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
        else
          let n0 := n / 2;
          let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
          let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
          t0.get ++ t1.get).get!
      k =
    (f (o + k / 4))[↑k]

State before:
f : ℕ → Color UInt8
n o chunk k : ℕ
lt : k < n * 4
⊢ ↑4 = 0
Tactic:
decide
State after:
no goals

State before:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
        else
          let n0 := n / 2;
          let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
          let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
          t0.get ++ t1.get).get!
      k =
    (f (o + k / 4))[↑k]
Tactic:
simp only [h, if_true, Task.spawn]
State after:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ (push_colors f n o (ByteArray.mkEmpty n)).get! k = (f (o + k / 4))[↑k]

State before:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ (push_colors f n o (ByteArray.mkEmpty n)).get! k = (f (o + k / 4))[↑k]
Tactic:
rw [get!_push_colors]
State after:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ (if k < (ByteArray.mkEmpty n).size then (ByteArray.mkEmpty n).get! k
    else (f (o + (k - (ByteArray.mkEmpty n).size) / 4))[↑(k - (ByteArray.mkEmpty n).size)]) =
    (f (o + k / 4))[↑k]

case pos.lt
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ k < (ByteArray.mkEmpty n).size + n * 4

State before:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ (if k < (ByteArray.mkEmpty n).size then (ByteArray.mkEmpty n).get! k
    else (f (o + (k - (ByteArray.mkEmpty n).size) / 4))[↑(k - (ByteArray.mkEmpty n).size)]) =
    (f (o + k / 4))[↑k]
Tactic:
simp only [ByteArray.size_mkEmpty, not_lt_zero', ↓reduceIte, tsub_zero]
State after:
no goals

State before:
case pos.lt
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ k < (ByteArray.mkEmpty n).size + n * 4
Tactic:
simpa only [ByteArray.size_mkEmpty, zero_add]
State after:
no goals

State before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : ¬n ≤ max 1 chunk
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
        else
          let n0 := n / 2;
          let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
          let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
          t0.get ++ t1.get).get!
      k =
    (f (o + k / 4))[↑k]
Tactic:
simp only [h, if_false, Task.spawn, ByteArray.get!_append, size_parallel_colors']
State after:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : ¬n ≤ max 1 chunk
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]

State before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : ¬n ≤ max 1 chunk
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]
Tactic:
simp only [le_max_iff, not_or, not_le] at h
State after:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]

State before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]
Tactic:
by_cases c : k < n/2 * 4
State after:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : k < n / 2 * 4
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]

case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]

State before:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : k < n / 2 * 4
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]
Tactic:
simp only [c, ↓reduceIte]
State after:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : k < n / 2 * 4
⊢ (parallel_colors' f (n / 2) o chunk).get! k = (f (o + k / 4))[↑k]

State before:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : k < n / 2 * 4
⊢ (parallel_colors' f (n / 2) o chunk).get! k = (f (o + k / 4))[↑k]
Tactic:
rw [i _ (by omega) _ _ (by omega)]
State after:
no goals

State before:
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : k < n / 2 * 4
⊢ n / 2 < n
Tactic:
omega
State after:
no goals

State before:
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : k < n / 2 * 4
⊢ k < n / 2 * 4
Tactic:
omega
State after:
no goals

State before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]
Tactic:
simp only [c, ↓reduceIte]
State after:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4) = (f (o + k / 4))[↑k]

State before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4) = (f (o + k / 4))[↑k]
Tactic:
rw [i]
State after:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ (f (o + n / 2 + (k - n / 2 * 4) / 4))[↑(k - n / 2 * 4)] = (f (o + k / 4))[↑k]

case neg.a
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ n - n / 2 < n

case neg.lt
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ k - n / 2 * 4 < (n - n / 2) * 4

State before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ (f (o + n / 2 + (k - n / 2 * 4) / 4))[↑(k - n / 2 * 4)] = (f (o + k / 4))[↑k]
Tactic:
have ke : o + n / 2 + (k - n / 2 * 4) / 4 = o + k / 4 := by omega
State after:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
ke : o + n / 2 + (k - n / 2 * 4) / 4 = o + k / 4
⊢ (f (o + n / 2 + (k - n / 2 * 4) / 4))[↑(k - n / 2 * 4)] = (f (o + k / 4))[↑k]

State before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
ke : o + n / 2 + (k - n / 2 * 4) / 4 = o + k / 4
⊢ (f (o + n / 2 + (k - n / 2 * 4) / 4))[↑(k - n / 2 * 4)] = (f (o + k / 4))[↑k]
Tactic:
rw [Nat.cast_sub (by omega), Nat.cast_mul, four, mul_zero, sub_zero, ke]
State after:
no goals

State before:
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ o + n / 2 + (k - n / 2 * 4) / 4 = o + k / 4
Tactic:
omega
State after:
no goals

State before:
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
ke : o + n / 2 + (k - n / 2 * 4) / 4 = o + k / 4
⊢ n / 2 * 4 ≤ k
Tactic:
omega
State after:
no goals

State before:
case neg.a
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ n - n / 2 < n
Tactic:
omega
State after:
no goals

State before:
case neg.lt
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ k - n / 2 * 4 < (n - n / 2) * 4
Tactic:
omega
State after:
no goals