From 7087c4a039cdc603123594ce564ef9a1a49cd8c0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 Oct 2025 10:28:14 -0700 Subject: [PATCH] feat: add `splitNext` `grind` action (#10801) This PR implements the `splitNext` action for `grind`. --- src/Lean/Meta/Tactic/Grind/Action.lean | 94 ------------- src/Lean/Meta/Tactic/Grind/Split.lean | 127 ++++++++++++++++++ src/Lean/Meta/Tactic/Grind/Types.lean | 22 +-- tests/lean/run/grind_cutsat_trim_context.lean | 11 +- tests/lean/run/grind_linarith_2.lean | 23 ++-- .../lean/run/grind_linarith_trim_context.lean | 48 +++---- tests/lean/run/grind_offset_cnstr.lean | 14 +- tests/lean/run/grind_ring_trim_context.lean | 39 +++--- tests/lean/run/grind_semiring_norm.lean | 15 ++- tests/lean/run/noConfusionCtorInjection.lean | 13 +- 10 files changed, 225 insertions(+), 181 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/Action.lean b/src/Lean/Meta/Tactic/Grind/Action.lean index 1d7e083e5f..cf1726bd59 100644 --- a/src/Lean/Meta/Tactic/Grind/Action.lean +++ b/src/Lean/Meta/Tactic/Grind/Action.lean @@ -151,33 +151,6 @@ Executes `x`, but behaves like a `skip` if it is not applicable. def skipIfNA (x : Action) : Action := fun goal _ kp => x goal kp kp -private def isTargetFalse (mvarId : MVarId) : MetaM Bool := do - return (← mvarId.getType).isFalse - -private def getFalseProof? (mvarId : MVarId) : MetaM (Option Expr) := mvarId.withContext do - let proof ← instantiateMVars (mkMVar mvarId) - if (← isTargetFalse mvarId) then - return some proof - else if proof.isAppOfArity ``False.elim 2 || proof.isAppOfArity ``False.casesOn 2 then - return some proof.appArg! - else - return none - -/-- -Returns the maximum free variable id occurring in `e` --/ -private def findMaxFVarIdx? (e : Expr) : MetaM (Option Nat) := do - let go (e : Expr) : StateT (Option Nat) MetaM Bool := do - unless e.hasFVar do return false - let .fvar fvarId := e | return true - let localDecl ← fvarId.getDecl - modify fun - | none => some localDecl.index - | some index => some (max index localDecl.index) - return false - let (_, s?) ← e.forEach' go |>.run none - return s? - private def mkGrindSeq (s : List (TSyntax `grind)) : TSyntax ``Parser.Tactic.Grind.grindSeq := let s := s.map (·.raw) let s := s.intersperse (mkNullNode #[]) @@ -236,73 +209,6 @@ def ungroup : Action := fun goal _ kp => do else return r -/-- -Returns `some falseProof` if we can use non-chronological backtracking with `subgoal`. -That is, `subgoal` was closed using `falseProof`, but its proof does not use any of the -new hypotheses. A hypothesis is new if its `index >= oldNumIndices`. --/ -def useNCB? (oldNumIndices : Nat) (subgoal : Goal) : MetaM (Option Expr) := do - let some falseProof ← getFalseProof? subgoal.mvarId - | return none - let some max ← subgoal.mvarId.withContext <| findMaxFVarIdx? falseProof - | return some falseProof -- Proof actually closes any pending split - if max < oldNumIndices then - return some falseProof - else - return none - -/-- -Helper function for implementing tactics that perform case-splits -**Note**: We will probably delete this function. --/ -def splitCore - (goal : Goal) - (anchor? : Option (Nat × UInt64)) - (s : MVarId → GrindM (List MVarId)) - (kp : ActionCont) : GrindM ActionResult := do - let mvarDecl ← goal.mvarId.getDecl - let numIndices := mvarDecl.lctx.numIndices - let mvarId ← goal.mkAuxMVar - let mvarIds ← s mvarId - let subgoals := mvarIds.map fun mvarId => { goal with mvarId } - let traceEnabled := (← getConfig).trace - let mut seqNew : Array (List (TSyntax `grind)) := #[] - let mut stuckNew : Array Goal := #[] - for subgoal in subgoals do - match (← kp subgoal) with - | .stuck gs => - -- *TODO*: Add support for saving multiple failures - return .stuck gs - | .closed seq => - if let some falseProof ← useNCB? numIndices subgoal then - goal.mvarId.assignFalseProof falseProof - return .closed seq - else - seqNew := seqNew.push seq - if stuckNew.isEmpty then - goal.mvarId.assign (← instantiateMVars (mkMVar mvarId)) - if traceEnabled then - let seqListNew ← if h : seqNew.size = 1 then - pure seqNew[0] - else - seqNew.toList.mapM fun s => mkGrindNext s - let mut seqListNew := seqListNew - if let some anchor := anchor? then - let hexnum := mkNode `hexnum #[mkAtom (anchorToString anchor.1 anchor.2)] - /- - *TODO*: We need to distinguish between user-facing `cases` which `intros` new hypotheses - automatically, and auto-generated `cases` produced by `grind?` and `finish?` which does not - `intros` automatically. Each branch provides includes its own `intros`. - *Current strategy*: Use only one `cases` (`intros`) automatically and add `rename_i`. - -/ - let cases ← `(grind| cases #$hexnum) - seqListNew := cases :: seqListNew - return .closed seqListNew - else - return .closed [] - else - return .stuck stuckNew.toList - section /-! Some sanity check properties. diff --git a/src/Lean/Meta/Tactic/Grind/Split.lean b/src/Lean/Meta/Tactic/Grind/Split.lean index 08166589e2..3a7979bc61 100644 --- a/src/Lean/Meta/Tactic/Grind/Split.lean +++ b/src/Lean/Meta/Tactic/Grind/Split.lean @@ -7,11 +7,13 @@ module prelude public import Lean.Meta.Tactic.Grind.Types public import Lean.Meta.Tactic.Grind.SearchM +public import Lean.Meta.Tactic.Grind.Action import Lean.Meta.Tactic.Grind.Intro import Lean.Meta.Tactic.Grind.Cases import Lean.Meta.Tactic.Grind.Util import Lean.Meta.Tactic.Grind.CasesMatch import Lean.Meta.Tactic.Grind.Internalize +import Lean.Meta.Tactic.Grind.Anchor public section namespace Lean.Meta.Grind @@ -242,6 +244,131 @@ private def casesWithTrace (mvarId : MVarId) (major : Expr) : GoalM (List MVarId saveCases declName false cases mvarId major +namespace Action + +/-- +Given a `mvarId` associated with a subgoal created by `splitCore`, inspects the +proof term assigned to `mvarId` and tries to extract the proof of `False` that does not +depend on hypotheses introduced in the subgoal. +For example: suppose the subgoal is of the form `p → q → False` where `p` and `q` are new +hypotheses introduced during case analysis. If the proof is of the form `fun _ _ => h`, returns +`some h`. +-/ +private def getFalseProof? (mvarId : MVarId) : MetaM (Option Expr) := mvarId.withContext do + let proof ← instantiateMVars (mkMVar mvarId) + go proof +where + go (proof : Expr) : MetaM (Option Expr) := do + match_expr proof with + | False.elim _ p => return some p + | False.casesOn _ p => return some p + | id α p => if α.isFalse then return some p else return none + | _ => + /- + **Note**: `intros` tactics may hide the `False` proof behind a `casesOn` + For example: suppose the subgoal has a type of the form `p₁ → q₁ ∧ q₂ → p₂ → False` + The proof will be of the form `fun _ h => h.casesOn (fun _ _ => hf)` where `hf` is the proof + of `False` we are looking for. + Non-chronological backtracking currently fails in this kind of example. + -/ + let .lam _ _ b _ := proof | return none + if b.hasLooseBVars then return none + go b + +/-- +Performs a case-split using `c`. +Remark: `numCases` and `isRec` are computed using `checkSplitStatus`. +-/ +private def splitCore (c : SplitInfo) (numCases : Nat) (isRec : Bool) (stopAtFirstFailure : Bool) : Action := fun goal _ kp => do + let mvarDecl ← goal.mvarId.getDecl + let numIndices := mvarDecl.lctx.numIndices + let mvarId ← goal.mkAuxMVar + let cExpr := c.getExpr + let (mvarIds, goal) ← GoalM.run goal do + let gen ← getGeneration cExpr + let genNew := if numCases > 1 || isRec then gen+1 else gen + saveSplitDiagInfo cExpr genNew numCases c.source + markCaseSplitAsResolved cExpr + trace_goal[grind.split] "{cExpr}, generation: {gen}" + let mvarIds ← if let .imp e h _ := c then + casesWithTrace mvarId (mkGrindEM (e.forallDomain h)) + else if (← isMatcherApp cExpr) then + casesMatch mvarId cExpr + else + casesWithTrace mvarId (← mkCasesMajor cExpr) + let subgoals := mvarIds.map fun mvarId => { goal with mvarId } + let traceEnabled := (← getConfig).trace + let mut seqNew : Array (List (TSyntax `grind)) := #[] + let mut stuckNew : Array Goal := #[] + for subgoal in subgoals do + match (← kp subgoal) with + | .stuck gs => + if stopAtFirstFailure then + /- + **Note**: We don't need to assign `goal.mvarId` when `stopAtFirstFailure = true` + because the caller will not be able to process the all failure/stuck goals anyway. + -/ + return .stuck gs + else + stuckNew := stuckNew ++ gs + | .closed seq => + if let some falseProof ← getFalseProof? subgoal.mvarId then + goal.mvarId.assignFalseProof falseProof + return .closed seq + else if !seq.isEmpty then + /- **Note**: if the sequence is empty, it means the user will never see this goal. -/ + seqNew := seqNew.push seq + if (← goal.mvarId.getType).isFalse then + /- **Note**: We add the marker to assist `getFalseExpr?` -/ + goal.mvarId.assign (mkExpectedPropHint (← instantiateMVars (mkMVar mvarId)) (mkConst ``False)) + else + goal.mvarId.assign (← instantiateMVars (mkMVar mvarId)) + if stuckNew.isEmpty then + if traceEnabled then + let seqListNew ← if h : seqNew.size = 1 then + pure seqNew[0] + else + seqNew.toList.mapM fun s => mkGrindNext s + let mut seqListNew := seqListNew + let anchor ← goal.withContext <| getAnchor cExpr + -- **TODO**: compute the exact number of digits + let numDigits := 4 + let anchorPrefix := anchor >>> (64 - 16) + let hexnum := mkNode `hexnum #[mkAtom (anchorToString numDigits anchorPrefix)] + let cases ← `(grind| cases #$hexnum) + seqListNew := cases :: seqListNew + return .closed seqListNew + else + return .closed [] + else + return .stuck stuckNew.toList + +/-- +Selects a case-split from the list of candidates, performs the split and applies +continuation to all subgoals. +If a subgoal is solved without using new hypotheses, closes the original goal using this proof. That is, +it performs non-chronological backtracking. +If `stopsAtFirstFailure = true`, it stops the search as soon as the given continuation cannot solve a subgoal. +-/ +def splitNext (stopAtFirstFailure := true) : Action := fun goal kna kp => do + let (r, goal) ← GoalM.run goal selectNextSplit? + let .some c numCases isRec _ := r + | kna goal + let cExpr := c.getExpr + let gen := goal.getGeneration cExpr + let x : Action := splitCore c numCases isRec stopAtFirstFailure >> intros gen + x goal kna kp + +end Action + +/-! +**------------------------------------------** +**------------------------------------------** +**TODO** Delete rest of the file +**------------------------------------------** +**------------------------------------------** +-/ + /-- Performs a case-split using `c`. Remarks: diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 714a750c14..8e29631f09 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -923,10 +923,15 @@ def Goal.getENode (goal : Goal) (e : Expr) : CoreM ENode := do def getENode (e : Expr) : GoalM ENode := do (← get).getENode e +def Goal.getGeneration (goal : Goal) (e : Expr) : Nat := + if let some n := goal.getENode? e then + n.generation + else + 0 + /-- Returns the generation of the given term. Is assumes it has been internalized -/ -def getGeneration (e : Expr) : GoalM Nat := do - let some n ← getENode? e | return 0 - return n.generation +def getGeneration (e : Expr) : GoalM Nat := + return (← get).getGeneration e /-- Returns `true` if `e` is in the equivalence class of `True`. -/ def isEqTrue (e : Expr) : GoalM Bool := do @@ -1244,7 +1249,10 @@ If type of `mvarId` is not `False`, then use `False.elim`. def _root_.Lean.MVarId.assignFalseProof (mvarId : MVarId) (falseProof : Expr) : MetaM Unit := mvarId.withContext do let target ← mvarId.getType if target.isFalse then - mvarId.assign falseProof + /- + **Note**: We add the marker to assist `getFalseExpr?` used to implement + non-chronological backtracking. -/ + mvarId.assign (mkExpectedPropHint falseProof (mkConst ``False)) else mvarId.assign (← mkFalseElim target falseProof) @@ -1341,12 +1349,6 @@ def propagateUp (e : Expr) : GoalM Unit := do def propagateDown (e : Expr) : GoalM Unit := do (← getMethods).propagateDown e -def Goal.getGeneration (goal : Goal) (e : Expr) : Nat := - if let some n := goal.getENode? e then - n.generation - else - 0 - /-- Returns expressions in the given expression equivalence class. -/ partial def Goal.getEqc (goal : Goal) (e : Expr) (sort := false) : List Expr := let eqc := go e e #[] diff --git a/tests/lean/run/grind_cutsat_trim_context.lean b/tests/lean/run/grind_cutsat_trim_context.lean index 8577fd2ded..90acc44ca2 100644 --- a/tests/lean/run/grind_cutsat_trim_context.lean +++ b/tests/lean/run/grind_cutsat_trim_context.lean @@ -1,11 +1,12 @@ module /-- trace: [grind.debug.proof] fun h h_1 h_2 h_3 h_4 h_5 h_6 h_7 h_8 => - let ctx := RArray.leaf (f 2); - let p_1 := Poly.add 1 0 (Poly.num 0); - let p_2 := Poly.add (-1) 0 (Poly.num 1); - let p_3 := Poly.num 1; - le_unsat ctx p_3 (eagerReduce (Eq.refl true)) (le_combine ctx p_2 p_1 p_3 (eagerReduce (Eq.refl true)) h_8 h_1) + id + (let ctx := RArray.leaf (f 2); + let p_1 := Poly.add 1 0 (Poly.num 0); + let p_2 := Poly.add (-1) 0 (Poly.num 1); + let p_3 := Poly.num 1; + le_unsat ctx p_3 (eagerReduce (Eq.refl true)) (le_combine ctx p_2 p_1 p_3 (eagerReduce (Eq.refl true)) h_8 h_1)) -/ #guard_msgs in -- `cutsat` context should contain only `f 2` open Lean Int Linear in diff --git a/tests/lean/run/grind_linarith_2.lean b/tests/lean/run/grind_linarith_2.lean index 293869e5dc..fc716a6d3f 100644 --- a/tests/lean/run/grind_linarith_2.lean +++ b/tests/lean/run/grind_linarith_2.lean @@ -8,17 +8,18 @@ example [IntModule α] [LE α] [LT α] [IsPreorder α] [OrderedAdd α] (a b : α /-- trace: [grind.debug.proof] Classical.byContradiction fun h => - let ctx := RArray.leaf One.one; - let p_1 := Poly.nil; - let e_1 := Expr.zero; - let e_2 := Expr.intMul 0 (Expr.var 0); - let rctx := RArray.branch 1 (RArray.leaf a) (RArray.leaf b); - let rp_1 := CommRing.Poly.num 0; - let re_1 := (CommRing.Expr.var 0).add (CommRing.Expr.var 1); - let re_2 := (CommRing.Expr.var 1).add (CommRing.Expr.var 0); - diseq_unsat ctx - (diseq_norm ctx e_2 e_1 p_1 (eagerReduce (Eq.refl true)) - (CommRing.diseq_norm rctx re_1 re_2 rp_1 (eagerReduce (Eq.refl true)) h)) + id + (let ctx := RArray.leaf One.one; + let p_1 := Poly.nil; + let e_1 := Expr.zero; + let e_2 := Expr.intMul 0 (Expr.var 0); + let rctx := RArray.branch 1 (RArray.leaf a) (RArray.leaf b); + let rp_1 := CommRing.Poly.num 0; + let re_1 := (CommRing.Expr.var 0).add (CommRing.Expr.var 1); + let re_2 := (CommRing.Expr.var 1).add (CommRing.Expr.var 0); + diseq_unsat ctx + (diseq_norm ctx e_2 e_1 p_1 (eagerReduce (Eq.refl true)) + (CommRing.diseq_norm rctx re_1 re_2 rp_1 (eagerReduce (Eq.refl true)) h))) -/ #guard_msgs in open Linarith in diff --git a/tests/lean/run/grind_linarith_trim_context.lean b/tests/lean/run/grind_linarith_trim_context.lean index 64275ad8d9..719a5211b0 100644 --- a/tests/lean/run/grind_linarith_trim_context.lean +++ b/tests/lean/run/grind_linarith_trim_context.lean @@ -1,29 +1,31 @@ module /-- trace: [grind.debug.proof] fun h h_1 h_2 h_3 h_4 h_5 h_6 h_7 h_8 => - let ctx := RArray.branch 1 (RArray.leaf One.one) (RArray.leaf (f 2)); - let p_1 := Poly.nil; - let p_2 := Poly.add 1 1 Poly.nil; - let p_3 := Poly.add 1 0 Poly.nil; - let p_4 := Poly.add (-1) 1 (Poly.add 1 0 Poly.nil); - let p_5 := Poly.add (-1) 0 Poly.nil; - let e_1 := (Expr.intMul 1 (Expr.var 1)).add (Expr.intMul 0 (Expr.var 0)); - let e_2 := Expr.zero; - let e_3 := (Expr.intMul (-1) (Expr.var 1)).add (Expr.intMul 1 (Expr.var 0)); - let rctx := RArray.leaf (f 2); - let rp_1 := CommRing.Poly.add 1 (CommRing.Mon.mult { x := 0, k := 1 } CommRing.Mon.unit) (CommRing.Poly.num 0); - let rp_2 := CommRing.Poly.add (-1) (CommRing.Mon.mult { x := 0, k := 1 } CommRing.Mon.unit) (CommRing.Poly.num 1); - let re_1 := CommRing.Expr.var 0; - let re_2 := CommRing.Expr.num 0; - let re_3 := ((CommRing.Expr.num 1).neg.mul (CommRing.Expr.var 0)).add (CommRing.Expr.num 1); - lt_unsat ctx - (le_lt_combine ctx p_3 p_5 p_1 (eagerReduce (Eq.refl true)) - (le_le_combine ctx p_4 p_2 p_3 (eagerReduce (Eq.refl true)) - (le_norm ctx e_3 e_2 p_4 (eagerReduce (Eq.refl true)) - (CommRing.le_norm rctx re_3 re_2 rp_2 (eagerReduce (Eq.refl true)) h_8)) - (le_norm ctx e_1 e_2 p_2 (eagerReduce (Eq.refl true)) - (CommRing.le_norm rctx re_1 re_2 rp_1 (eagerReduce (Eq.refl true)) h_1))) - (zero_lt_one ctx p_5 (eagerReduce (Eq.refl true)) (Eq.refl One.one))) + id + (let ctx := RArray.branch 1 (RArray.leaf One.one) (RArray.leaf (f 2)); + let p_1 := Poly.nil; + let p_2 := Poly.add 1 1 Poly.nil; + let p_3 := Poly.add 1 0 Poly.nil; + let p_4 := Poly.add (-1) 1 (Poly.add 1 0 Poly.nil); + let p_5 := Poly.add (-1) 0 Poly.nil; + let e_1 := (Expr.intMul 1 (Expr.var 1)).add (Expr.intMul 0 (Expr.var 0)); + let e_2 := Expr.zero; + let e_3 := (Expr.intMul (-1) (Expr.var 1)).add (Expr.intMul 1 (Expr.var 0)); + let rctx := RArray.leaf (f 2); + let rp_1 := CommRing.Poly.add 1 (CommRing.Mon.mult { x := 0, k := 1 } CommRing.Mon.unit) (CommRing.Poly.num 0); + let rp_2 := + CommRing.Poly.add (-1) (CommRing.Mon.mult { x := 0, k := 1 } CommRing.Mon.unit) (CommRing.Poly.num 1); + let re_1 := CommRing.Expr.var 0; + let re_2 := CommRing.Expr.num 0; + let re_3 := ((CommRing.Expr.num 1).neg.mul (CommRing.Expr.var 0)).add (CommRing.Expr.num 1); + lt_unsat ctx + (le_lt_combine ctx p_3 p_5 p_1 (eagerReduce (Eq.refl true)) + (le_le_combine ctx p_4 p_2 p_3 (eagerReduce (Eq.refl true)) + (le_norm ctx e_3 e_2 p_4 (eagerReduce (Eq.refl true)) + (CommRing.le_norm rctx re_3 re_2 rp_2 (eagerReduce (Eq.refl true)) h_8)) + (le_norm ctx e_1 e_2 p_2 (eagerReduce (Eq.refl true)) + (CommRing.le_norm rctx re_1 re_2 rp_1 (eagerReduce (Eq.refl true)) h_1))) + (zero_lt_one ctx p_5 (eagerReduce (Eq.refl true)) (Eq.refl One.one)))) -/ #guard_msgs in open Std Lean Grind Linarith in diff --git a/tests/lean/run/grind_offset_cnstr.lean b/tests/lean/run/grind_offset_cnstr.lean index 9dd73d0e3b..0a6394a120 100644 --- a/tests/lean/run/grind_offset_cnstr.lean +++ b/tests/lean/run/grind_offset_cnstr.lean @@ -263,12 +263,14 @@ trace: [grind.debug.proof] intro_with_eq (p ↔ a2 ≤ a1) (p = (a2 ≤ a1)) (¬ intro_with_eq (p ↔ a4 ≤ a3 + 2) (p = (a4 ≤ a3 + 2)) (a1 ≤ a4) (iff_eq p (a4 ≤ a3 + 2)) fun h_3 => Classical.byContradiction (intro_with_eq (¬a1 ≤ a4) (a4 + 1 ≤ a1) False (Nat.not_le_eq a1 a4) fun h_4 => - Eq.mp - (Eq.trans (Eq.symm (eq_true h_4)) - (Nat.lo_eq_false_of_lo a1 a4 7 1 rfl_true - (Nat.lo_lo a1 a2 a4 1 6 (Nat.of_le_eq_false a2 a1 (Eq.trans (Eq.symm h) (eq_false h_1))) - (Nat.lo_lo a2 a3 a4 3 3 h_2 (Nat.of_ro_eq_false a4 a3 2 (Eq.trans (Eq.symm h_3) (eq_false h_1))))))) - True.intro) + id + (Eq.mp + (Eq.trans (Eq.symm (eq_true h_4)) + (Nat.lo_eq_false_of_lo a1 a4 7 1 rfl_true + (Nat.lo_lo a1 a2 a4 1 6 (Nat.of_le_eq_false a2 a1 (Eq.trans (Eq.symm h) (eq_false h_1))) + (Nat.lo_lo a2 a3 a4 3 3 h_2 + (Nat.of_ro_eq_false a4 a3 2 (Eq.trans (Eq.symm h_3) (eq_false h_1))))))) + True.intro)) -/ #guard_msgs in open Lean Grind in diff --git a/tests/lean/run/grind_ring_trim_context.lean b/tests/lean/run/grind_ring_trim_context.lean index 9be264d8a9..7316771dbb 100644 --- a/tests/lean/run/grind_ring_trim_context.lean +++ b/tests/lean/run/grind_ring_trim_context.lean @@ -2,25 +2,26 @@ module /-- trace: [grind.debug.proof] fun h h_1 h_2 h_3 => Classical.byContradiction fun h_4 => - let ctx := RArray.branch 1 (RArray.leaf x) (RArray.leaf x⁻¹); - let e_1 := (Expr.var 0).mul (Expr.var 1); - let e_2 := Expr.num 0; - let e_3 := Expr.num 1; - let e_4 := (Expr.var 0).pow 2; - let m_1 := Mon.mult (Power.mk 1 1) Mon.unit; - let m_2 := Mon.mult (Power.mk 0 1) Mon.unit; - let p_1 := Poly.num (-1); - let p_2 := Poly.add (-1) (Mon.mult (Power.mk 0 1) Mon.unit) (Poly.num 0); - let p_3 := Poly.add 1 (Mon.mult (Power.mk 0 2) Mon.unit) (Poly.num 0); - let p_4 := Poly.add 1 (Mon.mult (Power.mk 0 1) (Mon.mult (Power.mk 1 1) Mon.unit)) (Poly.num (-1)); - let p_5 := Poly.add 1 (Mon.mult (Power.mk 0 1) Mon.unit) (Poly.num 0); - one_eq_zero_unsat ctx p_1 (eagerReduce (Eq.refl true)) - (Stepwise.simp ctx 1 p_4 (-1) m_1 p_5 p_1 (eagerReduce (Eq.refl true)) - (Stepwise.core ctx e_1 e_3 p_4 (eagerReduce (Eq.refl true)) (diseq0_to_eq x h_4)) - (Stepwise.mul ctx p_2 (-1) p_5 (eagerReduce (Eq.refl true)) - (Stepwise.superpose ctx 1 m_2 p_4 (-1) m_1 p_3 p_2 (eagerReduce (Eq.refl true)) - (Stepwise.core ctx e_1 e_3 p_4 (eagerReduce (Eq.refl true)) (diseq0_to_eq x h_4)) - (Stepwise.core ctx e_4 e_2 p_3 (eagerReduce (Eq.refl true)) h)))) + id + (let ctx := RArray.branch 1 (RArray.leaf x) (RArray.leaf x⁻¹); + let e_1 := (Expr.var 0).mul (Expr.var 1); + let e_2 := Expr.num 0; + let e_3 := Expr.num 1; + let e_4 := (Expr.var 0).pow 2; + let m_1 := Mon.mult (Power.mk 1 1) Mon.unit; + let m_2 := Mon.mult (Power.mk 0 1) Mon.unit; + let p_1 := Poly.num (-1); + let p_2 := Poly.add (-1) (Mon.mult (Power.mk 0 1) Mon.unit) (Poly.num 0); + let p_3 := Poly.add 1 (Mon.mult (Power.mk 0 2) Mon.unit) (Poly.num 0); + let p_4 := Poly.add 1 (Mon.mult (Power.mk 0 1) (Mon.mult (Power.mk 1 1) Mon.unit)) (Poly.num (-1)); + let p_5 := Poly.add 1 (Mon.mult (Power.mk 0 1) Mon.unit) (Poly.num 0); + one_eq_zero_unsat ctx p_1 (eagerReduce (Eq.refl true)) + (Stepwise.simp ctx 1 p_4 (-1) m_1 p_5 p_1 (eagerReduce (Eq.refl true)) + (Stepwise.core ctx e_1 e_3 p_4 (eagerReduce (Eq.refl true)) (diseq0_to_eq x h_4)) + (Stepwise.mul ctx p_2 (-1) p_5 (eagerReduce (Eq.refl true)) + (Stepwise.superpose ctx 1 m_2 p_4 (-1) m_1 p_3 p_2 (eagerReduce (Eq.refl true)) + (Stepwise.core ctx e_1 e_3 p_4 (eagerReduce (Eq.refl true)) (diseq0_to_eq x h_4)) + (Stepwise.core ctx e_4 e_2 p_3 (eagerReduce (Eq.refl true)) h))))) -/ #guard_msgs in -- Context should contains only `x` and its inverse. set_option trace.grind.debug.proof true in diff --git a/tests/lean/run/grind_semiring_norm.lean b/tests/lean/run/grind_semiring_norm.lean index d0c412d3d8..ee475a2a4c 100644 --- a/tests/lean/run/grind_semiring_norm.lean +++ b/tests/lean/run/grind_semiring_norm.lean @@ -14,13 +14,14 @@ example (a b : R) : (a + b)^2 ≠ a^2 + 2 * a * b + b^2 → False := by grind /-- trace: [grind.debug.proof] fun h h_1 => - h_1 - (CommRing.eq_normS (RArray.branch 1 (RArray.leaf a) (RArray.leaf b)) - (((CommRing.Expr.var 0).add (CommRing.Expr.var 1)).pow 2) - ((((CommRing.Expr.var 0).pow 2).add - (((CommRing.Expr.num 2).mul (CommRing.Expr.var 0)).mul (CommRing.Expr.var 1))).add - ((CommRing.Expr.var 1).pow 2)) - (eagerReduce (Eq.refl true))) + id + (h_1 + (CommRing.eq_normS (RArray.branch 1 (RArray.leaf a) (RArray.leaf b)) + (((CommRing.Expr.var 0).add (CommRing.Expr.var 1)).pow 2) + ((((CommRing.Expr.var 0).pow 2).add + (((CommRing.Expr.num 2).mul (CommRing.Expr.var 0)).mul (CommRing.Expr.var 1))).add + ((CommRing.Expr.var 1).pow 2)) + (eagerReduce (Eq.refl true)))) -/ #guard_msgs in -- context should contain only `a` and `b` set_option trace.grind.debug.proof true in diff --git a/tests/lean/run/noConfusionCtorInjection.lean b/tests/lean/run/noConfusionCtorInjection.lean index 4d32599416..e4493d680d 100644 --- a/tests/lean/run/noConfusionCtorInjection.lean +++ b/tests/lean/run/noConfusionCtorInjection.lean @@ -43,12 +43,13 @@ fun {α} {x} {xs} {y} {ys} h => Classical.byContradiction (Lean.Grind.intro_with_eq (¬(x = y ∧ xs = ys)) (¬x = y ∨ ¬xs = ys) False (Lean.Grind.not_and (x = y) (xs = ys)) fun h_1 => - Eq.mp - (Eq.trans (Eq.symm (eq_true x_eq)) - (Lean.Grind.eq_false_of_not_eq_true - (Eq.trans (Eq.symm (Lean.Grind.or_eq_of_eq_false_right (Lean.Grind.not_eq_of_eq_true (eq_true xs_eq)))) - (eq_true h_1)))) - True.intro) + id + (Eq.mp + (Eq.trans (Eq.symm (eq_true x_eq)) + (Lean.Grind.eq_false_of_not_eq_true + (Eq.trans (Eq.symm (Lean.Grind.or_eq_of_eq_false_right (Lean.Grind.not_eq_of_eq_true (eq_true xs_eq)))) + (eq_true h_1)))) + True.intro)) -/ #guard_msgs in #print ex3._proof_1_1