Theorem: List.countp.go_acc (One.lean)

State before:
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
acc : ℕ
⊢ go p l acc = acc + go p l 0
Tactic:
induction l generalizing acc with
| nil => unfold go; simp
| cons head tail ih =>
  unfold go
  cases p head with
  | true => simp only [@ih (acc + 1), add_assoc, zero_le, ge_iff_le, nonpos_iff_eq_zero, cond_true, zero_add, @ih 1]
  | false => simp only [@ih acc, zero_le, ge_iff_le, nonpos_iff_eq_zero, cond_false, zero_add]
State after:
no goals

State before:
case nil
α✝ : Type u_1
p : α✝ → Bool
acc : ℕ
⊢ go p [] acc = acc + go p [] 0
Tactic:
unfold go
State after:
case nil
α✝ : Type u_1
p : α✝ → Bool
acc : ℕ
⊢ acc = acc + 0

State before:
case nil
α✝ : Type u_1
p : α✝ → Bool
acc : ℕ
⊢ acc = acc + 0
Tactic:
simp
State after:
no goals

State before:
case cons
α✝ : Type u_1
p : α✝ → Bool
head : α✝
tail : List α✝
ih : ∀ {acc : ℕ}, go p tail acc = acc + go p tail 0
acc : ℕ
⊢ go p (head :: tail) acc = acc + go p (head :: tail) 0
Tactic:
unfold go
State after:
case cons
α✝ : Type u_1
p : α✝ → Bool
head : α✝
tail : List α✝
ih : ∀ {acc : ℕ}, go p tail acc = acc + go p tail 0
acc : ℕ
⊢ (bif p head then go p tail (acc + 1) else go p tail acc) = acc + bif p head then go p tail (0 + 1) else go p tail 0

State before:
case cons
α✝ : Type u_1
p : α✝ → Bool
head : α✝
tail : List α✝
ih : ∀ {acc : ℕ}, go p tail acc = acc + go p tail 0
acc : ℕ
⊢ (bif p head then go p tail (acc + 1) else go p tail acc) = acc + bif p head then go p tail (0 + 1) else go p tail 0
Tactic:
cases p head with
| true => simp only [@ih (acc + 1), add_assoc, zero_le, ge_iff_le, nonpos_iff_eq_zero, cond_true, zero_add, @ih 1]
| false => simp only [@ih acc, zero_le, ge_iff_le, nonpos_iff_eq_zero, cond_false, zero_add]
State after:
no goals

State before:
case cons.true
α✝ : Type u_1
p : α✝ → Bool
head : α✝
tail : List α✝
ih : ∀ {acc : ℕ}, go p tail acc = acc + go p tail 0
acc : ℕ
⊢ (bif true then go p tail (acc + 1) else go p tail acc) = acc + bif true then go p tail (0 + 1) else go p tail 0
Tactic:
simp only [@ih (acc + 1), add_assoc, zero_le, ge_iff_le, nonpos_iff_eq_zero, cond_true, zero_add, @ih 1]
State after:
no goals

State before:
case cons.false
α✝ : Type u_1
p : α✝ → Bool
head : α✝
tail : List α✝
ih : ∀ {acc : ℕ}, go p tail acc = acc + go p tail 0
acc : ℕ
⊢ (bif false then go p tail (acc + 1) else go p tail acc) = acc + bif false then go p tail (0 + 1) else go p tail 0
Tactic:
simp only [@ih acc, zero_le, ge_iff_le, nonpos_iff_eq_zero, cond_false, zero_add]
State after:
no goals