## Stream: maths

### Topic: non-terminal simp in complex.lean

#### 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.

#### Johan Commelin (May 25 2019 at 18:57):

What does squeeze_simp say?

#### 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.

#### 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