RefinedDiscrTree incompleteness

Stream: metaprogramming / tactics

[Jannis Limperg]

@Jovan Gerbscheid I was investigating the completeness of RefinedDiscrTree indexing and found this counterexample (for the RefinedDiscrTree in Mathlib):

import Mathlib.Tactic.FunProp.RefinedDiscrTree

open Lean Lean.Meta Lean.Elab.Term Lean.Elab.Tactic
open Mathlib.Meta.FunProp (RefinedDiscrTree)

elab "test " i:ident : tactic => do
  let e ← Lean.Elab.Tactic.elabTerm i none
  let t ← inferType e
  let (rdt, dt) ← withNewMCtxDepth do
    let (_, _, conclusion) ← forallMetaTelescope t
    let rdt ← ({} : RefinedDiscrTree String).insert conclusion "foo" (config := {})
    let dt  ← ({} : DiscrTree String).insert        conclusion "foo" (config := {})
    pure (rdt, dt)
  let tgt ← getMainTarget
  let ms  ← dt.getUnify tgt (config := {})
  logInfo m!"DiscrTree        has matches: {! ms.isEmpty}"
  let rms ← rdt.getMatchWithScore tgt (unify := true) (config := {})
  logInfo m!"RefinedDiscrTree has matches: {! rms.isEmpty}"

theorem foo {T : Type} {a b : T} {P : T → T → Prop}
    (p : ∀ (Q : T → T → Prop), Q a b) : P a b := by
  test p
  -- DiscrTree        has matches: true
  -- RefinedDiscrTree has matches: false
  apply p

Here apply manages to unify ?Q a b and P a b and the standard DiscrTree also finds ?Q a b as a possible match for P a b. However, the RefinedDiscrTree doesn't.

cc @Tomas Skrivan since you're using the tree for fun_prop.

[Jovan Gerbscheid]

The function getMatchWithScore takes an argument allowRootStar, which determines whether the pattern .star 0 in the discrimination tree should be matched with or not, since this patterns matches with everything. It is set to false by default. ?Q a b has the pattern .star 0 because it is a metavariable application.

[Jovan Gerbscheid]

By the way I'm working on the new version of RefinedDiscrTree that is lazy, and therefore doesn't require any cache when used with all of mathlib, and it is mostly finnished.

[Jovan Gerbscheid]

I should probably set it to true by default to avoid confusion, or not give it a default value.

[Jannis Limperg]

Ah, great! I was wondering where this behaviour was coming from.

[Jannis Limperg]

This one seems to be an actual issue:

import Mathlib.Tactic.FunProp.RefinedDiscrTree

open Lean Lean.Meta Lean.Elab.Term Lean.Elab.Tactic
open Mathlib.Meta.FunProp (RefinedDiscrTree)

elab "test " i:ident : tactic => do
  let e ← Lean.Elab.Tactic.elabTerm i none
  let t ← inferType e
  let (rdt, dt) ← withNewMCtxDepth do
    let (_, _, conclusion) ← forallMetaTelescope t
    let rdt ← ({} : RefinedDiscrTree String).insert conclusion "foo" (config := {})
    let dt  ← ({} : DiscrTree String).insert        conclusion "foo" (config := {})
    pure (rdt, dt)
  let tgt ← getMainTarget
  let ms  ← dt.getUnify tgt (config := {})
  logInfo m!"DiscrTree        has matches: {! ms.isEmpty}"
  let rms ← rdt.getMatchWithScore tgt (unify := true) (config := {}) (allowRootStar := true)
  logInfo m!"RefinedDiscrTree has matches: {! rms.isEmpty}"

theorem foo {A B : Type} {P : (A → B) → Prop} (f : A → B) (p : P f) :
    P (λ x => f x) := by
  test p
  apply p

From the description of the RefinedDiscrTree features, the issue seems to be that the RefinedDiscrTree indexes all eta-reducts of a pattern, but not all eta-expansions.

On that note: would it be possible to only index fully eta-expanded terms? This would avoid the combinatorial blowup of indexing all eta-reducts.

[Jovan Gerbscheid]

This problem also stems from an argument with an unfortunate default value, fvarInContext in the insert function (IIRC from memory, as I'm on mobile). Instead of indexing the free variable, this option instructs it to be indexed as a .opaque. I removed this feature/trap from the new version.

[Jovan Gerbscheid]

In this example my extra eta reduction handling doesn't apply, because the usual reduction already does this eta reduction

[Jannis Limperg]

I see. Indeed it works when I replace the fvars with axioms.