internlm/Lean-Github huggingface dataset:
Theorem: Array.pmap_eq_nat_fold'_push
Proof state before:
case succ.h.h
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
k : Nat
IH :
  ∀ (hk : k ≤ size as) (bs : Array β),
    pmapM.map f as h (size as - k) bs =
      Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) k hk bs
hk : Nat.succ k ≤ size as
bs : Array β
⊢ size as - Nat.succ k + 1 = size as - k
Tactic:
rewrite [← Nat.sub_add_comm hk]
Proof state after:
case succ.h.h
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
k : Nat
IH :
  ∀ (hk : k ≤ size as) (bs : Array β),
    pmapM.map f as h (size as - k) bs =
      Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) k hk bs
hk : Nat.succ k ≤ size as
bs : Array β
⊢ size as + 1 - Nat.succ k = size as - k
Theorem: Array.pmap_eq_nat_fold'_push
Proof state before:
case succ.h.h
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
k : Nat
IH :
  ∀ (hk : k ≤ size as) (bs : Array β),
    pmapM.map f as h (size as - k) bs =
      Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) k hk bs
hk : Nat.succ k ≤ size as
bs : Array β
⊢ size as + 1 - Nat.succ k = size as - k
Tactic:
exact Nat.succ_sub_succ_eq_sub as.size k
Proof state after:
no goals
Theorem: Array.size_pmap
Proof state before:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ size (pmap f as h) = size as
Tactic:
rewrite [pmap_eq_nat_fold'_push]
Proof state after:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ size (Nat.fold' (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) #[]) = size as
Theorem: Array.size_pmap
Proof state before:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ size (Nat.fold' (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) #[]) = size as
Tactic:
refine Nat.fold'_induction (motive := fun k (x : Array β) => x.size = k) as.size _ #[] rfl ?_
Proof 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 as) (a : Array β),
    (fun k x => size x = k) i a →
      (fun k x => size x = k) (i + 1)
        (push a (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val])))
Theorem: Array.size_pmap
Proof 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 as) (a : Array β),
    (fun k x => size x = k) i a →
      (fun k x => size x = k) (i + 1)
        (push a (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val])))
Tactic:
intro i hi x hx
Proof 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 as
x : Array β
hx : size x = i
⊢ size (push x (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val]))) = i + 1
Theorem: Array.size_pmap
Proof 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 as
x : Array β
hx : size x = i
⊢ size (push x (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val]))) = i + 1
Tactic:
simp only [size_push, hx]
Proof state after:
no goals
Theorem: Array.getElem_pop
Proof state before:
α : Type u
as : Array α
i : Nat
hi : i < size (pop as)
⊢ (pop as)[i] = as[i]
Tactic:
dsimp [pop]
Proof state after:
α : Type u
as : Array α
i : Nat
hi : i < size (pop as)
⊢ { data := List.dropLast as.data }[i] = as[i]
Theorem: Array.getElem_pop
Proof state before:
α : Type u
as : Array α
i : Nat
hi : i < size (pop as)
⊢ { data := List.dropLast as.data }[i] = as[i]
Tactic:
simp only [getElem_eq_data_get, List.dropLast_eq_take, List.get_take]
Proof state after:
α : Type u
as : Array α
i : Nat
hi : i < size (pop as)
⊢ List.get (List.take (List.length as.data - 1) as.data)
      { val := i, isLt := (_ : (fun xs i => i < size xs) { data := List.take (List.length as.data - 1) as.data } i) } =
    List.get as.data { val := i, isLt := (_ : i < size as) }
Theorem: Array.getElem_pop
Proof state before:
α : Type u
as : Array α
i : Nat
hi : i < size (pop as)
⊢ List.get (List.take (List.length as.data - 1) as.data)
      { val := i, isLt := (_ : (fun xs i => i < size xs) { data := List.take (List.length as.data - 1) as.data } i) } =
    List.get as.data { val := i, isLt := (_ : i < size as) }
Tactic:
exact as.data.get_take _ i
Proof state after:
no goals
Theorem: Array.getElem_swap
Proof state before:
α : Type u
as : Array α
i j : Fin (size as)
k : Nat
hk : k < size (swap as i j)
⊢ (swap as i j)[k] = if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]
Tactic:
have : ∀ {m n : Nat} (h : m = n) (i : Fin m), ((h ▸ i) : Fin n).val = i.val :=
  @fun
  | _, _, rfl, _ => rfl
