Theorem: Array.getElem_pmap (Fifteen/Data/Array/Basic.lean)

State before:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ (pmap f as h)[i] = f as[i] (_ : p as[i])
Tactic:
simp only [pmap_eq_nat_fold'_push]
State after:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ (Nat.fold' (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) #[])[i] = f as[i] (_ : p as[i])

State before:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ (Nat.fold' (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) #[])[i] = f as[i] (_ : p as[i])
Tactic:
refine Nat.fold'_induction
  (motive := fun (k : Nat) (bs : Array β) => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ as.size) (hbsk : bs.size = k), bs[j]'(hbsk ▸ hjk) = f (as[j]'(trans (r:=LT.lt (α:=Nat)) hjk hk)) (h j (trans (r:=LT.lt (α:=Nat)) hjk hk)))
  as.size _ #[] ?_ ?_ i (as.size_pmap f h ▸ hi) .refl ((as.pmap_eq_nat_fold'_push f h) ▸ as.size_pmap f h)
State after:
case refine_1
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])) 0 #[]

case refine_2
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ ∀ (i : Nat) (hi : i < size as) (a : Array β),
    (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])) i a →
      (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j]))
        (i + 1) (push a (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val])))

State before:
case refine_1
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])) 0 #[]

case refine_2
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ ∀ (i : Nat) (hi : i < size as) (a : Array β),
    (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])) i a →
      (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j]))
        (i + 1) (push a (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val])))
Tactic:
. intro k hk; cases hk
State after:
case refine_2
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ ∀ (i : Nat) (hi : i < size as) (a : Array β),
    (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])) i a →
      (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j]))
        (i + 1) (push a (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val])))

State before:
case refine_2
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ ∀ (i : Nat) (hi : i < size as) (a : Array β),
    (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])) i a →
      (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j]))
        (i + 1) (push a (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val])))
Tactic:
. intro k hk bs IH j hj _ hbsk
  simp only [Array.size_push] at hbsk ⊢
  cases hbsk
  cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hj) with
  | inl heq =>
    cases heq; exact get_push_eq ..
  | inr hlt =>
    rewrite [bs.get_push_lt _ j hlt]
    exact IH j hlt (Nat.le_of_lt hk) rfl
State after:
no goals

State before:
case refine_1
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])) 0 #[]
Tactic:
intro k hk
State after:
case refine_1
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
k : Nat
hk : k < 0
⊢ ∀ (hk_1 : 0 ≤ size as) (hbsk : size #[] = 0), #[][k] = f as[k] (_ : p as[k])

State before:
case refine_1
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
k : Nat
hk : k < 0
⊢ ∀ (hk_1 : 0 ≤ size as) (hbsk : size #[] = 0), #[][k] = f as[k] (_ : p as[k])
Tactic:
cases hk
State after:
no goals

State before:
case refine_2
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ ∀ (i : Nat) (hi : i < size as) (a : Array β),
    (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])) i a →
      (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j]))
        (i + 1) (push a (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val])))
Tactic:
intro k hk bs IH j hj _ hbsk
State after:
case refine_2
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
k : Nat
hk : k < size as
bs : Array β
IH : ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])
j : Nat
hj : j < k + 1
hk✝ : k + 1 ≤ size as
hbsk : size (push bs (f as[{ val := k, isLt := hk }.val] (_ : p as[{ val := k, isLt := hk }.val]))) = k + 1
⊢ (push bs (f as[{ val := k, isLt := hk }.val] (_ : p as[{ val := k, isLt := hk }.val])))[j] = f as[j] (_ : p as[j])

State before:
case refine_2
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
k : Nat
hk : k < size as
bs : Array β
IH : ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])
j : Nat
hj : j < k + 1
hk✝ : k + 1 ≤ size as
hbsk : size (push bs (f as[{ val := k, isLt := hk }.val] (_ : p as[{ val := k, isLt := hk }.val]))) = k + 1
⊢ (push bs (f as[{ val := k, isLt := hk }.val] (_ : p as[{ val := k, isLt := hk }.val])))[j] = f as[j] (_ : p as[j])
Tactic:
simp only [Array.size_push] at hbsk ⊢
State after:
case refine_2
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
k : Nat
hk : k < size as
bs : Array β
IH : ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])
j : Nat
hj : j < k + 1
hk✝ : k + 1 ≤ size as
hbsk✝ : size (push bs (f as[{ val := k, isLt := hk }.val] (_ : p as[{ val := k, isLt := hk }.val]))) = k + 1
hbsk : size bs + 1 = k + 1
⊢ (push bs (f as[k] (_ : p as[{ val := k, isLt := hk }.val])))[j] = f as[j] (_ : p as[j])

State before:
case refine_2
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
k : Nat
hk : k < size as
bs : Array β
IH : ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])
j : Nat
hj : j < k + 1
hk✝ : k + 1 ≤ size as
hbsk✝ : size (push bs (f as[{ val := k, isLt := hk }.val] (_ : p as[{ val := k, isLt := hk }.val]))) = k + 1
hbsk : size bs + 1 = k + 1
⊢ (push bs (f as[k] (_ : p as[{ val := k, isLt := hk }.val])))[j] = f as[j] (_ : p as[j])
Tactic:
cases hbsk
State after:
case refine_2.refl
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
⊢ (push bs (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[j] =
    f as[j] (_ : p as[j])

State before:
case refine_2.refl
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
⊢ (push bs (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[j] =
    f as[j] (_ : p as[j])
Tactic:
cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hj) with
| inl heq =>
  cases heq; exact get_push_eq ..
| inr hlt =>
  rewrite [bs.get_push_lt _ j hlt]
  exact IH j hlt (Nat.le_of_lt hk) rfl
State after:
no goals

State before:
case refine_2.refl.inl
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
heq : j = List.length bs.data
⊢ (push bs (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[j] =
    f as[j] (_ : p as[j])
Tactic:
cases heq
State after:
case refine_2.refl.inl.refl
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
hj : List.length bs.data < List.length bs.data + 1
⊢ (push bs
        (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[List.length bs.data] =
    f as[List.length bs.data] (_ : p as[List.length bs.data])

State before:
case refine_2.refl.inl.refl
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
hj : List.length bs.data < List.length bs.data + 1
⊢ (push bs
        (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[List.length bs.data] =
    f as[List.length bs.data] (_ : p as[List.length bs.data])
Tactic:
exact get_push_eq ..
State after:
no goals

State before:
case refine_2.refl.inr
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
hlt : j < List.length bs.data
⊢ (push bs (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[j] =
    f as[j] (_ : p as[j])
Tactic:
rewrite [bs.get_push_lt _ j hlt]
State after:
case refine_2.refl.inr
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
hlt : j < List.length bs.data
⊢ bs[j] = f as[j] (_ : p as[j])

State before:
case refine_2.refl.inr
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
hlt : j < List.length bs.data
⊢ bs[j] = f as[j] (_ : p as[j])
Tactic:
exact IH j hlt (Nat.le_of_lt hk) rfl
State after:
no goals