internlm/Lean-Github huggingface dataset:
Theorem: Array.init_succ
Proof state before:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
ih :
  i ≤ n →
    ∀ (o : Array α),
      size o = n - i →
        Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
            (Nat.succ i) (n - i) ⋯ o =
          push
            (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i (n - i) ⋯
              o)
            (f { val := n, isLt := ⋯ })
hi : Nat.succ i ≤ n
o : Array α
ho : size o = n - Nat.succ i
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
⊢ n - Nat.succ i + 1 = n - i
Tactic:
simp [Nat.sub_succ]
Proof state after:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
ih :
  i ≤ n →
    ∀ (o : Array α),
      size o = n - i →
        Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
            (Nat.succ i) (n - i) ⋯ o =
          push
            (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i (n - i) ⋯
              o)
            (f { val := n, isLt := ⋯ })
hi : Nat.succ i ≤ n
o : Array α
ho : size o = n - Nat.succ i
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
⊢ Nat.pred (n - i) + 1 = n - i
Theorem: Array.init_succ
Proof state before:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
ih :
  i ≤ n →
    ∀ (o : Array α),
      size o = n - i →
        Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
            (Nat.succ i) (n - i) ⋯ o =
          push
            (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i (n - i) ⋯
              o)
            (f { val := n, isLt := ⋯ })
hi : Nat.succ i ≤ n
o : Array α
ho : size o = n - Nat.succ i
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
⊢ Nat.pred (n - i) + 1 = n - i
Tactic:
rw [Nat.add_one, Nat.succ_pred_eq_of_pos (Nat.zero_lt_sub_of_lt hi)]
Proof state after:
no goals
Theorem: Array.mem_push
Proof state before:
α : Type u_1
A : Array α
x y : α
⊢ y ∈ push A x ↔ y ∈ A ∨ y = x
Tactic:
simp [push, Array.mem_def]
Proof state after:
no goals
Theorem: Array.size_init
Proof state before:
n : Nat
α✝ : Type u_1
f : Fin n → α✝
⊢ size (init n f) = n
Tactic:
induction n
Proof state after:
case zero
α✝ : Type u_1
f : Fin Nat.zero → α✝
⊢ size (init Nat.zero f) = Nat.zero

case succ
α✝ : Type u_1
n✝ : Nat
n_ih✝ : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init (Nat.succ n✝) f) = Nat.succ n✝
Theorem: Array.size_init
Proof state before:
case zero
α✝ : Type u_1
f : Fin Nat.zero → α✝
⊢ size (init Nat.zero f) = Nat.zero

case succ
α✝ : Type u_1
n✝ : Nat
n_ih✝ : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init (Nat.succ n✝) f) = Nat.succ n✝
Tactic:
. simp [size, init_zero]
Proof state after:
case succ
α✝ : Type u_1
n✝ : Nat
n_ih✝ : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init (Nat.succ n✝) f) = Nat.succ n✝
Theorem: Array.size_init
Proof state before:
case succ
α✝ : Type u_1
n✝ : Nat
n_ih✝ : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init (Nat.succ n✝) f) = Nat.succ n✝
Tactic:
. next ih =>
  simp [init_succ]; exact ih
