Allow the simplifier to use facts in its can_prove() predicates.

[mcourteaux]

Problem statement

While preparing #9371, I hit several dead ends trying to produce very neat IR. The reason is the simplifier cannot simplify max(x, y) = x when we give the assumption x >= y. Intuitively, one would write in Simplify_Max.cpp:

   rewrite(max(x, y), a, can_prove(x >= y, this))

However, the way can_prove(Expr, Prover) is implemented is to recursively mutate() the Expr with the Prover (i.e., this instance of Simplify). This however, does not substitute in the facts (truths), and therefore fails to "prove" that x > y.

A secondary problem with rewrite rules that use can_prove() is that they recursively invoke the simplifier, which leads potentially to infinite recursions. Specifically, Andrew stated:

Calling can_prove as the third arg to rewrite recursively invokes the simplifier on every expr that matches that LHS. If one of them itself creates an intermediate expression that also matches the LHS, you get infinite recursion.

Solution

This PR makes it possible to use facts in a can_prove(), prevents infinite recursion, and offers known_true() as a lightweight alternative.

Using facts / truths.

In order to match simple truths into expressions, whenever new facts are learned, they are canonicalized, such that lookup can do the same, and a > b matches with b < a.
The can_prove(Expr, Prover) entry-point now calls out to simplify_can_prove_condition(), which is the full power of the Simplifier at work, but using canonicalized facts.

As a bonus: substitute_facts benefits from this canonicalization and manages to substitute in more facts, even when the fact is not IR-tree-wise an exact match.

As an additional bonus: weaker forms of inequalities are also substituted in as facts if the stronger inequality is known as a fact. Example: x >= y (which is weak) is replaced by true if the fact that x > y is known.

Limiting recursion.

Implementing this, I indeed hit an infinite recursion quickly, so this PR also limits the recursion depth to 1. Experiments performed with higher recursion depth explode compile time for no measured benefit. The recursion limit of 1 means that a call to simplify() can call simplify() only once within a can_prove() but not more. This is done in the call simplify_can_prove_condition() which is exactly the new behavior of can_prove().

A lightweight alternative: known_true().

Instead of running the full simplifier for a can_prove(), we can now also write rewrite-predicates using a known_true() which is just the simple lookup in the Simplifier's fact list using the canonicalization. This naturally cannot recurse, and also does not spend time trying to simplify things when not needed. This is especially useful for when you would match max(x, y) on every such Expr and then try to can_prove(x > y), which is expensive. Instead the rewrite rule is:

   rewrite(max(x, y), a, known_true(x >= y, this))

Which is a very fast lookup, instead of a whole run through the simplifier.

A few such example rules are implemented in Simplify_Div.

Checklist

• Tests added or updated (not required for docs, CI config, or typo fixes)
• Documentation updated (if public API changed)
• Python bindings updated (if public API changed)
• Benchmarks are included here if the change is intended to affect performance.
• Commits include AI attribution where applicable (see Code of Conduct)

[codecov]

Codecov Report

❌ Patch coverage is 87.01299% with 10 lines in your changes missing coverage. Please review.
✅ Project coverage is 70.09%. Comparing base (347b0d1) to head (032f724).
⚠️ Report is 1 commits behind head on main.

Files with missing lines	Patch %	Lines
src/Simplify.cpp	81.13%	6 Missing and 4 partials ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #9400      +/-   ##
==========================================
- Coverage   70.14%   70.09%   -0.05%     
==========================================
  Files         261      261              
  Lines       79388    79468      +80     
  Branches    19357    19381      +24     
==========================================
+ Hits        55690    55707      +17     
- Misses      17874    17895      +21     
- Partials     5824     5866      +42     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.