Working with complex numbers

Stream: new members

[Martin C. Martin]

The following fails with a deterministic timeout:

import data.complex.basic
open complex

#reduce (complex.mk 2 3) * (complex.mk 4 5)
#reduce 2 + 3 * I

If I use #eval instead, it says result type does not have an instance of type class 'has_repr', dumping internal representation.

Also, simp and norm_num don't seem to know about complex numbers; I need to use ext to turn it into two similar problems involving reals:

import data.complex.basic
open complex

example : 2 + 3 * I = (complex.mk 2 3) := by {ext; simp}
example : (complex.mk 2 3) * (complex.mk 4 5) = (complex.mk (-7) 22) := by {ext; norm_num}

Is there a one-tactic proof for such simple examples?

[Alex J. Best]

Using complex.mk feels a bit low-tech to me, proving things about 3 + 2 * I seems more natural.
Probably these calculations are in scope for norm_num but someone would have to write an extension for it I guess.
ext; norm_num is pretty quick to write so there doesn't seem to be too pressing a need for it though

[Alex J. Best]

And in general as soon as you get to sufficiently complicated objects (e.g. reals) #reduce and #eval aren't so useful (how would you print an arbitrary real number!), there are many threads about this here but thats why we added commands like #norm_num for people to get this "calculator style" output

[Martin C. Martin]

Thanks! #norm_num doesn't seem to actually do the multiplication though, it just returns it's input:

#norm_num (complex.mk 2 3) * (complex.mk 4 5)
#norm_num (2 + 3 * I) * (4 + 5 * I)

[Martin C. Martin]

Glad to hear that ext; norm_num is canonical in this case, I'll use that.

[Alex J. Best]

#norm_num will just show you what norm num does, so without a plugin being written it indeed doesn't work well. I just mean in general for this sort of explicit evaluation thing that may serve you better than #reduce