From 70df9742f4aeba78da72434dff4bdcf26c600a56 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Apr 2026 01:51:21 +0200 Subject: [PATCH] fix: kernel error in `grind` order module for `Nat` casts to non-`Int` types (#13453) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR fixes a kernel error in `grind` when propagating a `Nat` equality to an order structure whose carrier type is not `Int` (e.g. `Rat`). The auxiliary `Lean.Grind.Order.of_nat_eq` lemma was specialized to `Int`, so the kernel rejected the application when the cast destination differed. We add a polymorphic `of_natCast_eq` lemma over `{α : Type u} [NatCast α]` and cache the cast destination type in `TermMapEntry`. `processNewEq` now uses the original `of_nat_eq` when the destination is `Int` (the common case) and the new lemma otherwise. The symmetric `nat_eq` propagation (deriving `Nat` equality from a derived cast equality) is now guarded to fire only when the destination is `Int`, since the `nat_eq` lemma is still specialized to `Int`. Closes #13265. --- src/Init/Grind/Order.lean | 3 ++ src/Lean/Meta/Tactic/Grind/Order/Assert.lean | 30 ++++++++++++------- .../Meta/Tactic/Grind/Order/Internalize.lean | 14 ++++----- src/Lean/Meta/Tactic/Grind/Order/Types.lean | 9 +++++- tests/elab/grind_order_eq.lean | 3 ++ 5 files changed, 41 insertions(+), 18 deletions(-) diff --git a/src/Init/Grind/Order.lean b/src/Init/Grind/Order.lean index 88e200c572..ded0305dae 100644 --- a/src/Init/Grind/Order.lean +++ b/src/Init/Grind/Order.lean @@ -75,6 +75,9 @@ theorem nat_eq (a b : Nat) (x y : Int) : NatCast.natCast a = x → NatCast.natCa theorem of_nat_eq (a b : Nat) (x y : Int) : NatCast.natCast a = x → NatCast.natCast b = y → a = b → x = y := by intro _ _; subst x y; intro; simp [*] +theorem of_natCast_eq {α : Type u} [NatCast α] (a b : Nat) (x y : α) : NatCast.natCast a = x → NatCast.natCast b = y → a = b → x = y := by + intro h₁ h₂ h; subst h; exact h₁.symm.trans h₂ + theorem le_of_not_le {α} [LE α] [Std.IsLinearPreorder α] {a b : α} : ¬ a ≤ b → b ≤ a := by intro h diff --git a/src/Lean/Meta/Tactic/Grind/Order/Assert.lean b/src/Lean/Meta/Tactic/Grind/Order/Assert.lean index 3aa8b3a36b..594ada1a08 100644 --- a/src/Lean/Meta/Tactic/Grind/Order/Assert.lean +++ b/src/Lean/Meta/Tactic/Grind/Order/Assert.lean @@ -148,11 +148,14 @@ def propagatePending : OrderM Unit := do - `h₁ : ↑ue' = ue` - `h₂ : ↑ve' = ve` - `h : ue = ve` - **Note**: We currently only support `Nat`. Thus `↑a` is actually - `NatCast.natCast a`. If we decide to support arbitrary semirings - in this module, we must adjust this code. + **Note**: We currently only support `Nat` originals. Thus `↑a` is actually + `NatCast.natCast a`. The lemma `nat_eq` is specialized to `Int`, so we + only invoke it when the cast destination is `Int`. For other types (e.g. + `Rat`), `pushEq ue ve h` above is sufficient and `grind` core can derive + the `Nat` equality via `norm_cast`/cast injectivity if needed. -/ - pushEq ue' ve' <| mkApp7 (mkConst ``Grind.Order.nat_eq) ue' ve' ue ve h₁ h₂ h + if (← inferType ue) == Int.mkType then + pushEq ue' ve' <| mkApp7 (mkConst ``Grind.Order.nat_eq) ue' ve' ue ve h₁ h₂ h where /-- If `e` is an auxiliary term used to represent some term `a`, returns @@ -343,7 +346,7 @@ def getStructIdOf? (e : Expr) : GoalM (Option Nat) := do return (← get').exprToStructId.find? { expr := e } def propagateIneq (e : Expr) : GoalM Unit := do - if let some (e', he) := (← get').termMap.find? { expr := e } then + if let some { e := e', h := he, .. } := (← get').termMap.find? { expr := e } then go e' (some he) else go e none @@ -369,20 +372,27 @@ builtin_grind_propagator propagateLT ↓LT.lt := propagateIneq public def processNewEq (a b : Expr) : GoalM Unit := do unless isSameExpr a b do let h ← mkEqProof a b - if let some (a', h₁) ← getAuxTerm? a then - let some (b', h₂) ← getAuxTerm? b | return () + if let some { e := a', h := h₁, α } ← getAuxTerm? a then + let some { e := b', h := h₂, .. } ← getAuxTerm? b | return () /- We have - `h : a = b` - `h₁ : ↑a = a'` - `h₂ : ↑b = b'` + where `a'` and `b'` are `NatCast.natCast α inst _` for some type `α`. -/ - let h := mkApp7 (mkConst ``Grind.Order.of_nat_eq) a b a' b' h₁ h₂ h - go a' b' h + if α == Int.mkType then + let h := mkApp7 (mkConst ``Grind.Order.of_nat_eq) a b a' b' h₁ h₂ h + go a' b' h + else + let u ← getDecLevel α + let inst ← synthInstance (mkApp (mkConst ``NatCast [u]) α) + let h := mkApp9 (mkConst ``Grind.Order.of_natCast_eq [u]) α inst a b a' b' h₁ h₂ h + go a' b' h else go a b h where - getAuxTerm? (e : Expr) : GoalM (Option (Expr × Expr)) := do + getAuxTerm? (e : Expr) : GoalM (Option TermMapEntry) := do return (← get').termMap.find? { expr := e } go (a b h : Expr) : GoalM Unit := do diff --git a/src/Lean/Meta/Tactic/Grind/Order/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Order/Internalize.lean index c7851d46d9..17752c2e08 100644 --- a/src/Lean/Meta/Tactic/Grind/Order/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Order/Internalize.lean @@ -166,9 +166,9 @@ def setStructId (e : Expr) : OrderM Unit := do exprToStructId := s.exprToStructId.insert { expr := e } structId } -def updateTermMap (e eNew h : Expr) : GoalM Unit := do +def updateTermMap (e eNew h α : Expr) : GoalM Unit := do modify' fun s => { s with - termMap := s.termMap.insert { expr := e } (eNew, h) + termMap := s.termMap.insert { expr := e } { e := eNew, h, α } termMapInv := s.termMapInv.insert { expr := eNew } (e, h) } @@ -198,9 +198,9 @@ where getOriginal? (e : Expr) : GoalM (Option Expr) := do if let some (e', _) := (← get').termMapInv.find? { expr := e } then return some e' - let_expr NatCast.natCast _ _ a := e | return none + let_expr NatCast.natCast α _ a := e | return none if (← alreadyInternalized a) then - updateTermMap a e (← mkEqRefl e) + updateTermMap a e (← mkEqRefl e) α return some a else return none @@ -290,7 +290,7 @@ def internalizeTerm (e : Expr) : OrderM Unit := do open Arith.Cutsat in def adaptNat (e : Expr) : GoalM Expr := do - if let some (eNew, _) := (← get').termMap.find? { expr := e } then + if let some { e := eNew, .. } := (← get').termMap.find? { expr := e } then return eNew else match_expr e with | LE.le _ _ lhs rhs => adaptCnstr lhs rhs (isLT := false) @@ -307,12 +307,12 @@ where let h := mkApp6 (mkConst (if isLT then ``Nat.ToInt.lt_eq else ``Nat.ToInt.le_eq)) lhs rhs lhs' rhs' h₁ h₂ - updateTermMap e eNew h + updateTermMap e eNew h (← getIntExpr) return eNew adaptTerm : GoalM Expr := do let (eNew, h) ← natToInt e - updateTermMap e eNew h + updateTermMap e eNew h (← getIntExpr) return eNew def adapt (α : Expr) (e : Expr) : GoalM (Expr × Expr) := do diff --git a/src/Lean/Meta/Tactic/Grind/Order/Types.lean b/src/Lean/Meta/Tactic/Grind/Order/Types.lean index 9a28bf13c9..9cd979851c 100644 --- a/src/Lean/Meta/Tactic/Grind/Order/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Order/Types.lean @@ -128,6 +128,13 @@ structure Struct where propagate : List ToPropagate := [] deriving Inhabited +/-- Entry/Value for the map `termMap` in `State` -/ +structure TermMapEntry where + e : Expr + h : Expr + α : Expr +deriving Inhabited + /-- State for all order types detected by `grind`. -/ structure State where /-- Order structures detected. -/ @@ -143,7 +150,7 @@ structure State where Example: given `x y : Nat`, `x ≤ y + 1` is mapped to `Int.ofNat x ≤ Int.ofNat y + 1`, and proof of equivalence. -/ - termMap : PHashMap ExprPtr (Expr × Expr) := {} + termMap : PHashMap ExprPtr TermMapEntry := {} /-- `termMap` inverse -/ termMapInv : PHashMap ExprPtr (Expr × Expr) := {} deriving Inhabited diff --git a/tests/elab/grind_order_eq.lean b/tests/elab/grind_order_eq.lean index fd88de2f88..3788923aa9 100644 --- a/tests/elab/grind_order_eq.lean +++ b/tests/elab/grind_order_eq.lean @@ -30,3 +30,6 @@ example example : a = b + 1 → a ≤ b + 2 := by grind -lia -linarith -ring (splits := 0) only + +-- Issue #13265: kernel error from `of_nat_eq` when the cast is to a non-`Int` type. +example (j k : Nat) (h : j = k) : (j + 1 : Rat) = (k + 1 : Rat) := by grind