[Merged by Bors] - feat(Tactic): linarith and rify for NNReal

[DavidLedvinka]

No description provided.

[github-actions]

PR summary cde919c85c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Tactic.Rify Mathlib.Tactic	1
Mathlib.Tactic.Linarith.NNRealPreprocessor (new file)	910

---

Declarations diff

+ coe_sub_of_lt
+ isNNRealtoReal
+ mkRifyContext
+ mk_toReal_nonneg_prf
+ nnrealToReal
+ rifyProof
+ toReal_eq
+ toReal_le
+ toReal_lt
+ toReal_ne

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

---

note: file MathlibTest/linarith.lean` was renamed to `MathlibTest/Linarith/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[JovanGerb]

For the trick you to do add the preprocessor in a later file, wouldn't it be more natural to have

initialize defaultPreprocessors : IO.Ref (Array GlobalBranchingPreprocessor) ←
  IO.mkRef #[filterComparisons, removeNegations, natToInt, strengthenStrictInt,
    compWithZero, cancelDenoms]

And then in the later file, you can use initialize to push the NNReal preprocessor onto this array.
This way, the preprocessing can be extended in other ways in the future.

[DavidLedvinka]

For the trick you to do add the preprocessor in a later file, wouldn't it be more natural to have

initialize defaultPreprocessors : IO.Ref (Array GlobalBranchingPreprocessor) ←
  IO.mkRef #[filterComparisons, removeNegations, natToInt, strengthenStrictInt,
    compWithZero, cancelDenoms]

And then in the later file, you can use initialize to push the NNReal preprocessor onto this array. This way, the preprocessing can be extended in other ways in the future.

I thought about this but the reason I decided against it was:

a) I suspect there won't need to be that many uses of this trick
b) Order is important for preprocessors.

It seems more convenient to see the order of everything up front given any subset is being used rather than make sure we are threading a bunch of preprocessors in separate files correctly.

[JovanGerb]

Aha, I didn't realize that their order was important. In that case I'm happy with the current implementation.

Thank you 🎉

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by JovanGerb.

[hrmacbeth]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job