internlm/Lean-Github huggingface dataset:
Theorem: Array.foldlM_cons
Proof state before:
α : Type u
β : Type v
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
a : α
as : Array α
l : List α
⊢ foldlM f init (cons a { data := l }) 0 (size (cons a { data := l })) = do
    let b ← f init a
    foldlM f b { data := l } 0 (size { data := l })
Tactic:
simp only [foldlM_eq_foldlM_data', cons]
Proof state after:
α : Type u
β : Type v
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
a : α
as : Array α
l : List α
⊢ List.foldlM f init (a :: l) = do
    let b ← f init a
    List.foldlM f b l
Theorem: Array.foldlM_cons
Proof state before:
α : Type u
β : Type v
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
a : α
as : Array α
l : List α
⊢ List.foldlM f init (a :: l) = do
    let b ← f init a
    List.foldlM f b l
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.foldl_cons
Proof state before:
α : Type u
β : Type v
f : β → α → β
init : β
a : α
as : Array α
⊢ foldl f init (cons a as) 0 (size (cons a as)) = foldl f (f init a) as 0 (size as)
Tactic:
exact foldlM_cons (m:=Id) (λ b a => pure (f b a)) init a as
Proof state after:
no goals
Theorem: Array.foldlM_push
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type v
f : β → α → m β
init : β
as : Array α
a : α
⊢ foldlM f init (push as a) 0 (size (push as a)) = do
    let b ← foldlM f init as 0 (size as)
    f b a
Tactic:
simp only [foldlM_eq_foldlM_data', as.push_data a]
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type v
f : β → α → m β
init : β
as : Array α
a : α
⊢ List.foldlM f init (as.data ++ [a]) = do
    let b ← List.foldlM f init as.data
    f b a
Theorem: Array.foldlM_push
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type v
f : β → α → m β
init : β
as : Array α
a : α
⊢ List.foldlM f init (as.data ++ [a]) = do
    let b ← List.foldlM f init as.data
    f b a
Tactic:
conv => lhs; rw [List.foldlM_append]; rhs; ext; simp only [List.foldlM, bind_pure]
Proof state after:
no goals
Theorem: Array.foldlM_eq_foldl
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type v
f : β → α → m β
init : β
x✝ a : Array α
x : α
IH :
  foldlM f init a 0 (size a) =
    foldl
      (fun z a => do
        let b ← z
        f b a)
      (pure init) a 0 (size a)
⊢ foldlM f init (push a x) 0 (size (push a x)) =
    foldl
      (fun z a => do
        let b ← z
        f b a)
      (pure init) (push a x) 0 (size (push a x))
Tactic:
rw [foldlM_push, foldl_push, IH]
Proof state after:
no goals
Theorem: Array.mapM.map_cons_succ
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
⊢ map f (cons a x) (i + 1) (cons b y) = do
    let y ← map f x i y
    pure (cons b y)
Tactic:
unfold map
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
⊢ (if hlt : i + 1 < size (cons a x) then do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)
    else pure (cons b y)) =
    do
    let y ←
      if hlt : i < size x then do
          let __do_lift ← f x[i]
          map f x (i + 1) (push y __do_lift)
        else pure y
    pure (cons b y)
Theorem: Array.mapM.map_cons_succ
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
⊢ (if hlt : i + 1 < size (cons a x) then do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)
    else pure (cons b y)) =
    do
    let y ←
      if hlt : i < size x then do
          let __do_lift ← f x[i]
          map f x (i + 1) (push y __do_lift)
        else pure y
    pure (cons b y)
Tactic:
simp only [size_cons]
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
⊢ (if hlt : i + 1 < Nat.succ (size x) then do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)
    else pure (cons b y)) =
    do
    let y ←
      if hlt : i < size x then do
          let __do_lift ← f x[i]
          map f x (i + 1) (push y __do_lift)
        else pure y
    pure (cons b y)
Theorem: Array.mapM.map_cons_succ
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
⊢ (if hlt : i + 1 < Nat.succ (size x) then do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)
    else pure (cons b y)) =
    do
    let y ←
      if hlt : i < size x then do
          let __do_lift ← f x[i]
          map f x (i + 1) (push y __do_lift)
        else pure y
    pure (cons b y)
