-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_induction
    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive as.size init) {f : α → β → β}
    (hf : ∀ i : Fin as.size, ∀ b, motive (i.1 + 1) b → motive i.1 (f as[i] b)) :
    motive 0 (as.foldr f init)

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
i : Nat
b : β
hi✝ : i ≤ as.size
H : motive i b
hi : ¬i = 0
⊢ motive 0
    (match i, hi✝ with
    | 0, x => b
    | i.succ, h => foldrM.fold f as 0 i ⋯ (f as[i] b))

Tactic:
split

Result:
case h_1
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
b : β
x✝² : Nat
x✝¹ : x✝² ≤ as.size
x✝ : 0 ≤ as.size
H : motive 0 b
hi : ¬0 = 0
⊢ motive 0 b

case h_2
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
b : β
x✝¹ : Nat
x✝ : x✝¹ ≤ as.size
i✝ : Nat
h✝ : i✝ + 1 ≤ as.size
H : motive i✝.succ b
hi : ¬i✝.succ = 0
⊢ motive 0 (foldrM.fold f as 0 i✝ ⋯ (f as[i✝] b))

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
i : Nat
b : β
hi : i ≤ as.size
H : motive i b
⊢ motive 0
    (if (i == 0) = true then pure b
    else
      match i, hi with
      | 0, x => pure b
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f as[i] b
        foldrM.fold f as 0 i ⋯ __do_lift)

Tactic:
simp

Result:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
i : Nat
b : β
hi : i ≤ as.size
H : motive i b
⊢ motive 0
    (if i = 0 then b
    else
      match i, hi with
      | 0, x => b
      | i.succ, h => foldrM.fold f as 0 i ⋯ (f as[i] b))

Proof state:
case isTrue
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
h✝ : 0 < as.size
⊢ motive 0 (foldrM.fold f as 0 as.size ⋯ init).run

Tactic:
exact go _ h0

Result:
no goals

Proof state:
case h_2
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
b : β
x✝¹ : Nat
x✝ : x✝¹ ≤ as.size
i✝ : Nat
h✝ : i✝ + 1 ≤ as.size
H : motive i✝.succ b
hi : ¬i✝.succ = 0
⊢ motive 0 (foldrM.fold f as 0 i✝ ⋯ (f as[i✝] b))

Tactic:
next i hi' =>
exact go _ (hf ⟨i, hi'⟩ b H)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
h : ¬0 < as.size
⊢ motive 0 (Id.run init)

Tactic:
exact (Nat.eq_zero_of_not_pos h ▸ h0)

Result:
no goals

Proof state:
case h_1
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
b : β
x✝² : Nat
x✝¹ : x✝² ≤ as.size
x✝ : 0 ≤ as.size
H : motive 0 b
hi : ¬0 = 0
⊢ motive 0 b

Tactic:
simp at hi

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
i : Nat
b : β
hi✝ : i ≤ as.size
H : motive i b
hi : i = 0
⊢ motive 0 b

Tactic:
exact (hi ▸ H)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
⊢ motive 0 (foldr f init as)

Tactic:
simp [foldr, foldrM]

Result:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
⊢ motive 0 (if 0 < as.size then foldrM.fold f as 0 as.size ⋯ init else init).run

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
i : Nat
b : β
hi : i ≤ as.size
H : motive i b
⊢ motive 0
    (if i = 0 then b
    else
      match i, hi with
      | 0, x => b
      | i.succ, h => foldrM.fold f as 0 i ⋯ (f as[i] b))

Tactic:
split

Result:
case isTrue
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
i : Nat
b : β
hi : i ≤ as.size
H : motive i b
h✝ : i = 0
⊢ motive 0 b

case isFalse
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
i : Nat
b : β
hi : i ≤ as.size
H : motive i b
h✝ : ¬i = 0
⊢ motive 0
    (match i, hi with
    | 0, x => b
    | i.succ, h => foldrM.fold f as 0 i ⋯ (f as[i] b))

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
i : Nat
b : β
hi : i ≤ as.size
H : motive i b
⊢ motive 0 (foldrM.fold f as 0 i hi b)

Tactic:
unfold foldrM.fold

Result:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
i : Nat
b : β
hi : i ≤ as.size
H : motive i b
⊢ motive 0
    (if (i == 0) = true then pure b
    else
      match i, hi with
      | 0, x => pure b
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f as[i] b
        foldrM.fold f as 0 i ⋯ __do_lift)

Proof state:
case isTrue
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
h✝ : 0 < as.size
⊢ motive 0 (foldrM.fold f as 0 as.size ⋯ init).run

case isFalse
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
h✝ : ¬0 < as.size
⊢ motive 0 (Id.run init)

Tactic:
{exact go _ h0}

Result:
case isFalse
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
h✝ : ¬0 < as.size
⊢ motive 0 (Id.run init)

Proof state:
case isTrue
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive as.size init
f : α → β → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)
i : Nat
b : β
hi : i ≤ as.size
H : motive i b
h✝ : i = 0
⊢ motive 0 b

Tactic:
next hi => exact (hi ▸ H)

Result:
no goals