Theorem: Array.pmap_eq_nat_fold'_push (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]
⊢ 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]
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]))) #[]

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]
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)) #[]

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 #[])
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

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
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

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
State after:
no goals

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]
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

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
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

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
State after:
no goals

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
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

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))]
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

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]
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)])))

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) _]
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)])))

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
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)

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
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

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]
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

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
State after:
no goals