Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: add support for other types in norm_num #8100

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

feat: add support for other types in norm_num #8100

wants to merge 1 commit into from
+177 −12

Conversation

digama0
Copy link
Member

@digama0 digama0 commented Nov 1, 2023

Open in Gitpod

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Nov 20, 2023
dwrensha
dwrensha reviewed Nov 22, 2023
View reviewed changes
Mathlib/Tactic/NormNum/Result.lean
@@ -279,6 +281,12 @@ and `q` is the value of `n / d`. -/
∀ (inst : Q(DivisionRing $α) := by assumption) (q : Rat) (n : Q(ℤ)) (d : Q(ℕ))
(proof : Q(IsRat $x $n $d)), Result x := Result'.isRat

/-- The result is `proof : isRat x n d`, where `n` is either `.ofNat lit` or `.negOfNat lit`
with `lit` a raw nat literal and `d` is a raw nat literal (not 0 or 1),
and `q` is the value of `n / d`. -/
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This doc comment is a verbatim copy of the Result.isRat comment. Did you mean to have something different here?

dwrensha
dwrensha reviewed Nov 22, 2023
View reviewed changes
Mathlib/Tactic/NormNum/Structural.lean
have : $e =Q $e' := ⟨⟩
return .other e' q(@rfl _ $e')

/-- The `norm_num` extension which identifies expressions of the form `(a, b)`,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(a, b) -> a::b

dwrensha
dwrensha reviewed Nov 22, 2023
View reviewed changes
test/norm_num.lean
@@ -679,3 +679,5 @@ example : (1 : R PUnit.{u+1} PUnit.{v+1}) <= 2 := by

-- Check that we avoid deep recursion in evaluating large powers.
example : 10^40000000 = 10^40000000 := by norm_num

example : (1 + 1, 2 * 2) = (2, 4) := by norm_num1
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be good to add a similar test for lists.

@dwrensha
Copy link
Member

dwrensha commented Feb 11, 2024 •
edited
Loading

I was excited about this PR because it looked like a good way to get norm_num to work on Nat.digits. However, now that simprocs exists (in Lean 4.6.0), norm_num already can handle Nat.digits (via reduceLE, reduceMod, etc. -- see #10429), and #10428 shows a way to provide finer-grained control.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@dwrensha dwrensha dwrensha left review comments

Assignees
No one assigned
Labels
merge-conflict The PR has a merge conflict with master, and needs manual merging.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@digama0 @dwrensha @leanprover-community-mathlib4-bot