internlm/Lean-Github huggingface dataset:
Theorem: Array.mapIdxM_cons
Proof state before:
case h.succ
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ (do
      let __do_lift ← f' { val := j, isLt := (_ : j < size x) } x[j]
      mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) __do_lift)) =
    do
    let y ←
      do
        let __do_lift ← f' { val := j, isLt := (_ : j < size x) } x[j]
        mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y __do_lift)
    pure (cons b y)
Tactic:
simp only [bind_assoc]
Proof state after:
case h.succ
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ (do
      let __do_lift ← f' { val := j, isLt := (_ : j < size x) } x[j]
      mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) __do_lift)) =
    do
    let x_1 ← f' { val := j, isLt := (_ : j < size x) } x[j]
    let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y x_1)
    pure (cons b y)
Theorem: Array.mapIdxM_cons
Proof state before:
case h.succ
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ (do
      let __do_lift ← f' { val := j, isLt := (_ : j < size x) } x[j]
      mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) __do_lift)) =
    do
    let x_1 ← f' { val := j, isLt := (_ : j < size x) } x[j]
    let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y x_1)
    pure (cons b y)
Tactic:
apply bind_congr
Proof state after:
case h.succ.h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ ∀ (a : β),
    mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) a) = do
      let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y a)
      pure (cons b y)
Theorem: Array.mapIdxM_cons
Proof state before:
case h.succ.h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ ∀ (a : β),
    mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) a) = do
      let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y a)
      pure (cons b y)
Tactic:
intro b'
Proof state after:
case h.succ.h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
b' : β
⊢ mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) b') = do
    let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y b')
    pure (cons b y)
Theorem: Array.mapIdxM_cons
Proof state before:
case h.succ.h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
b' : β
⊢ mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) b') = do
    let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y b')
    pure (cons b y)
Tactic:
dsimp [push, cons, List.concat]
Proof state after:
case h.succ.h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
b' : β
⊢ mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) { data := b :: List.concat y.data b' } = do
    let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) { data := List.concat y.data b' }
    pure { data := b :: y.data }
Theorem: Array.mapIdxM_cons
Proof state before:
case h.succ.h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
b' : β
⊢ mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) { data := b :: List.concat y.data b' } = do
    let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) { data := List.concat y.data b' }
    pure { data := b :: y.data }
Tactic:
exact IH ..
Proof state after:
no goals
Theorem: Array.size_mapIdx'
Proof state before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x✝ : Array α
f✝ : Fin (size x✝) → α → β
a : α
x : Array α
IH : ∀ (x_1 : Fin (size x) → α → β), size (mapIdx x x_1) = size x
f : Fin (size (cons a x)) → α → β
⊢ size (mapIdx (cons a x) f) = size (cons a x)
Tactic:
rw [mapIdx_cons]
Proof state after:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x✝ : Array α
f✝ : Fin (size x✝) → α → β
a : α
x : Array α
IH : ∀ (x_1 : Fin (size x) → α → β), size (mapIdx x x_1) = size x
f : Fin (size (cons a x)) → α → β
⊢ size (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ))) = size (cons a x)
Theorem: Array.size_mapIdx'
Proof state before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x✝ : Array α
f✝ : Fin (size x✝) → α → β
a : α
x : Array α
IH : ∀ (x_1 : Fin (size x) → α → β), size (mapIdx x x_1) = size x
f : Fin (size (cons a x)) → α → β
⊢ size (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ))) = size (cons a x)
Tactic:
dsimp [cons]
Proof state after:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x✝ : Array α
f✝ : Fin (size x✝) → α → β
a : α
x : Array α
IH : ∀ (x_1 : Fin (size x) → α → β), size (mapIdx x x_1) = size x
f : Fin (size (cons a x)) → α → β
⊢ size { data := f 0 a :: (mapIdx x (f ∘ Fin.succ)).data } = size { data := a :: x.data }
Theorem: Array.size_mapIdx'
Proof state before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x✝ : Array α
f✝ : Fin (size x✝) → α → β
a : α
x : Array α
IH : ∀ (x_1 : Fin (size x) → α → β), size (mapIdx x x_1) = size x
f : Fin (size (cons a x)) → α → β
⊢ size { data := f 0 a :: (mapIdx x (f ∘ Fin.succ)).data } = size { data := a :: x.data }
Tactic:
exact congrArg Nat.succ (IH (f ∘ Fin.succ))
Proof state after:
no goals
Theorem: Array.getElem_mapIdx_safe
Proof state before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x : Array α
f : Fin (size x) → α → β
i : Nat
hi : i < size (mapIdx x f)
⊢ (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
Tactic:
induction x using cons_induction generalizing i with
| empty => cases hi
| cons a x IH =>
  simp only [mapIdx_cons]
  cases i with
  | zero => simp only [getElem_cons_zero]
  | succ i =>
    simp only [getElem_cons_succ]
    have : i < x.size :=
      Nat.lt_of_succ_lt_succ <| trans (s:=Eq) hi (size_mapIdx' ..)
    rw [IH (f ∘ Fin.succ) i ((x.size_mapIdx' (f ∘ Fin.succ)).symm ▸ this)]
    rfl
Proof state after:
no goals
Theorem: Array.getElem_mapIdx_safe
Proof state before:
case empty
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : Fin (size #[]) → α → β
i : Nat
hi : i < size (mapIdx #[] f)
⊢ (mapIdx #[] f)[i] = f { val := i, isLt := (_ : i < size #[]) } #[][i]
Tactic:
cases hi
Proof state after:
no goals
Theorem: Array.getElem_mapIdx_safe
Proof state before:
case cons
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : i < size (mapIdx (cons a x) f)
⊢ (mapIdx (cons a x) f)[i] = f { val := i, isLt := (_ : i < size (cons a x)) } (cons a x)[i]
Tactic:
simp only [mapIdx_cons]
Proof state after:
case cons
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : i < size (mapIdx (cons a x) f)
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ)))[i] =
    f { val := i, isLt := (_ : i < size (cons a x)) } (cons a x)[i]
Theorem: Array.getElem_mapIdx_safe
Proof state before:
case cons
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : i < size (mapIdx (cons a x) f)
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ)))[i] =
    f { val := i, isLt := (_ : i < size (cons a x)) } (cons a x)[i]
Tactic:
cases i with
| zero => simp only [getElem_cons_zero]
| succ i =>
  simp only [getElem_cons_succ]
  have : i < x.size :=
    Nat.lt_of_succ_lt_succ <| trans (s:=Eq) hi (size_mapIdx' ..)
  rw [IH (f ∘ Fin.succ) i ((x.size_mapIdx' (f ∘ Fin.succ)).symm ▸ this)]
  rfl
Proof state after:
no goals
Theorem: Array.getElem_mapIdx_safe
Proof state before:
case cons.zero
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
hi : Nat.zero < size (mapIdx (cons a x) f)
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ)))[Nat.zero] =
    f { val := Nat.zero, isLt := (_ : Nat.zero < size (cons a x)) } (cons a x)[Nat.zero]
Tactic:
simp only [getElem_cons_zero]
Proof state after:
no goals
Theorem: Array.getElem_mapIdx_safe
Proof state before:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ)))[Nat.succ i] =
    f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } (cons a x)[Nat.succ i]
