Discrimination tree lookup

Stream: lean4

[Jannis Limperg]

My mental model of discrimination trees used to be that if you insert a key expression k into the tree and then query it with getUnify q, the returned array will include the value associated to k whenever k unifies with q. However, this does not seem to be the case. A concrete example from Aesop, where I use discr trees with default transparency for indexing: if k = _ ++ _ and q = [a] ++ l, then the first thing getUnify does is whnf q, which reduces q to a :: l and so the ++ branch of the tree is never explored and k is not found. I can whip up an MWE if desired.

Is this expected or a bug? I guess if you wanted to fix this, you'd have to perform two traversals, one before whnf which explores the ++ branch and one after whnf which explores the :: branch (and similar recursively, for every iteration of the lookup loop). But this may not even be enough: q may have additional reducts with different head symbols(?). So this fix sounds quite expensive.

cc @Jasmin Blanchette

[Gabriel Ebner]

where I use discr trees with default transparency for indexing:

This is the problem. We always use reducible transparency for discrimination trees.

[Gabriel Ebner]

As you've observed, extending this to default transparency requires extra work. We would indeed need to store multiple reductions in the discrimination tree.

[Jannis Limperg]

Okay, but the problem remains when I use reducible transparency, doesn't it? For example, I can make ++ reducible and get the same behaviour with stock discr trees.

I also don't see how I could put more information into the tree to fix this. At the point where I put a lemma with conclusion, say, l ++ l' = l' in the tree, it seems really hard to anticipate all the possible instances of l and l' that would lead to a different reduction (e.g. l = [a]).

[Gabriel Ebner]

I can make ++ reducible and get the same behaviour with stock discr trees.

You shouldn't and we don't.

[Gabriel Ebner]

The general rule being that recursive definitions are not reducible.

[Gabriel Ebner]

We have lots of non-recursive reducible definitions, but those are fine because they can just be expanded as a preprocessing.

[Jannis Limperg]

Okay, thanks. I guess for the moment I'll go back to using reducible transparency for indexing; that's also an unfortunate restriction but at least it provides predictable behaviour. Longer-term I'd like to see whether this can be fixed properly without tanking performance too much.

[Gabriel Ebner]

I feel like this is a bit of an #xy question. Many other parts of Lean also work with reducible transparency, in particular all other proof search procedures: simp, type-class synthesis, etc. Using the same transparency setting is a consistency feature, not a bug.™

[Jannis Limperg]

I see the argument, but I'm really not sure about this in the context of Aesop. When I do indexing with reducible transparency, apply rules don't work like the apply tactic any more; they work like applywith reducible transparency. So a rule which concludes P (a :: l) doesn't apply to the goal P ([a] ++ l). I guess the Lean way is to let simp compensate for this by registering all the reduction rules as simp lemmas.

One particular application where this will be problematic is using Aesop to emulate tactics such as measurability. The banged version, which uses default transparency, cannot easily be expressed as an Aesop call if Aesop is effectively restricted to reducible.

[Gabriel Ebner]

AFAICT measurability! is never used in mathlib. And continuity! is only used five times, which would be easy to fix.

[Gabriel Ebner]

From a high-level point of view, I think it would be better to use reducible transparency exclusively and add extra lemmas to bridge the gaps.

[Gabriel Ebner]

Looking at some of the uses of continuity! in mathlib, this would imho be an improvement: e.g. in unit_interval.lean, we can just replace continuity! with unfold symm; continuity.

[Kevin Buzzard]

As an end user I've seen this unfold thing; high-powered-tactic idiom before and I always wish that the tactic was that bit more powerful; you can see why things like continiity! have ended up existing

[Jasmin Blanchette]

Jannis, I think your mental model was very simplistic. I'd expect the current behavior to be a feature, not a bug -- doing lookup up to computation must be very difficult.

[Jasmin Blanchette]

Oh, I just discovered the rest of the thread. Just ignore my comment. ;)