m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
this : arr = #[] ∨ 0 < size arr
⊢ foldrM f init arr (size arr) = List.foldlM (fun x y => f y x) init (List.reverse arr.data)
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
⊢ foldrM f init arr (size arr) = List.foldlM (fun x y => f y x) init (List.reverse arr.data)
have : arr = #[] ∨ 0 < arr.size :=
  match arr with | ⟨[]⟩ => .inl rfl | ⟨a::l⟩ => .inr (Nat.zero_lt_succ _)
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr✝ : Array α
this : arr✝ = #[] ∨ 0 < size arr✝
arr : Array α
h : 0 < size arr
⊢ foldrM f init arr (size arr) = List.foldlM (fun x y => f y x) init (List.reverse arr.data)
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
this : arr = #[] ∨ 0 < size arr
⊢ foldrM f init arr (size arr) = List.foldlM (fun x y => f y x) init (List.reverse arr.data)
match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr✝ : Array α
this : arr✝ = #[] ∨ 0 < size arr✝
arr : Array α
h : 0 < size arr
⊢ foldrM f init arr (size arr) = List.foldlM (fun x y => f y x) init (List.reverse arr.data)
simp [foldrM, h, ← foldrM_eq_reverse_foldlM_data.aux, List.take_length]
no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
this : arr = #[] ∨ 0 < size arr
⊢ foldrM f init #[] (size #[]) = List.foldlM (fun x y => f y x) init (List.reverse #[].data)
rfl