Skip to content

feat: better universe normalization #8769

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
arthur-adjedj wants to merge 5 commits into
base: master
Choose a base branch
from
Draft

feat: better universe normalization #8769

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
1ed0538
feat: better normalisation procedure for `imax`es
arthur-adjedj Jun 13, 2025
aaed391
feat: Sort-polymorphic linear `NoConfusion`
arthur-adjedj Jun 13, 2025
f9f3323
fix: useless new branch
arthur-adjedj Jun 13, 2025
00ba1a2
more fixes
arthur-adjedj Jun 13, 2025
6c06b91
fix: don't reduce `imax u (max v w), remove `offset` accumulator in `…
arthur-adjedj Jun 13, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 9 additions & 4 deletions src/Lean/Level.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -359,10 +359,10 @@ private def isExplicitSubsumed (lvls : Array Level) (firstNonExplicit : Nat) : B
let max := lvls[firstNonExplicit - 1]!.getOffset
isExplicitSubsumedAux lvls max firstNonExplicit

partial def normalize (l : Level) : Level :=
partial def normalize (l : Level) (offset := 0): Level :=
if isAlreadyNormalizedCheap l then l
Copy link
Contributor

@Rob23oba Rob23oba Jun 13, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm assuming this is meant to make normalize l off equivalent to addOffset (normalize l) off? Then surely the then part of here should return addOffset l off

Copy link
Contributor Author

@arthur-adjedj arthur-adjedj Jun 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You're right, I'll just remove the offset for now (I mainly just wanted for the function to be tail-recursive).

else
let k := l.getOffset
let k := offset + l.getOffset
let u := l.getLevelOffset
match u with
| max l₁ l₂ =>
Expand All @@ -376,11 +376,16 @@ partial def normalize (l : Level) : Level :=
let prevK := lvl₁.getOffset
mkMaxAux lvls k (i+1) prev prevK levelZero
| imax l₁ l₂ =>
if l₂.isNeverZero then addOffset (normalize (mkLevelMax l₁ l₂)) k
if l₂.isNeverZero then normalize (mkLevelMax l₁ l₂) k
else
let l₁ := normalize l₁
let l₂ := normalize l₂
addOffset (mkIMaxAux l₁ l₂) k
match l₂ with
| max l₂ l₃ =>
normalize (mkLevelMax (mkIMaxAux l₁ l₂) (mkIMaxAux l₁ l₃)) k
Copy link
Contributor

@Rob23oba Rob23oba Jun 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This might be a bad idea, since that adds a lot of duplication (also, dedent the match arms)

Copy link
Contributor Author

@arthur-adjedj arthur-adjedj Jun 13, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm also not a fan of this particular branch. I wonder how many terms of the form imax u (max v w) appear in real world examples ? In my mental model of universes, maxes only appear when manipulating things that are already for sure in Types and not in arbitrary Sorts, as such, I don't see how such a thing could appear on the rhs of an imax ? Examples are welcome.

| imax l₂ l₃ =>
normalize (mkIMaxAux (mkLevelMax l₁ l₂) l₃) k
| _ => addOffset (mkIMaxAux l₁ l₂) k
| _ => unreachable!

