New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - fix(data/list/basic): Ensure that ball_cons actually works as a simp lemma #4281
Conversation
…l_cons` are synonyms
…lemma The LHS of ball_cons (aka forall_mem_cons) is not in simp-normal form, as `mem_cons_iff` rewrites it. This adds a new simp lemma which is the form that `mem_cons_iff` rewrites it to.
I think we don't need |
I agree, although there are a few places that refer to it directly by name. If CI passes on this one, I'll come back and:
I'm expecting the worst given the behavior of lemmas in #4143, which is a similar sort of change. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
bors r+
…lemma (#4281) The LHS of the simp lemma `list.ball_cons` (aka `list.forall_mem_cons`) is not in simp-normal form, as `list.mem_cons_iff` rewrites it. This adds a new simp lemma which is the form that `list.mem_cons_iff` rewrites it to.
Pull request successfully merged into master. Build succeeded: |
The LHS of the simp lemma
list.ball_cons
(akalist.forall_mem_cons
) is not in simp-normal form, aslist.mem_cons_iff
rewrites it.This adds a new simp lemma which is the form that
list.mem_cons_iff
rewrites it to.https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Case-bashing.20.60list.2Epairwise.60.20with.20.60simp.60/near/211276203
First commit is #4279