Commit 2025-06-14 09:56 af6fe588

feat: improvements to RefinedDiscrTree (#11968) This PR defines RefinedDiscrTree, which is an improved version of DiscrTree with many new features, such as

• indexing lambda terms, dependent forall terms, and bound variables.
• giving a score to matches, in order to sort them
• indexing star patterns so that a+b and a+a are indexed differently
• taking into account eta reductions, so that exp can still be matched with the library pattern fun x => exp (f x). This PR makes RefinedDiscrTree into a lazy data structure, meaning that it can be used without a cache, just like LazyDiscrTree. This PR also removes these features:
• indexing fun x => x as id
• indexing fun x => f x + g x as f + g, and similarly for -, *, /, ⁻¹, ^.
• indexing fun _ => 42 as 42 These equivalent indexings do not hold definitionally in the reducible transparency, which is the transparency that is used for unification when using a discrimination tree. Therefore, indexing these different expressions the same is actually inefficient rather than helpful. This is part of the bigger #11768, which uses this discrimination tree for a library rewriting tactic. This replaces an older version of RefinedDiscrTree.