refactor: make List.length_eq_countP_add_countP avoid Prop
#808
Conversation
|
Is this repo accepting PRs that could break downstream? Is there anything I need to do to make sure mathlib doesn't break here? |
BoltonBailey
changed the title
List.length_eq_countP_add_countP avoid Prop
|
WIP |
There's a bot that will add a merge-conflict label if this is an issue. |
| theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (fun a => ! p a) l := by | ||
| induction l with | ||
| | nil => rfl | ||
| | cons x h ih => | ||
| if h : p x then | ||
| rw [countP_cons_of_pos _ _ h, countP_cons_of_neg _ _ _, length, ih] | ||
| · rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc] | ||
| · simp only [h, not_true_eq_false, decide_False, not_false_eq_true] | ||
| · simp only [h, not_true_eq_false, decide_False, not_false_eq_true, Bool.not_true, | ||
| Bool.false_eq_true, not_false_eq_true] | ||
| else | ||
| rw [countP_cons_of_pos (fun a => ¬p a) _ _, countP_cons_of_neg _ _ h, length, ih] | ||
| rw [countP_cons_of_pos (fun a => ! p a) _ _, countP_cons_of_neg _ _ h, length, ih] | ||
| · rfl | ||
| · simp only [h, not_false_eq_true, decide_True] | ||
| · simp only [h, not_false_eq_true, decide_True, Bool.not_false] |
There was a problem hiding this comment.
Simplified proof:
theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (!p ·) l := by
induction l with
| nil => rfl
| cons x _ _ => cases h : p x <;> simp_arith [*]
On second thoughts, I might help to make one of those testing PRs in mathlib. I was asked to make this for another PR. Im such a PR, one basically changes the repository's batteries dependency to one's own fork and PR branch in Mathlib's lakefile and lake manifest |
leanprover-community-mathlib4-bot
added
the
merge-conflict
Changes this lemma to use boolean not rather than propositional not.