feat: virtual one-field structures

src/Init/NotationExtra.lean

@@ -316,6 +316,32 @@ macro_rules
     `($mods:declModifiers class $id $params* $[: $ty:term]? extends $[$parents:term],*
       attribute [instance] $ctor)
 
+/--
+`newtype N params := ty with proj` declares a type `N` definitionally equal to `ty`, together with a
+constructor `N.mk` and a projector `N.proj`, and marks all three `@[irreducible]`. For example,
+```
+newtype OrderDual (α : Type u) := α with ofDual
+```
+produces
+```
+@[irreducible] def OrderDual (α : Type u) := α
+@[irreducible] def OrderDual.mk {α : Type u} (ofDual : α) : OrderDual α := ofDual
+@[irreducible] def OrderDual.ofDual {α : Type u} (self : OrderDual α) : α := self
+```
+Modifiers, parameters, universe parameters, section variables and auto-bound implicits are handled
+exactly as for `def`; as for `structure`, explicit parameters become implicit in the constructor
+and projector.
+
+This is the "irreducible type alias" pattern used to avoid defeq abuse while keeping a
+zero-overhead representation identical to `ty` (e.g. to cast `List ty` to `List N`). Unlike a
+hand-written version of this pattern, `newtype` also registers `N.mk`/`N.proj` as a virtual
+constructor/projector pair, so that `N.proj (N.mk a)` reduces to `a` and `N.mk (N.proj x)` is
+definitionally `x` (see `Lean.Meta.reduceVirtualProj?`), even though `N`, `N.mk` and `N.proj` stay
+irreducible otherwise. Use `unsealing_newtype N => ...` to locally lift the irreducibility.
+-/
+syntax (name := Lean.Parser.Command.newtypeCmd)
+  declModifiers "newtype " declId bracketedBinder* " := " term " with " ident : command
+
 namespace Lean
 syntax cdotTk := unicode("· ", ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/

src/Init/Tactics.lean

@@ -1810,6 +1810,39 @@ a lemma from the list until it gets stuck.
 syntax (name := applyRules) "apply_rules" optConfig (&" only")? (args)? (using_)? : tactic
 end SolveByElim
 
+/--
+The reducibility status that `unsealing_newtype` temporarily assigns to a `newtype`-declared
+type, its constructor and its projector. Mirrors `Lean.ReducibilityStatus` without `irreducible`.
+-/
+inductive UnsealingNewtypeReducibility where
+  /-- Unfolded at reducible transparency and above. -/
+  | reducible
+  /-- Unfolded at instances transparency and above. -/
+  | instanceReducible
+  /-- Unfolded at implicit transparency and above. -/
+  | implicitReducible
+  /-- Unfolded at default transparency and above, like an ordinary definition. -/
+  | semireducible
+
+/--
+Configuration for the `unsealing_newtype` tactic.
+-/
+structure UnsealingNewtypeConfig where
+  /-- The reducibility status to use within the tactic block (default: `.semireducible`). -/
+  reducibility : UnsealingNewtypeReducibility := .semireducible
+
+/--
+`unsealing_newtype N => tacs` runs `tacs` with the `newtype`-declared type `N` -- together with
+its auto-generated constructor and projector -- treated as `[semireducible]` instead of
+`[irreducible]`. This is the escape hatch for a `newtype`: within the block, `N`, `N.mk` and its
+projector unfold like ordinary definitions, e.g. `N = Nat` can be proved by `rfl`.
+
+`unsealing_newtype (reducibility := .instanceReducible) N => tacs` uses the given reducibility
+status instead; see `UnsealingNewtypeReducibility`.
+-/
+syntax (name := unsealingNewtype)
+  "unsealing_newtype " optConfig ident " => " tacticSeq : tactic
+
 /--
 Configuration for the `exact?` and `apply?` tactics.
 -/

src/Lean/Elab.lean

@@ -32,6 +32,7 @@ public import Lean.Elab.Structure
 public import Lean.Elab.Print
 public import Lean.Elab.MutualDef
 public import Lean.Elab.AuxDef
+public import Lean.Elab.NewType
 public import Lean.Elab.PreDefinition
 public import Lean.Elab.Deriving
 public import Lean.Elab.DeclarationRange

src/Lean/Elab/NewType.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Lean.Elab.Command
+public import Lean.Elab.DeclModifiers
+public import Lean.Elab.DeclarationRange
+public import Lean.Meta.VirtualStructure
+
+public section
+
+namespace Lean.Elab.Command
+open Meta
+
+/--
+Adds the constructor `ctorName` and projector `projName` of the already elaborated `newtype`
+`declName`, whose underlying type is the body of its definition. Reading the parameters off the
+elaborated `declName` (instead of re-elaborating its binders) is what makes section variables,
+auto-bound implicits and universe parameters behave exactly as for `def`.
+-/
+private def addNewtypeCtorProj (declName ctorName projName fieldName : Name) : TermElabM Nat := do
+  let info ← getConstInfoDefn declName
+  let us := info.levelParams.map mkLevelParam
+  forallTelescope info.type fun params resultType => do
+    unless (← whnf resultType).isSort do
+      throwError "invalid `newtype`, the right-hand side must be a type, but has type{indentExpr resultType}"
+    let underlying := info.value.beta params
+    let self := mkAppN (mkConst declName us) params
+    let implicitParams ← params.filterMapM fun p => do
+      return if (← p.fvarId!.getDecl).binderInfo.isExplicit then some (p.fvarId!, .implicit) else none
+    -- Importers can only reduce `projName (ctorName a)` in the kernel if both bodies are exposed,
+    -- so mirror whatever the `def` elaborator decided for `declName`.
+    let exposed := (← getEnv).hasExposedBody declName
+    withNewBinderInfos implicitParams do
+      let addIdentity (name argName : Name) (argType resultType : Expr) : TermElabM Unit :=
+        withLocalDeclD argName argType fun a => do
+          let type ← mkForallFVars (params.push a) resultType
+          let value ← mkLambdaFVars (params.push a) a
+          let hints := .regular (getMaxHeight (← getEnv) value + 1)
+          let decl := .defnDecl (← mkDefinitionValInferringUnsafe name info.levelParams type value hints)
+          addDecl decl (forceExpose := exposed)
+          compileDecl decl
+      addIdentity ctorName fieldName underlying self
+      addIdentity projName `self self underlying
+    return params.size
+
+@[builtin_command_elab Lean.Parser.Command.newtypeCmd]
+def elabNewtype : CommandElab
+  | `($mods:declModifiers newtype $declId $params* := $ty with $projId:ident) => do
+    let modifiers ← elabModifiers mods
+    let { declName, .. } ← liftTermElabM <|
+      Term.expandDeclId (← getCurrNamespace) (← getLevelNames) declId modifiers
+    let ctorName := declName ++ `mk
+    let projName := declName ++ projId.getId
+    elabCommand <| ← `($mods:declModifiers def $declId $params* := $ty)
+    let numParams ← liftTermElabM <| addNewtypeCtorProj declName ctorName projName projId.getId
+    addDeclarationRangesFromSyntax ctorName declId
+    addDeclarationRangesFromSyntax projName projId
+    addConstInfo projId projName
+    for n in [declName, ctorName, projName] do
+      setIrreducibleAttribute n
+    modifyEnv (registerVirtualStructure · { typeName := declName, ctorName, projName, numParams })
+    for n in [ctorName, projName] do
+      liftCoreM <| enableRealizationsForConst n
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Command

src/Lean/Elab/Tactic.lean

@@ -46,6 +46,7 @@ public import Lean.Elab.Tactic.DiscrTreeKey
 public import Lean.Elab.Tactic.BVDecide
 public import Lean.Elab.Tactic.BoolToPropSimps
 public import Lean.Elab.Tactic.Classical
+public import Lean.Elab.Tactic.NewType
 public import Lean.Elab.Tactic.Impossible
 public import Lean.Elab.Tactic.Grind
 public import Lean.Elab.Tactic.Monotonicity

src/Lean/Elab/Tactic/NewType.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Lean.Elab.Tactic.Basic
+public import Lean.Meta.VirtualStructure
+import Lean.Elab.Tactic.Config
+
+public section
+
+namespace Lean.Elab.Tactic
+open Meta
+
+/--
+Runs `t` with the declarations `names` treated as having reducibility status `status`. The
+combinator underlying the `unsealing_newtype` tactic; see its docstring.
+-/
+def unsealingNewtype [Monad m] [MonadEnv m] [MonadFinally m] (names : Array Name)
+    (status : ReducibilityStatus := .semireducible) (t : m α) : m α := do
+  modifyEnv reducibilityExtraExt.pushScope
+  for n in names do
+    setLocalReducibilityStatus n status
+  try
+    t
+  finally
+    modifyEnv reducibilityExtraExt.popScope
+
+declare_config_elab elabUnsealingNewtypeConfig Parser.Tactic.UnsealingNewtypeConfig
+
+def _root_.Lean.Parser.Tactic.UnsealingNewtypeReducibility.toReducibilityStatus :
+    Parser.Tactic.UnsealingNewtypeReducibility → ReducibilityStatus
+  | .reducible => .reducible
+  | .instanceReducible => .instanceReducible
+  | .implicitReducible => .implicitReducible
+  | .semireducible => .semireducible
+
+@[builtin_tactic Lean.Parser.Tactic.unsealingNewtype] def evalUnsealingNewtype : Tactic :=
+  fun stx => do
+    let cfg ← elabUnsealingNewtypeConfig stx[1]
+    let typeStx := stx[2]
+    let typeName ← resolveGlobalConstNoOverload typeStx
+    let some info ← getVirtualStructureInfo? typeName
+      | throwErrorAt typeStx "'{typeName}' is not a `newtype`-declared type"
+    addConstInfo typeStx typeName
+    unsealingNewtype #[info.typeName, info.ctorName, info.projName]
+      cfg.reducibility.toReducibilityStatus (evalTactic stx[4])
+
+end Lean.Elab.Tactic

src/Lean/Meta/ExprDefEq.lean

@@ -204,6 +204,26 @@ where
       else
         return false
 
+/--
+Virtual analog of `isDefEqEtaStruct`, for types declared by the `newtype` command
+(`VirtualStructureInfo`). Recognizes `b := ctorName arg`, where `ctorName` is a `newtype`-generated
+constructor, and — provided `a` is not itself such a constructor application, in which case
+`isDefEqArgs` handles the comparison more directly — reduces `a =?= b` to `projName a =?= arg`.
+Combined with `reduceVirtualProj?`, this gives `newtype`-declared types the same iota/eta behavior
+as a real one-field structure, even though `N`, `N.mk` and `N.toNat` never unfold.
+-/
+private def isDefEqVirtualEtaStruct (a b : Expr) : MetaM Bool := do
+  let .const ctorName us := b.getAppFn | return false
+  let some info ← getVirtualCtorInfo? ctorName | return false
+  unless b.getAppNumArgs == info.numParams + 1 do return false
+  if let .const ctorName' _ := a.getAppFn then
+    if ctorName' == info.ctorName then return false
+  if (← isDefEq (← inferType a) (← inferType b)) then
+    let params := b.getAppArgs.extract 0 info.numParams
+    checkpointDefEq <| isDefEq (mkApp (mkAppN (mkConst info.projName us) params) a) b.appArg!
+  else
+    return false
+
 /--
   Try to solve `a := (fun x => t) =?= b` by eta-expanding `b`,
   resulting in `t =?= b x` (with a fresh free variable `x`).
@@ -2407,10 +2427,28 @@ private def isDefEqAppFallback (t : Expr) (s : Expr) : MetaM Bool := do
       Meta.throwIsDefEqStuck
     return false
 
+/--
+Virtual analog of `isDefEqProj.isDefEqSingleton` for `newtype`-generated projectors: solves
+`projName params (?m ...) =?= v` as `?m ... =?= ctorName params v`.
+-/
+private def isDefEqVirtualProj (t v : Expr) : MetaM Bool := do
+  let .const projName us := t.getAppFn | return false
+  let some info ← getVirtualProjInfo? projName | return false
+  unless t.getAppNumArgs == info.numParams + 1 do return false
+  let s ← whnf (t.getArg! info.numParams)
+  let sFn := s.getAppFn
+  unless sFn.isMVar do return false
+  if (← isAssignable sFn) then
+    let params := t.getAppArgs.extract 0 info.numParams
+    processAssignment' s (mkApp (mkAppN (mkConst info.ctorName us) params) v)
+  else
+    return false
+
 private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
   whenUndefDo (isDefEqEta t s) do
   whenUndefDo (isDefEqEta s t) do
   if (← isDefEqProj t s) then return true
+  if (← (isDefEqVirtualProj t s <||> isDefEqVirtualProj s t)) then return true
   let t' ← whnfCore t
   let s' ← whnfCore s
   if t != t' || s != s' then
@@ -2425,6 +2463,8 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
     -- which is very costly because it requires us to unify the fields.
     if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then
       return true
+    if (← (isDefEqVirtualEtaStruct t s <||> isDefEqVirtualEtaStruct s t)) then
+      return true
     if t.isConst && s.isConst then
       if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
     else if (← pure t.isApp <&&> pure s.isApp) then

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

@@ -226,6 +226,9 @@ private def reduceStep (e : Expr) : SimpM Expr := do
     | none =>
     match (← reduceProjFn? e) with
     | some e => return e
+    | none =>
+    match (← reduceVirtualProj? e) with
+    | some e => return e
     | none   => pure ()
   if cfg.iota then
     match (← reduceRecMatcher? e) with

src/Lean/Meta/VirtualStructure.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Lean.EnvExtension
+
+public section
+
+namespace Lean
+
+/--
+Registered by the `newtype` command for a declaration such as
+```
+newtype N := Nat with toNat
+```
+Associates the auto-generated constructor (`N.mk`) and projector (`N.toNat`) with each other and
+with the type they wrap (`N`), so that `Lean.Meta.whnf`/`isDefEq` can treat `N.toNat (N.mk a)` and
+`N.mk (N.toNat x)` like the iota/eta reduction of a real one-field structure's constructor and
+projector, even though `N`, `N.mk` and `N.toNat` are ordinary `def`s (marked `@[irreducible]`)
+rather than a genuine inductive type.
+-/
+structure VirtualStructureInfo where
+  /-- The `newtype`-declared type. -/
+  typeName : Name
+  /-- The auto-generated constructor, wrapping a value of the underlying type as `typeName`. -/
+  ctorName : Name
+  /-- The auto-generated projector, unwrapping a `typeName` value back to the underlying type. -/
+  projName : Name
+  /-- The number of parameters of `typeName`. The constructor and projector take them as their
+  leading arguments, followed by the wrapped value resp. the `typeName` value. -/
+  numParams : Nat
+  deriving Inhabited, Repr
+
+builtin_initialize virtualStructureTypeExt : MapDeclarationExtension VirtualStructureInfo ←
+  mkMapDeclarationExtension
+builtin_initialize virtualStructureCtorExt : MapDeclarationExtension VirtualStructureInfo ←
+  mkMapDeclarationExtension
+builtin_initialize virtualStructureProjExt : MapDeclarationExtension VirtualStructureInfo ←
+  mkMapDeclarationExtension
+
+/-- Registers `info` under its type, constructor and projector names, so all three can be looked
+up from any of them. -/
+def registerVirtualStructure (env : Environment) (info : VirtualStructureInfo) : Environment :=
+  let env := virtualStructureTypeExt.insert env info.typeName info
+  let env := virtualStructureCtorExt.insert env info.ctorName info
+  virtualStructureProjExt.insert env info.projName info
+
+namespace Environment
+
+/-- If `typeName` was declared via `newtype`, return its virtual structure info. -/
+def getVirtualStructureInfo? (env : Environment) (typeName : Name) : Option VirtualStructureInfo :=
+  virtualStructureTypeExt.find? env typeName
+
+/-- If `ctorName` is the constructor auto-generated by `newtype`, return its virtual structure
+info. -/
+def getVirtualCtorInfo? (env : Environment) (ctorName : Name) : Option VirtualStructureInfo :=
+  virtualStructureCtorExt.find? env ctorName
+
+/-- If `projName` is the projector auto-generated by `newtype`, return its virtual structure
+info. -/
+def getVirtualProjInfo? (env : Environment) (projName : Name) : Option VirtualStructureInfo :=
+  virtualStructureProjExt.find? env projName
+
+end Environment
+
+def getVirtualStructureInfo? [Monad m] [MonadEnv m] (typeName : Name) :
+    m (Option VirtualStructureInfo) :=
+  return (← getEnv).getVirtualStructureInfo? typeName
+
+def getVirtualCtorInfo? [Monad m] [MonadEnv m] (ctorName : Name) : m (Option VirtualStructureInfo) :=
+  return (← getEnv).getVirtualCtorInfo? ctorName
+
+def getVirtualProjInfo? [Monad m] [MonadEnv m] (projName : Name) : m (Option VirtualStructureInfo) :=
+  return (← getEnv).getVirtualProjInfo? projName
+
+end Lean