Proof state after:
no goals
Theorem: Array.size_init
Proof state before:
case zero
α✝ : Type u_1
f : Fin Nat.zero → α✝
⊢ size (init Nat.zero f) = Nat.zero
Tactic:
simp [size, init_zero]
Proof state after:
no goals
Theorem: Array.size_init
Proof state before:
case succ
α✝ : Type u_1
n✝ : Nat
n_ih✝ : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init (Nat.succ n✝) f) = Nat.succ n✝
Tactic:
next ih =>
simp [init_succ]; exact ih
Proof state after:
no goals
Theorem: Array.size_init
Proof state before:
α✝ : Type u_1
n✝ : Nat
ih : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init (Nat.succ n✝) f) = Nat.succ n✝
Tactic:
simp [init_succ]
Proof state after:
α✝ : Type u_1
n✝ : Nat
ih : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init n✝ fun i => f { val := ↑i, isLt := ⋯ }) = n✝
Theorem: Array.size_init
Proof state before:
α✝ : Type u_1
n✝ : Nat
ih : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init n✝ fun i => f { val := ↑i, isLt := ⋯ }) = n✝
Tactic:
exact ih
Proof state after:
no goals
Theorem: Array.get_init
Proof state before:
n : Nat
α✝ : Type u_1
f : Fin n → α✝
i : Nat
h : i < size (init n f)
⊢ (init n f)[i] = f { val := i, isLt := ⋯ }
Tactic:
induction n generalizing i with
| zero => simp at h; exact False.elim <| Nat.not_lt_zero _ h
| succ n ih =>
  simp [init_succ, get_push]
  split
  next h =>
    have := @ih (fun i => f ⟨i,Nat.lt_trans i.isLt (by exact Nat.le_refl _)⟩) i (by simp; assumption)
    simp at this ⊢
    rw [this]
  next h' =>
    simp at h'
    have : i = n := Nat.le_antisymm
      (Nat.le_of_succ_le_succ (by rw [size_init] at h; exact h))
      h'
    cases this
    congr
Proof state after:
no goals
Theorem: Array.get_init
Proof state before:
case zero
α✝ : Type u_1
f : Fin Nat.zero → α✝
i : Nat
h : i < size (init Nat.zero f)
⊢ (init Nat.zero f)[i] = f { val := i, isLt := ⋯ }
Tactic:
simp at h
Proof state after:
case zero
α✝ : Type u_1
f : Fin Nat.zero → α✝
i : Nat
h✝ : i < size (init Nat.zero f)
h : i < 0
⊢ (init Nat.zero f)[i] = f { val := i, isLt := ⋯ }
Theorem: Array.get_init
Proof state before:
case zero
α✝ : Type u_1
f : Fin Nat.zero → α✝
i : Nat
h✝ : i < size (init Nat.zero f)
h : i < 0
⊢ (init Nat.zero f)[i] = f { val := i, isLt := ⋯ }
Tactic:
exact False.elim <| Nat.not_lt_zero _ h
Proof state after:
no goals
Theorem: Array.get_init
Proof state before:
case succ
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
⊢ (init (Nat.succ n) f)[i] = f { val := i, isLt := ⋯ }
Tactic:
simp [init_succ, get_push]
Proof state after:
case succ
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
⊢ (if h : i < n then (init n fun i => f { val := ↑i, isLt := ⋯ })[i] else f { val := n, isLt := ⋯ }) =
    f { val := i, isLt := ⋯ }
Theorem: Array.get_init
Proof state before:
case succ
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
⊢ (if h : i < n then (init n fun i => f { val := ↑i, isLt := ⋯ })[i] else f { val := n, isLt := ⋯ }) =
    f { val := i, isLt := ⋯ }
Tactic:
split
Proof state after:
case succ.inl
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h✝ : i < n
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }

case succ.inr
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h✝ : ¬i < n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Theorem: Array.get_init
Proof state before:
case succ.inl
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h✝ : i < n
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }

case succ.inr
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h✝ : ¬i < n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Tactic:
next h =>
  have := @ih (fun i => f ⟨i,Nat.lt_trans i.isLt (by exact Nat.le_refl _)⟩) i (by simp; assumption)
  simp at this ⊢
  rw [this]
Proof state after:
case succ.inr
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h✝ : ¬i < n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Theorem: Array.get_init
Proof state before:
case succ.inr
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h✝ : ¬i < n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Tactic:
next h' =>
  simp at h'
  have : i = n := Nat.le_antisymm
    (Nat.le_of_succ_le_succ (by rw [size_init] at h; exact h))
    h'
  cases this
  congr
