From 9565334c0e5b98fc814e101aba3695f3972ce9be Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Jan 2025 11:53:26 -0800 Subject: [PATCH] fix: `Grind.MatchCond` in `checkParents` (#6776) This PR fixes the `checkParents` sanity checker used in `grind`. It did not have support for checking the auxiliary gadget `Grind.MatchCond`. --- src/Lean/Meta/AbstractNestedProofs.lean | 8 +++- src/Lean/Meta/Tactic/Grind/CasesMatch.lean | 4 +- src/Lean/Meta/Tactic/Grind/Inv.lean | 56 +++++++++++++++------- src/Lean/Meta/Tactic/Grind/MatchCond.lean | 3 ++ 4 files changed, 51 insertions(+), 20 deletions(-) diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean index 0aaf8d50d2..36124e8d75 100644 --- a/src/Lean/Meta/AbstractNestedProofs.lean +++ b/src/Lean/Meta/AbstractNestedProofs.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude +import Init.Grind.Util import Lean.Meta.Closure namespace Lean.Meta @@ -16,7 +17,12 @@ def getLambdaBody (e : Expr) : Expr := def isNonTrivialProof (e : Expr) : MetaM Bool := do if !(← isProof e) then - pure false + return false + else if e.isAppOf ``Grind.nestedProof then + -- Grind.nestedProof is a gadget created by the `grind` tactic. + -- We want to avoid the situation where `grind` keeps creating them, + -- and this module, which is used by `grind`, keeps abstracting them. + return false else -- We consider proofs such as `fun x => f x a` as trivial. -- For example, we don't want to abstract the body of `def rfl` diff --git a/src/Lean/Meta/Tactic/Grind/CasesMatch.lean b/src/Lean/Meta/Tactic/Grind/CasesMatch.lean index 0244bb1eef..777f3a78df 100644 --- a/src/Lean/Meta/Tactic/Grind/CasesMatch.lean +++ b/src/Lean/Meta/Tactic/Grind/CasesMatch.lean @@ -14,7 +14,7 @@ namespace Lean.Meta.Grind /-- Returns `true` if `e` is of the form `∀ ..., _ = _ ... -> False` -/ -private def isMatchCond (e : Expr) : Bool := Id.run do +private def isMatchCondCandidate (e : Expr) : Bool := Id.run do let mut e := e let mut hasEqs := false repeat @@ -31,7 +31,7 @@ conditions corresponding to overlapping patterns. private def addMatchCondsToAlt (alt : Expr) : Expr := Id.run do let .forallE _ d b _ := alt | return alt - let d := if isMatchCond d then markAsMatchCond d else d + let d := if isMatchCondCandidate d then markAsMatchCond d else d return alt.updateForallE! d (addMatchCondsToAlt b) /-- diff --git a/src/Lean/Meta/Tactic/Grind/Inv.lean b/src/Lean/Meta/Tactic/Grind/Inv.lean index cfebc1653f..0a0bc3a25a 100644 --- a/src/Lean/Meta/Tactic/Grind/Inv.lean +++ b/src/Lean/Meta/Tactic/Grind/Inv.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura prelude import Lean.Meta.Tactic.Grind.Types import Lean.Meta.Tactic.Grind.Proof +import Lean.Meta.Tactic.Grind.MatchCond import Lean.Meta.Tactic.Grind.Arith.Inv namespace Lean.Meta.Grind @@ -46,27 +47,48 @@ private def checkEqc (root : ENode) : GoalM Unit := do -- The size of the equivalence class is correct. assert! root.size == size +def checkChild (e : Expr) (child : Expr) : GoalM Bool := do + let some childRoot ← getRoot? child | return false + return isSameExpr childRoot e + +private def checkMatchCondParent (e : Expr) (parent : Expr) : GoalM Bool := do + let_expr Grind.MatchCond parent ← parent | return false + let mut curr := parent + repeat + let .forallE _ d b _ := curr + | return false + match_expr d with + | Eq _ lhs _ => if (← checkChild e lhs) then return true -- found it + | HEq α lhs _ _ => if (← checkChild e α <||> checkChild e lhs) then return true -- found it + | _ => pure () + curr := b + return false + private def checkParents (e : Expr) : GoalM Unit := do if (← isRoot e) then for parent in (← getParents e) do - let mut found := false - let checkChild (child : Expr) : GoalM Bool := do - let some childRoot ← getRoot? child | return false - return isSameExpr childRoot e - -- There is an argument `arg` s.t. root of `arg` is `e`. - for arg in parent.getAppArgs do - if (← checkChild arg) then - found := true - break - -- Recall that we have support for `Expr.forallE` propagation. See `ForallProp.lean`. - if let .forallE _ d b _ := parent then - if (← checkChild d) then - found := true - unless b.hasLooseBVars do - if (← checkChild b) then + if isMatchCond parent then + unless (← checkMatchCondParent e parent) do + throwError "e: {e}, parent: {parent}" + assert! (← checkMatchCondParent e parent) + else + let mut found := false + -- There is an argument `arg` s.t. root of `arg` is `e`. + for arg in parent.getAppArgs do + if (← checkChild e arg) then found := true - unless found do - assert! (← checkChild parent.getAppFn) + break + -- Recall that we have support for `Expr.forallE` propagation. See `ForallProp.lean`. + if let .forallE _ d b _ := parent then + if (← checkChild e d) then + found := true + unless b.hasLooseBVars do + if (← checkChild e b) then + found := true + unless found do + unless (← checkChild e parent.getAppFn) do + throwError "e: {e}, parent: {parent}" + assert! (← checkChild e parent.getAppFn) else -- All the parents are stored in the root of the equivalence class. assert! (← getParents e).isEmpty diff --git a/src/Lean/Meta/Tactic/Grind/MatchCond.lean b/src/Lean/Meta/Tactic/Grind/MatchCond.lean index a904745839..b5e6bf0c3f 100644 --- a/src/Lean/Meta/Tactic/Grind/MatchCond.lean +++ b/src/Lean/Meta/Tactic/Grind/MatchCond.lean @@ -81,6 +81,9 @@ and we have special support for propagating is truth value. def markAsMatchCond (e : Expr) : Expr := mkApp (mkConst ``Grind.MatchCond) e +def isMatchCond (e : Expr) : Bool := + e.isAppOfArity ``Grind.MatchCond 1 + builtin_dsimproc_decl reduceMatchCond (Grind.MatchCond _) := fun e => do let_expr Grind.MatchCond _ ← e | return .continue return .done e