internlm/Lean-Github huggingface dataset:
Theorem: Array.any_eq_any_data
Proof state before:
case refine_1
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) j) = List.any (List.drop j as.data) p
Tactic:
unfold anyM.loop
Proof state after:
case refine_1
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
⊢ Id.run
      (if hlt : j < size as then
        let_fun this := (_ : j < size as);
        do
        let __do_lift ← p as[j]
        if __do_lift = true then pure true else anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)
      else pure false) =
    List.any (List.drop j as.data) p
Theorem: Array.any_eq_any_data
Proof state before:
case refine_1
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
⊢ Id.run
      (if hlt : j < size as then
        let_fun this := (_ : j < size as);
        do
        let __do_lift ← p as[j]
        if __do_lift = true then pure true else anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)
      else pure false) =
    List.any (List.drop j as.data) p
Tactic:
dsimp
Proof state after:
case refine_1
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
⊢ Id.run
      (if hlt : j < size as then
        if p as[j] = true then true else anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)
      else false) =
    List.any (List.drop j as.data) p
Theorem: Array.any_eq_any_data
Proof state before:
case refine_1
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
⊢ Id.run
      (if hlt : j < size as then
        if p as[j] = true then true else anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)
      else false) =
    List.any (List.drop j as.data) p
Tactic:
if hlt : j < as.size then
  rewrite [dif_pos hlt, ← List.get_drop_eq_drop _ _ hlt, List.any_cons, List.getElem_eq_get, ← Array.getElem_eq_data_get]
  if hpj : p (as[j]'hlt) = true then
    rewrite [if_pos hpj, hpj, Bool.true_or]
    rfl
  else
    rw [if_neg hpj, IH, Bool.eq_false_iff.mpr hpj, Bool.false_or]
else
  rewrite [dif_neg hlt, List.drop_eq_nil_of_le (Nat.le_of_not_lt hlt)]
  rfl
Proof state after:
no goals
Theorem: Array.any_eq_any_data
Proof state before:
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
hlt : j < size as
⊢ Id.run
      (if hlt : j < size as then
        if p as[j] = true then true else anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)
      else false) =
    List.any (List.drop j as.data) p
Tactic:
rewrite [dif_pos hlt, ← List.get_drop_eq_drop _ _ hlt, List.any_cons, List.getElem_eq_get, ← Array.getElem_eq_data_get]
Proof state after:
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
hlt : j < size as
⊢ Id.run (if p as[j] = true then true else anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) =
    (p as[j] || List.any (List.drop (j + 1) as.data) p)
Theorem: Array.any_eq_any_data
Proof state before:
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
hlt : j < size as
⊢ Id.run (if p as[j] = true then true else anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) =
    (p as[j] || List.any (List.drop (j + 1) as.data) p)
Tactic:
if hpj : p (as[j]'hlt) = true then
  rewrite [if_pos hpj, hpj, Bool.true_or]
  rfl
else
  rw [if_neg hpj, IH, Bool.eq_false_iff.mpr hpj, Bool.false_or]
Proof state after:
no goals
Theorem: Array.any_eq_any_data
Proof state before:
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
hlt : j < size as
hpj : p as[j] = true
⊢ Id.run (if p as[j] = true then true else anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) =
    (p as[j] || List.any (List.drop (j + 1) as.data) p)
Tactic:
rewrite [if_pos hpj, hpj, Bool.true_or]
Proof state after:
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
hlt : j < size as
hpj : p as[j] = true
⊢ Id.run true = true
Theorem: Array.any_eq_any_data
Proof state before:
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
hlt : j < size as
hpj : p as[j] = true
⊢ Id.run true = true
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.any_eq_any_data
Proof state before:
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
hlt : j < size as
hpj : ¬p as[j] = true
⊢ Id.run (if p as[j] = true then true else anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) =
    (p as[j] || List.any (List.drop (j + 1) as.data) p)
Tactic:
rw [if_neg hpj, IH, Bool.eq_false_iff.mpr hpj, Bool.false_or]
Proof state after:
no goals
Theorem: Array.any_eq_any_data
Proof state before:
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
hlt : ¬j < size as
⊢ Id.run
      (if hlt : j < size as then
        if p as[j] = true then true else anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)
      else false) =
    List.any (List.drop j as.data) p