Tactic:
simp only [getElem_cons_succ]
Proof state after:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
⊢ (mapIdx x (f ∘ Fin.succ))[i] = f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]
Theorem: Array.getElem_mapIdx_safe
Proof state before:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
⊢ (mapIdx x (f ∘ Fin.succ))[i] = f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]
Tactic:
have : i < x.size :=
  Nat.lt_of_succ_lt_succ <| trans (s:=Eq) hi (size_mapIdx' ..)
Proof state after:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
this : i < size x
⊢ (mapIdx x (f ∘ Fin.succ))[i] = f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]
Theorem: Array.getElem_mapIdx_safe
Proof state before:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
this : i < size x
⊢ (mapIdx x (f ∘ Fin.succ))[i] = f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]
Tactic:
rw [IH (f ∘ Fin.succ) i ((x.size_mapIdx' (f ∘ Fin.succ)).symm ▸ this)]
Proof state after:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
this : i < size x
⊢ (f ∘ Fin.succ) { val := i, isLt := (_ : i < size x) } x[i] =
    f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]
Theorem: Array.getElem_mapIdx_safe
Proof state before:
case cons.succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (f : Fin (size x) → α → β) (i : Nat) (hi : i < size (mapIdx x f)),
    (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : Nat.succ i < size (mapIdx (cons a x) f)
this : i < size x
⊢ (f ∘ Fin.succ) { val := i, isLt := (_ : i < size x) } x[i] =
    f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.append_data'
Proof state before:
α : Type u
x y : Array α
⊢ (x ++ y).data = x.data ++ y.data
Tactic:
show (Array.append x y).data = x.data ++ y.data
Proof state after:
α : Type u
x y : Array α
⊢ (Array.append x y).data = x.data ++ y.data
Theorem: Array.append_data'
Proof state before:
α : Type u
x y : Array α
⊢ (Array.append x y).data = x.data ++ y.data
Tactic:
unfold Array.append
Proof state after:
α : Type u
x y : Array α
⊢ (foldl (fun r v => push r v) x y 0 (size y)).data = x.data ++ y.data
Theorem: Array.append_data'
Proof state before:
α : Type u
x y : Array α
⊢ (foldl (fun r v => push r v) x y 0 (size y)).data = x.data ++ y.data
Tactic:
rw [foldl_eq_foldl_data']
Proof state after:
α : Type u
x y : Array α
⊢ (List.foldl (fun r v => push r v) x y.data).data = x.data ++ y.data
Theorem: Array.append_data'
Proof state before:
α : Type u
x y : Array α
⊢ (List.foldl (fun r v => push r v) x y.data).data = x.data ++ y.data
Tactic:
rw [← y.data.foldl_hom Array.data Array.push (λ l a => l ++ [a]) x λ arr a => (arr.push_data a).symm]
Proof state after:
α : Type u
x y : Array α
⊢ List.foldl (fun l a => l ++ [a]) x.data y.data = x.data ++ y.data
Theorem: Array.append_data'
Proof state before:
α : Type u
x y : Array α
⊢ List.foldl (fun l a => l ++ [a]) x.data y.data = x.data ++ y.data
Tactic:
generalize x.data = l
Proof state after:
α : Type u
x y : Array α
l : List α
⊢ List.foldl (fun l a => l ++ [a]) l y.data = l ++ y.data
Theorem: Array.append_data'
Proof state before:
α : Type u
x y : Array α
l : List α
⊢ List.foldl (fun l a => l ++ [a]) l y.data = l ++ y.data
Tactic:
generalize y.data = l'
Proof state after:
α : Type u
x y : Array α
l l' : List α
⊢ List.foldl (fun l a => l ++ [a]) l l' = l ++ l'
Theorem: Array.append_data'
Proof state before:
α : Type u
x y : Array α
l l' : List α
⊢ List.foldl (fun l a => l ++ [a]) l l' = l ++ l'
Tactic:
induction l' generalizing l with
| nil => exact Eq.symm $ l.append_nil
| cons b bs IH =>
  unfold List.foldl; rw [IH]; exact Eq.symm $ l.append_cons b bs
Proof state after:
no goals
Theorem: Array.append_data'
Proof state before:
case nil
α : Type u
x y : Array α
l : List α
⊢ List.foldl (fun l a => l ++ [a]) l [] = l ++ []
Tactic:
exact Eq.symm $ l.append_nil
Proof state after:
no goals
Theorem: Array.append_data'
Proof state before:
case cons
α : Type u
x y : Array α
b : α
bs : List α
IH : ∀ (l : List α), List.foldl (fun l a => l ++ [a]) l bs = l ++ bs
l : List α
⊢ List.foldl (fun l a => l ++ [a]) l (b :: bs) = l ++ b :: bs
Tactic:
unfold List.foldl
Proof state after:
case cons
α : Type u
x y : Array α
b : α
bs : List α
IH : ∀ (l : List α), List.foldl (fun l a => l ++ [a]) l bs = l ++ bs
l : List α
⊢ List.foldl (fun l a => l ++ [a]) (l ++ [b]) bs = l ++ b :: bs
Theorem: Array.append_data'
Proof state before:
case cons
α : Type u
x y : Array α
b : α
bs : List α
IH : ∀ (l : List α), List.foldl (fun l a => l ++ [a]) l bs = l ++ bs
l : List α
⊢ List.foldl (fun l a => l ++ [a]) (l ++ [b]) bs = l ++ b :: bs
Tactic:
rw [IH]
Proof state after:
case cons
α : Type u
x y : Array α
b : α
bs : List α
IH : ∀ (l : List α), List.foldl (fun l a => l ++ [a]) l bs = l ++ bs
l : List α
⊢ l ++ [b] ++ bs = l ++ b :: bs
Theorem: Array.append_data'
Proof state before:
case cons
α : Type u
x y : Array α
b : α
bs : List α
IH : ∀ (l : List α), List.foldl (fun l a => l ++ [a]) l bs = l ++ bs
l : List α
⊢ l ++ [b] ++ bs = l ++ b :: bs
Tactic:
exact Eq.symm $ l.append_cons b bs
Proof state after:
no goals
Theorem: Array.append_assoc
Proof state before:
α : Type u
x y z✝ z : Array α
c : α
IH : x ++ y ++ z = x ++ (y ++ z)
⊢ x ++ y ++ push z c = x ++ (y ++ push z c)
Tactic:
simp only [append_push]
Proof state after:
α : Type u
x y z✝ z : Array α
c : α
IH : x ++ y ++ z = x ++ (y ++ z)
⊢ push (x ++ y ++ z) c = push (x ++ (y ++ z)) c
Theorem: Array.size_append
Proof state before:
α : Type u
x y : Array α
⊢ size (x ++ y) = size x + size y
Tactic:
dsimp [size]
Proof state after:
α : Type u
x y : Array α
⊢ List.length (x ++ y).data = List.length x.data + List.length y.data
Theorem: Array.size_append
Proof state before:
α : Type u
x y : Array α
⊢ List.length (x ++ y).data = List.length x.data + List.length y.data
Tactic:
rw [append_data' x y]
Proof state after:
α : Type u
x y : Array α
⊢ List.length (x.data ++ y.data) = List.length x.data + List.length y.data
Theorem: Array.size_append
Proof state before:
α : Type u
x y : Array α
⊢ List.length (x.data ++ y.data) = List.length x.data + List.length y.data
Tactic:
exact List.length_append x.data y.data
Proof state after:
no goals
Theorem: Array.zipWithAux_nil_first
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array β
n : Nat
z : Array γ
⊢ zipWithAux f #[] x n z = z
Tactic:
unfold Array.zipWithAux
Proof state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array β
n : Nat
z : Array γ
⊢ (if h : n < size #[] then
      let a := #[][n];
      if h : n < size x then
        let b := x[n];
        zipWithAux f #[] x (n + 1) (push z (f a b))
      else z
    else z) =
    z
Theorem: Array.zipWithAux_nil_first
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array β
n : Nat
z : Array γ
⊢ (if h : n < size #[] then
      let a := #[][n];
      if h : n < size x then
        let b := x[n];
        zipWithAux f #[] x (n + 1) (push z (f a b))
      else z
    else z) =
    z
Tactic:
exact dif_neg n.not_lt_zero
Proof state after:
no goals
Theorem: Array.zipWithAux_nil_second
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ zipWithAux f x #[] n z = z
Tactic:
unfold Array.zipWithAux
Proof state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ (if h : n < size x then
      let a := x[n];
      if h : n < size #[] then
        let b := #[][n];
        zipWithAux f x #[] (n + 1) (push z (f a b))
      else z
    else z) =
    z
Theorem: Array.zipWithAux_nil_second
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ (if h : n < size x then
      let a := x[n];
      if h : n < size #[] then
        let b := #[][n];
        zipWithAux f x #[] (n + 1) (push z (f a b))
      else z
    else z) =
    z
Tactic:
dsimp [size]
Proof state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ (if h : n < List.length x.data then if h_1 : n < 0 then zipWithAux f x #[] (n + 1) (push z (f x[n] #[][n])) else z
    else z) =
    z
Theorem: Array.zipWithAux_nil_second
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ (if h : n < List.length x.data then if h_1 : n < 0 then zipWithAux f x #[] (n + 1) (push z (f x[n] #[][n])) else z
    else z) =
    z
Tactic:
simp only [dif_neg n.not_lt_zero]
Proof state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ (if h : n < List.length x.data then z else z) = z
Theorem: Array.zipWithAux_nil_second
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ (if h : n < List.length x.data then z else z) = z
Tactic:
apply dite (n < x.size) <;> (intro h; simp only [h, dif_neg, dif_pos])
Proof state after:
no goals
Theorem: Array.zipWithAux_nil_second
Proof state before:
case e
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ ¬n < size x → (if h : n < List.length x.data then z else z) = z
Tactic:
intro h
Proof state after:
case e
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
h : ¬n < size x
⊢ (if h : n < List.length x.data then z else z) = z
Theorem: Array.zipWithAux_nil_second
Proof state before:
case e
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
h : ¬n < size x
⊢ (if h : n < List.length x.data then z else z) = z
Tactic:
simp only [h, dif_neg, dif_pos]
Proof state after:
no goals
Theorem: Array.zipWithAux_cons_cons_succ
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
⊢ zipWithAux f (cons a x) (cons b y) (n + 1) z = zipWithAux f x y n z
Tactic:
unfold zipWithAux
Proof state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
⊢ (if h : n + 1 < size (cons a x) then
      let a_1 := (cons a x)[n + 1];
      if h : n + 1 < size (cons b y) then
        let b_1 := (cons b y)[n + 1];
        zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f a_1 b_1))
      else z
    else z) =
    if h : n < size x then
      let a := x[n];
      if h : n < size y then
        let b := y[n];
        zipWithAux f x y (n + 1) (push z (f a b))
      else z
    else z