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

State before:
α : Type u
as : Array α
p : α → Bool
⊢ any as p 0 (size as) = List.any as.data p
Tactic:
dsimp [any, anyM]
State after:
α : Type u
as : Array α
p : α → Bool
⊢ Id.run
      (if h : size as ≤ size as then anyM.loop p as (size as) h 0
      else anyM.loop p as (size as) (_ : size as ≤ size as) 0) =
    List.any as.data p

State before:
α : Type u
as : Array α
p : α → Bool
⊢ Id.run
      (if h : size as ≤ size as then anyM.loop p as (size as) h 0
      else anyM.loop p as (size as) (_ : size as ≤ size as) 0) =
    List.any as.data p
Tactic:
simp
State after:
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) 0) = List.any as.data p

State before:
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) 0) = List.any as.data p
Tactic:
conv => rhs; change (as.data.drop 0).any p
State after:
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) 0) = List.any (List.drop 0 as.data) p

State before:
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) 0) = List.any (List.drop 0 as.data) p
Tactic:
refine Nat.decreasing_induction (m:=0) (n:=as.size) ?_ ?_ as.size.zero_le
State after:
case refine_1
α : Type u
as : Array α
p : α → Bool
⊢ ∀ (n : Nat),
    Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (n + 1)) = List.any (List.drop (n + 1) as.data) p →
      Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) n) = List.any (List.drop n as.data) p

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

State before:
case refine_1
α : Type u
as : Array α
p : α → Bool
⊢ ∀ (n : Nat),
    Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (n + 1)) = List.any (List.drop (n + 1) as.data) p →
      Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) n) = List.any (List.drop n as.data) p

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:
. intro j IH
  unfold anyM.loop; dsimp
  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
State after:
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

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; dsimp
  rewrite [dif_neg (Nat.lt_irrefl _), List.drop_eq_nil_of_le .refl]
  rfl
State after:
no goals

State before:
case refine_1
α : Type u
as : Array α
p : α → Bool
⊢ ∀ (n : Nat),
    Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (n + 1)) = List.any (List.drop (n + 1) as.data) p →
      Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) n) = List.any (List.drop n as.data) p
Tactic:
intro j IH
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 (anyM.loop p as (size as) (_ : size as ≤ size as) j) = List.any (List.drop j as.data) p

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

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

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

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

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

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

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

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

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

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

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

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

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]
State after:
case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run false = List.any [] p

State before:
case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run false = List.any [] p
Tactic:
rfl
State after:
no goals