Tactic:
rewrite [dif_neg hlt, List.drop_eq_nil_of_le (Nat.le_of_not_lt hlt)]
Proof state after:
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
hlt : ¬j < size as
⊢ Id.run false = List.any [] p
Theorem: Array.any_eq_any_data
Proof state before:
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
hlt : ¬j < size as
⊢ Id.run false = List.any [] p
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.any_eq_any_data
Proof state before:
case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (size as)) = List.any (List.drop (size as) as.data) p
Tactic:
unfold anyM.loop
Proof state after:
case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run
      (if hlt : size as < size as then
        let_fun this := (_ : size as < size as);
        do
        let __do_lift ← p as[size as]
        if __do_lift = true then pure true else anyM.loop p as (size as) (_ : size as ≤ size as) (size as + 1)
      else pure false) =
    List.any (List.drop (size as) as.data) p
Theorem: Array.any_eq_any_data
Proof state before:
case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run
      (if hlt : size as < size as then
        let_fun this := (_ : size as < size as);
        do
        let __do_lift ← p as[size as]
        if __do_lift = true then pure true else anyM.loop p as (size as) (_ : size as ≤ size as) (size as + 1)
      else pure false) =
    List.any (List.drop (size as) as.data) p
Tactic:
dsimp
Proof state after:
case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run
      (if hlt : size as < size as then
        if p as[size as] = true then true else anyM.loop p as (size as) (_ : size as ≤ size as) (size as + 1)
      else false) =
    List.any (List.drop (size as) as.data) p
Theorem: Array.any_eq_any_data
Proof state before:
case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run
      (if hlt : size as < size as then
        if p as[size as] = true then true else anyM.loop p as (size as) (_ : size as ≤ size as) (size as + 1)
      else false) =
    List.any (List.drop (size as) as.data) p
Tactic:
rewrite [dif_neg (Nat.lt_irrefl _), List.drop_eq_nil_of_le .refl]
Proof state after:
case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run false = List.any [] p
Theorem: Array.any_eq_any_data
Proof state before:
case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run false = List.any [] p
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.swap_comm
Proof state before:
α : Type u
as : Array α
i j : Fin (size as)
⊢ swap as i j = swap as j i
Tactic:
apply Array.ext'
Proof state after:
case h
α : Type u
as : Array α
i j : Fin (size as)
⊢ (swap as i j).data = (swap as j i).data
Theorem: Array.swap_comm
Proof state before:
case h
α : Type u
as : Array α
i j : Fin (size as)
⊢ (swap as i j).data = (swap as j i).data
Tactic:
simp only [Array.data_swap]
Proof state after:
case h
α : Type u
as : Array α
i j : Fin (size as)
⊢ List.set (List.set as.data i.val (get as j)) j.val (get as i) =
    List.set (List.set as.data j.val (get as i)) i.val (get as j)
Theorem: Array.swap_comm
Proof state before:
case h
α : Type u
as : Array α
i j : Fin (size as)
⊢ List.set (List.set as.data i.val (get as j)) j.val (get as i) =
    List.set (List.set as.data j.val (get as i)) i.val (get as j)
Tactic:
if h : i.1 = j.1 then
  cases Fin.eq_of_val_eq h; rfl
else
  rw [List.set_comm _ _ _ h]
Proof state after:
no goals
Theorem: Array.swap_comm
Proof state before:
α : Type u
as : Array α
i j : Fin (size as)
h : i.val = j.val
⊢ List.set (List.set as.data i.val (get as j)) j.val (get as i) =
    List.set (List.set as.data j.val (get as i)) i.val (get as j)
Tactic:
cases Fin.eq_of_val_eq h
Proof state after:
case refl
α : Type u
as : Array α
i : Fin (size as)
h : i.val = i.val
⊢ List.set (List.set as.data i.val (get as i)) i.val (get as i) =
    List.set (List.set as.data i.val (get as i)) i.val (get as i)