Proof state after:
no goals
Theorem: Array.get_init
Proof state before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }
Tactic:
have := @ih (fun i => f ⟨i,Nat.lt_trans i.isLt (by exact Nat.le_refl _)⟩) i (by simp; assumption)
Proof state after:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
this : (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := ↑{ val := i, isLt := ⋯ }, isLt := ⋯ }
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }
Theorem: Array.get_init
Proof state before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
this : (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := ↑{ val := i, isLt := ⋯ }, isLt := ⋯ }
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }
Tactic:
simp at this ⊢
Proof state after:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
this : (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }
Theorem: Array.get_init
Proof state before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
this : (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }
Tactic:
rw [this]
Proof state after:
no goals
Theorem: Array.get_init
Proof state before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i✝ : Nat
h✝ : i✝ < size (init (Nat.succ n) f)
h : i✝ < n
i : Fin n
⊢ n < Nat.succ n
Tactic:
exact Nat.le_refl _
Proof state after:
no goals
Theorem: Array.get_init
Proof state before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
⊢ i < size (init n fun i => f { val := ↑i, isLt := ⋯ })
Tactic:
simp
Proof state after:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
⊢ i < n
Theorem: Array.get_init
Proof state before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
⊢ i < n
Tactic:
assumption
Proof state after:
no goals
Theorem: Array.get_init
Proof state before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h' : ¬i < n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Tactic:
simp at h'
Proof state after:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h' : n ≤ i
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Theorem: Array.get_init
Proof state before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h' : n ≤ i
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Tactic:
have : i = n := Nat.le_antisymm
  (Nat.le_of_succ_le_succ (by rw [size_init] at h; exact h))
  h'
