feat: a norm_num extension for complex numbers by Whysoserioushah · Pull Request #26975 · leanprover-community/mathlib4

Whysoserioushah · 2025-07-10T17:29:00Z

co-authored-by : @thefundamentaltheor3m, @hrmacbeth

depends on: [Merged by Bors] - feat: add ofScientific lemmas for Complex/RCLike/Quaternion #39628
depends on: [Merged by Bors] - feat: missing nnratCast lemmas for RCLike #39620

github-actions · 2025-07-10T17:30:13Z

PR summary 69e27a97b7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Tactic`	1
`Mathlib.Tactic.NormNum.NormNumI` (new file)	1657

Declarations diff

+ Result.eq
+ Result.toBool
+ ResultI
+ ResultI.add
+ ResultI.conj
+ ResultI.eq
+ ResultI.eqTrans
+ ResultI.eqeq
+ ResultI.inv
+ ResultI.mk'
+ ResultI.mul
+ ResultI.neg
+ ResultI.sub
+ eq_of_eq_of_eq
+ evalComplexEq
+ evalIm
+ evalRe
+ im_ofScientific
+ im_pow_zero
+ instance (a : Q(ℂ)) : ToMessageData (ResultI a)
+ ne_of_im_ne
+ ne_of_re_ne
+ nnratCast_im
+ nnratCast_re
+ ofReal_ofScientific
+ of_pow_negSucc
+ of_pow_ofNat
+ pow_bit_false
+ pow_bit_true
+ re_ofScientific
+ re_pow_zero

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

eric-wieser · 2025-07-10T18:41:04Z

Please add a file that tests all the operations handled here; I assume you already have some tests downstream that you can include here?

Whysoserioushah · 2025-07-10T18:49:01Z

where should I put the test file?

hrmacbeth · 2025-07-10T20:12:43Z

where should I put the test file?

Please make a new file in MathlibTest.

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Vierkantor

I implemented exponentiation in the style of the other operations. If you're happy with this, I can do a full review.

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Whysoserioushah · 2026-04-30T23:57:02Z

I implemented exponentiation in the style of the other operations. If you're happy with this, I can do a full review.

@eric-wieser Are you happy with this implementation? I think it's okay

eric-wieser · 2026-05-20T06:18:00Z

  | .isNegNNRat dα .., _ | _, .isNegNNRat dα .. => ratArm dα
  -- mixing positive rationals and negative naturals means we need to use the full rat handler
-  | .isNNRat dsα .., .isNegNat rα .. | .isNegNat rα .., .isNNRat dsα .. =>
+  | .isNNRat _ .., .isNegNat _ .. | .isNegNat _ .., .isNNRat _ .. =>


Removing these names makes the comment below not make any sense any more.

eric-wieser · 2026-05-20T06:25:47Z

+/-- Result of `norm_num` running on lift of natural numbers in real -/
+def NormNum.Resultn (n0 : ℕ) : MetaM (NormNum.Result q(OfNat.ofNat (α := ℝ) $n0)) := do
+  have n : Q(ℕ) := .lit (.natVal n0)
+  let ⟨_, (pa)⟩ ← NormNum.mkOfNat q(ℝ) q(inferInstance) n
+  return NormNum.Result.isNat (α := q(ℝ)) q(inferInstance) n q(NormNum.isNat_ofNat ℝ $pa)
+
+/-- Result of `norm_num` on scientific expressions in real -/
+def NormNum.ResultOfScientific (mantissa : ℕ) (exponentSign : Bool) (decimalExponent : ℕ) :
+    MetaM (NormNum.Result q(OfScientific.ofScientific (α := ℝ) $mantissa
+    $exponentSign $decimalExponent )) := do


These two look misnamed; they are not types so should not be TitleCase.

This also looks fishy in general though; is this duplicating the implementation of some norm_num extensions?

when I was writing these two I had the same doubt and I failed to find any, I'd love to be proved wrong!

I've replaced both with a call to derive.

eric-wieser · 2026-05-20T15:42:57Z

+@[simp, rclike_simps]
+theorem nnratCast_re (q : ℚ≥0) : re (q : K) = q := by rw [← ofReal_nnratCast, ofReal_re]
+
+@[simp, rclike_simps, norm_cast]
+theorem nnratCast_im (q : ℚ≥0) : im (q : K) = 0 := by rw [← ofReal_nnratCast, ofReal_im]
+


#39620, which also adds one more

eric-wieser · 2026-05-26T01:19:34Z

+-- casts
+example : (Nat.cast 3 : ℂ) = 3 := by norm_num1
+example : (Int.cast (-2) : ℂ) = -2 := by norm_num1
+example : (Rat.cast 1.5 : ℂ) = 3 / 2 := by norm_num1


NNRat.cast needs #34805

create

10d9741

Whysoserioushah requested review from eric-wieser and hrmacbeth July 10, 2025 17:29

github-actions Bot added the t-meta Tactics, attributes or user commands label Jul 10, 2025

Whysoserioushah requested a review from b-mehta July 10, 2025 17:40

Whysoserioushah added 2 commits July 10, 2025 18:42

fix build1

5782814

add docstring

1d184d4

grunweg changed the title ~~feat(Mathlib/Tactic/NormNum/NormNumI): a norm_num tactic for complex~~ feat: a norm_num extension for complex numbers Jul 10, 2025

eric-wieser added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 10, 2025

eric-wieser reviewed Jul 10, 2025

View reviewed changes

Comment thread Mathlib/Tactic/NormNum/NormNumI.lean Outdated

eric-wieser reviewed Jul 10, 2025

View reviewed changes

Comment thread Mathlib/Tactic/NormNum/NormNumI.lean Outdated

Whysoserioushah and others added 2 commits July 11, 2025 02:07

Update Mathlib/Tactic/NormNum/NormNumI.lean

b551d88

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Update Mathlib/Tactic/NormNum/NormNumI.lean

e2dfbc3

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

eric-wieser reviewed Jul 11, 2025

View reviewed changes

Comment thread Mathlib/Tactic/NormNum/NormNumI.lean Outdated

eric-wieser and others added 5 commits July 11, 2025 14:10

Do the IsComplex refactor

bcd9e57

create test file

fdf6c4b

missing import

88c0610

fix test

f6e3afd

Use Simp.ResultQ

4164091

eric-wieser reviewed Jul 11, 2025

View reviewed changes

Comment thread MathlibTest/norm_numI.lean Outdated

golf

5f12f47

eric-wieser reviewed Jul 11, 2025

View reviewed changes

Comment thread Mathlib/Tactic/NormNum/NormNumI.lean Outdated

eric-wieser reviewed Jul 11, 2025

View reviewed changes

Comment thread Mathlib/Tactic/NormNum/NormNumI.lean Outdated

eric-wieser reviewed Jul 11, 2025

View reviewed changes

Comment thread Mathlib/Tactic/NormNum/NormNumI.lean Outdated

Whysoserioushah added 2 commits July 11, 2025 16:09

remove comment

ab93cef

change sub

916b6f5

Exponentiation seems to work, but it needs tests.

c3a04be

Vierkantor reviewed Mar 4, 2026

View reviewed changes

Comment thread Mathlib/Analysis/RCLike/Basic.lean Outdated

Vierkantor added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 4, 2026

seewoo5 mentioned this pull request Mar 6, 2026

feat: norm_numI improvements from Gauss thefundamentaltheor3m/Sphere-Packing-Lean#345

Open

Whysoserioushah and others added 2 commits May 1, 2026 00:55

Update Mathlib/Analysis/RCLike/Basic.lean

60eef3d

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Merge branch 'master' into edison/norm_numI

d085c6f

Vierkantor removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 15, 2026

Vierkantor assigned eric-wieser and unassigned Vierkantor May 15, 2026

eric-wieser mentioned this pull request May 18, 2026

feat(Data/Complex/Basic): add simproc to reduce powers of I #39506

Open

eric-wieser reviewed May 20, 2026

View reviewed changes

Comment thread Mathlib/Tactic/NormNum/NormNumI.lean Outdated

eric-wieser reviewed May 20, 2026

View reviewed changes

Comment thread Mathlib/Tactic/NormNum/NormNumI.lean Outdated

eric-wieser reviewed May 20, 2026

View reviewed changes

Comment thread Mathlib/Tactic/NormNum/NormNumI.lean Outdated

eric-wieser reviewed May 20, 2026

View reviewed changes

Comment thread Mathlib/Tactic/NormNum/NormNumI.lean Outdated

eric-wieser added 5 commits May 20, 2026 06:37

avoid duplicate work in inv

bde41b8

fix indents and bool parsing

875d018

style: drop parens

d8dcbee

simplify

bd872e0

further cleanup

8706129

eric-wieser reviewed May 20, 2026

View reviewed changes

eric-wieser added 6 commits May 20, 2026 17:41

fix tests and improve tracing

1ebdc63

fix def names

22623c2

remove helper functions in favor of derive

4de4c8f

rework constants

36ff0f5

remove test_sorry

6ff80fe

actually commit the cast code

69e27a9

eric-wieser reviewed May 26, 2026

View reviewed changes

Uh oh!

Conversation

Whysoserioushah commented Jul 10, 2025 • edited by eric-wieser Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 69e27a97b7

Import changes for modified files

Declarations diff

Uh oh!

eric-wieser commented Jul 10, 2025

Uh oh!

Whysoserioushah commented Jul 10, 2025

Uh oh!

hrmacbeth commented Jul 10, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Whysoserioushah commented Apr 30, 2026

Uh oh!

eric-wieser May 20, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

eric-wieser May 20, 2026

Choose a reason for hiding this comment

Uh oh!

Whysoserioushah May 20, 2026

Choose a reason for hiding this comment

Uh oh!

eric-wieser May 20, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

eric-wieser May 20, 2026

Choose a reason for hiding this comment

Uh oh!

eric-wieser May 26, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

9 participants

Whysoserioushah commented Jul 10, 2025 •

edited by eric-wieser

Loading

github-actions Bot commented Jul 10, 2025 •

edited

Loading