diff --git a/src/Lean/Meta/Tactic/Contradiction.lean b/src/Lean/Meta/Tactic/Contradiction.lean index 534c7a0cb8..0b16d48327 100644 --- a/src/Lean/Meta/Tactic/Contradiction.lean +++ b/src/Lean/Meta/Tactic/Contradiction.lean @@ -96,12 +96,12 @@ private abbrev isGenDiseq (e : Expr) : Bool := See `processGenDiseq` -/ -private def mkGenDiseqMask (e : Expr) : Array Bool := +def mkGenDiseqMask (e : Expr) : Array Bool := go e #[] where go (e : Expr) (acc : Array Bool) : Array Bool := match e with - | Expr.forallE _ d b _ => go b (acc.push (!b.hasLooseBVar 0 && (d.isEq || d.isHEq))) + | .forallE _ d b _ => go b (acc.push (!b.hasLooseBVar 0 && (d.isEq || d.isHEq))) | _ => acc /-- diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean index 0ee855d596..a060bbaf84 100644 --- a/src/Lean/Meta/Tactic/Grind/Core.lean +++ b/src/Lean/Meta/Tactic/Grind/Core.lean @@ -234,7 +234,8 @@ private def popNextEq? : GoalM (Option NewEq) := do modify fun s => { s with newEqs := s.newEqs.pop } return r -private def processNewEqs : GoalM Unit := do +@[export lean_grind_process_new_eqs] +private def processNewEqsImpl : GoalM Unit := do repeat if (← isInconsistent) then resetNewEqs @@ -246,7 +247,7 @@ private def processNewEqs : GoalM Unit := do private def addEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do addEqStep lhs rhs proof isHEq - processNewEqs + processNewEqsImpl /-- Adds a new equality `lhs = rhs`. It assumes `lhs` and `rhs` have already been internalized. -/ private def addEq (lhs rhs proof : Expr) : GoalM Unit := do @@ -311,56 +312,4 @@ where def addHypothesis (fvarId : FVarId) (generation := 0) : GoalM Unit := do add (← fvarId.getType) (mkFVar fvarId) generation -/-- -Helper function for executing `x` with a fresh `newEqs` and without modifying -the goal state. - -/ -private def withoutModifyingState (x : GoalM α) : GoalM α := do - let saved ← get - modify fun goal => { goal with newEqs := {} } - try - x - finally - set saved - -/-- -If `e` has not been internalized yet, simplify it, and internalize the result. --/ -private def simpAndInternalize (e : Expr) (gen : Nat := 0) : GoalM Simp.Result := do - if (← alreadyInternalized e) then - return { expr := e } - else - let r ← simp e - internalize r.expr gen - return r - -/-- -Try to construct a proof that `lhs = rhs` using the information in the -goal state. If `lhs` and `rhs` have not been internalized, this function -will internalize then, process propagated equalities, and then check -whether they are in the same equivalence class or not. -The goal state is not modified by this function. -This function mainly relies on congruence closure, and constraint -propagation. It will not perform case analysis. --/ -def proveEq? (lhs rhs : Expr) : GoalM (Option Expr) := do - if (← alreadyInternalized lhs <&&> alreadyInternalized rhs) then - if (← isEqv lhs rhs) then - return some (← mkEqProof lhs rhs) - else - return none - else withoutModifyingState do - let lhs ← simpAndInternalize lhs - let rhs ← simpAndInternalize rhs - processNewEqs - unless (← isEqv lhs.expr rhs.expr) do return none - unless (← hasSameType lhs.expr rhs.expr) do return none - let h ← mkEqProof lhs.expr rhs.expr - let h ← match lhs.proof?, rhs.proof? with - | none, none => pure h - | none, some h₂ => mkEqTrans h (← mkEqSymm h₂) - | some h₁, none => mkEqTrans h₁ h - | some h₁, some h₂ => mkEqTrans (← mkEqTrans h₁ h) (← mkEqSymm h₂) - return some h - end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/MatchCond.lean b/src/Lean/Meta/Tactic/Grind/MatchCond.lean index 9800c3f334..4c4287375a 100644 --- a/src/Lean/Meta/Tactic/Grind/MatchCond.lean +++ b/src/Lean/Meta/Tactic/Grind/MatchCond.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura prelude import Init.Grind import Init.Simproc +import Lean.Meta.Tactic.Contradiction import Lean.Meta.Tactic.Simp.Simproc +import Lean.Meta.Tactic.Grind.ProveEq import Lean.Meta.Tactic.Grind.PropagatorAttr namespace Lean.Meta.Grind @@ -318,10 +320,94 @@ where else return none -def tryToProveFalse (e : Expr) : GoalM Unit := do +/-- +Given a `match`-expression condition `e` that is known to be equal to `True`, +try to close the goal by proving `False`. We use the following to example to illustrate +the purpose of this function. +``` +def f : List Nat → List Nat → Nat + | _, 1 :: _ :: _ => 1 + | _, _ :: _ => 2 + | _, _ => 0 + +example : z = a :: as → y = z → f x y > 0 := by + grind [f.eq_def] +``` +After `grind` unfolds `f`, it case splits on the `match`-expression producing +three subgoals. The first two are easily closed by it. In the third one, +we have the following two `match`-expression conditions stating that we +are **not** in the first and second cases. +``` +Lean.Grind.MatchCond (∀ (head : Nat) (tail : List Nat), x✝² = 1 :: head :: tail → False) +Lean.Grind.MatchCond (∀ (head : Nat) (tail : List Nat), x✝² = head :: tail → False) +``` +Moreover, we have the following equivalence class. +``` +{z, y, x✝², a :: as} +``` +Thus, we can close the goal by using the second `match`-expression condition, +we just have to instantiate `head` and `tail` with `a` and `as` respectively, +and use the fact that `x✝²` is equal to `a :: as`. +-/ +partial def tryToProveFalse (e : Expr) : GoalM Unit := do trace_goal[grind.debug.matchCond.proveFalse] "{e}" - -- TODO - return () + let_expr Grind.MatchCond body ← e | return () + let proof? ← withNewMCtxDepth do + let (args, _, _) ← forallMetaTelescope body + let mask := mkGenDiseqMask body + for arg in args, target in mask do + if target then + let some (α?, lhs, rhs) := isEqHEq? (← inferType arg) + | return none + let lhs' ← go lhs + trace[grind.debug.matchCond.proveFalse] "{lhs'} =?= {rhs}" + unless (← withDefault <| isDefEq lhs' rhs) do + return none + let isHEq := α?.isSome + let some lhsEqLhs' ← if isHEq then proveHEq? lhs lhs' else proveEq? lhs lhs' + | return none + unless (← isDefEq arg lhsEqLhs') do + return none + let he := mkOfEqTrueCore e (← mkEqTrueProof e) + let falseProof ← instantiateMVars (mkAppN he args) + if (← hasAssignableMVar falseProof) then + return none + trace[grind.debug.matchCond.proveFalse] "{falseProof} : {← inferType falseProof}" + return some falseProof + let some proof := proof? | return () + closeGoal proof +where + /-- + Returns a term that is equal to `e`, but containing constructor applications + and literal values. `e` is the left-hand side of the equations in a `match`-expression + condition. + Remark: we could use the right-hand side to interrupt the recursion. For example, + suppose the equation is `x = ?head :: ?tail`. We only need to show that `x` is equal to + some term of the form `a :: as` to satisfy it. This function may return `a₁ :: b :: bs`, + which still allows us to satisfy the equation, but may have a bigger proof (e.g., + a proof that `as` is equal to `b::bs`) + -/ + go (e : Expr) : GoalM Expr := do + let root ← getRootENode e + if root.ctor then + let ctor := root.self + let some ctorInfo ← isConstructorApp? ctor | return ctor + let mut ctorArgs := ctor.getAppArgs + let mut modified := false + for i in [ctorInfo.numParams : ctorInfo.numParams + ctorInfo.numFields] do + let arg := ctorArgs[i]! + let arg' ← go arg + unless isSameExpr arg arg' do + ctorArgs := ctorArgs.set! i arg' + modified := true + if modified then + shareCommon <| mkAppN ctor.getAppFn ctorArgs + else + return root.self + else if root.interpreted then + return root.self + else + return e /-- Propagates `MatchCond` upwards -/ builtin_grind_propagator propagateMatchCondUp ↑Grind.MatchCond := fun e => do diff --git a/src/Lean/Meta/Tactic/Grind/ProveEq.lean b/src/Lean/Meta/Tactic/Grind/ProveEq.lean new file mode 100644 index 0000000000..87c705765e --- /dev/null +++ b/src/Lean/Meta/Tactic/Grind/ProveEq.lean @@ -0,0 +1,85 @@ +/- +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.Grind.Types +import Lean.Meta.Tactic.Grind.Simp + +namespace Lean.Meta.Grind + +/-- +Helper function for executing `x` with a fresh `newEqs` and without modifying +the goal state. + -/ +private def withoutModifyingState (x : GoalM α) : GoalM α := do + let saved ← get + modify fun goal => { goal with newEqs := {} } + try + x + finally + set saved + +/-- +If `e` has not been internalized yet, simplify it, and internalize the result. +-/ +private def simpAndInternalize (e : Expr) (gen : Nat := 0) : GoalM Simp.Result := do + if (← alreadyInternalized e) then + return { expr := e } + else + let r ← simp e + internalize r.expr gen + return r + +/-- +Try to construct a proof that `lhs = rhs` using the information in the +goal state. If `lhs` and `rhs` have not been internalized, this function +will internalize then, process propagated equalities, and then check +whether they are in the same equivalence class or not. +The goal state is not modified by this function. +This function mainly relies on congruence closure, and constraint +propagation. It will not perform case analysis. +-/ +def proveEq? (lhs rhs : Expr) : GoalM (Option Expr) := do + if (← alreadyInternalized lhs <&&> alreadyInternalized rhs) then + if (← isEqv lhs rhs) then + return some (← mkEqProof lhs rhs) + else + return none + else withoutModifyingState do + let lhs ← simpAndInternalize lhs + let rhs ← simpAndInternalize rhs + processNewEqs + unless (← isEqv lhs.expr rhs.expr) do return none + unless (← hasSameType lhs.expr rhs.expr) do return none + let h ← mkEqProof lhs.expr rhs.expr + let h ← match lhs.proof?, rhs.proof? with + | none, none => pure h + | none, some h₂ => mkEqTrans h (← mkEqSymm h₂) + | some h₁, none => mkEqTrans h₁ h + | some h₁, some h₂ => mkEqTrans (← mkEqTrans h₁ h) (← mkEqSymm h₂) + return some h + +/-- Similiar to `proveEq?`, but for heterogeneous equality. -/ +def proveHEq? (lhs rhs : Expr) : GoalM (Option Expr) := do + if (← alreadyInternalized lhs <&&> alreadyInternalized rhs) then + if (← isEqv lhs rhs) then + return some (← mkHEqProof lhs rhs) + else + return none + else withoutModifyingState do + let lhs ← simpAndInternalize lhs + let rhs ← simpAndInternalize rhs + processNewEqs + unless (← isEqv lhs.expr rhs.expr) do return none + let h ← mkHEqProof lhs.expr rhs.expr + let h ← match lhs.proof?, rhs.proof? with + | none, none => pure h + | none, some h₂ => mkHEqTrans h (← mkHEqSymm h₂) + | some h₁, none => mkHEqTrans h₁ h + | some h₁, some h₂ => mkHEqTrans (← mkHEqTrans h₁ h) (← mkHEqSymm h₂) + return some h + + +end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 9876b5b3ae..6aeddb164a 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -744,6 +744,10 @@ opaque mkHEqProof (a b : Expr) : GoalM Expr @[extern "lean_grind_internalize"] opaque internalize (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit +-- Forward definition +@[extern "lean_grind_process_new_eqs"] +opaque processNewEqs : GoalM Unit + /-- Returns a proof that `a = b` if they have the same type. Otherwise, returns a proof of `HEq a b`. It assumes `a` and `b` are in the same equivalence class. diff --git a/tests/lean/run/grind_match_cond_contra.lean b/tests/lean/run/grind_match_cond_contra.lean new file mode 100644 index 0000000000..74960767ef --- /dev/null +++ b/tests/lean/run/grind_match_cond_contra.lean @@ -0,0 +1,7 @@ +def f : List Nat → List Nat → Nat + | _, 1 :: _ :: _ => 1 + | _, _ :: _ => 2 + | _, _ => 0 + +example : z = a :: as → y = z → f x y > 0 := by + grind [f.eq_def]