Zulip Chat Archive

Stream: maths

Topic: non-terminal simp in complex.lean


view this post on Zulip Kevin Buzzard (May 25 2019 at 18:54):

The proof that the complex numbers form a ring here

https://github.com/leanprover-community/mathlib/blob/c6a7f300ea43cfc0478e3ee81a141d5288d90df6/src/data/complex/basic.lean#L190

goes "to check all the axioms, it suffices to show the real and imaginary parts are equal, which we do by ring; however to get the real and imaginary parts into a form where ring will work, we use a non-terminating simp".

I was trying to write complex.lean without looking at complex.lean and I independently decided that the simp, ring idea would be a pretty painless way to do it. But is it bad style? Obviously one could write suffices : blah, by simpa ten or more times, but that would look really inelegant.

view this post on Zulip Johan Commelin (May 25 2019 at 18:57):

What does squeeze_simp say?

view this post on Zulip Reid Barton (May 25 2019 at 19:01):

Personally I think stuff like simp, refl or simp, ring or simp, cc is fine. It could break, but if it does it will probably be obvious how to repair it.

view this post on Zulip Rob Lewis (May 25 2019 at 19:19):

The slogan is "avoid nonterminal simp," but the intention is to avoid following a simp call with a tactic that's sensitive to the exact shape of the goal. Minor changes to the simp set are less likely to break ring than rw, apply, etc.


Last updated: May 09 2021 at 09:11 UTC