AtomM cache?

Stream: mathlib4

[Thomas Murrills]

Should AtomM have a cache for the atoms? Currently addAtom gets the atom of an expression e by looking at an array atoms : Array Expr, then checks each element of this array in turn against e by isDefEq.

Is the current AtomM behavior less expensive than it sounds? Would there be any benefit in doing a cheaper check in a HashMap Expr Nat, then falling back on iterating through the array if that fails? I imagine this might have been considered already, but thought I'd check.

[Henrik Böving]

The HashMap behavior is what both LeanSAT and omega are doing for performance reasons + actually no fallback to isDefEq at all.

[Eric Wieser]

Doesn't that mean that a + b can end up not matching a + b if the HAdd instance is different-but-defeq?

[Eric Wieser]

This test-case passes, so it seems omega is doing something with defeq:

import Mathlib

def my_add {α} [AddSemigroup α] (a b : α) := a + b

example : ⌊(1 + 2 : ℝ)⌋ - ⌊(my_add 1 2 : ℝ)⌋ = 0 := by
  rw [my_add]
  omega

[Kim Morrison]

omega uses Lean.Meta.Canonicalizer. This is much more efficient than AtomM.

[Thomas Murrills]

Is Canonicalizer strictly better than AtomM all around, or do they have different use cases?

[Eric Wieser]

(https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Canonicalizer.html)

[Eric Wieser]

I think there's quite a difference in philosophy between the two, and so picking between them is more than just a performance choice

[Eric Wieser]

I think the two things going for AtomM are:

• It "sees through" abbrev, which depending on your model of what abbrev is supposed to mean, could be a feature
• It can be used to unify metavariables; though perhaps CanonM could special case expressions with metavariables, assigning them all the same hash, for parity here.

[Thomas Murrills]

Hmm, it also seems that there are some expression reductions omega/CanonM doesn’t do, which AtomM would in the course of isDefEq, e.g.

import Mathlib

example : ⌊(fun x => x) (1 + 2 : ℝ)⌋ - ⌊(1 + 2 : ℝ)⌋ = 0 := by
  omega --error

[Thomas Murrills]

Though I wonder how “CanonM plus expression reductions” would compare to AtomM.

[Mario Carneiro]

AtomM is a linear scan exactly because it can't use the discrimination tree because it works up to unfolding semireducibles

[Mario Carneiro]

I've thought about having a hybrid version where if the reducibility setting is reducible then it uses a discrimination tree instead

[Mario Carneiro]

in practice I don't think it's a major issue, but it is quadratic in the size of the statement

[Mario Carneiro]

Note that ring/linarith actually used to be using something closer to the discrimination tree approach, this is the result of a feature request