Tactic:
if h : i < x.size then
  rw [dif_pos (Nat.succ_lt_succ h), dif_pos h, bind_assoc]
  apply bind_congr; intro b'
  exact mapM.map_cons_succ f a x (i+1) b (push y b')
else
  rw [dif_neg h, dif_neg (h ∘ Nat.lt_of_succ_lt_succ)]
  rw [pure_bind]
Proof state after:
no goals
Theorem: Array.mapM.map_cons_succ
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
⊢ (if hlt : i + 1 < Nat.succ (size x) then do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)
    else pure (cons b y)) =
    do
    let y ←
      if hlt : i < size x then do
          let __do_lift ← f x[i]
          map f x (i + 1) (push y __do_lift)
        else pure y
    pure (cons b y)
Tactic:
rw [dif_pos (Nat.succ_lt_succ h), dif_pos h, bind_assoc]
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
⊢ (do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)) =
    do
    let x_1 ← f x[i]
    let y ← map f x (i + 1) (push y x_1)
    pure (cons b y)
Theorem: Array.mapM.map_cons_succ
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
⊢ (do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)) =
    do
    let x_1 ← f x[i]
    let y ← map f x (i + 1) (push y x_1)
    pure (cons b y)
Tactic:
apply bind_congr
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
⊢ ∀ (a_1 : β),
    map f (cons a x) (i + 1 + 1) (push (cons b y) a_1) = do
      let y ← map f x (i + 1) (push y a_1)
      pure (cons b y)
Theorem: Array.mapM.map_cons_succ
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
⊢ ∀ (a_1 : β),
    map f (cons a x) (i + 1 + 1) (push (cons b y) a_1) = do
      let y ← map f x (i + 1) (push y a_1)
      pure (cons b y)