Proof state after:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h' : n ≤ i
this : i = n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Theorem: Array.get_init
Proof state before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h' : n ≤ i
this : i = n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Tactic:
cases this
Proof state after:
case refl
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
h : n < size (init (Nat.succ n) f)
h' : n ≤ n
⊢ f { val := n, isLt := ⋯ } = f { val := n, isLt := ⋯ }
Theorem: Array.get_init
Proof state before:
case refl
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
h : n < size (init (Nat.succ n) f)
h' : n ≤ n
⊢ f { val := n, isLt := ⋯ } = f { val := n, isLt := ⋯ }
Tactic:
congr
Proof state after:
no goals
Theorem: Array.get_init
Proof state before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h' : n ≤ i
⊢ Nat.succ i ≤ Nat.succ n
Tactic:
rw [size_init] at h
Proof state after:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < Nat.succ n
h' : n ≤ i
⊢ Nat.succ i ≤ Nat.succ n
Theorem: Array.get_init
Proof state before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < Nat.succ n
h' : n ≤ i
⊢ Nat.succ i ≤ Nat.succ n
Tactic:
exact h
Proof state after:
no goals
Theorem: Array.size_pop?
Proof state before:
α✝ : Type u_1
A' : Array α✝
a : α✝
A : Array α✝
⊢ pop? A = some (A', a) → size A' + 1 = size A
Tactic:
rcases A with ⟨h,t⟩
  <;> simp [pop?, back?, getElem?, pop]
Proof state after:
case mk.cons
α✝ : Type u_1
A' : Array α✝
a head✝ : α✝
tail✝ : List α✝
⊢ { data := List.dropLast (head✝ :: tail✝) } = A' →
    { data := head✝ :: tail✝ }[List.length tail✝] = a → size A' = List.length tail✝
Theorem: Array.size_pop?
Proof state before:
case mk.cons
α✝ : Type u_1
A' : Array α✝
a head✝ : α✝
tail✝ : List α✝
⊢ { data := List.dropLast (head✝ :: tail✝) } = A' →
    { data := head✝ :: tail✝ }[List.length tail✝] = a → size A' = List.length tail✝
Tactic:
rintro rfl
Proof state after:
case mk.cons
α✝ : Type u_1
a head✝ : α✝
tail✝ : List α✝
⊢ { data := head✝ :: tail✝ }[List.length tail✝] = a →
    size { data := List.dropLast (head✝ :: tail✝) } = List.length tail✝
Theorem: Array.size_pop?
Proof state before:
case mk.cons
α✝ : Type u_1
a head✝ : α✝
tail✝ : List α✝
⊢ { data := head✝ :: tail✝ }[List.length tail✝] = a →
    size { data := List.dropLast (head✝ :: tail✝) } = List.length tail✝
Tactic:
simp
Proof state after:
no goals
Theorem: Array.mkArray_succ
Proof state before:
α : Type u_1
n : Nat
a : α
⊢ mkArray (n + 1) a = #[a] ++ mkArray n a
Tactic:
apply Array.ext'
Proof state after:
case h
α : Type u_1
n : Nat
a : α
⊢ (mkArray (n + 1) a).data = (#[a] ++ mkArray n a).data
Theorem: Array.mkArray_succ
Proof state before:
case h
α : Type u_1
n : Nat
a : α
⊢ (mkArray (n + 1) a).data = (#[a] ++ mkArray n a).data
Tactic:
simp
Proof state after:
no goals
Theorem: Array.mkArray_succ'
Proof state before:
α : Type u_1
n : Nat
a : α
⊢ mkArray (n + 1) a = push (mkArray n a) a
Tactic:
apply Array.ext'
Proof state after:
case h
α : Type u_1
n : Nat
a : α
⊢ (mkArray (n + 1) a).data = (push (mkArray n a) a).data
Theorem: Array.mkArray_succ'
Proof state before:
case h
α : Type u_1
n : Nat
a : α
⊢ (mkArray (n + 1) a).data = (push (mkArray n a) a).data
Tactic:
simp [mkArray_data, List.replicate]
Proof state after:
case h
α : Type u_1
n : Nat
a : α
⊢ a :: List.replicate n a = List.replicate n a ++ [a]
Theorem: Array.mkArray_succ'
Proof state before:
case h
α : Type u_1
n : Nat
a : α
⊢ a :: List.replicate n a = List.replicate n a ++ [a]
Tactic:
induction n with
| zero => rfl
| succ n ih => simp; exact ih
Proof state after:
no goals
Theorem: Array.mkArray_succ'
Proof state before:
case h.zero
α : Type u_1
a : α
⊢ a :: List.replicate Nat.zero a = List.replicate Nat.zero a ++ [a]
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.mkArray_succ'
Proof state before:
case h.succ
α : Type u_1
a : α
n : Nat
ih : a :: List.replicate n a = List.replicate n a ++ [a]
⊢ a :: List.replicate (Nat.succ n) a = List.replicate (Nat.succ n) a ++ [a]
Tactic:
simp
Proof state after:
case h.succ
α : Type u_1
a : α
n : Nat
ih : a :: List.replicate n a = List.replicate n a ++ [a]
⊢ a :: List.replicate n a = List.replicate n a ++ [a]
Theorem: Array.mkArray_succ'
Proof state before:
case h.succ
α : Type u_1
a : α
n : Nat
ih : a :: List.replicate n a = List.replicate n a ++ [a]
⊢ a :: List.replicate n a = List.replicate n a ++ [a]
Tactic:
exact ih
Proof state after:
no goals
Theorem: Array.foldl_empty
Proof state before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
⊢ foldl f init #[] start stop = init
Tactic:
simp [foldl, foldlM, Id.run]
Proof state after:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init
Theorem: Array.foldl_empty
Proof state before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init
Tactic:
by_cases h : stop = 0
Proof state after:
case pos
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : stop = 0
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init

case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init
Theorem: Array.foldl_empty
Proof state before:
case pos
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : stop = 0
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init
Tactic:
simp [h, foldlM.loop]
Proof state after:
no goals
Theorem: Array.foldl_empty
Proof state before:
case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init
Tactic:
simp [h]
Proof state after:
case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ foldlM.loop f #[] 0 ⋯ 0 start init = init
Theorem: Array.foldl_empty
Proof state before:
case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ foldlM.loop f #[] 0 ⋯ 0 start init = init
Tactic:
unfold foldlM.loop
Proof state after:
case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ (if hlt : start < 0 then
      match 0 with
      | 0 => pure init
      | Nat.succ i' =>
        let_fun this := ⋯;
        do
        let __do_lift ← f init #[][start]
        foldlM.loop f #[] 0 ⋯ i' (start + 1) __do_lift
    else pure init) =
    init
Theorem: Array.foldl_empty
Proof state before:
case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ (if hlt : start < 0 then
      match 0 with
      | 0 => pure init
      | Nat.succ i' =>
        let_fun this := ⋯;
        do
        let __do_lift ← f init #[][start]
        foldlM.loop f #[] 0 ⋯ i' (start + 1) __do_lift
    else pure init) =
    init
Tactic:
simp [Nat.not_lt_zero start]
Proof state after:
no goals
Theorem: Array.foldl_cons
Proof state before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
a : α
as : List α
⊢ foldl f init { data := a :: as } 0 = foldl f (f init a) { data := as } 0
Tactic:
simp only [foldl_eq_foldl_data]
Proof state after:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
a : α
as : List α
⊢ List.foldl f init (a :: as) = List.foldl f (f init a) as
Theorem: Array.foldl_cons
Proof state before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
a : α
as : List α
⊢ List.foldl f init (a :: as) = List.foldl f (f init a) as
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.foldl_append
Proof state before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A B : Array α
⊢ foldl f init (A ++ B) 0 = foldl f (foldl f init A 0) B 0
Tactic:
have ⟨A⟩ := A
Proof state after:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B : Array α
A : List α
⊢ foldl f init ({ data := A } ++ B) 0 = foldl f (foldl f init { data := A } 0) B 0
Theorem: Array.foldl_append
Proof state before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B : Array α
A : List α
⊢ foldl f init ({ data := A } ++ B) 0 = foldl f (foldl f init { data := A } 0) B 0
Tactic:
have ⟨B⟩ := B
Proof state after:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B✝ : Array α
A B : List α
⊢ foldl f init ({ data := A } ++ { data := B }) 0 = foldl f (foldl f init { data := A } 0) { data := B } 0
Theorem: Array.foldl_append
Proof state before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B✝ : Array α
A B : List α
⊢ foldl f init ({ data := A } ++ { data := B }) 0 = foldl f (foldl f init { data := A } 0) { data := B } 0
Tactic:
simp only [foldl_eq_foldl_data, append_data]
Proof state after:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B✝ : Array α
A B : List α
⊢ List.foldl f init (A ++ B) = List.foldl f (List.foldl f init A) B
Theorem: Array.foldl_append
Proof state before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B✝ : Array α
A B : List α
⊢ List.foldl f init (A ++ B) = List.foldl f (List.foldl f init A) B
Tactic:
exact List.foldl_append _ _ _ _
Proof state after:
no goals
Theorem: Array.size_set!
Proof state before:
α : Type u_1
A : Array α
i : Nat
v : α
⊢ size (set! A i v) = size A
Tactic:
rw [set!, Array.size_setD]
Proof state after:
no goals
Theorem: List.length_fins
Proof state before:
n : Nat
⊢ length (fins n) = n
Tactic:
unfold fins
Proof state after:
n : Nat
⊢ length (fins.finsAux n n ⋯ []) = n
Theorem: List.length_fins
Proof state before:
n : Nat
⊢ length (fins.finsAux n n ⋯ []) = n
Tactic:
suffices ∀ i (hi : i ≤ n) acc, length (fins.finsAux n i hi acc) = length acc + i
  by have := this n (Nat.le_refl _) []; simp at this; exact this
Proof state after:
n : Nat
⊢ ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i