max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: better support for partial applications in the E-matching procedure (#6654)

Browse source 
This PR improves the support for partial applications in the E-matching
procedure used in `grind`.
This commit is contained in:
Leonardo de Moura 2025-01-15 10:31:34 -08:00 • committed by GitHub
parent b3f8feffd3
commit 54f06ccd64
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 13 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Lean/Meta/Tactic/Grind/EMatch.lean
View file

@ -129,6 +129,16 @@ private partial def matchArgs? (c : Choice) (p : Expr) (e : Expr) : OptionT Goal
let c ← matchArg? c pArg eArg
matchArgs? c p.appFn! e.appFn!
/-- Similar to `matchArgs?` but if `p` has fewer arguments than `e`, we match `p` with a prefix of `e`. -/
private partial def matchArgsPrefix? (c : Choice) (p : Expr) (e : Expr) : OptionT GoalM Choice := do
let pn := p.getAppNumArgs
let en := e.getAppNumArgs
guard (pn <= en)
if pn == en then
matchArgs? c p e
else
matchArgs? c p (e.getAppPrefix pn)
/--
Matches pattern `p` with term `e` with respect to choice `c`.
We traverse the equivalence class of `e` looking for applications compatible with `p`.
@ -194,7 +204,7 @@ private def processContinue (c : Choice) (p : Expr) : M Unit := do
let n ← getENode app
if n.generation < maxGeneration
&& (n.heqProofs || n.isCongrRoot) then
if let some c ← matchArgs? c p app |>.run then
if let some c ← matchArgsPrefix? c p app |>.run then
let gen := n.generation
let c := { c with gen := Nat.max gen c.gen }
modify fun s => { s with choiceStack := c :: s.choiceStack }
@ -300,7 +310,7 @@ private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
if (n.heqProofs || n.isCongrRoot) &&
(!useMT || n.mt == gmt) then
withInitApp app do
if let some c ← matchArgs? { cnstrs, assignment, gen := n.generation } p app |>.run then
if let some c ← matchArgsPrefix? { cnstrs, assignment, gen := n.generation } p app |>.run then
modify fun s => { s with choiceStack := [c] }
processChoices

2
src/Lean/Meta/Tactic/Grind/PP.lean
View file

@ -101,7 +101,7 @@ private def ppEqcs (goal : Goal) : MetaM (Array MessageData) := do
return result
private def ppEMatchTheorem (thm : EMatchTheorem) : MetaM MessageData := do
let m := m!"{← thm.origin.pp}\n{← inferType thm.proof}\npatterns: {thm.patterns.map ppPattern}"
let m := m!"{← thm.origin.pp}:\n{← inferType thm.proof}\npatterns: {thm.patterns.map ppPattern}"
return .trace { cls := `thm } m #[]
private def ppActiveTheorems (goal : Goal) : MetaM MessageData := do