Teaching norm_num about complex numbers

Stream: metaprogramming / tactics

[Julian Berman]

Hi. @Shing Tak Lam already gave me some helpful pointers to track this down, but I'm afraid I don't know enough to get it over the finishing line yet.

I noticed that norm_num can't solve arithmetic equations in complex numbers despite its docstring seemingly saying it should (my original example was example : (2 + 3 * I) * (4 + 5 * I) = -7 + 22 * I := by norm_num which does not work without by ext; norm_num).

Two questions:

1) Is this indeed within the intended scope of norm_num? Its docstring does seem to say "Supports the operations + - * / ^ and % over numerical types such as ℕ, ℤ, ℚ, ℝ, ℂ".
2) Assuming it is, I added the failing example : complex.I ≠ 2 := by norm_num to test/norm_num.lean -- is the right way to fix this say to try calling tactic.ext within norm_num1 and if it succeeds recurse into each of the constructors with what's done today? (If so, can I have a hint as to how that's done?) Or should I try to figure out a way to add a @[norm_num] extension to data.complex specific to complex numbers? I can't quite tell whether the latter is precisely meant for this use case, it seems to talk about being used for new functions really, not types.

[Mario Carneiro]

norm_num does not support complex number arithmetic. It supports the operations + - * etc over ℂ, but I is not supported so you can prove (2 + 2 : ℂ) = 4 but not (2 + I) * I = -1 + 2 * I

[Mario Carneiro]

One general way to handle it would be to use the grobner tactic (that doesn't exist) to prove ring equalities in C given the equation I * I + 1 = 0

[Julian Berman]

Got it, so it's indeed not in the intended scope sounds like, thanks. Would a docstring fix be welcome then, I don't think I was the only one slightly confused by the way it's phrased now. Maybe even just "Supports the operations + - * / ^ and % over numerical types such as ℕ, ℤ, ℚ, ℝ, and partially over ℂ"?

[Mario Carneiro]

Adding new types to norm_num can be done, but it is tricky if the set of normal forms needs to be expanded. Most of it assumes that normal forms are numerals with maybe a minus sign (for integers) or fraction (for rationals), over any type (i.e. 3 / 5 : ℝ is a normal form but not pi : ℝ). Adding complex numbers would require some specific recognizable normal form that matches the existing one for real numbers

[Julian Berman]

Ah interesting ok, so my wording up top isn't appropriate then either -- it's about whether it's a numeric literal moreso than what type it is?

[Mario Carneiro]

yes

[Mario Carneiro]

you can do "rational number arithmetic" proofs over any field

[Julian Berman]

nod thanks I think that's making some more sense now -- Though, just because I thought of this playfully yesterday when playing around and you mentioned it -- by "recognizable normal form" -- does that have to be across all types? E.g. if you encode complexes by say concatenating the digits of the real and imaginary parts with some numeric separator like 00 does that "work" (preserve the type info) or does that mean that now norm_num will think (1 + 2i) = (1002 : R)?

[Kevin Buzzard]

For complexes you can just use ext then simp then norm_num

[Julian Berman]

Right I know that works (it was what Shing or Bhavik told me to use instead of ring + simp) I was mostly asking to see whether norm_num should have worked alone, which the docstring to us I think seemed like it should have.

[Julian Berman]

But I think I follow how to read it now at least.

[Mario Carneiro]

I'm not sure I understand your suggestion. The normal form has to be sound, at least - any expression that can be normalized should normalize to a normal form that is provably equal to the original. Your 1002 example doesn't satisfy that

[Mario Carneiro]

One example of a normal form is <numeral> + <numeral> * I, but an issue with this representation is that it includes operations that norm_num understands, so it will attempt to add and multiply the components, resulting in added busywork

[Mario Carneiro]

also you might want to support other kinds of square roots as well, not just I

[Mario Carneiro]

but the normal form for quadratic algebraics gets a lot more complicated

[Julian Berman]

I see. My misunderstandingwas that all norm_num needed was some invertible encoding from numerals of C to R or something but never mind I see that's nonsense and it needs more than that.

[Julian Berman]

Thanks for explaining I think I follow a bit more at least.

[Eric Wieser]

Is there a github issue that describes this missing grobner basis tactic that keeps being mentioned? Does coq or similar have such a tactic?

[Mario Carneiro]

Not that I know of. The best reference is probably the conversation at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/groebner.20basis.20algorithm