8000 feat: generalize withCtor functions to eliminate to Sort by nomeata · Pull Request #8994 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

feat: generalize withCtor functions to eliminate to Sort #8994

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
wants to merge 1 commit into
base: joachim/linearNoConfusionULift
Choose a base branch
from
Draft

feat: generalize withCtor functions to eliminate to Sort #8994

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
16 changes: 5 additions & 11 deletions src/Lean/Meta/Constructions/NoConfusionLinear.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,12 +23,6 @@ definition, rather than one for each constructor, using a `withCtorType` helper
See the `linearNoConfusion.lean` test for exemplary output of this translation (checked to be
up-to-date).

The `withCtor` functions could be generally useful, but for that they should probably eliminate into
`Sort _` rather than `Type _`, and then writing the `withCtorType` function runs into universe level
confusion, which may be solvable if the kernel had more complete univere level normalization.
Until then we put these helper in the `noConfusionType` namespace to indicate that they are not
general purpose.

This module is written in a rather manual style, constructing the `Expr` directly. It's best
read with the expected output to the side.
-/
Expand Down Expand Up @@ -137,7 +131,7 @@ def mkWithCtorType (indName : Name) : MetaM Unit := do
let indTyCon := mkConst indName us
let indTyKind ← inferType indTyCon
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 es ← info.ctors.toArray.mapM fun ctorName => do
let ctor := mkAppN (mkConst ctorName us) xs
Expand Down Expand Up @@ -168,7 +162,7 @@ def mkWithCtor (indName : Name) : MetaM Unit := do
let indTyCon := mkConst indName us
let indTyKind ← inferType indTyCon
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 @@ -178,7 +172,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 @@ -197,7 +191,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 @@ -244,7 +238,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
15 changes: 8 additions & 7 deletions tests/lean/run/issue8962.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,12 +11,13 @@ inductive S where
| b

/--
info: @[reducible] protected def S.noConfusionType.withCtorType.{u_1, u, v} : Type u_1 → Nat → Type (max u u_1 (v + 1)) :=
info: @[reducible] protected def S.noConfusionType.withCtorType.{u_1, u, v} : Sort u_1 →
Nat → Sort (max 1 u_1 (imax (u + 1) (v + 2) (max u (v + 1)) u_1)) :=
fun P ctorIdx =>
bif Nat.blt ctorIdx 1 then
PULift.{max (u + 1) (u_1 + 1) (v + 2), max (max (u + 1) (u_1 + 1)) (v + 2)}
PULift.{max u_1 (imax (u + 1) (v + 2) (max u (v + 1)) u_1), imax (u + 1) (v + 2) (max u (v + 1)) u_1}
({α : Sort u} → {β : Type v} → (α → β) → P)
else PULift.{max (u + 1) (u_1 + 1) (v + 2), u_1 + 1} P
else PULift.{max u_1 (imax (u + 1) (v + 2) (max u (v + 1)) u_1), u_1} P
-/
#guard_msgs in
#print S.noConfusionType.withCtorType
Expand All @@ -28,13 +29,13 @@ inductive T where
| b

/--
info: @[reducible] protected def T.noConfusionType.withCtorType.{u_1, u, v} : Type u_1 →
Nat → Sort (max (u + 1) (u_1 + 1) (v + 1) (imax u v)) :=
info: @[reducible] protected def T.noConfusionType.withCtorType.{u_1, u, v} : Sort u_1 →
Nat → Sort (max 1 u_1 (imax (u + 1) (v + 1) (imax u v) u_1)) :=
fun P ctorIdx =>
bif Nat.blt ctorIdx 1 then
PULift.{max (u + 1) (u_1 + 1) (v + 1) (imax u v), max (max (max (u + 1) (u_1 + 1)) (v + 1)) (imax u v)}
PULift.{max u_1 (imax (u + 1) (v + 1) (imax u v) u_1), imax (u + 1) (v + 1) (imax u v) u_1}
({α : Sort u} → {β : Sort v} → (α → β) → P)
else PULift.{max (u + 1) (u_1 + 1) (v + 1) (imax u v), u_1 + 1} P
else PULift.{max u_1 (imax (u + 1) (v + 1) (imax u v) u_1), u_1} P
-/
#guard_msgs in
#print T.noConfusionType.withCtorType
17 changes: 9 additions & 8 deletions tests/lean/run/linearNoConfusion.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,16 +14,17 @@ inductive Vec.{u} (α : Type) : Nat → Type u where


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

/--
info: @[reducible] protected def Vec.noConfusionType.withCtorType.{u_1, u} : Type → Type u_1 → Nat → Type (max u u_1) :=
info: @[reducible] protected def Vec.noConfusionType.withCtorType.{u_1, u} : Type →
Sort u_1 → Nat → Sort (max 1 u_1 (imax (u + 1) u_1)) :=
fun α P ctorIdx =>
bif Nat.blt ctorIdx 1 then PULift.{max (u + 1) (u_1 + 1), u_1 + 1} P
else PULift.{max (u + 1) (u_1 + 1), max (u + 1) (u_1 + 1)} ({n : Nat} → α → Vec.{u} α n → P)
bif Nat.blt ctorIdx 1 then PULift.{max u_1 (imax (u + 1) u_1), u_1} P
else PULift.{max u_1 (imax (u + 1) u_1), imax (u + 1) u_1} ({n : Nat} → α → Vec.{u} α n → P)
-/
#guard_msgs in
set_option pp.universes true in
Expand All @@ -33,15 +34,15 @@ example : @Vec.noConfusionType.withCtorType.{u_1,u} = @Vec.noConfusionType.withC


@[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).down else k')
(fun a a_1 => if h : ctorIdx = 1 then (Eq.ndrec k h).down 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).down else k') fun {n} a a_1 =>
if h : ctorIdx = 1 then (h ▸ k).down a a_1 else k'
Expand Down
Loading
0