index under fvars

Author: kim-em

src/Lean/Meta/LazyDiscrTree.lean

@@ -368,7 +368,13 @@ def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) :
       let nargs := e.getAppNumArgs
       push (.proj s i nargs) nargs (todo.push a)
     | .fvar _fvarId   =>
-      return (.star, todo)
+      let nargs := e.getAppNumArgs
+      if nargs == 0 then
+        return (.star, todo)
+      else
+        let info ← getFunInfoNArgs fn nargs
+        let todo ← MatchClone.pushArgsAux info.paramInfo (nargs-1) e todo
+        return (.star, todo)
     | .mvar mvarId   =>
       if mvarId == MatchClone.tmpMVarId then
         -- We use `tmp to mark implicit arguments and proofs
@@ -678,18 +684,12 @@ def getMatchCore (root : Std.HashMap Key TrieIndex) (e : Expr) :
   let cases ← match k with
     | .star  =>
       pure #[]
-    /- When goal has fvar head like `p (ite c t e)`, also search by first argument's key.
+    /- When goal has fvar head like `p (ite c t e)`, follow the star edge with the fvar's arguments.
        This finds "eliminator-style" theorems indexed by argument structure. -/
     | .fvar _ _ =>
-      if h : 0 < args.size then
-        let firstArg := args[args.size - 1]  -- args are reversed
-        let (argK, argArgs) ← MatchClone.getMatchKeyArgs firstArg (root := true) (← read)
-        if argK != .star && argK != .other then
-          pure (#[] |> pushRootCase root argK argArgs)
-        else
-          pure #[]
-      else
-        pure #[]
+      match root[Key.star]? with
+      | some c => pure #[{ todo := args, score := 0, c }]
+      | none => pure #[]
     /- See note about "dep-arrow vs arrow" at `getMatchLoop` -/
     | .arrow =>
       pure (#[] |> pushRootCase root .other #[]

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -137,37 +137,16 @@ to find candidate lemmas.
 
 open LazyDiscrTree (InitEntry findMatches)
 
-/-- When conclusion is fvar-headed, create an entry keyed by the first concrete argument.
-    For `motive (ite c t e)`, creates entry with key `.const ite 4`.
-    This enables `exact?` to find "eliminator-style" theorems like `iteInduction`. -/
-private def getFirstArgEntry (type : Expr) (value : Name × DeclMod) :
-    MetaM (Option (InitEntry (Name × DeclMod))) := do
-  let type ← DiscrTree.reduceDT type true
-  let fn := type.getAppFn
-  if !fn.isFVar then return none
-  let args := type.getAppArgs
-  if args.isEmpty then return none
-  let firstArg := args[0]!
-  let firstArg ← DiscrTree.reduceDT firstArg false
-  let argFn := firstArg.getAppFn
-  if !argFn.isConst then return none
-  some <$> InitEntry.fromExpr firstArg value
-
 private def addImport (name : Name) (constInfo : ConstantInfo) :
     MetaM (Array (InitEntry (Name × DeclMod))) :=
   -- Don't report lemmas from metaprogramming namespaces.
   if name.isMetaprogramming then return #[] else
   forallTelescope constInfo.type fun _ type => do
     let e ← InitEntry.fromExpr type (name, DeclMod.none)
-    let mut a := #[e]
-    -- If root key is star (fvar-headed), also index by argument structure
-    if e.key == .star then
-      if let some argEntry ← getFirstArgEntry type (name, DeclMod.none) then
-        a := a.push argEntry
     if e.key == .const ``Iff 2 then
-      a := a.push (← e.mkSubEntry 0 (name, DeclMod.mp))
-      a := a.push (← e.mkSubEntry 1 (name, DeclMod.mpr))
-    pure a
+      return #[e, ← e.mkSubEntry 0 (name, DeclMod.mp), ← e.mkSubEntry 1 (name, DeclMod.mpr)]
+    else
+      return #[e]
 
 /-- Stores import discrimination tree. -/
 private def LibSearchState := IO.Ref (Option (LazyDiscrTree (Name × DeclMod)))