Theorem: List.mapM_loop_map (MLIR/Util/KDTensor.lean)

State before:
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
l : List α
f : α → β
fM : α → M β
results : List β
⊢ (∀ (a : α), fM a = pure (f a)) → mapM.loop fM l results = pure (reverse results ++ map f l)
Tactic:
intros h
State after:
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
l : List α
f : α → β
fM : α → M β
results : List β
h : ∀ (a : α), fM a = pure (f a)
⊢ mapM.loop fM l results = pure (reverse results ++ map f l)

State before:
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
l : List α
f : α → β
fM : α → M β
results : List β
h : ∀ (a : α), fM a = pure (f a)
⊢ mapM.loop fM l results = pure (reverse results ++ map f l)
Tactic:
revert results
State after:
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
l : List α
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
⊢ ∀ (results : List β), mapM.loop fM l results = pure (reverse results ++ map f l)

State before:
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
l : List α
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
⊢ ∀ (results : List β), mapM.loop fM l results = pure (reverse results ++ map f l)
Tactic:
induction l with
| nil => intros results; simp [map];
| cons a l ih =>
    intros results
    simp [mapM.loop, map, h, ih, reverse_cons, append_assoc]
State after:
no goals

State before:
case nil
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
⊢ ∀ (results : List β), mapM.loop fM [] results = pure (reverse results ++ map f [])
Tactic:
intros results
State after:
case nil
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
results : List β
⊢ mapM.loop fM [] results = pure (reverse results ++ map f [])

State before:
case nil
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
results : List β
⊢ mapM.loop fM [] results = pure (reverse results ++ map f [])
Tactic:
simp [map]
State after:
no goals

State before:
case cons
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
a : α
l : List α
ih : ∀ (results : List β), mapM.loop fM l results = pure (reverse results ++ map f l)
⊢ ∀ (results : List β), mapM.loop fM (a :: l) results = pure (reverse results ++ map f (a :: l))
Tactic:
intros results
State after:
case cons
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
a : α
l : List α
ih : ∀ (results : List β), mapM.loop fM l results = pure (reverse results ++ map f l)
results : List β
⊢ mapM.loop fM (a :: l) results = pure (reverse results ++ map f (a :: l))

State before:
case cons
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
a : α
l : List α
ih : ∀ (results : List β), mapM.loop fM l results = pure (reverse results ++ map f l)
results : List β
⊢ mapM.loop fM (a :: l) results = pure (reverse results ++ map f (a :: l))
Tactic:
simp [mapM.loop, map, h, ih, reverse_cons, append_assoc]
State after:
no goals