complex.ext_iff a simp lemma?

Stream: maths

[Kevin Buzzard]

Should complex.ext_iff be a simp lemma? In data.complex.basic I added the attribute to it, and the following happened: two proofs broke, but they were easily fixed (one became shorter), and about 20 proofs could be changed from ext_iff.2 $ by simp to by simp. I then tried compiling the rest of mathlib and a bunch of stuff had broken. I cannot currently contemplate fixing it, but I was just interested in hearing the community's ideas about whether this is a bad idea in general. The lemma says z = w ↔ z.re = w.re ∧ z.im = w.im. In the complex number game it seems to work fine.

[Scott Morrison]

Doesn't sound like a good idea to me. You won't ever be able to reason about equality of complex numbers without having the argue separately about their real and imaginary parts...

[Scott Morrison]

When you're first setting up complex numbers in terms of pairs of real numbers, it's great and helpful. Less so once you want to seal off that implementation detail! :-)

[Sebastien Gouezel]

Instead, you could use local attribute [simp] ext_iff just in this file.

[Kevin Buzzard]

I think that making it a local attribute is a great idea, because it really makes data.complex.basic look a lot sexier.

[Scott Morrison]

There's a slight counter argument: that having _all_ the proofs in a good introductory pedagogical file consist of by simp may induce superstition about the power of simp. :-)

[Scott Morrison]

At least by { ext; simp } may lead people to understand: "think about it in components; then it's easy".

[Kevin Buzzard]

That's an interesting counter-argument.

[Kevin Buzzard]

So I see that there is no module docstring either, and the doc_blame linter is actually complaining a lot, so at some point when marking is over in a few days I will probably fix this up; to be quite honest I even prefer by {ext; simp} to what we currently have, but I am looking at this from a different point of view to some people, perhaps (for all I know I just put compilation time up by 20% which might be a cardinal sin)

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/tree/complex-tidyup ; I won't make a PR until I've added the module docstrong (and won't make a PR of this edit at all if people think that ext_iff.2 $ by simp is better). In the complex number game I'll perhaps play with the idea when I'm streaming live

[Reid Barton]

On a somewhat related note, I wonder whether ext should only locally be an ext lemma.

[Reid Barton]

If you have two, I don't know, bundled holomorphic functions and you want to prove they're equal because they're pointwise equal, probably you do not want to split into real and imaginary components.