From 83098cdaec01dc982a4b5f81ad621e97ee413f42 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 8 Jan 2025 01:25:01 +1100 Subject: [PATCH] chore: typos / improvements to grind messages (#6561) This PR fixes some typos and makes minor improvements to grind doc-strings and messages. --- src/Init/Grind/Tactics.lean | 2 +- src/Init/Grind/Util.lean | 2 - src/Lean/Meta/Tactic/Grind/Canon.lean | 12 ++--- src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 48 +++++++++++-------- src/Lean/Meta/Tactic/Grind/Internalize.lean | 6 +-- src/Lean/Meta/Tactic/Grind/Split.lean | 8 ++-- src/Lean/Meta/Tactic/Grind/Types.lean | 12 ++--- 7 files changed, 49 insertions(+), 41 deletions(-) diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean index 3696eca31c..f4678adfc6 100644 --- a/src/Init/Grind/Tactics.lean +++ b/src/Init/Grind/Tactics.lean @@ -21,7 +21,7 @@ end Lean.Parser.Attr namespace Lean.Grind /-- The configuration for `grind`. -Passed to `grind` using, for example, the `grind (config := { eager := true })` syntax. +Passed to `grind` using, for example, the `grind (config := { matchEqs := true })` syntax. -/ structure Config where /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/ diff --git a/src/Init/Grind/Util.lean b/src/Init/Grind/Util.lean index 9a231e3181..9ef005388f 100644 --- a/src/Init/Grind/Util.lean +++ b/src/Init/Grind/Util.lean @@ -21,8 +21,6 @@ def doNotSimp {α : Sort u} (a : α) : α := a /-- Gadget for representing offsets `t+k` in patterns. -/ def offset (a b : Nat) : Nat := a + b -set_option pp.proofs true - theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (nestedProof p hp) (nestedProof q hq) := by subst h; apply HEq.refl diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean index 0505712170..6ac02c336e 100644 --- a/src/Lean/Meta/Tactic/Grind/Canon.lean +++ b/src/Lean/Meta/Tactic/Grind/Canon.lean @@ -22,7 +22,7 @@ to detect when two structurally different atoms are definitionally equal. The `grind` tactic, on the other hand, uses congruence closure. Moreover, types, type formers, proofs, and instances are considered supporting elements and are not factored into congruence detection. -This module minimizes the number of `isDefEq` checks by comparing two terms `a` and `b` only if they instances, +This module minimizes the number of `isDefEq` checks by comparing two terms `a` and `b` only if they are instances, types, or type formers and are the `i`-th arguments of two different `f`-applications. This approach is sufficient for the congruence closure procedure used by the `grind` tactic. @@ -129,17 +129,17 @@ where else let pinfos := (← getFunInfo f).paramInfo let mut modified := false - let mut args := args - for i in [:args.size] do - let arg := args[i]! + let mut args := args.toVector + for h : i in [:args.size] do + let arg := args[i] let arg' ← match (← shouldCanon pinfos i arg) with | .canonType => canonType f i arg | .canonInst => canonInst f i arg | .visit => visit arg unless ptrEq arg arg' do - args := args.set! i arg' + args := args.set i arg' modified := true - pure <| if modified then mkAppN f args else e + pure <| if modified then mkAppN f args.toArray else e | .forallE _ d b _ => -- Recall that we have `ForallProp.lean`. let d' ← visit d diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index 9605c8e116..c8299413f0 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -218,7 +218,7 @@ private def getPatternFn? (pattern : Expr) : Option Expr := | _ => none /-- -Returns a bit-mask `mask` s.t. `mask[i]` is true if the the corresponding argument is +Returns a bit-mask `mask` s.t. `mask[i]` is true if the corresponding argument is - a type (that is not a proposition) or type former, or - a proof, or - an instance implicit argument @@ -248,13 +248,13 @@ private partial def go (pattern : Expr) (root := false) : M Expr := do | throwError "invalid pattern, (non-forbidden) application expected{indentExpr pattern}" assert! f.isConst || f.isFVar saveSymbol f.toHeadIndex - let mut args := pattern.getAppArgs + let mut args := pattern.getAppArgs.toVector let supportMask ← getPatternSupportMask f args.size - for i in [:args.size] do - let arg := args[i]! + for h : i in [:args.size] do + let arg := args[i] let isSupport := supportMask[i]?.getD false - args := args.set! i (← goArg arg isSupport) - return mkAppN f args + args := args.set i (← goArg arg isSupport) + return mkAppN f args.toArray where goArg (arg : Expr) (isSupport : Bool) : M Expr := do if !arg.hasLooseBVars then @@ -556,8 +556,8 @@ private partial def collect (e : Expr) : CollectorM Unit := do -- restore state and continue search set saved catch _ => - -- restore state and continue search trace[grind.ematch.pattern.search] "skip, exception during normalization" + -- restore state and continue search set saved let args := e.getAppArgs for arg in args, flag in (← NormalizePattern.getPatternSupportMask f args.size) do @@ -592,7 +592,7 @@ private def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name | .fwd => let ps ← getPropTypes xs if ps.isEmpty then - throwError "invalid `grind` forward theorem, theorem `{← origin.pp}` does not have proposional hypotheses" + throwError "invalid `grind` forward theorem, theorem `{← origin.pp}` does not have propositional hypotheses" pure ps | .bwd => pure #[type] | .default => pure <| #[type] ++ (← getPropTypes xs) @@ -623,7 +623,7 @@ private def getKind (stx : Syntax) : TheoremKind := else .bwd -private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (useLhs := true) : MetaM Unit := do +private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) (useLhs := true) : MetaM Unit := do if (← getConstInfo declName).isTheorem then ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs)) attrKind else if let some eqns ← getEqnsFor? declName then @@ -632,18 +632,18 @@ private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (useLhs for eqn in eqns do ematchTheoremsExt.add (← mkEMatchEqTheorem eqn) attrKind else - throwError "`[grind_eq]` attribute can only be applied to equational theorems or function definitions" + throwError s!"`{thmKind.toAttribute}` attribute can only be applied to equational theorems or function definitions" private def addGrindAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) : MetaM Unit := do if thmKind == .eqLhs then - addGrindEqAttr declName attrKind (useLhs := true) + addGrindEqAttr declName attrKind thmKind (useLhs := true) else if thmKind == .eqRhs then - addGrindEqAttr declName attrKind (useLhs := false) + addGrindEqAttr declName attrKind thmKind (useLhs := false) else if thmKind == .eqBoth then - addGrindEqAttr declName attrKind (useLhs := true) - addGrindEqAttr declName attrKind (useLhs := false) + addGrindEqAttr declName attrKind thmKind (useLhs := true) + addGrindEqAttr declName attrKind thmKind (useLhs := false) else if !(← getConstInfo declName).isTheorem then - addGrindEqAttr declName attrKind + addGrindEqAttr declName attrKind thmKind else let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind | throwError "`@{thmKind.toAttribute} theorem {declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command" @@ -653,11 +653,21 @@ builtin_initialize registerBuiltinAttribute { name := `grind descr := - "The `[grind_eq]` attribute is used to annotate equational theorems and functions.\ - When applied to an equational theorem, it marks the theorem for use in heuristic instantiations by the `grind` tactic.\ - When applied to a function, it automatically annotates the equational theorems associated with that function.\ + "The `[grind]` attribute is used to annotate declarations.\ + \ + When applied to an equational theorem, `[grind =]`, `[grind =_]`, or `[grind _=_]`\ + will mark the theorem for use in heuristic instantiations by the `grind` tactic, + using respectively the left-hand side, the right-hand side, or both sides of the theorem.\ + When applied to a function, `[grind =]` automatically annotates the equational theorems associated with that function.\ + When applied to a theorem `[grind ←]` will instantiate the theorem whenever it encounters the conclusion of the theorem + (that is, it will use the theorem for backwards reasoning).\ + When applied to a theorem `[grind →]` will instantiate the theorem whenever it encounters sufficiently many of the propositional hypotheses + (that is, it will use the theorem for forwards reasoning).\ + \ + The attribute `[grind]` by itself will effectively try `[grind ←]` (if the conclusion is sufficient for instantiation) and then `[grind →]`.\ + \ The `grind` tactic utilizes annotated theorems to add instances of matching patterns into the local context during proof search.\ - For example, if a theorem `@[grind_eq] theorem foo_idempotent : foo (foo x) = foo x` is annotated,\ + For example, if a theorem `@[grind =] theorem foo_idempotent : foo (foo x) = foo x` is annotated,\ `grind` will add an instance of this theorem to the local context whenever it encounters the pattern `foo (foo x)`." applicationTime := .afterCompilation add := fun declName stx attrKind => do diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index 75b4743033..b0ee4931e2 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -47,13 +47,13 @@ private def updateAppMap (e : Expr) : GoalM Unit := do /-- Inserts `e` into the list of case-split candidates. -/ private def addSplitCandidate (e : Expr) : GoalM Unit := do trace[grind.split.candidate] "{e}" - modify fun s => { s with splitCadidates := e :: s.splitCadidates } + modify fun s => { s with splitCandidates := e :: s.splitCandidates } -- TODO: add attribute to make this extensible private def forbiddenSplitTypes := [``Eq, ``HEq, ``True, ``False] /-- Inserts `e` into the list of case-split candidates if applicable. -/ -private def checkAndaddSplitCandidate (e : Expr) : GoalM Unit := do +private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do unless e.isApp do return () if e.isIte || e.isDIte then addSplitCandidate e @@ -148,7 +148,7 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do -- We do not want to internalize the components of a literal value. mkENode e generation else e.withApp fun f args => do - checkAndaddSplitCandidate e + checkAndAddSplitCandidate e addMatchEqns f generation if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then -- We only internalize the proposition. We can skip the proof because of diff --git a/src/Lean/Meta/Tactic/Grind/Split.lean b/src/Lean/Meta/Tactic/Grind/Split.lean index 7c98474232..df1ff3f285 100644 --- a/src/Lean/Meta/Tactic/Grind/Split.lean +++ b/src/Lean/Meta/Tactic/Grind/Split.lean @@ -52,23 +52,23 @@ private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do if (← isResolvedCaseSplit e) then return .resolved if (← isMatcherApp e) then - return .notReady -- TODO: implement splittes for `match` + return .notReady -- TODO: implement splitters for `match` -- return .ready let .const declName .. := e.getAppFn | unreachable! if (← isInductivePredicate declName <&&> isEqTrue e) then return .ready return .notReady -/-- Returns the next case-split to be peformed. It uses a very simple heuristic. -/ +/-- Returns the next case-split to be performed. It uses a very simple heuristic. -/ private def selectNextSplit? : GoalM (Option Expr) := do if (← isInconsistent) then return none if (← checkMaxCaseSplit) then return none - go (← get).splitCadidates none [] + go (← get).splitCandidates none [] where go (cs : List Expr) (c? : Option Expr) (cs' : List Expr) : GoalM (Option Expr) := do match cs with | [] => - modify fun s => { s with splitCadidates := cs'.reverse } + modify fun s => { s with splitCandidates := cs'.reverse } if c?.isSome then -- Remark: we reset `numEmatch` after each case split. -- We should consider other strategies in the future. diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 4544196da5..e76d726275 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -29,7 +29,7 @@ def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]") /-- Returns `true` if `e` is `True`, `False`, or a literal value. -See `LitValues` for supported literals. +See `Lean.Meta.LitValues` for supported literals. -/ def isInterpreted (e : Expr) : MetaM Bool := do if e.isTrue || e.isFalse then return true @@ -59,11 +59,11 @@ structure CongrTheoremCacheKey where f : Expr numArgs : Nat --- We manually define `BEq` because we wannt to use pointer equality. +-- We manually define `BEq` because we want to use pointer equality. instance : BEq CongrTheoremCacheKey where beq a b := isSameExpr a.f b.f && a.numArgs == b.numArgs --- We manually define `Hashable` because we wannt to use pointer equality. +-- We manually define `Hashable` because we want to use pointer equality. instance : Hashable CongrTheoremCacheKey where hash a := mixHash (unsafe ptrAddrUnsafe a.f).toUInt64 (hash a.numArgs) @@ -123,7 +123,7 @@ def abstractNestedProofs (e : Expr) : GrindM Expr := do /-- Applies hash-consing to `e`. Recall that all expressions in a `grind` goal have -been hash-consing. We perform this step before we internalize expressions. +been hash-consed. We perform this step before we internalize expressions. -/ def shareCommon (e : Expr) : GrindM Expr := do modifyGet fun { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr, simpStats } => @@ -193,7 +193,7 @@ structure ENode where interpreted : Bool := false /-- `ctor := true` if the head symbol is a constructor application. -/ ctor : Bool := false - /-- `hasLambdas := true` if equivalence class contains lambda expressions. -/ + /-- `hasLambdas := true` if the equivalence class contains lambda expressions. -/ hasLambdas : Bool := false /-- If `heqProofs := true`, then some proofs in the equivalence class are based @@ -383,7 +383,7 @@ structure Goal where /-- `match` auxiliary functions whose equations have already been created and activated. -/ matchEqNames : PHashSet Name := {} /-- Case-split candidates. -/ - splitCadidates : List Expr := [] + splitCandidates : List Expr := [] /-- Number of splits performed to get to this goal. -/ numSplits : Nat := 0 /-- Case-splits that do not have to be performed anymore. -/