fix: omega: ignore levels in canonicalizer (#3853)

fixes #3848
leanprover · Apr 10, 2024 · 280525f · 280525f
1 parent 892bfe2
commit 280525f
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 1 deletion.
diff --git a/src/Lean/Meta/Canonicalizer.lean b/src/Lean/Meta/Canonicalizer.lean
@@ -82,8 +82,10 @@ private partial def mkKey (e : Expr) : CanonM Key := do
     return key
   else
     let key ← match e with
-      | .sort .. | .fvar .. | .bvar .. | .const .. | .lit .. =>
+      | .sort .. | .fvar .. | .bvar .. | .lit .. =>
         pure { e := (← shareCommon e) }
+      | .const n ls =>
+        pure { e := (← shareCommon (.const n (List.replicate ls.length levelZero))) }
       | .mvar .. =>
         -- We instantiate assigned metavariables because the
         -- pretty-printer also instantiates them.

diff --git a/tests/lean/run/issue3848.lean b/tests/lean/run/issue3848.lean
@@ -0,0 +1,12 @@
+theorem sizeOf_snd_lt_sizeOf_list
+  {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] {x : α × β} {xs : List (α × β)} :
+  x ∈ xs → sizeOf x.snd < 1 + sizeOf xs
+:= by
+  intro h
+  have h1 := List.sizeOf_lt_of_mem h
+  have h2 : sizeOf x = 1 + sizeOf x.1 + sizeOf x.2 := rfl
+  cases x; dsimp at *
+  omega -- this only works if  universe levels are normalizes by the omega canonicalizier
+
+-- another example
+theorem ex.{u,v} : sizeOf PUnit.{(max u v) + 1} = sizeOf PUnit.{max (u + 1) (v + 1)} := by omega