/--
Expand Down
10 changes: 5 additions & 5 deletions src/Lean/Meta/Constructions/NoConfusionLinear.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ def mkWithCtorType (indName : Name) : MetaM Unit := do
let indTyKind ← inferType indTyCon
let indLevel ← getLevel indTyKind
let e ← forallBoundedTelescope indTyKind info.numParams fun xs _ => do
withLocalDeclD `P (mkSort v.succ) fun P => do
withLocalDeclD `P (mkSort v) fun P => do
withLocalDeclD `ctorIdx (mkConst ``Nat) fun ctorIdx => do
let default ← mkArrow (mkConst ``PUnit [indLevel]) P
let es ← info.ctors.toArray.mapM fun ctorName => do
Expand Down Expand Up @@ -111,7 +111,7 @@ def mkWithCtor (indName : Name) : MetaM Unit := do
let indTyKind ← inferType indTyCon
let indLevel ← getLevel indTyKind
let e ← forallBoundedTelescope indTyKind info.numParams fun xs t => do
withLocalDeclD `P (mkSort v.succ) fun P => do
withLocalDeclD `P (mkSort v) fun P => do
withLocalDeclD `ctorIdx (mkConst ``Nat) fun ctorIdx => do
let withCtorTypeNameApp := mkAppN (mkConst withCtorTypeName (v :: us)) (xs.push P)
let kType := mkApp withCtorTypeNameApp ctorIdx
Expand All @@ -121,7 +121,7 @@ def mkWithCtor (indName : Name) : MetaM Unit := do
let t' ← whnfD t'
assert! t'.isSort
withLocalDeclD `x (mkAppN indTyCon (xs ++ ys)) fun x => do
let e := mkConst (mkCasesOnName indName) (v.succ :: us)
let e := mkConst (mkCasesOnName indName) (v :: us)
let e := mkAppN e xs
let motive ← mkLambdaFVars (ys.push x) P
let e := mkApp e motive
Expand All @@ -140,7 +140,7 @@ def mkWithCtor (indName : Name) : MetaM Unit := do
mkLambdaFVars #[h] e
let «else» ← withLocalDeclD `h (mkNot heq) fun h =>
mkLambdaFVars #[h] k'
let alt := mkApp5 (mkConst ``dite [v.succ])
let alt := mkApp5 (mkConst ``dite [v])
P heq (mkApp2 (mkConst ``Nat.decEq) ctorIdx (mkRawNatLit i))
«then» «else»
mkLambdaFVars zs alt
Expand Down Expand Up @@ -187,7 +187,7 @@ def mkNoConfusionTypeLinear (indName : Name) : MetaM Unit := do
let alts' ← alts.mapIdxM fun i alt => do
let altType ← inferType alt
forallTelescope altType fun zs1 _ => do
let alt := mkConst (mkWithCtorName indName) (v :: us)
let alt := mkConst (mkWithCtorName indName) (v.succ :: us)
let alt := mkAppN alt xs
let alt := mkApp alt PType
let alt := mkApp alt (mkRawNatLit i)
Expand Down
14 changes: 13 additions & 1 deletion src/kernel/level.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -448,7 +448,19 @@ level normalize(level const & l) {
case level_kind::IMax: {
auto l1 = normalize(imax_lhs(r));
auto l2 = normalize(imax_rhs(r));
return mk_succ(mk_imax(l1, l2), p.second);
switch (kind(l2)) {
case level_kind::IMax: {
auto l3 = imax_lhs(l2);
auto l4 = imax_rhs(l2);
return mk_succ(normalize(mk_imax(mk_max(l1,l3),l4)),p.second);
}
case level_kind::Max: {
auto l3 = max_lhs(l2);
auto l4 = max_rhs(l2);
return mk_succ(normalize(mk_max(mk_imax(l1,l3),mk_imax(l1,l4))),p.second);
}
default: return mk_succ(mk_imax(l1, l2), p.second);
}
}
case level_kind::Max: {
buffer<level> todo;
Expand Down
7 changes: 7 additions & 0 deletions tests/lean/run/betterimaxnormalize.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
universe u v w

variable (A : Type u) (B : Sort v)

/-- info: A → A → B : Sort (imax (u + 1) v) -/
#guard_msgs in
#check A → A → B
9 changes: 5 additions & 4 deletions tests/lean/run/linearNoConfusion.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,14 @@ inductive Vec.{u} (α : Type) : Nat → Type u where
| cons {n} : α → Vec α n → Vec α (n + 1)

@[reducible] protected def Vec.noConfusionType.withCtorType'.{u_1, u} :
Type → Type u_1 → Nat → Type (max (u + 1) u_1) := fun α P ctorIdx =>
Type → Sort u_1 → Nat → Sort (imax (u + 2) u_1) := fun α P ctorIdx =>
bif Nat.blt ctorIdx 1
then PUnit.{u + 2} → P
else PUnit.{u + 2} → {n : Nat} → α → Vec.{u} α n → P

/--
info: @[reducible] protected def Vec.noConfusionType.withCtorType.{u_1, u} : Type → Type u_1 → Nat → Type (max (u + 1) u_1) :=
info: @[reducible] protected def Vec.noConfusionType.withCtorType.{u_1, u} : Type →
Sort u_1 → Nat → Sort (imax (u + 2) u_1) :=
fun α P ctorIdx => bif ctorIdx.blt 1 then PUnit → P else PUnit → {n : Nat} → α → Vec α n → P
-/
#guard_msgs in
Expand All @@ -28,15 +29,15 @@ fun α P ctorIdx => bif ctorIdx.blt 1 then PUnit → P else PUnit → {n : Nat}
example : @Vec.noConfusionType.withCtorType.{u_1,u} = @Vec.noConfusionType.withCtorType'.{u_1,u} := rfl

@[reducible] protected noncomputable def Vec.noConfusionType.withCtor'.{u_1, u} : (α : Type) →
(P : Type u_1) → (ctorIdx : Nat) → Vec.noConfusionType.withCtorType' α P ctorIdx → P → (a : Nat) → Vec.{u} α a → P :=
(P : Sort u_1) → (ctorIdx : Nat) → Vec.noConfusionType.withCtorType' α P ctorIdx → P → (a : Nat) → Vec.{u} α a → P :=
fun _α _P ctorIdx k k' _a x =>
Vec.casesOn x
(if h : ctorIdx = 0 then Eq.ndrec k h PUnit.unit else k')
(fun a a_1 => if h : ctorIdx = 1 then Eq.ndrec k h PUnit.unit a a_1 else k')

/--
info: @[reducible] protected def Vec.noConfusionType.withCtor.{u_1, u} : (α : Type) →
(P : Type u_1) → (ctorIdx : Nat) → Vec.noConfusionType.withCtorType α P ctorIdx → P → (a : Nat) → Vec α a → P :=
(P : Sort u_1) → (ctorIdx : Nat) → Vec.noConfusionType.withCtorType α P ctorIdx → P → (a : Nat) → Vec α a → P :=
fun α P ctorIdx k k' a x =>
Vec.casesOn x (if h : ctorIdx = 0 then (h ▸ k) PUnit.unit else k') fun {n} a a_1 =>
if h : ctorIdx = 1 then (h ▸ k) PUnit.unit a a_1 else k'
Expand Down
Loading