Proof state after:
α : Type u
as : Array α
i j : Fin (size as)
k : Nat
hk : k < size (swap as i j)
this : ∀ {m n : Nat} (h : m = n) (i : Fin m), (h ▸ i).val = i.val
⊢ (swap as i j)[k] = if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]
Theorem: Array.getElem_swap
Proof state before:
α : Type u
as : Array α
i j : Fin (size as)
k : Nat
hk : k < size (swap as i j)
this : ∀ {m n : Nat} (h : m = n) (i : Fin m), (h ▸ i).val = i.val
⊢ (swap as i j)[k] = if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]
Tactic:
simp [swap, getElem_eq_data_get, List.get_set, this]
Proof state after:
no goals
Theorem: Array.getElem_append_left
Proof state before:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ (as ++ bs)[i] = as[i]
Tactic:
rewrite [getElem_eq_data_get]
Proof state after:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ List.get (as ++ bs).data { val := i, isLt := h' } = as[i]
Theorem: Array.getElem_append_left
Proof state before:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ List.get (as ++ bs).data { val := i, isLt := h' } = as[i]
Tactic:
rewrite [List.get_of_eq (Array.append_data as bs)]
Proof state after:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ List.get (as.data ++ bs.data)
      { val := { val := i, isLt := h' }.val,
        isLt := (_ : { val := i, isLt := h' }.val < List.length (as.data ++ bs.data)) } =
    as[i]
Theorem: Array.getElem_append_left
Proof state before:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ List.get (as.data ++ bs.data)
      { val := { val := i, isLt := h' }.val,
        isLt := (_ : { val := i, isLt := h' }.val < List.length (as.data ++ bs.data)) } =
    as[i]
Tactic:
rewrite [List.get_append_left as.data bs.data h]
Proof state after:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ List.get as.data { val := i, isLt := h } = as[i]
Theorem: Array.getElem_append_left
Proof state before:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ List.get as.data { val := i, isLt := h } = as[i]
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.getElem_append_right
Proof state before:
α : Type u
i : Nat
as bs : Array α
h : i ≥ size as
h' : i < size (as ++ bs)
⊢ (as ++ bs)[i] = bs[i - size as]
Tactic:
rewrite [getElem_eq_data_get]
Proof state after:
α : Type u
i : Nat
as bs : Array α
h : i ≥ size as
h' : i < size (as ++ bs)
⊢ List.get (as ++ bs).data { val := i, isLt := h' } = bs[i - size as]
Theorem: Array.getElem_append_right
Proof state before:
α : Type u
i : Nat
as bs : Array α
h : i ≥ size as
h' : i < size (as ++ bs)
⊢ List.get (as ++ bs).data { val := i, isLt := h' } = bs[i - size as]
Tactic:
rewrite [List.get_of_eq (Array.append_data as bs)]
Proof state after:
α : Type u
i : Nat
as bs : Array α
h : i ≥ size as
h' : i < size (as ++ bs)
⊢ List.get (as.data ++ bs.data)
      { val := { val := i, isLt := h' }.val,
        isLt := (_ : { val := i, isLt := h' }.val < List.length (as.data ++ bs.data)) } =
    bs[i - size as]
Theorem: Array.getElem_append_right
Proof state before:
α : Type u
i : Nat
as bs : Array α
h : i ≥ size as
h' : i < size (as ++ bs)
⊢ List.get (as.data ++ bs.data)
      { val := { val := i, isLt := h' }.val,
        isLt := (_ : { val := i, isLt := h' }.val < List.length (as.data ++ bs.data)) } =
    bs[i - size as]
Tactic:
rewrite [List.get_append_right' h]
Proof state after:
α : Type u
i : Nat
as bs : Array α
h : i ≥ size as
h' : i < size (as ++ bs)
⊢ List.get bs.data { val := i - List.length as.data, isLt := (_ : i - List.length as.data < List.length bs.data) } =
    bs[i - size as]
Theorem: Array.getElem_append_right
Proof state before:
α : Type u
i : Nat
as bs : Array α
h : i ≥ size as
h' : i < size (as ++ bs)
⊢ List.get bs.data { val := i - List.length as.data, isLt := (_ : i - List.length as.data < List.length bs.data) } =
    bs[i - size as]
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.getElem_shrink
Proof state before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
i : Nat
hi : i < size (shrink as n)
⊢ (shrink as n)[i] = as[i]
Tactic:
dsimp [shrink] at hi ⊢
Proof state after:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
i : Nat
hi : i < size (shrink.loop (size as - n) as)
⊢ (shrink.loop (size as - n) as)[i] = as[i]
Theorem: Array.getElem_shrink
Proof state before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
i : Nat
hi : i < size (shrink.loop (size as - n) as)
⊢ (shrink.loop (size as - n) as)[i] = as[i]
Tactic:
revert i
Proof state after:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ ∀ (i : Nat) (hi : i < size (shrink.loop (size as - n) as)), (shrink.loop (size as - n) as)[i] = as[i]
Theorem: Array.getElem_shrink
Proof state before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ ∀ (i : Nat) (hi : i < size (shrink.loop (size as - n) as)), (shrink.loop (size as - n) as)[i] = as[i]
Tactic:
suffices ∀ (i k : Nat) (hk : k ≤ as.size) (hi : i < as.size - k), (shrink.loop k as)[i]'(as.size_shrink_loop hk ▸ hi) = as[i]'(trans (r:=LT.lt (α:=Nat)) hi (as.size.sub_le_self k))
from fun i hi =>
  this i (as.size - n) (as.size.sub_le_self n) (by rw [Nat.sub_sub_self h]; exact trans (r:=LT.lt (α:=Nat)) (s:=Eq) hi (as.size_shrink h))
Proof state after:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
Theorem: Array.getElem_shrink
Proof state before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
Tactic:
clear h n
Proof state after:
α : Type u
as : Array α
⊢ ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
Theorem: Array.getElem_shrink
Proof state before:
α : Type u
as : Array α
⊢ ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
Tactic:
intro i k hk hi
Proof state after:
α : Type u
as : Array α
i k : Nat
hk : k ≤ size as
hi : i < size as - k
⊢ (shrink.loop k as)[i] = as[i]
Theorem: Array.getElem_shrink
Proof state before:
α : Type u
as : Array α
i k : Nat
hk : k ≤ size as
hi : i < size as - k
⊢ (shrink.loop k as)[i] = as[i]
Tactic:
induction k generalizing as with
| zero => rfl
| succ k IH =>
  dsimp [shrink.loop]
  specialize IH as.pop (as.size_pop ▸ Nat.le_sub_of_add_le hk) (by rewrite [as.size_pop, Nat.sub_sub, Nat.add_comm]; exact hi)
  rewrite [IH]
  exact as.getElem_pop i _
Proof state after:
no goals
Theorem: Array.getElem_shrink
Proof state before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
this : ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
i : Nat
hi : i < size (shrink.loop (size as - n) as)
⊢ i < size as - (size as - n)
Tactic:
rw [Nat.sub_sub_self h]
Proof state after:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
this : ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
i : Nat
hi : i < size (shrink.loop (size as - n) as)
⊢ i < n
Theorem: Array.getElem_shrink
Proof state before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
this : ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
i : Nat
hi : i < size (shrink.loop (size as - n) as)
⊢ i < n
Tactic:
exact trans (r:=LT.lt (α:=Nat)) (s:=Eq) hi (as.size_shrink h)
Proof state after:
no goals
Theorem: Array.getElem_shrink
Proof state before:
case zero
α : Type u
i : Nat
as : Array α
hk : Nat.zero ≤ size as
hi : i < size as - Nat.zero
⊢ (shrink.loop Nat.zero as)[i] = as[i]
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.getElem_shrink
Proof state before:
case succ
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ (shrink.loop (Nat.succ k) as)[i] = as[i]
Tactic:
dsimp [shrink.loop]
Proof state after:
case succ
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ (shrink.loop k (pop as))[i] = as[i]
Theorem: Array.getElem_shrink
Proof state before:
case succ
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ (shrink.loop k (pop as))[i] = as[i]
Tactic:
specialize IH as.pop (as.size_pop ▸ Nat.le_sub_of_add_le hk) (by rewrite [as.size_pop, Nat.sub_sub, Nat.add_comm]; exact hi)
Proof state after:
case succ
α : Type u
i k : Nat
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
IH : (shrink.loop k (pop as))[i] = (pop as)[i]
⊢ (shrink.loop k (pop as))[i] = as[i]
Theorem: Array.getElem_shrink
Proof state before:
case succ
α : Type u
i k : Nat
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
IH : (shrink.loop k (pop as))[i] = (pop as)[i]
⊢ (shrink.loop k (pop as))[i] = as[i]
Tactic:
rewrite [IH]
Proof state after:
case succ
α : Type u
i k : Nat
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
IH : (shrink.loop k (pop as))[i] = (pop as)[i]
⊢ (pop as)[i] = as[i]
Theorem: Array.getElem_shrink
Proof state before:
case succ
α : Type u
i k : Nat
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
IH : (shrink.loop k (pop as))[i] = (pop as)[i]
⊢ (pop as)[i] = as[i]
Tactic:
exact as.getElem_pop i _
Proof state after:
no goals
Theorem: Array.getElem_shrink
Proof state before:
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ i < size (pop as) - k
Tactic:
rewrite [as.size_pop, Nat.sub_sub, Nat.add_comm]
Proof state after:
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ i < size as - (k + 1)
Theorem: Array.getElem_shrink
Proof state before:
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ i < size as - (k + 1)
Tactic:
exact hi
Proof state after:
no goals
Theorem: Array.getElem_pmap
Proof 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]
Proof 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])
Theorem: Array.getElem_pmap
Proof 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)
Proof 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])))
Theorem: Array.getElem_pmap
Proof 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
Proof 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])))
Theorem: Array.getElem_pmap
Proof 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
Proof state after:
no goals
Theorem: Array.getElem_pmap
Proof 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
Proof 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])
Theorem: Array.getElem_pmap
Proof 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
Proof state after:
no goals
Theorem: Array.getElem_pmap
Proof 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
Proof 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])
Theorem: Array.getElem_pmap
Proof 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 ⊢
Proof 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])