Theorem: LoVe.List.countp.go_accum (LoVe/LoVelib.lean)

State before:
α : Type
p : α → Bool
as : List α
acc : ℕ
⊢ List.countp.go p as acc = List.countp p as + acc
Tactic:
induction as generalizing acc with
| nil           => simp [List.countp.go, List.countp]
| cons a as' ih =>
  simp [List.countp, List.countp.go]
  cases Classical.em (p a) with
  | inl hp =>
    simp [hp, ih]
    ac_rfl
  | inr hp => simp [hp, ih]
State after:
no goals

State before:
case nil
α : Type
p : α → Bool
acc : ℕ
⊢ List.countp.go p [] acc = List.countp p [] + acc
Tactic:
simp [List.countp.go, List.countp]
State after:
no goals

State before:
case cons
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
⊢ List.countp.go p (a :: as') acc = List.countp p (a :: as') + acc
Tactic:
simp [List.countp, List.countp.go]
State after:
case cons
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
⊢ (bif p a then List.countp.go p as' (acc + 1) else List.countp.go p as' acc) =
    (bif p a then List.countp.go p as' 1 else List.countp.go p as' 0) + acc

State before:
case cons
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
⊢ (bif p a then List.countp.go p as' (acc + 1) else List.countp.go p as' acc) =
    (bif p a then List.countp.go p as' 1 else List.countp.go p as' 0) + acc
Tactic:
cases Classical.em (p a) with
| inl hp =>
  simp [hp, ih]
  ac_rfl
| inr hp => simp [hp, ih]
State after:
no goals

State before:
case cons.inl
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
hp : p a = true
⊢ (bif p a then List.countp.go p as' (acc + 1) else List.countp.go p as' acc) =
    (bif p a then List.countp.go p as' 1 else List.countp.go p as' 0) + acc
Tactic:
simp [hp, ih]
State after:
case cons.inl
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
hp : p a = true
⊢ List.countp p as' + (acc + 1) = List.countp p as' + 1 + acc

State before:
case cons.inl
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
hp : p a = true
⊢ List.countp p as' + (acc + 1) = List.countp p as' + 1 + acc
Tactic:
ac_rfl
State after:
no goals

State before:
case cons.inr
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
hp : ¬p a = true
⊢ (bif p a then List.countp.go p as' (acc + 1) else List.countp.go p as' acc) =
    (bif p a then List.countp.go p as' 1 else List.countp.go p as' 0) + acc
Tactic:
simp [hp, ih]
State after:
no goals