mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
cfa8c5a036
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>
46 lines
1.5 KiB
Lean4
46 lines
1.5 KiB
Lean4
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"
|