Simprocs for the Working Mathematician

[giscus[bot]]

Simprocs for the Working Mathematician

Informal introduction to simprocs and what they are useful for

https://leanprover-community.github.io/blog/posts/simprocs-for-the-working-mathematician/

[Louddy]

Thank you for the blog post.
I have a quick question about Finset.Icc_ofNat_ofNat, what is the limitation preventing the last example from going through? Could the simproc be made to work with variables?

[vasnesterov]

Thank you for the post!
I think there is a slight inaccuracy in the first example about reduceIte. In the simp only call, simp “knows” only the lemmas that are explicitly passed to it, and it does not use the mul_zero lemma. Instead, it relies on the fact that 37 * 0 is definitionally equal to 0. This is why the example does not work for (if (37 : ℤ) * 0 = 0 then 1 else 2) = 1.