From 08ec2541c755b8797c09766ea55b4d7bc19e3526 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Jan 2025 21:22:05 -0800 Subject: [PATCH] feat: add support for constructors and axioms to the `grind` E-matching module (#6839) This PR ensures `grind` can use constructors and axioms for heuristic instantiation based on E-matching. It also allows patterns without pattern variables for theorems such as `theorem evenz : Even 0`. --- src/Lean/Declaration.lean | 4 + src/Lean/Elab/Tactic/Grind.lean | 2 +- src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 82 ++++++++++++++++--- src/Lean/Meta/Tactic/Grind/ForallProp.lean | 2 +- tests/lean/run/grind_ctor_ematch.lean | 69 ++++++++++++++++ tests/lean/run/grind_pattern1.lean | 4 +- 6 files changed, 145 insertions(+), 18 deletions(-) create mode 100644 tests/lean/run/grind_ctor_ematch.lean diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 038b1467d441..bcd3b8d390a4 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -478,6 +478,10 @@ def isCtor : ConstantInfo → Bool | .ctorInfo _ => true | _ => false +def isAxiom : ConstantInfo → Bool + | .axiomInfo _ => true + | _ => false + def isInductive : ConstantInfo → Bool | .inductInfo _ => true | _ => false diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index 03081441bf29..d9e3a0d95a62 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/src/Lean/Elab/Tactic/Grind.lean @@ -93,7 +93,7 @@ where addEMatchTheorem (params : Grind.Params) (declName : Name) (kind : Grind.EMatchTheoremKind) : MetaM Grind.Params := do let info ← getConstInfo declName match info with - | .thmInfo _ => + | .thmInfo _ | .axiomInfo _ | .ctorInfo _ => if kind == .eqBoth then let params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqLhs) } return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqRhs) } diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index ad0fb4e9b615..da3e23d186cc 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -359,9 +359,7 @@ def getPatternSupportMask (f : Expr) (numArgs : Nat) : MetaM (Array Bool) := do else return (← x.fvarId!.getDecl).binderInfo matches .instImplicit -private partial def go (pattern : Expr) (root := false) : M Expr := do - if root && !pattern.hasLooseBVars then - throwError "invalid pattern, it does not have pattern variables" +private partial def go (pattern : Expr) : M Expr := do if let some (e, k) := isOffsetPattern? pattern then let e ← goArg e (isSupport := false) if e == dontCare then @@ -550,9 +548,11 @@ def mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams levelParams, origin, kind } -private def getProofFor (declName : Name) : CoreM Expr := do - let .thmInfo info ← getConstInfo declName - | throwError "`{declName}` is not a theorem" +private def getProofFor (declName : Name) : MetaM Expr := do + let info ← getConstInfo declName + unless info.isTheorem do + unless (← isProp info.type) do + throwError "invalid E-matching theorem `{declName}`, type is not a proposition" let us := info.levelParams.map mkLevelParam return mkConst declName us @@ -699,7 +699,55 @@ private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Ar | return none return some (ps, s.symbols.toList) -def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) : MetaM (Option EMatchTheorem) := do +/-- +Tries to find a ground pattern to activate the theorem. +This is used for theorems such as `theorem evenZ : Even 0`. +This function is only used if `collectPatterns?` returns `none`. +-/ +private partial def collectGroundPattern? (proof : Expr) (xs : Array Expr) (searchPlaces : Array Expr) : MetaM (Option (Expr × List HeadIndex)) := do + unless (← checkCoverage proof xs.size {}) matches .ok do + return none + let go? : CollectorM (Option Expr) := do + for place in searchPlaces do + let place ← preprocessPattern place + if let some r ← visit? place then + return r + return none + let (some p, s) ← go? { proof, xs } |>.run' {} |>.run {} + | return none + return some (p, s.symbols.toList) +where + visit? (e : Expr) : CollectorM (Option Expr) := do + match e with + | .app .. => + let f := e.getAppFn + if (← isPatternFnCandidate f) then + let e ← NormalizePattern.normalizePattern e + return some e + else + let args := e.getAppArgs + for arg in args, flag in (← NormalizePattern.getPatternSupportMask f args.size) do + unless flag do + if let some r ← visit? arg then + return r + return none + | .forallE _ d b _ => + if (← pure e.isArrow <&&> isProp d <&&> isProp b) then + if let some d ← visit? d then return d + visit? b + else + return none + | _ => return none + +/-- +Creates an E-match theorem using the given proof and kind. +If `groundPatterns` is `true`, it accepts patterns without pattern variables. This is useful for +theorems such as `theorem evenZ : Even 0`. For local theorems, we use `groundPatterns := false` +since the theorem is already in the `grind` state and there is nothing to be instantiated. +-/ +def mkEMatchTheoremWithKind? + (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) + (groundPatterns := true) : MetaM (Option EMatchTheorem) := do if kind == .eqLhs then return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true)) else if kind == .eqRhs then @@ -720,8 +768,14 @@ def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof go xs searchPlaces where go (xs : Array Expr) (searchPlaces : Array Expr) : MetaM (Option EMatchTheorem) := do - let some (patterns, symbols) ← collectPatterns? proof xs searchPlaces - | return none + let (patterns, symbols) ← if let some r ← collectPatterns? proof xs searchPlaces then + pure r + else if !groundPatterns then + return none + else if let some (pattern, symbols) ← collectGroundPattern? proof xs searchPlaces then + pure ([pattern], symbols) + else + return none let numParams := xs.size trace[grind.ematch.pattern] "{← origin.pp}: {patterns.map ppPattern}" return some { @@ -774,11 +828,13 @@ def addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatch else if thmKind == .eqBoth then addGrindEqAttr declName attrKind thmKind (useLhs := true) addGrindEqAttr declName attrKind thmKind (useLhs := false) - else if !(← getConstInfo declName).isTheorem then - addGrindEqAttr declName attrKind thmKind else - let thm ← mkEMatchTheoremForDecl declName thmKind - ematchTheoremsExt.add thm attrKind + let info ← getConstInfo declName + if !info.isTheorem && !info.isCtor && !info.isAxiom then + addGrindEqAttr declName attrKind thmKind + else + let thm ← mkEMatchTheoremForDecl declName thmKind + ematchTheoremsExt.add thm attrKind def eraseEMatchAttr (declName : Name) : MetaM Unit := do /- diff --git a/src/Lean/Meta/Tactic/Grind/ForallProp.lean b/src/Lean/Meta/Tactic/Grind/ForallProp.lean index dcdaea8f595c..4b5688a3e2ea 100644 --- a/src/Lean/Meta/Tactic/Grind/ForallProp.lean +++ b/src/Lean/Meta/Tactic/Grind/ForallProp.lean @@ -55,7 +55,7 @@ private def isEqTrueHyp? (proof : Expr) : Option FVarId := Id.run do /-- Similar to `mkEMatchTheoremWithKind?`, but swallow any exceptions. -/ private def mkEMatchTheoremWithKind'? (origin : Origin) (proof : Expr) (kind : EMatchTheoremKind) : MetaM (Option EMatchTheorem) := do try - mkEMatchTheoremWithKind? origin #[] proof kind + mkEMatchTheoremWithKind? origin #[] proof kind (groundPatterns := false) catch _ => return none diff --git a/tests/lean/run/grind_ctor_ematch.lean b/tests/lean/run/grind_ctor_ematch.lean new file mode 100644 index 000000000000..69d126f0b9fa --- /dev/null +++ b/tests/lean/run/grind_ctor_ematch.lean @@ -0,0 +1,69 @@ +inductive Even : Nat → Prop + | zero : Even 0 + | plus_two {n} : Even n → Even (n + 2) + +example : Even 2 := by + grind [Even.plus_two, Even.zero] + +attribute [grind] Even.zero +attribute [grind] Even.plus_two + +example : Even 2 := by + grind + +example : Even 4 := by + grind + +/-- +error: `grind` failed +case grind +x✝ : ¬Even 16 +⊢ False +[grind] Diagnostics + [facts] Asserted facts + [prop] ¬Even 16 + [prop] Even 14 → Even 16 + [prop] Even 12 → Even 14 + [prop] Even 10 → Even 12 + [prop] Even 8 → Even 10 + [prop] Even 6 → Even 8 + [eqc] True propositions + [prop] Even 14 → Even 16 + [prop] Even 12 → Even 14 + [prop] Even 10 → Even 12 + [prop] Even 8 → Even 10 + [prop] Even 6 → Even 8 + [eqc] False propositions + [prop] Even 16 + [ematch] E-matching patterns + [thm] Even.plus_two: [Even (Lean.Grind.offset #1 (2))] + [thm] Even.zero: [Even `[0]] + [limits] Thresholds reached + [limit] maximum number of E-matching rounds has been reached, threshold: `(ematch := 5)` + [limit] maximum term generation has been reached, threshold: `(gen := 5)` +[grind] Counters + [thm] E-Matching instances + [thm] Even.plus_two ↦ 5 +-/ +#guard_msgs (error) in +example : Even 16 := by + grind + +example : Even 16 := by + grind (gen := 9) (ematch := 9) + +opaque f : Nat → Nat + +axiom fax (x : Nat) : f (f x) = f x + +example : f (f (f x)) = f x := by + grind [fax] + +attribute [grind] fax + +example : f (f (f x)) = f x := by + grind + +/-- error: invalid E-matching theorem `Nat.succ`, type is not a proposition -/ +#guard_msgs in +attribute [grind] Nat.succ diff --git a/tests/lean/run/grind_pattern1.lean b/tests/lean/run/grind_pattern1.lean index d827e1efa0d5..c01604ddb5fd 100644 --- a/tests/lean/run/grind_pattern1.lean +++ b/tests/lean/run/grind_pattern1.lean @@ -19,9 +19,7 @@ grind_pattern List.mem_concat_self => a ∈ xs ++ [a] def foo (x : Nat) := x + x -/-- -error: `foo` is not a theorem --/ +/-- error: invalid E-matching theorem `foo`, type is not a proposition -/ #guard_msgs in grind_pattern foo => x + x