NormNumI

Stream: mathlib4

[Edison Xie]

Hi everyone! So this tactic norm_numI that @Sidharth Hariharan , @Heather Macbeth and I have been working is soon going to be PRed into mathlib, so I think it's best to let everyone check if this is what they'd want norm_num to do.

So currently, what it DOES handle:

• ofNat n: Natural numbers coerced to complex;
• z1 + z2: Addition of complexes;
• z1 * z2: Multiplication of complexes;
• z⁻¹: Inverse of complexes;
• z1/z2: Division of complexes;
• -z: Negation of complexes;
• z1 - z2: Subtraction of complexes;
• conj z: Conjugation of complexes;
• @HPow.hPow ℂ ℕ ℂ: Natural exponents of complexes, e.g. z^(2 + 3) ;
• @HPow.hPow ℂ ℤ ℂ: Integral exponents of complexes, e.g. z^(-1-2*3 : ℤ);
• Scientific expressions of complexes; e.g. (0.25 : ℂ) + (0.25 : ℂ).

And currently it DOES NOT handle :

• free variables in complexes, e.g. x y : ℂ, x * I = y * I for x = y
• constructor mode in complexes, e.g ⟨1, 0⟩ + ⟨38, 0⟩ - 1 = (⟨37, 0⟩ : ℂ)

I will soon post the PR number once we PR this, in the mean time, feel free to let us know whether you think this is enough/not enough for norm_numI in complexes, your advice will be valued and appreciated, thanks!

[Eric Wieser]

Here's a few more additions, in order of difficulty:

• Nat.cast
• Int.cast
• Rat.cast
• smul from docs#Complex.module
• Complex powers of complex numbers, when the power turns out to be an integer
• NNRat.cast

[Eric Wieser]

Edison Xie said:

• free variables in complexes, e.g. x y : ℂ, x * I = y * I for x = y

I'm pretty sure that this is explicitly out of scope for norm_num, so this seems like a good thing

[Floris van Doorn]

This is great! I'd like to see more extensions to norm_num!

[Floris van Doorn]

I'm a bit worried about the number of new tactics we're introducing. I think it would be much better if we have fewer tactics that do more themselves.

Would it be possible to incorporate this into norm_num? This will require changing some hard-coded internal data-structures of norm_num (I don't know if it would be feasible to make that more extensible?)

[Eric Wieser]

I'd advocate for a separate tactic with a TODO comment for now

[Floris van Doorn]

I'm perfectly happy with that.

[Eric Wieser]

Making norm_num extensible over types is a really hard problem I think

[Floris van Doorn]

I was afraid that would be the case... It would be nice if it could also represent lists and list-like types (Finset)

[Eric Wieser]

I think that's squarely in the "this should be a simproc" scope creep territory

[Eric Wieser]

Even supporting Complex in norm_num without also supporting GaussianInt (or other quadratic extensions) seems like something we should try to avoid

[Floris van Doorn]

I'd definitely also be happy if simp can simplify those kinds of things.

[Eric Wieser]

Note that the proposed norm_numI already partially integrates into norm_num; it can register an extension for (in)equalities of complex numbers, but can't simplify complex numerals that don't participate in a comparison.

[Eric Wieser]

Should the tactic be called norm_num_complex or norm_num_I or norm_num +complex? (where the latter is an unrelated syntax that happens to start with the same word)

[Edison Xie]

I think currently we have our tactic as a norm_num extension already? @Sidharth Hariharan what's the current state of it :-)

[Eric Wieser]

When I checked it was an extension for equality only, but that won't help with simplifying cexp (I*I) to cexp (-1)

[Sidharth Hariharan]

As it stands, we have

1. a conv tactic called norm_numI
2. a norm_num extension that integrates the parsing and normalisation procedures of norm_numI into norm_num

I am exploring how it can be made into a separate tactic, but the advice I've gotten so far is that we should make it a simproc as well as a norm_num extension. (I don't know how to make it into a simproc, but I'd love to learn!)

[Eric Wieser]

Sidharth Hariharan said:

but the advice I've gotten so far

To clarify the advice I gave, for others; I think we should get a version merged that uses some combinations of norm_num extensions and simprocs, and then think about a standalone version / integration into norm_num's internals after that.

[Heather Macbeth]

Eric Wieser said:

I think we should get a version merged that uses some combinations of norm_num extensions and simprocs

I think it would be fine to merge even less, namely what they have now: the norm_num extension that handles complex (dis)equalities, plus the new conv tactic norm_numI.

For tasks like simplifying cexp (I*I), it's less user-friendly to require the user to build a conv => .... norm_numI than to have a simproc find the location automatically, but it's perfectly workable (and, in my opinion, mergeable).

[Eric Wieser]

I think the simproc is probably on the order of 5 lines of code calling what they already have, which I could probably suggest in the review!

[Edison Xie]

Eric Wieser said:

• smul from docs#Complex.module
  

do you mean docs#Complex.instModule?

[Edison Xie]

a PR has been made! #26975