non-terminal simp in complex.lean

Stream: maths

[Kevin Buzzard]

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.

[Johan Commelin]

What does squeeze_simp say?

[Reid Barton]

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.

[Rob Lewis]

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.