Zulip Chat Archive

Stream: maths

Topic: complex.ext_iff a simp lemma?


view this post on Zulip Kevin Buzzard (May 28 2020 at 14:05):

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.

view this post on Zulip Scott Morrison (May 28 2020 at 14:06):

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

view this post on Zulip Scott Morrison (May 28 2020 at 14:07):

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! :-)

view this post on Zulip Sebastien Gouezel (May 28 2020 at 14:08):

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

view this post on Zulip Kevin Buzzard (May 28 2020 at 14:11):

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

view this post on Zulip Scott Morrison (May 28 2020 at 14:13):

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. :-)

view this post on Zulip Scott Morrison (May 28 2020 at 14:13):

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

view this post on Zulip Kevin Buzzard (May 28 2020 at 14:19):

That's an interesting counter-argument.

view this post on Zulip Kevin Buzzard (May 28 2020 at 14:22):

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)

view this post on Zulip Kevin Buzzard (May 28 2020 at 14:25):

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

view this post on Zulip Reid Barton (May 28 2020 at 14:29):

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

view this post on Zulip Reid Barton (May 28 2020 at 14:31):

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.


Last updated: May 18 2021 at 06:15 UTC