fix: handle universe level commutativity in sym pattern matching (#12923)

This PR fixes a bug where `max u v` and `max v u` fail to match in
SymM's pattern matching. Both `processLevel` (Phase 1) and
`isLevelDefEqS` (Phase 2) treated `max` positionally, so `max u v ≠ max
v u` structurally even though they are semantically equal.

The fix has three parts:
- Eagerly normalize universe levels in patterns at creation time
(`preprocessDeclPattern`, `preprocessExprPattern`,
`mkSimprocPatternFromExpr`)
- Normalize the target level in `processLevel` before matching, using a
`where go` refactor
- Add `tryApproxMaxMax` to `processLevel` and `isLevelDefEqS`: when
positional `max/max` matching would fail, check if one argument from
each side matches structurally and match the remaining pair

Also moves `normalizeLevels` from `Grind.Util` to `Sym.Util` to avoid
code duplication, since both Sym and Grind need it.

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Meta/Sym/Pattern.lean

@@ -17,6 +17,7 @@ import Lean.Meta.Sym.ProofInstInfo
 import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.Offset
 import Lean.Meta.Sym.Eta
+import Lean.Meta.Sym.Util
 import Lean.Meta.AbstractMVars
 import Init.Data.List.MapIdx
 import Init.Data.Nat.Linear
@@ -31,7 +32,9 @@ framework (`Sym`). The design prioritizes performance by using a two-phase appro
 # Phase 1 (Syntactic Matching)
 - Patterns use de Bruijn indices for expression variables and renamed level params (`_uvar.0`, `_uvar.1`, ...) for universe variables
 - Matching is purely structural after reducible definitions are unfolded during preprocessing
-- Universe levels treat `max` and `imax` as uninterpreted functions (no AC reasoning)
+- Universe levels are eagerly normalized in patterns and normalized on the target side during matching
+- `tryApproxMaxMax` handles `max` commutativity when one argument matches structurally. It is relevant
+  for constraints such as `max ?u a =?= max a b`
 - Binders and term metavariables are deferred to Phase 2
 
 # Phase 2 (Pending Constraints)
@@ -107,6 +110,7 @@ def preprocessDeclPattern (declName : Name) : MetaM (List Name × Expr) := do
   let us := levelParams.map mkLevelParam
   let type ← instantiateTypeLevelParams info.toConstantVal us
   let type ← preprocessType type
+  let type ← normalizeLevels type
   return (levelParams, type)
 
 def preprocessExprPattern (e : Expr) (levelParams₀ : List Name) : MetaM (List Name × Expr) := do
@@ -115,6 +119,7 @@ def preprocessExprPattern (e : Expr) (levelParams₀ : List Name) : MetaM (List
   let us := levelParams.map mkLevelParam
   let type := type.instantiateLevelParams levelParams₀ us
   let type ← preprocessType type
+  let type ← normalizeLevels type
   return (levelParams, type)
 
 /--
@@ -298,6 +303,7 @@ public def mkSimprocPatternFromExpr (e : Expr) : MetaM Pattern := do
   let levelParams := result.paramNames.mapIdx fun i _ => Name.num uvarPrefix i
   let us := levelParams.toList.map mkLevelParam
   let expr := result.expr.instantiateLevelParamsArray result.paramNames us.toArray
+  let expr ← normalizeLevels expr
   mkPatternFromLambda levelParams.toList expr
 
 structure UnifyM.Context where
@@ -365,35 +371,42 @@ def assignLevel (uidx : Nat) (u : Level) : UnifyM Bool := do
     modify fun s => { s with uAssignment := s.uAssignment.set! uidx (some u) }
     return true
 
-def processLevel (u : Level) (v : Level) : UnifyM Bool := do
-  match u, v with
-  | .zero, .zero => return true
-  | .succ u, .succ v => processLevel u v
-  | .zero, .succ _ => return false
-  | .succ _, .zero => return false
-  | .zero, .max v₁ v₂ => processLevel .zero v₁ <&&> processLevel .zero v₂
-  | .max u₁ u₂, .zero => processLevel u₁ .zero <&&> processLevel u₂ .zero
-  | .zero, .imax _ v => processLevel .zero v
-  | .imax _ u, .zero => processLevel u .zero
-  | .max u₁ u₂, .max v₁ v₂ => processLevel u₁ v₁ <&&> processLevel u₂ v₂
-  | .imax u₁ u₂, .imax v₁ v₂ => processLevel u₁ v₁ <&&> processLevel u₂ v₂
-  | .param uName, _ =>
-    if let some uidx := isUVar? uName then
-      assignLevel uidx v
-    else if u == v then
-      return true
-    else if v.isMVar && (← read).unify then
-      pushLevelPending u v
-      return true
-    else
-      return false
-  | .mvar _, _ | _, .mvar _ =>
-    if (← read).unify then
-      pushLevelPending u v
-      return true
-    else
-      return false
-  | _, _ => return false
+def processLevel (u : Level) (v : Level) : UnifyM Bool :=
+  go u v.normalize
+where
+  go (u : Level) (v : Level) : UnifyM Bool := do
+    match u, v with
+    | .zero, .zero => return true
+    | .succ u, .succ v => go u v
+    | .zero, .succ _ => return false
+    | .succ _, .zero => return false
+    | .zero, .max v₁ v₂ => go .zero v₁ <&&> go .zero v₂
+    | .max u₁ u₂, .zero => go u₁ .zero <&&> go u₂ .zero
+    | .zero, .imax _ v => go .zero v
+    | .imax _ u, .zero => go u .zero
+    | .max u₁ u₂, .max v₁ v₂ =>
+      -- tryApproxMaxMax: find a shared concrete arg between both sides
+      if u₂ == v₁ then go u₁ v₂
+      else if u₁ == v₂ then go u₂ v₁
+      else go u₁ v₁ <&&> go u₂ v₂
+    | .imax u₁ u₂, .imax v₁ v₂ => go u₁ v₁ <&&> go u₂ v₂
+    | .param uName, _ =>
+      if let some uidx := isUVar? uName then
+        assignLevel uidx v
+      else if u == v then
+        return true
+      else if v.isMVar && (← read).unify then
+        pushLevelPending u v
+        return true
+      else
+        return false
+    | .mvar _, _ | _, .mvar _ =>
+      if (← read).unify then
+        pushLevelPending u v
+        return true
+      else
+        return false
+    | _, _ => return false
 
 def processLevels (us : List Level) (vs : List Level) : UnifyM Bool := do
   match us, vs with
@@ -542,7 +555,7 @@ def tryAssignLevelMVar (u : Level) (v : Level) : MetaM Bool := do
 
 /--
 Structural definitional equality for universe levels.
-Treats `max` and `imax` as uninterpreted functions (no AC reasoning).
+Uses `tryApproxMaxMax` to handle `max` commutativity when one argument matches structurally.
 Attempts metavariable assignment in both directions if structural matching fails.
 -/
 def isLevelDefEqS (u : Level) (v : Level) : MetaM Bool := do
@@ -556,7 +569,10 @@ def isLevelDefEqS (u : Level) (v : Level) : MetaM Bool := do
   | .max u₁ u₂, .zero => isLevelDefEqS u₁ .zero <&&> isLevelDefEqS u₂ .zero
   | .zero, .imax _ v => isLevelDefEqS .zero v
   | .imax _ u, .zero => isLevelDefEqS u .zero
-  | .max u₁ u₂, .max v₁ v₂ => isLevelDefEqS u₁ v₁ <&&> isLevelDefEqS u₂ v₂
+  | .max u₁ u₂, .max v₁ v₂ =>
+    if u₂ == v₁ then isLevelDefEqS u₁ v₂
+    else if u₁ == v₂ then isLevelDefEqS u₂ v₁
+    else isLevelDefEqS u₁ v₁ <&&> isLevelDefEqS u₂ v₂
   | .imax u₁ u₂, .imax v₁ v₂ => isLevelDefEqS u₁ v₁ <&&> isLevelDefEqS u₂ v₂
   | _, _ => tryAssignLevelMVar u v <||> tryAssignLevelMVar v u
 

src/Lean/Meta/Sym/Util.lean

@@ -109,4 +109,23 @@ where
 public def _root_.Lean.MVarId.checkMaxShared (mvarId : MVarId) (msg := "") : SymM Unit := do
   (← mvarId.getDecl).type.checkMaxShared msg
 
+/-- Quick filter for checking whether we can skip `normalizeLevels`. -/
+def levelsAlreadyNormalized (e : Expr) : Bool :=
+  Option.isNone <| e.find? fun
+    | .const _ us => us.any (! ·.isAlreadyNormalizedCheap)
+    | .sort u => !u.isAlreadyNormalizedCheap
+    | _ => false
+
+/--
+Normalizes universe levels in constants and sorts.
+-/
+public def normalizeLevels (e : Expr) : CoreM Expr := do
+  if levelsAlreadyNormalized e then return e
+  let pre (e : Expr) := do
+    match e with
+    | .sort u => return .done <| e.updateSort! u.normalize
+    | .const _ us => return .done <| e.updateConst! (us.map Level.normalize)
+    | _ => return .continue
+  Core.transform e (pre := pre)
+
 end Lean.Meta.Sym

src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean

@@ -109,7 +109,7 @@ where
     let e ← eraseIrrelevantMData e
     /- We must fold kernel projections like it is done in the preprocessor. -/
     let e ← foldProjs e
-    normalizeLevels e
+    Sym.normalizeLevels e
 
 private def markNestedProof (e : Expr) : M Expr := do
   let prop ← inferType e

src/Lean/Meta/Tactic/Grind/Simp.lean

@@ -63,7 +63,7 @@ def preprocessImpl (e : Expr) : GoalM Simp.Result := do
   let e' ← markNestedSubsingletons e'
   let e' ← eraseIrrelevantMData e'
   let e' ← foldProjs e'
-  let e' ← normalizeLevels e'
+  let e' ← Sym.normalizeLevels e'
   let r' ← eraseSimpMatchDiscrsOnly e'
   let r ← r.mkEqTrans r'
   let e' := r'.expr
@@ -98,6 +98,6 @@ but ensures assumptions made by `grind` are satisfied.
 -/
 def preprocessLight (e : Expr) : GoalM Expr := do
   let e ← instantiateMVars e
-  shareCommon (← canon (← normalizeLevels (← foldProjs (← eraseIrrelevantMData (← markNestedSubsingletons (← Sym.unfoldReducible e))))))
+  shareCommon (← canon (← Sym.normalizeLevels (← foldProjs (← eraseIrrelevantMData (← markNestedSubsingletons (← Sym.unfoldReducible e))))))
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Util.lean

@@ -153,25 +153,6 @@ def foldProjs (e : Expr) : MetaM Expr := do
       return .done e
   Meta.transform e (post := post)
 
-/-- Quick filter for checking whether we can skip `normalizeLevels`. -/
-private def levelsAlreadyNormalized (e : Expr) : Bool :=
-  Option.isNone <| e.find? fun
-    | .const _ us => us.any (! ·.isAlreadyNormalizedCheap)
-    | .sort u => !u.isAlreadyNormalizedCheap
-    | _ => false
-
-/--
-Normalizes universe levels in constants and sorts.
--/
-def normalizeLevels (e : Expr) : CoreM Expr := do
-  if levelsAlreadyNormalized e then return e
-  let pre (e : Expr) := do
-    match e with
-    | .sort u => return .done <| e.updateSort! u.normalize
-    | .const _ us => return .done <| e.updateConst! (us.map Level.normalize)
-    | _ => return .continue
-  Core.transform e (pre := pre)
-
 /--
 Normalizes the given expression using the `grind` simplification theorems and simprocs.
 This function is used for normalizing E-matching patterns. Note that it does not return a proof.

tests/elab/sym_pattern_level.lean

@@ -0,0 +1,45 @@
+import Lean.Meta.Sym
+
+open Lean Meta Sym
+
+/-! ## Level commutativity: `max u v` vs `max v u` with concrete params -/
+
+/--
+info: rule.apply succeeds: max u v matches max v u
+-/
+#guard_msgs in
+#eval show MetaM Unit from do
+  let u := Level.param `u
+  let v := Level.param `v
+  let maxUV := Level.max u v
+  let maxVU := Level.max v u
+  let proof := mkApp2 (mkConst ``Eq.refl [maxUV.succ]) (mkSort maxUV) (mkSort maxUV)
+  let rule ← mkBackwardRuleFromExpr proof (levelParams := [`u, `v])
+  let goalType := mkApp3 (mkConst ``Eq [maxVU.succ]) (mkSort maxVU) (mkSort maxVU) (mkSort maxVU)
+  let r ← SymM.run do
+    let mvar ← mkFreshExprMVar goalType
+    let mvarId ← preprocessMVar mvar.mvarId!
+    rule.apply mvarId
+  match r with
+  | .goals _ => logInfo "rule.apply succeeds: max u v matches max v u"
+  | .failed  => logInfo "rule.apply FAILED: max u v did not match max v u"
+
+/-! ## `tryApproxMaxMax`: pattern `max _uvar 1` matching target `max 1 u` -/
+
+axiom lvlAxiom : ∀ (α : Sort (max u 1)), α → α
+
+/--
+info: pattern match succeeded
+-/
+#guard_msgs in
+#eval show MetaM Unit from do
+  let pat ← mkPatternFromDecl ``lvlAxiom
+  -- Target has `max 1 u` (swapped from pattern's `max u 1`)
+  let u := Level.param `u
+  let lvl := Level.max (.succ .zero) u  -- max 1 u
+  let targetType := Expr.forallE `α (.sort lvl) (Expr.forallE `a (.bvar 0) (.bvar 1) .default) .implicit
+  let r ← SymM.run do
+    pat.match? targetType
+  match r with
+  | some _ => logInfo "pattern match succeeded"
+  | none   => logInfo "pattern match FAILED"