From 64b5bedc8c2ed6915387e5ff37f6e1b372dc278e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 1 Feb 2025 22:37:49 -0800 Subject: [PATCH] feat: `try?` tactic (#6905) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds the `try?` tactic. This is the first draft, but it can already solve examples such as: ```lean example (e : Expr) : e.simplify.eval σ = e.eval σ := by try? ``` in `grind_constProp.lean`. In the example above, it suggests: ```lean induction e using Expr.simplify.induct <;> grind? ``` In the same test file, we have ```lean example (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by try? ``` and the following suggestion is produced ```lean induction σ₁, σ₂ using State.join.induct <;> grind? ``` --- src/Init.lean | 1 + src/Init/Try.lean | 30 +++ src/Lean/Elab/Tactic.lean | 1 + src/Lean/Elab/Tactic/Try.lean | 166 ++++++++++++++ src/Lean/Meta/Tactic.lean | 1 + src/Lean/Meta/Tactic/Grind/Cases.lean | 4 + src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 4 + src/Lean/Meta/Tactic/LibrarySearch.lean | 2 +- src/Lean/Meta/Tactic/Try.lean | 17 ++ src/Lean/Meta/Tactic/Try/Collect.lean | 210 ++++++++++++++++++ tests/lean/run/grind_constProp.lean | 12 +- tests/lean/run/prelude-injectivity.lean | 1 + tests/lean/run/try_trace1.lean | 44 ++++ 13 files changed, 491 insertions(+), 2 deletions(-) create mode 100644 src/Init/Try.lean create mode 100644 src/Lean/Elab/Tactic/Try.lean create mode 100644 src/Lean/Meta/Tactic/Try.lean create mode 100644 src/Lean/Meta/Tactic/Try/Collect.lean create mode 100644 tests/lean/run/try_trace1.lean diff --git a/src/Init.lean b/src/Init.lean index 4a387d46e3..f3badf34c5 100644 --- a/src/Init.lean +++ b/src/Init.lean @@ -38,3 +38,4 @@ import Init.Grind import Init.While import Init.Syntax import Init.Internal +import Init.Try diff --git a/src/Init/Try.lean b/src/Init/Try.lean new file mode 100644 index 0000000000..56b944d8f0 --- /dev/null +++ b/src/Init/Try.lean @@ -0,0 +1,30 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Tactics + +namespace Lean.Try +/-- +Configuration for `try?`. +-/ +structure Config where + /-- If `main` is `true`, all functions in the current module are considered for function induction, unfolding, etc. -/ + 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 + deriving Inhabited + +end Lean.Try + +namespace Lean.Parser.Tactic + +syntax (name := tryTrace) "try?" optConfig : tactic + +end Lean.Parser.Tactic diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean index add9aea409..31e99106a5 100644 --- a/src/Lean/Elab/Tactic.lean +++ b/src/Lean/Elab/Tactic.lean @@ -46,3 +46,4 @@ import Lean.Elab.Tactic.BoolToPropSimps import Lean.Elab.Tactic.Classical import Lean.Elab.Tactic.Grind import Lean.Elab.Tactic.Monotonicity +import Lean.Elab.Tactic.Try diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean new file mode 100644 index 0000000000..6871380c9a --- /dev/null +++ b/src/Lean/Elab/Tactic/Try.lean @@ -0,0 +1,166 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Try +import Init.Grind.Tactics +import Lean.Meta.Tactic.Try +import Lean.Meta.Tactic.TryThis +import Lean.Elab.Tactic.Config + +namespace Lean.Elab.Tactic +open Meta +/-! +A **very** simple `try?` tactic implementation. +-/ + +declare_config_elab elabTryConfig Try.Config + +structure Try.Context where + mvarId : MVarId + config : Try.Config + tk : Syntax + +private abbrev M := ReaderT Try.Context TacticM + +instance : OrElse (M α) where + orElse a b := fun ctx => a ctx <|> b () ctx + +open Tactic in +private def addSuggestion (stx : TryThis.Suggestion) : M Bool := do + TryThis.addSuggestion (← read).tk stx (origSpan? := (← getRef)) + return true + +-- TODO: vanilla `induction`. +-- TODO: cleanup the whole file, and use better combinators +-- TODO: make it extensible. +-- TODO: librarySearch integration. +-- TODO: premise selection. + +private def failed (msg : MessageData) : M Bool := do + trace[«try»] msg + return false + +private def tryTac (stx : TSyntax `tactic) (msg : MessageData) : M Bool := + (do + focusAndDone <| evalTactic stx + addSuggestion stx) + <|> failed msg + +private def trySimp : M Bool := do + tryTac (← `(tactic| simp)) "`simp` failed" + +set_option hygiene false in +private def trySimpArith : M Bool := do + tryTac (← `(tactic| simp +arith)) "`simp +arith` failed" + +private def tryGrind : M Bool := do + (do + evalTactic (← `(tactic| grind -verbose)) + addSuggestion (← `(tactic| grind?))) + <|> failed "`grind` failed" + +private def collect : M Try.Info := do + Try.collect (← read).mvarId (← read).config + +private def toIdent (declName : Name) : MetaM Ident := do + return mkIdent (← unresolveNameGlobalAvoidingLocals declName) + +inductive TacticKind where + | exec + | suggestion + | error + +private def mkGrindStx (params : Array (TSyntax ``Parser.Tactic.grindParam)) (kind : TacticKind) : MetaM (TSyntax `tactic) := do + let result ← match kind with + | .exec => `(tactic| grind -verbose) + | .suggestion => `(tactic| grind?) + | .error => `(tactic| grind) + if params.isEmpty then + return result + else + let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"] + return ⟨result.raw.setArg 3 (mkNullNode paramsStx)⟩ + +private def mkGrindEqnsStx (declNames : Std.HashSet Name) : M (TacticKind → MetaM (TSyntax `tactic)) := do + let mut params := #[] + for declName in declNames do + params := params.push (← `(Parser.Tactic.grindParam| = $(← toIdent declName))) + return mkGrindStx params + +private def tryTac' (mkTac : TacticKind → MetaM (TSyntax `tactic)) : M Bool := do + let stx ← mkTac .exec + (do + focusAndDone <| evalTactic stx + addSuggestion (← mkTac .suggestion)) + <|> + (do failed m!"`{← mkTac .error}` failed") + +private def tryGrindEqns (info : Try.Info) : M Bool := do + if info.eqnCandidates.isEmpty then return false + tryTac' (← mkGrindEqnsStx info.eqnCandidates) + +private def tryGrindUnfold (info : Try.Info) : M Bool := do + if info.unfoldCandidates.isEmpty then return false + tryTac' (← mkGrindEqnsStx info.unfoldCandidates) + +private def allAccessible (majors : Array FVarId) : MetaM Bool := + majors.allM fun major => do + let localDecl ← major.getDecl + -- TODO: we are not checking shadowed variables + return !localDecl.userName.hasMacroScopes + +open Try.Collector in +private partial def tryFunIndsCore (info : Try.Info) (mkBody : TacticKind → MetaM (TSyntax `tactic)) : M Bool := do + go info.funIndCandidates.toList +where + go' (c : FunIndCandidate) : M Bool := do + if (← allAccessible c.majors) then + let mut terms := #[] + for major in c.majors do + let localDecl ← major.getDecl + terms := terms.push (← `($(mkIdent localDecl.userName):term)) + let indFn ← toIdent c.funIndDeclName + tryTac' fun k => do + let body ← mkBody k + `(tactic| induction $terms,* using $indFn <;> $body) + else + -- TODO: use `rename_i` + failed "`induction` failed, majors contain inaccessible vars {c.majors.map mkFVar}" + + go (cs : List FunIndCandidate) : M Bool := do + match cs with + | [] => return false + | c::cs => + trace[try.debug.funInd] "{c.funIndDeclName}, {c.majors.map mkFVar}" + go' c <||> go cs + +private partial def tryFunIndsGrind (info : Try.Info) : M Bool := + tryFunIndsCore info (mkGrindStx #[]) + +private partial def tryFunIndsGrindEqns (info : Try.Info) : M Bool := do + if info.eqnCandidates.isEmpty then return false + tryFunIndsCore info (← mkGrindEqnsStx info.eqnCandidates) + +private def evalTryTraceCore : M Unit := do + if (← trySimp) then return () + if (← trySimpArith) then return () + if (← tryGrind) then return () + let info ← collect + if (← tryGrindEqns info) then return () + if (← tryGrindUnfold info) then return () + if (← tryFunIndsGrind info) then return () + if (← tryFunIndsGrindEqns info) then return () + Meta.throwTacticEx `«try?» (← read).mvarId "consider using `grind` manually, `set_option trace.try true` shows everything `try?` tried" + +@[builtin_tactic Lean.Parser.Tactic.tryTrace] def evalTryTrace : Tactic := fun stx => do + match stx with + | `(tactic| try?%$tk $config:optConfig) => + let mvarId ← getMainGoal + let config ← elabTryConfig config + evalTryTraceCore { config, tk, mvarId } + | _ => throwUnsupportedSyntax + +end Lean.Elab.Tactic diff --git a/src/Lean/Meta/Tactic.lean b/src/Lean/Meta/Tactic.lean index 604576f54c..93dbc506b1 100644 --- a/src/Lean/Meta/Tactic.lean +++ b/src/Lean/Meta/Tactic.lean @@ -42,3 +42,4 @@ import Lean.Meta.Tactic.Rfl import Lean.Meta.Tactic.Rewrites import Lean.Meta.Tactic.Grind import Lean.Meta.Tactic.Ext +import Lean.Meta.Tactic.Try diff --git a/src/Lean/Meta/Tactic/Grind/Cases.lean b/src/Lean/Meta/Tactic/Grind/Cases.lean index 2a3f851723..448b70064b 100644 --- a/src/Lean/Meta/Tactic/Grind/Cases.lean +++ b/src/Lean/Meta/Tactic/Grind/Cases.lean @@ -66,6 +66,10 @@ def resetCasesExt : CoreM Unit := do def getCasesTypes : CoreM CasesTypes := return casesExt.getState (← getEnv) +/-- Returns `true` is `declName` is a builtin split or has been tagged with `[grind]` attribute. -/ +def isSplit (declName : Name) : CoreM Bool := do + return (← getCasesTypes).isSplit declName + private def getAlias? (value : Expr) : MetaM (Option Name) := lambdaTelescope value fun _ body => do if let .const declName _ := body.getAppFn' then diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index c5219109cb..0adba42996 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -228,6 +228,10 @@ private builtin_initialize ematchTheoremsExt : SimpleScopedEnvExtension EMatchTh initial := {} } +/-- Returns `true` if `declName` has been tagged as an E-match theorem using `[grind]`. -/ +def isEMatchTheorem (declName : Name) : CoreM Bool := do + return ematchTheoremsExt.getState (← getEnv) |>.omap.contains (.decl declName) + def resetEMatchTheoremsExt : CoreM Unit := do modifyEnv fun env => ematchTheoremsExt.modifyState env fun _ => {} diff --git a/src/Lean/Meta/Tactic/LibrarySearch.lean b/src/Lean/Meta/Tactic/LibrarySearch.lean index 493bc1a29e..f49becf53f 100644 --- a/src/Lean/Meta/Tactic/LibrarySearch.lean +++ b/src/Lean/Meta/Tactic/LibrarySearch.lean @@ -58,7 +58,7 @@ inductive DeclMod | /-- the original declaration -/ none | /-- the forward direction of an `iff` -/ mp | /-- the backward direction of an `iff` -/ mpr -deriving DecidableEq, Inhabited, Ord +deriving DecidableEq, Inhabited, Ord, Hashable /-- LibrarySearch has an extension mechanism for replacing the function used diff --git a/src/Lean/Meta/Tactic/Try.lean b/src/Lean/Meta/Tactic/Try.lean new file mode 100644 index 0000000000..18b0fbb463 --- /dev/null +++ b/src/Lean/Meta/Tactic/Try.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Lean.Meta.Tactic.Try.Collect + +namespace Lean + +builtin_initialize registerTraceClass `try +builtin_initialize registerTraceClass `try.collect +builtin_initialize registerTraceClass `try.collect.funInd + +builtin_initialize registerTraceClass `try.debug.funInd + +end Lean diff --git a/src/Lean/Meta/Tactic/Try/Collect.lean b/src/Lean/Meta/Tactic/Try/Collect.lean new file mode 100644 index 0000000000..2750721d86 --- /dev/null +++ b/src/Lean/Meta/Tactic/Try/Collect.lean @@ -0,0 +1,210 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Try +import Lean.Meta.Tactic.LibrarySearch +import Lean.Meta.Tactic.Util +import Lean.Meta.Tactic.Grind.Cases +import Lean.Meta.Tactic.Grind.EMatchTheorem + +namespace Lean.Meta.Try.Collector + +structure InductionCandidate where + fvarId : FVarId + val : InductiveVal + +structure FunIndCandidate where + funIndDeclName : Name + majors : Array FVarId + deriving Hashable, BEq + +structure Result where + /-- All constant symbols occurring in the gal. -/ + allConsts : Std.HashSet Name := {} + /-- Unfolding candiates. -/ + unfoldCandidates : Std.HashSet Name := {} + /-- Equation function candiates. -/ + eqnCandidates : Std.HashSet Name := {} + /-- Function induction candidates. -/ + funIndCandidates : Std.HashSet FunIndCandidate := {} + /-- Induction candidates. -/ + indCandidates : Array InductionCandidate := #[] + /-- Relevant declarations by `libSearch` -/ + libSearchResults : Std.HashSet (Name × Grind.EMatchTheoremKind) := {} + +structure Context where + config : Try.Config + +abbrev M := ReaderT Context <| StateRefT Result MetaM + +def getConfig : M Try.Config := do + return (← read).config + +def saveConst (declName : Name) : M Unit := do + modify fun s => { s with allConsts := s.allConsts.insert declName } + +/-- Returns `true` if `declName` is in the module being compiled. -/ +def inCurrentModule (declName : Name) : CoreM Bool := do + return ((← getEnv).getModuleIdxFor? declName).isNone + +def getFunInductName (declName : Name) : Name := + declName ++ `induct + +def getFunInduct? (declName : Name) : MetaM (Option Name) := do + let .defnInfo _ ← getConstInfo declName | return none + try + let result ← realizeGlobalConstNoOverloadCore (getFunInductName declName) + return some result + catch _ => + return none + +def isEligible (declName : Name) : M Bool := do + if declName.hasMacroScopes then + return false + if (← getConfig).main then + return (← inCurrentModule declName) + if (← getConfig).name then + let ns ← getCurrNamespace + return ns.isPrefixOf declName + return false + +def saveEqnCandidate (declName : Name) : M Unit := do + if (← isEligible declName) then + let some eqns ← getEqnsFor? declName | return () + if eqns.isEmpty then return () + unless (← Grind.isEMatchTheorem eqns[0]!) do + modify fun s => { s with eqnCandidates := s.eqnCandidates.insert declName } + +def getEqDefDecl? (declName : Name) : MetaM (Option Name) := do + let declName := declName ++ `eq_def + if (← Grind.isEMatchTheorem declName) then return none + try + let result ← realizeGlobalConstNoOverloadCore declName + return some result + catch _ => + return none + +def saveUnfoldCandidate (declName : Name) : M Unit := do + if (← isEligible declName) then + let some eqDefName ← getEqDefDecl? declName | return () + modify fun s => { s with unfoldCandidates := s.unfoldCandidates.insert eqDefName } + +def visitConst (declName : Name) : M Unit := do + saveConst declName + saveUnfoldCandidate declName + +-- Horrible temporary hack: compute the mask assuming parameters appear before a variable named `motive` +-- It assumes major premises appear after variables with name `case?` +-- It assumes if something is not a parameter, then it is major :( +-- TODO: save the mask while generating the induction principle. +def getFunIndMask? (declName : Name) (indDeclName : Name) : MetaM (Option (Array Bool)) := do + let info ← getConstInfo declName + let indInfo ← getConstInfo indDeclName + let (numParams, numMajor) ← forallTelescope indInfo.type fun xs _ => do + let mut foundCase := false + let mut foundMotive := false + let mut numParams : Nat := 0 + let mut numMajor : Nat := 0 + for x in xs do + let localDecl ← x.fvarId!.getDecl + let n := localDecl.userName + if n == `motive then + foundMotive := true + else if !foundMotive then + numParams := numParams + 1 + else if n.isStr && "case".isPrefixOf n.getString! then + foundCase := true + else if foundCase then + numMajor := numMajor + 1 + return (numParams, numMajor) + if numMajor == 0 then return none + forallTelescope info.type fun xs _ => do + if xs.size != numParams + numMajor then + return none + return some (mkArray numParams false ++ mkArray numMajor true) + +def saveFunInd (_e : Expr) (declName : Name) (args : Array Expr) : M Unit := do + if (← isEligible declName) then + let some funIndDeclName ← getFunInduct? declName + | saveUnfoldCandidate declName; return () + let some mask ← getFunIndMask? declName funIndDeclName | return () + if mask.size != args.size then return () + let mut majors := #[] + for arg in args, isMajor in mask do + if isMajor then + if !arg.isFVar then return () + majors := majors.push arg.fvarId! + trace[try.collect.funInd] "{funIndDeclName}, {majors.map mkFVar}" + modify fun s => { s with funIndCandidates := s.funIndCandidates.insert { majors, funIndDeclName }} + +open LibrarySearch in +def saveLibSearchCandidates (e : Expr) : M Unit := do + if (← getConfig).lib then + for (declName, declMod) in (← libSearchFindDecls e) do + unless (← Grind.isEMatchTheorem declName) do + let kind := match declMod with + | .none => .default + | .mp => .leftRight + | .mpr => .rightLeft + modify fun s => { s with libSearchResults := s.libSearchResults.insert (declName, kind) } + +def visitApp (e : Expr) (declName : Name) (args : Array Expr) : M Unit := do + saveEqnCandidate declName + saveFunInd e declName args + saveLibSearchCandidates e + +def checkInductive (localDecl : LocalDecl) : M Unit := do + let .const declName _ ← whnfD localDecl.type | return () + let .inductInfo val ← getConstInfo declName | return () + if (← isEligible declName) then + unless (← Grind.isSplit declName) do + modify fun s => { s with indCandidates := s.indCandidates.push { fvarId := localDecl.fvarId, val } } + +unsafe abbrev Cache := PtrSet Expr + +unsafe def visit (e : Expr) : StateRefT Cache M Unit := do + unless (← get).contains e do + modify fun s => s.insert e + match e with + | .const declName _ => visitConst declName + | .forallE _ d b _ => visit d; visit b + | .lam _ d b _ => visit d; visit b + | .mdata _ b => visit b + | .letE _ t v b _ => visit t; visit v; visit b + | .app .. => e.withApp fun f args => do + if let .const declName _ := f then + saveConst declName + unless e.hasLooseBVars do + visitApp e declName args + else + visit f + args.forM visit + | .proj _ _ b => visit b + | _ => return () + +unsafe def main (mvarId : MVarId) (config : Try.Config) : MetaM Result := mvarId.withContext do + let (_, s) ← go |>.run mkPtrSet |>.run { config } |>.run {} + return s +where + go : StateRefT Cache M Unit := do + unless (← getConfig).targetOnly do + for localDecl in (← getLCtx) do + unless localDecl.isAuxDecl do + if let some val := localDecl.value? then + visit val + else + checkInductive localDecl + visit localDecl.type + visit (← mvarId.getType) + +end Collector + +abbrev Info := Collector.Result + +def collect (mvarId : MVarId) (config : Try.Config) : MetaM Info := do + unsafe Collector.main mvarId config + +end Lean.Meta.Try diff --git a/tests/lean/run/grind_constProp.lean b/tests/lean/run/grind_constProp.lean index 8c40908ee1..acd43b7a66 100644 --- a/tests/lean/run/grind_constProp.lean +++ b/tests/lean/run/grind_constProp.lean @@ -207,6 +207,11 @@ def evalExpr (e : Expr) : EvalM Val := do @[grind] theorem UnaryOp.simplify_eval (op : UnaryOp) : (op.simplify a).eval σ = (Expr.una op a).eval σ := by grind [UnaryOp.simplify.eq_def] +/-- info: Try this: (induction e using Expr.simplify.induct) <;> grind? -/ +#guard_msgs (info) in +example (e : Expr) : e.simplify.eval σ = e.eval σ := by + try? + @[simp, grind =] theorem Expr.eval_simplify (e : Expr) : e.simplify.eval σ = e.eval σ := by induction e, σ using Expr.simplify.induct <;> grind @@ -293,7 +298,7 @@ theorem State.cons_le_of_eq (h₁ : σ' ≼ σ) (h₂ : σ.find? x = some v) : ( grind @[grind] theorem State.erase_le (σ : State) : σ.erase x ≼ σ := by - induction σ, x using State.erase.induct <;> grind + grind @[grind] theorem State.join_le_left (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₁ := by induction σ₁, σ₂ using State.join.induct <;> grind @@ -301,6 +306,11 @@ theorem State.cons_le_of_eq (h₁ : σ' ≼ σ) (h₂ : σ.find? x = some v) : ( @[grind] theorem State.join_le_left_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₁.join σ₃ ≼ σ₂ := by grind +/-- info: Try this: (induction σ₁, σ₂ using State.join.induct) <;> grind? -/ +#guard_msgs (info) in +example (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by + try? + @[grind] theorem State.join_le_right (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by induction σ₁, σ₂ using State.join.induct <;> grind diff --git a/tests/lean/run/prelude-injectivity.lean b/tests/lean/run/prelude-injectivity.lean index 7760408ff5..abb1fc027c 100644 --- a/tests/lean/run/prelude-injectivity.lean +++ b/tests/lean/run/prelude-injectivity.lean @@ -19,6 +19,7 @@ gen_injective_theorems% Macro.State gen_injective_theorems% Syntax.Preresolved gen_injective_theorems% Syntax.SepArray gen_injective_theorems% Syntax.TSepArray +gen_injective_theorems% Try.Config gen_injective_theorems% Parser.Tactic.DecideConfig -/ #guard_msgs in diff --git a/tests/lean/run/try_trace1.lean b/tests/lean/run/try_trace1.lean new file mode 100644 index 0000000000..bf9a0a2e77 --- /dev/null +++ b/tests/lean/run/try_trace1.lean @@ -0,0 +1,44 @@ +set_option grind.warning false + +/-- info: Try this: simp -/ +#guard_msgs (info) in +example : [1, 2] ≠ [] := by + try? + +/-- info: Try this: simp +arith -/ +#guard_msgs (info) in +example : 4 + x + y ≥ 1 + x := by + try? + +/-- info: Try this: grind? -/ +#guard_msgs (info) in +example (f : Nat → Nat) : f a = b → a = c → f c = b := by + try? + +def f : Nat → Nat + | 0 => 1 + | _ => 2 + +/-- info: Try this: grind? [= f] -/ +#guard_msgs (info) in +example : f (f 0) > 0 := by + try? + +/-- info: Try this: grind? [= f.eq_def] -/ +#guard_msgs (info) in +example : f x > 0 := by + try? + +def app : List α → List α → List α + | [], bs => bs + | a::as, bs => a :: app as bs + +/-- info: Try this: grind? [= app] -/ +#guard_msgs (info) in +example : app [a, b] [c] = [a, b, c] := by + try? + +/-- info: Try this: (induction as, bs using app.induct) <;> grind? [= app] -/ +#guard_msgs (info) in +example : app (app as bs) cs = app as (app bs cs) := by + try?