From 6d46e31ad8fbde38b5a412f4d3187f131ef86561 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Feb 2025 11:17:25 -0800 Subject: [PATCH] feat: compress `try?` suggestions (#6994) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds the `Try.Config.merge` flag (`true` by default) to the `try?` tactic. When set to `true`, `try?` compresses suggestions such as: ```lean · induction xs, ys using bla.induct · grind only [List.length_reverse] · grind only [bla] ``` into: ```lean induction xs, ys using bla.induct <;> grind only [List.length_reverse, bla] ``` This PR also ensures `try?` does not generate suggestions that mixes `grind` and `grind only`, or `simp` and `simp only` tactics. This PR also adds the `try? +harder` option (previously called `lib`), but it has not been fully implemented yet. --- src/Init/Try.lean | 17 ++++- src/Lean/Elab/Tactic/Grind.lean | 27 ++++++-- src/Lean/Elab/Tactic/Simp.lean | 24 ++++++- src/Lean/Elab/Tactic/Try.lean | 91 ++++++++++++++++++++++++--- src/Lean/Meta/Tactic/Try/Collect.lean | 2 +- tests/lean/run/grind_try_trace.lean | 38 +++++++++-- 6 files changed, 173 insertions(+), 26 deletions(-) diff --git a/src/Init/Try.lean b/src/Init/Try.lean index 774533c61780..f7a432661d11 100644 --- a/src/Init/Try.lean +++ b/src/Init/Try.lean @@ -15,8 +15,6 @@ structure Config where main := true /-- If `name` is `true`, all functions in the same namespace are considere for function induction, unfolding, etc. -/ name := true - /-- If `lib` is `true`, uses `libSearch` results. -/ - lib := true /-- If `targetOnly` is `true`, `try?` collects information using the goal target only. -/ targetOnly := false /-- Maximum number of suggestions. -/ @@ -25,6 +23,21 @@ structure Config where missing := false /-- If `only` is `true`, generates solutions using `grind only` and `simp only`. -/ only := true + /-- If `harder` is `true`, more expensive tactics and operations are tried. -/ + harder := false + /-- + If `merge` is `true`, it tries to compress suggestions such as + ``` + induction a + · grind only [= f] + · grind only [→ g] + ``` + as + ``` + induction a <;> grind only [= f, → g] + ``` + -/ + merge := true deriving Inhabited end Lean.Try diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index 4cc82c5b351e..7e802118a622 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/src/Lean/Elab/Tactic/Grind.lean @@ -174,8 +174,27 @@ def evalGrindCore replaceMainGoal [] return result +/-- Position for the `[..]` child syntax in the `grind` tactic. -/ +def grindParamsPos := 3 + +/-- Position for the `only` child syntax in the `grind` tactic. -/ +def grindOnlyPos := 2 + +def isGrindOnly (stx : TSyntax `tactic) : Bool := + stx.raw.getKind == ``Parser.Tactic.grind && !stx.raw[grindOnlyPos].isNone + +def setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `tactic := + if params.isEmpty then + ⟨stx.raw.setArg grindParamsPos (mkNullNode)⟩ + else + let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"] + ⟨stx.raw.setArg grindParamsPos (mkNullNode paramsStx)⟩ + +def getGrindParams (stx : TSyntax `tactic) : Array Syntax := + stx.raw[grindParamsPos][1].getSepArgs + def mkGrindOnly - (config : TSyntax `Lean.Parser.Tactic.optConfig) + (config : TSyntax ``Lean.Parser.Tactic.optConfig) (fallback? : Option Term) (trace : Grind.Trace) : MetaM (TSyntax `tactic) := do @@ -218,11 +237,7 @@ def mkGrindOnly `(tactic| grind $config:optConfig only on_failure $fallback) else `(tactic| grind $config:optConfig only) - if params.isEmpty then - return result - else - let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"] - return ⟨result.raw.setArg 3 (mkNullNode paramsStx)⟩ + return setGrindParams result params @[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do match stx with diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 1bcf5a319b42..1616aa69e1c0 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -294,6 +294,25 @@ where s := s.insert fvarId return s +/-- Position for the `[..]` child syntax in the `simp` tactic. -/ +def simpParamsPos := 4 + +/-- Position for the `only` child syntax in the `simp` tactic. -/ +def simpOnlyPos := 3 + +def isSimpOnly (stx : TSyntax `tactic) : Bool := + stx.raw.getKind == ``Parser.Tactic.simp && !stx.raw[simpOnlyPos].isNone + +def getSimpParams (stx : TSyntax `tactic) : Array Syntax := + stx.raw[simpParamsPos][1].getSepArgs + +def setSimpParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `tactic := + if params.isEmpty then + ⟨stx.raw.setArg simpParamsPos (mkNullNode)⟩ + else + let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"] + ⟨stx.raw.setArg simpParamsPos (mkNullNode paramsStx)⟩ + @[inline] def simpOnlyBuiltins : List Name := [``eq_self, ``iff_self] structure MkSimpContextResult where @@ -321,7 +340,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) if kind == SimpKind.dsimp then throwError "'dsimp' tactic does not support 'discharger' option" let dischargeWrapper ← mkDischargeWrapper stx[2] - let simpOnly := !stx[3].isNone + let simpOnly := !stx[simpOnlyPos].isNone let simpTheorems ← if simpOnly then simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems) else @@ -412,8 +431,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do args := args ++ (← locals.mapM fun id => `(Parser.Tactic.simpLemma| $(mkIdent id):ident)) else args := args.push (← `(Parser.Tactic.simpStar| *)) - let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"] - return stx.setArg 4 (mkNullNode argsStx) + return setSimpParams stx args def traceSimpCall (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Unit := do logInfoAt stx[0] m!"Try this: {← mkSimpOnly stx usedSimps}" diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean index 59c0ee93df0c..e1fd1c87fe29 100644 --- a/src/Lean/Elab/Tactic/Try.lean +++ b/src/Lean/Elab/Tactic/Try.lean @@ -169,6 +169,69 @@ def observing (x : M α) : M (TacticResult α) := do s.restore (restoreInfo := true) return .error ex sNew +private def mergeParams (ps1 ps2 : Array Syntax) : Array Syntax := Id.run do + let mut r := ps1 + for p in ps2 do + unless r.contains p do + r := r.push p + return r + +private def mergeSimp? (tac1 tac2 : TSyntax `tactic) : Option (TSyntax `tactic) := Id.run do + if setSimpParams tac1 #[] != setSimpParams tac2 #[] then return none + let ps1 := getSimpParams tac1 + let ps2 := getSimpParams tac2 + return some (setSimpParams tac1 (mergeParams ps1 ps2)) + +private def mergeGrind? (tac1 tac2 : TSyntax `tactic) : Option (TSyntax `tactic) := Id.run do + if setGrindParams tac1 #[] != setGrindParams tac2 #[] then return none + let ps1 := getGrindParams tac1 + let ps2 := getGrindParams tac2 + return some (setGrindParams tac1 (mergeParams ps1 ps2)) + +private def merge? (tac1 tac2 : TSyntax `tactic) : Option (TSyntax `tactic) := + let k := tac1.raw.getKind + -- TODO: we can make this extensible by having a command that allows users to register + -- `merge?` functions for different tactics. + if k == ``Parser.Tactic.simp then + mergeSimp? tac1 tac2 + else if k == ``Parser.Tactic.grind then + mergeGrind? tac1 tac2 + else + none + +private def mergeAll? (tacs : Array (TSyntax `tactic)) : M (Option (TSyntax `tactic)) := do + if !(← read).config.merge || tacs.isEmpty then + return none + let tac0 := tacs[0]! + if tacs.any fun tac => tac.raw.getKind != tac0.raw.getKind then + return none + let mut tac := tac0 + for h : i in [1:tacs.size] do + let some tac' := merge? tac tacs[i] + | return none + tac := tac' + return some tac + +/-- +Returns `true` IF `tacs2` contains only tactics of the same kind, and one of the following +- contains `simp only ...` and `simp ...` +- contains `grind only ..` and `grind ...` + +We say suggestions mixing `only` and non-`only` tactics are suboptimal and should not be displayed to +the user. +-/ +-- TODO: we may add a mechanism for making this extensible. +private def isOnlyAndNonOnly (tacs2 : Array (TSyntax `tactic)) : Bool := Id.run do + if tacs2.isEmpty then return false + let k := tacs2[0]!.raw.getKind + unless tacs2.all fun tac => tac.raw.getKind == k do return false + if k == ``Parser.Tactic.simp then + return tacs2.any (isSimpOnly ·) && tacs2.any (!isSimpOnly ·) + else if k == ``Parser.Tactic.grind then + return tacs2.any (isGrindOnly ·) && tacs2.any (!isGrindOnly ·) + else + return false + private def mkChainResult (tac1 : TSyntax `tactic) (tacss2 : Array (TSyntax `tactic)) : M (TSyntax `tactic) := do let tacss2 := tacss2.map getSuggestionsCore if (← isTracingEnabledFor `try.debug) then @@ -213,17 +276,27 @@ where return () else if h : i < tacss2.size then if tacss2[i].isEmpty then - go tacss2 (i+1) ((← `(tactic| · sorry)) :: acc) kind? + go tacss2 (i+1) ((← `(tactic| sorry)) :: acc) kind? else for tac in tacss2[i] do if let some kind := kind? then if tac.raw.getKind == kind then - go tacss2 (i+1) ((← `(tactic| · $tac:tactic)) :: acc) kind? + go tacss2 (i+1) (tac :: acc) kind? else - go tacss2 (i+1) ((← `(tactic| · $tac:tactic)) :: acc) kind? + go tacss2 (i+1) (tac :: acc) kind? else - let tac ← `(tactic| · $tac1:tactic - $(acc.toArray.reverse)*) + let tacs2 := acc.toArray.reverse + if kind?.isSome && isOnlyAndNonOnly tacs2 then + -- Suboptimal combination. See comment at `isOnlyAndNonOnly` + return () + let tac ← if let some tac2 ← mergeAll? tacs2 then + -- TODO: when merging tactics, there is a possibility the compressed version will not work. + -- TODO: if this is a big issue in practice, we should "replay" the tactic here. + `(tactic| $tac1:tactic <;> $tac2:tactic) + else + let tacs2 ← tacs2.mapM fun tac2 => `(tactic| · $tac2:tactic) + `(tactic| · $tac1:tactic + $tacs2*) modify (·.push tac) private def evalSuggestGrindTrace (tac : TSyntax `tactic) : M (TSyntax `tactic) := do @@ -363,6 +436,8 @@ private partial def evalSuggestImpl (tac : TSyntax `tactic) : M (TSyntax `tactic throwError "unsolved goals" return r +/-! `evalAndSuggest` frontend -/ + private def toSuggestion (t : TSyntax `tactic) : Tactic.TryThis.Suggestion := t @@ -432,11 +507,11 @@ private def mkGrindStx (info : Try.Info) : MetaM (TSyntax `tactic) := do set_option hygiene false in -- Avoid tagger at `+arith` /-- `simp` tactic syntax generator -/ private def mkSimpStx : CoreM (TSyntax `tactic) := - `(tactic| first | simp? | simp? +arith | simp_all) + `(tactic| first | simp? | simp? [*] | simp? +arith | simp? +arith [*]) /-- `simple` tactics -/ private def mkSimpleTacStx : CoreM (TSyntax `tactic) := - `(tactic| attempt_all | rfl | assumption | contradiction) + `(tactic| attempt_all | rfl | assumption) /-! Function induction generators -/ @@ -481,7 +556,7 @@ private def mkTryEvalSuggestStx (info : Try.Info) : MetaM (TSyntax `tactic) := d let simple ← mkSimpleTacStx let simp ← mkSimpStx let grind ← mkGrindStx info - let atomic ← `(tactic| attempt_all | $simple:tactic | $simp:tactic | $grind:tactic) + let atomic ← `(tactic| attempt_all | $simple:tactic | $simp:tactic | $grind:tactic | simp_all) let funInds ← mkAllFunIndStx info atomic `(tactic| first | $atomic:tactic | $funInds:tactic) diff --git a/src/Lean/Meta/Tactic/Try/Collect.lean b/src/Lean/Meta/Tactic/Try/Collect.lean index 38f5a496dd38..20e9eca006fc 100644 --- a/src/Lean/Meta/Tactic/Try/Collect.lean +++ b/src/Lean/Meta/Tactic/Try/Collect.lean @@ -158,7 +158,7 @@ def saveFunInd (_e : Expr) (declName : Name) (args : Array Expr) : M Unit := do open LibrarySearch in def saveLibSearchCandidates (e : Expr) : M Unit := do - if (← getConfig).lib then + if (← getConfig).harder then for (declName, declMod) in (← libSearchFindDecls e) do unless (← Grind.isEMatchTheorem declName) do let kind := match declMod with diff --git a/tests/lean/run/grind_try_trace.lean b/tests/lean/run/grind_try_trace.lean index 043df9311132..1f3d73bce919 100644 --- a/tests/lean/run/grind_try_trace.lean +++ b/tests/lean/run/grind_try_trace.lean @@ -7,6 +7,7 @@ info: Try these: • simp only [ne_eq, reduceCtorEq, not_false_eq_true] • grind • grind only +• simp_all -/ #guard_msgs (info) in example : [1, 2] ≠ [] := by @@ -123,18 +124,25 @@ attribute [simp] concat /-- info: Try these: -• · - induction as, a using concat.induct - · rfl - · simp_all +• (induction as, a using concat.induct) <;> simp_all +• (induction as, a using concat.induct) <;> simp [*] +-/ +#guard_msgs (info) in +example (as : List α) (a : α) : concat as a = as ++ [a] := by + try? -only + +/-- +info: Try these: +• (induction as, a using concat.induct) <;> simp_all • · induction as, a using concat.induct · simp - · simp_all + · simp [*] -/ #guard_msgs (info) in example (as : List α) (a : α) : concat as a = as ++ [a] := by - try? -only + try? -only -merge + def foo : Nat → Nat | 0 => 1 @@ -160,3 +168,21 @@ x : Nat #guard_msgs (error) in example : foo x > 0 := by try? + +@[simp] def bla : List Nat → List Nat → List Nat + | [], ys => ys.reverse + | _::xs, ys => bla xs ys + +attribute [grind] List.length_reverse bla + +/-- +info: Try these: +• (induction xs, ys using bla.induct) <;> grind +• (induction xs, ys using bla.induct) <;> simp_all +• (induction xs, ys using bla.induct) <;> simp [*] +• (induction xs, ys using bla.induct) <;> simp only [bla, List.length_reverse, *] +• (induction xs, ys using bla.induct) <;> grind only [List.length_reverse, bla] +-/ +#guard_msgs (info) in +example : (bla xs ys).length = ys.length := by + try?