Theorem: Array.swap_comm
Proof state before:
case refl
α : Type u
as : Array α
i : Fin (size as)
h : i.val = i.val
⊢ List.set (List.set as.data i.val (get as i)) i.val (get as i) =
    List.set (List.set as.data i.val (get as i)) i.val (get as i)
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.swap_comm
Proof state before:
α : Type u
as : Array α
i j : Fin (size as)
h : ¬i.val = j.val
⊢ List.set (List.set as.data i.val (get as j)) j.val (get as i) =
    List.set (List.set as.data j.val (get as i)) i.val (get as j)
Tactic:
rw [List.set_comm _ _ _ h]
Proof state after:
no goals
Theorem: Array.pmap_eq_nat_fold'_push
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]
⊢ pmap f as h = Nat.fold' (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) #[]
Tactic:
rewrite [Nat.fold'_eq_fold'TR]
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]
⊢ pmap f as h = Nat.fold'TR (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) #[]
Theorem: Array.pmap_eq_nat_fold'_push
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]
⊢ pmap f as h = Nat.fold'TR (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) #[]
Tactic:
dsimp [pmap, pmapM, Nat.fold'TR]
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]
⊢ pmapM.map f as h 0 #[] =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) (size as)
      (_ : Nat.le (size as) (size as)) #[]
Theorem: Array.pmap_eq_nat_fold'_push
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]
⊢ pmapM.map f as h 0 #[] =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) (size as)
      (_ : Nat.le (size as) (size as)) #[]
Tactic:
suffices ∀ (k : Nat) (hk : k ≤ as.size) (bs : Array β), pmapM.map (m:=Id) f as h (as.size - k) bs = Nat.fold'TR.loop as.size _ k hk bs
from Eq.trans (as.size.sub_self ▸ rfl) (this as.size .refl #[])
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]
⊢ ∀ (k : Nat) (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
Theorem: Array.pmap_eq_nat_fold'_push
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]
⊢ ∀ (k : Nat) (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
Tactic:
intro k hk bs
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]
k : Nat
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
Theorem: Array.pmap_eq_nat_fold'_push
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]
k : Nat
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
Tactic:
induction k generalizing bs with
| zero =>
  simp only [Nat.zero_eq, Nat.sub_zero]
  unfold pmapM.map
  exact dif_neg <| Nat.lt_irrefl as.size
| succ k IH =>
  unfold pmapM.map
  rewrite [dif_pos (trans (as.size.sub_succ_lt_self _ hk) (as.size.sub_le k))]
  dsimp [Nat.fold'TR.loop]
  rw [← IH (Nat.le_of_succ_le hk) _]
  apply congrFun; apply congrArg
  rewrite [← Nat.sub_add_comm hk]
  exact Nat.succ_sub_succ_eq_sub as.size k
Proof state after:
no goals
Theorem: Array.pmap_eq_nat_fold'_push
Proof state before:
case zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
hk : Nat.zero ≤ size as
bs : Array β
⊢ pmapM.map f as h (size as - Nat.zero) bs =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) Nat.zero hk bs
Tactic:
simp only [Nat.zero_eq, Nat.sub_zero]
Proof state after:
case zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
hk : Nat.zero ≤ size as
bs : Array β
⊢ pmapM.map f as h (size as) bs = Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) 0 hk bs
Theorem: Array.pmap_eq_nat_fold'_push
Proof state before:
case zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
hk : Nat.zero ≤ size as
bs : Array β
⊢ pmapM.map f as h (size as) bs = Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) 0 hk bs
Tactic:
unfold pmapM.map
Proof state after:
case zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
hk : Nat.zero ≤ size as
bs : Array β
⊢ (if hlt : size as < size as then do
      let __do_lift ← f as[size as] (_ : p as[size as])
      pmapM.map f as h (size as + 1) (push bs __do_lift)
    else pure bs) =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) 0 hk bs
Theorem: Array.pmap_eq_nat_fold'_push
Proof state before:
case zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
hk : Nat.zero ≤ size as
bs : Array β
⊢ (if hlt : size as < size as then do
      let __do_lift ← f as[size as] (_ : p as[size as])
      pmapM.map f as h (size as + 1) (push bs __do_lift)
    else pure bs) =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) 0 hk bs