Tactic:
intro b'
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
b' : β
⊢ map f (cons a x) (i + 1 + 1) (push (cons b y) b') = do
    let y ← map f x (i + 1) (push y b')
    pure (cons b y)
Theorem: Array.mapM.map_cons_succ
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
b' : β
⊢ map f (cons a x) (i + 1 + 1) (push (cons b y) b') = do
    let y ← map f x (i + 1) (push y b')
    pure (cons b y)
Tactic:
exact mapM.map_cons_succ f a x (i+1) b (push y b')
Proof state after:
no goals
Theorem: Array.mapM.map_cons_succ
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : ¬i < size x
⊢ (if hlt : i + 1 < Nat.succ (size x) then do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)
    else pure (cons b y)) =
    do
    let y ←
      if hlt : i < size x then do
          let __do_lift ← f x[i]
          map f x (i + 1) (push y __do_lift)
        else pure y
    pure (cons b y)
Tactic:
rw [dif_neg h, dif_neg (h ∘ Nat.lt_of_succ_lt_succ)]
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : ¬i < size x
⊢ pure (cons b y) = do
    let y ← pure y
    pure (cons b y)
Theorem: Array.mapM.map_cons_succ
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : ¬i < size x
⊢ pure (cons b y) = do
    let y ← pure y
    pure (cons b y)
Tactic:
rw [pure_bind]
Proof state after:
no goals
Theorem: Array.mapM_cons
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
⊢ mapM f (cons a x) = do
    let b ← f a
    let y ← mapM f x
    pure (cons b y)
Tactic:
unfold mapM
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
⊢ mapM.map f (cons a x) 0 (mkEmpty (size (cons a x))) = do
    let b ← f a
    let y ← mapM.map f x 0 (mkEmpty (size x))
    pure (cons b y)
Theorem: Array.mapM_cons
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
⊢ mapM.map f (cons a x) 0 (mkEmpty (size (cons a x))) = do
    let b ← f a
    let y ← mapM.map f x 0 (mkEmpty (size x))
    pure (cons b y)
Tactic:
conv =>
  lhs; unfold mapM.map; simp only [size_cons]
  rw [dif_pos x.size.zero_lt_succ]
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
⊢ (do
      let __do_lift ← f (cons a x)[0]
      mapM.map f (cons a x) (0 + 1) (push (mkEmpty (Nat.succ (size x))) __do_lift)) =
    do
    let b ← f a
    let y ← mapM.map f x 0 (mkEmpty (size x))
    pure (cons b y)
Theorem: Array.mapM_cons
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
⊢ (do
      let __do_lift ← f (cons a x)[0]
      mapM.map f (cons a x) (0 + 1) (push (mkEmpty (Nat.succ (size x))) __do_lift)) =
    do
    let b ← f a
    let y ← mapM.map f x 0 (mkEmpty (size x))
    pure (cons b y)
Tactic:
apply bind_congr
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
⊢ ∀ (a_1 : β),
    mapM.map f (cons a x) (0 + 1) (push (mkEmpty (Nat.succ (size x))) a_1) = do
      let y ← mapM.map f x 0 (mkEmpty (size x))
      pure (cons a_1 y)
Theorem: Array.mapM_cons
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
⊢ ∀ (a_1 : β),
    mapM.map f (cons a x) (0 + 1) (push (mkEmpty (Nat.succ (size x))) a_1) = do
      let y ← mapM.map f x 0 (mkEmpty (size x))
      pure (cons a_1 y)
Tactic:
intro b
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
b : β
⊢ mapM.map f (cons a x) (0 + 1) (push (mkEmpty (Nat.succ (size x))) b) = do
    let y ← mapM.map f x 0 (mkEmpty (size x))
    pure (cons b y)
Theorem: Array.mapM_cons
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
b : β
⊢ mapM.map f (cons a x) (0 + 1) (push (mkEmpty (Nat.succ (size x))) b) = do
    let y ← mapM.map f x 0 (mkEmpty (size x))
    pure (cons b y)
Tactic:
exact mapM.map_cons_succ f a x 0 b #[]
Proof state after:
no goals
Theorem: Array.mapM_push
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
a : α
⊢ (do
      let b ← f a
      let y ← mapM f #[]
      pure (cons b y)) =
    do
    let y ← mapM f #[]
    let b ← f a
    pure (push y b)
Tactic:
simp only [mapM_empty, pure_bind]
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
a : α
⊢ (do
      let b ← f a
      pure (cons b #[])) =
    do
    let b ← f a
    pure (push #[] b)
Theorem: Array.mapM_push
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
a : α
⊢ (do
      let b ← f a
      pure (cons b #[])) =
    do
    let b ← f a
    pure (push #[] b)
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.mapM_push
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ mapM f (push (cons a x) a✝) = do
    let y ← mapM f (cons a x)
    let b ← f a✝
    pure (push y b)
Tactic:
show mapM f (cons a (push x _)) = _
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ mapM f (cons a (push x a✝)) = do
    let y ← mapM f (cons a x)
    let b ← f a✝
    pure (push y b)
Theorem: Array.mapM_push
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ mapM f (cons a (push x a✝)) = do
    let y ← mapM f (cons a x)
    let b ← f a✝
    pure (push y b)
Tactic:
simp only [mapM_cons f, bind_assoc]
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ (do
      let b ← f a
      let y ← mapM f (push x a✝)
      pure (cons b y)) =
    do
    let x_1 ← f a
    let x ← mapM f x
    let y ← pure (cons x_1 x)
    let b ← f a✝
    pure (push y b)
Theorem: Array.mapM_push
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ (do
      let b ← f a
      let y ← mapM f (push x a✝)
      pure (cons b y)) =
    do
    let x_1 ← f a
    let x ← mapM f x
    let y ← pure (cons x_1 x)
    let b ← f a✝
    pure (push y b)
Tactic:
apply bind_congr
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ ∀ (a : β),
    (do
        let y ← mapM f (push x a✝)
        pure (cons a y)) =
      do
      let x ← mapM f x
      let y ← pure (cons a x)
      let b ← f a✝
      pure (push y b)
Theorem: Array.mapM_push
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ ∀ (a : β),
    (do
        let y ← mapM f (push x a✝)
        pure (cons a y)) =
      do
      let x ← mapM f x
      let y ← pure (cons a x)
      let b ← f a✝
      pure (push y b)
Tactic:
intro b
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
b : β
⊢ (do
      let y ← mapM f (push x a✝)
      pure (cons b y)) =
    do
    let x ← mapM f x
    let y ← pure (cons b x)
    let b ← f a✝
    pure (push y b)
Theorem: Array.mapM_push
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
b : β
⊢ (do
      let y ← mapM f (push x a✝)
      pure (cons b y)) =
    do
    let x ← mapM f x
    let y ← pure (cons b x)
    let b ← f a✝
    pure (push y b)
Tactic:
rw [IH]
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
b : β
⊢ (do
      let y ←
        do
          let y ← mapM f x
          let b ← f a✝
          pure (push y b)
      pure (cons b y)) =
    do
    let x ← mapM f x
    let y ← pure (cons b x)
    let b ← f a✝
    pure (push y b)
Theorem: Array.mapM_push
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
b : β
⊢ (do
      let y ←
        do
          let y ← mapM f x
          let b ← f a✝
          pure (push y b)
      pure (cons b y)) =
    do
    let x ← mapM f x
    let y ← pure (cons b x)
    let b ← f a✝
    pure (push y b)
Tactic:
simp only [bind_assoc, pure_bind]
Proof state after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
b : β
⊢ (do
      let x ← mapM f x
      let x_1 ← f a✝
      pure (cons b (push x x_1))) =
    do
    let x ← mapM f x
    let b_1 ← f a✝
    pure (push (cons b x) b_1)
Theorem: Array.mapM_push
Proof state before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
b : β
⊢ (do
      let x ← mapM f x
      let x_1 ← f a✝
      pure (cons b (push x x_1))) =
    do
    let x ← mapM f x
    let b_1 ← f a✝
    pure (push (cons b x) b_1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.map_data'
Proof state before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr x : Array α
a : α
IH : (map f x).data = List.map f x.data
⊢ (map f (push x a)).data = List.map f (push x a).data
Tactic:
simp only [map_push, push_data, IH, List.map_append]
Proof state after:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr x : Array α
a : α
IH : (map f x).data = List.map f x.data
⊢ List.map f x.data ++ [f a] = List.map f x.data ++ List.map f [a]
Theorem: Array.map_data'
Proof state before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr x : Array α
a : α
IH : (map f x).data = List.map f x.data
⊢ List.map f x.data ++ [f a] = List.map f x.data ++ List.map f [a]
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.map_cons
Proof state before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
a : α
x : Array α
⊢ (map f (cons a x)).data = (cons (f a) (map f x)).data
Tactic:
simp only [map_data', cons]
Proof state after:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
a : α
x : Array α
⊢ List.map f (a :: x.data) = f a :: List.map f x.data
Theorem: Array.map_cons
Proof state before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
a : α
x : Array α
⊢ List.map f (a :: x.data) = f a :: List.map f x.data
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.size_mapM'
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
⊢ Subtype.val <$> pure { val := #[], property := (_ : size #[] = size #[]) } = mapM f #[]
Tactic:
rw [map_pure]
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
⊢ pure { val := #[], property := (_ : size #[] = size #[]) }.val = mapM f #[]
Theorem: Array.size_mapM'
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
⊢ pure { val := #[], property := (_ : size #[] = size #[]) }.val = mapM f #[]
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.size_mapM'
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ (Subtype.val <$> do
      let y ← y
      push' y <$> f a) =
    mapM f (push x a)
Tactic:
rw [mapM_push, ← h]
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ (Subtype.val <$> do
      let y ← y
      push' y <$> f a) =
    do
    let y ← Subtype.val <$> y
    let b ← f a
    pure (push y b)
Theorem: Array.size_mapM'
Proof state before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ (Subtype.val <$> do
      let y ← y
      push' y <$> f a) =
    do
    let y ← Subtype.val <$> y
    let b ← f a
    pure (push y b)
Tactic:
simp only [map_eq_pure_bind, bind_assoc]
Proof state after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ (do
      let x_1 ← y
      let x_2 ← f a
      let a_1 ← pure { val := push x_1.val x_2, property := (_ : size (push x_1.val x_2) = size (push x a)) }
      pure a_1.val) =
    do
    let x_1 ← y
    let y ← pure x_1.val
    let b ← f a
    pure (push y b)