Tactic:
exact dif_neg <| Nat.lt_irrefl as.size
Proof state after:
no goals
Theorem: Array.pmap_eq_nat_fold'_push
Proof state before:
case succ
α : 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 β
⊢ pmapM.map f as h (size as - Nat.succ k) bs =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) (Nat.succ k) hk bs
Tactic:
unfold pmapM.map
Proof state after:
case succ
α : 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 β
⊢ (if hlt : size as - Nat.succ k < size as then do
      let __do_lift ← f as[size as - Nat.succ k] (_ : p as[size as - Nat.succ k])
      pmapM.map f as h (size as - Nat.succ k + 1) (push bs __do_lift)
    else pure bs) =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) (Nat.succ k) hk bs
Theorem: Array.pmap_eq_nat_fold'_push
Proof state before:
case succ
α : 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 β
⊢ (if hlt : size as - Nat.succ k < size as then do
      let __do_lift ← f as[size as - Nat.succ k] (_ : p as[size as - Nat.succ k])
      pmapM.map f as h (size as - Nat.succ k + 1) (push bs __do_lift)
    else pure bs) =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) (Nat.succ k) hk bs
Tactic:
rewrite [dif_pos (trans (as.size.sub_succ_lt_self _ hk) (as.size.sub_le k))]
Proof state after:
case succ
α : 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 β
⊢ (do
      let __do_lift ← f as[size as - Nat.succ k] (_ : p as[size as - Nat.succ k])
      pmapM.map f as h (size as - Nat.succ k + 1) (push bs __do_lift)) =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) (Nat.succ k) hk bs
Theorem: Array.pmap_eq_nat_fold'_push
Proof state before:
case succ
α : 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 β
⊢ (do
      let __do_lift ← f as[size as - Nat.succ k] (_ : p as[size as - Nat.succ k])
      pmapM.map f as h (size as - Nat.succ k + 1) (push bs __do_lift)) =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) (Nat.succ k) hk bs
Tactic:
dsimp [Nat.fold'TR.loop]
Proof state after:
case succ
α : 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 β
⊢ pmapM.map f as h (size as - Nat.succ k + 1) (push bs (f as[size as - Nat.succ k] (_ : p as[size as - Nat.succ k]))) =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) k (_ : k ≤ size as)
      (push bs (f as[size as - (k + 1)] (_ : p as[size as - (k + 1)])))
Theorem: Array.pmap_eq_nat_fold'_push
Proof state before:
case succ
α : 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 β
⊢ pmapM.map f as h (size as - Nat.succ k + 1) (push bs (f as[size as - Nat.succ k] (_ : p as[size as - Nat.succ k]))) =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) k (_ : k ≤ size as)
      (push bs (f as[size as - (k + 1)] (_ : p as[size as - (k + 1)])))
Tactic:
rw [← IH (Nat.le_of_succ_le hk) _]
Proof state after:
case succ
α : 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 β
⊢ pmapM.map f as h (size as - Nat.succ k + 1) (push bs (f as[size as - Nat.succ k] (_ : p as[size as - Nat.succ k]))) =
    pmapM.map f as h (size as - k) (push bs (f as[size as - (k + 1)] (_ : p as[size as - (k + 1)])))
Theorem: Array.pmap_eq_nat_fold'_push
Proof state before:
case succ
α : 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 β
⊢ pmapM.map f as h (size as - Nat.succ k + 1) (push bs (f as[size as - Nat.succ k] (_ : p as[size as - Nat.succ k]))) =
    pmapM.map f as h (size as - k) (push bs (f as[size as - (k + 1)] (_ : p as[size as - (k + 1)])))
Tactic:
apply congrFun
Proof state after:
case succ.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 β
⊢ pmapM.map f as h (size as - Nat.succ k + 1) = pmapM.map f as h (size as - k)
Theorem: Array.pmap_eq_nat_fold'_push
Proof state before:
case succ.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 β
⊢ pmapM.map f as h (size as - Nat.succ k + 1) = pmapM.map f as h (size as - k)
Tactic:
apply congrArg
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 - Nat.succ k + 1 = size as - k