feat: omit (#5000)

releases_drafts/new-variable.md

@@ -0,0 +1,17 @@
+**breaking change**
+
+The effect of the `variable` command on proofs of `theorem`s has been changed. Whether such section variables are accessible in the proof now depends only on the theorem signature and other top-level commands, not on the proof itself.
+This change ensures that
+* the statement of a theorem is independent of its proof. In other words, changes in the proof cannot change the theorem statement.
+* tactics such as `induction` cannot accidentally include a section variable.
+* the proof can be elaborated in parallel to subsequent declarations in a future version of Lean.
+
+The effect of `variable`s on the theorem header as well as on other kinds of declarations is unchanged.
+
+Specifically, section variables are included if they
+* are directly referenced by the theorem header,
+* are included via the new `include` command in the current section and not subsequently mentioned in an `omit` statement,
+* are directly referenced by any variable included by these rules, OR
+* are instance-implicit variables that reference only variables included by these rules.
+
+For porting, a new option `deprecated.oldSectionVars` is included to locally switch back to the old behavior.

src/Lean/Elab/BuiltinCommand.lean

@@ -504,12 +504,60 @@ def elabRunMeta : CommandElab := fun stx =>
 
 @[builtin_command_elab Lean.Parser.Command.include] def elabInclude : CommandElab
   | `(Lean.Parser.Command.include| include $ids*) => do
-    let vars := (← getScope).varDecls.concatMap getBracketedBinderIds
+    let sc ← getScope
+    let vars := sc.varDecls.concatMap getBracketedBinderIds
+    let mut uids := #[]
     for id in ids do
-      unless vars.contains id.getId do
+      if let some idx := vars.findIdx? (· == id.getId) then
+        uids := uids.push sc.varUIds[idx]!
+      else
         throwError "invalid 'include', variable '{id}' has not been declared in the current scope"
-    modifyScope fun sc =>
-      { sc with includedVars := sc.includedVars ++ ids.toList.map (·.getId) }
+    modifyScope fun sc => { sc with
+      includedVars := sc.includedVars ++ uids.toList
+      omittedVars := sc.omittedVars.filter (!uids.contains ·) }
+  | _ => throwUnsupportedSyntax
+
+@[builtin_command_elab Lean.Parser.Command.omit] def elabOmit : CommandElab
+  | `(Lean.Parser.Command.omit| omit $omits*) => do
+    -- TODO: this really shouldn't have to re-elaborate section vars... they should come
+    -- pre-elaborated
+    let omittedVars ← runTermElabM fun vars => do
+      Term.synthesizeSyntheticMVarsNoPostponing
+      -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
+      -- So, we use `Core.resetMessageLog`.
+      Core.resetMessageLog
+      -- resolve each omit to variable user name or type pattern
+      let elaboratedOmits : Array (Sum Name Expr) ← omits.mapM fun
+        | `(ident| $id:ident) => pure <| Sum.inl id.getId
+        | `(Lean.Parser.Term.instBinder| [$id : $_]) => pure <| Sum.inl id.getId
+        | `(Lean.Parser.Term.instBinder| [$ty]) =>
+          Sum.inr <$> Term.withoutErrToSorry (Term.elabTermAndSynthesize ty none)
+        | _ => throwUnsupportedSyntax
+      -- check that each omit is actually used in the end
+      let mut omitsUsed := omits.map fun _ => false
+      let mut omittedVars := #[]
+      let mut revSectionFVars : Std.HashMap FVarId Name := {}
+      for (uid, var) in (← read).sectionFVars do
+        revSectionFVars := revSectionFVars.insert var.fvarId! uid
+      for var in vars do
+        let ldecl ← var.fvarId!.getDecl
+        if let some idx := (← elaboratedOmits.findIdxM? fun
+            | .inl id => return ldecl.userName == id
+            | .inr ty => do
+              let mctx ← getMCtx
+              isDefEq ty ldecl.type <* setMCtx mctx) then
+          if let some uid := revSectionFVars[var.fvarId!]? then
+            omittedVars := omittedVars.push uid
+            omitsUsed := omitsUsed.set! idx true
+          else
+            throwError "invalid 'omit', '{ldecl.userName}' has not been declared in the current scope"
+      for o in omits, used in omitsUsed do
+        unless used do
+          throwError "'{o}' did not match any variables in the current scope"
+      return omittedVars
+    modifyScope fun sc => { sc with
+      omittedVars := sc.omittedVars ++ omittedVars.toList
+      includedVars := sc.includedVars.filter (!omittedVars.contains ·) }
   | _ => throwUnsupportedSyntax
 
 @[builtin_command_elab Parser.Command.exit] def elabExit : CommandElab := fun _ =>

src/Lean/Elab/Command.lean

@@ -51,8 +51,6 @@ structure Scope where
   even if they do not work with binders per se.
   -/
   varDecls      : Array (TSyntax ``Parser.Term.bracketedBinder) := #[]
-  /-- `include`d section variable names -/
-  includedVars  : List Name := []
   /--
   Globally unique internal identifiers for the `varDecls`.
   There is one identifier per variable introduced by the binders
@@ -62,6 +60,10 @@ structure Scope where
   that capture these variables.
   -/
   varUIds       : Array Name := #[]
+  /-- `include`d section variable names (from `varUIds`) -/
+  includedVars  : List Name := []
+  /-- `omit`ted section variable names (from `varUIds`) -/
+  omittedVars  : List Name := []
   /--
   If true (default: false), all declarations that fail to compile
   automatically receive the `noncomputable` modifier.

src/Lean/Elab/MutualDef.lean

@@ -336,30 +336,42 @@ def instantiateMVarsProfiling (e : Expr) : MetaM Expr := do
 /--
 Runs `k` with a restricted local context where only section variables from `vars` are included that
 * are directly referenced in any `headers`,
-* are included in `includedVars` (via the `include` command),
+* are included in `sc.includedVars` (via the `include` command),
 * are directly referenced in any variable included by these rules, OR
-* are instance-implicit variables that only reference section variables included by these rules.
+* are instance-implicit variables that only reference section variables included by these rules AND
+  are not listed in `sc.omittedVars` (via `omit`; note that `omit` also subtracts from
+  `sc.includedVars`).
 -/
-private def withHeaderSecVars {α} (vars : Array Expr) (includedVars : List Name) (headers : Array DefViewElabHeader)
+private def withHeaderSecVars {α} (vars : Array Expr) (sc : Command.Scope) (headers : Array DefViewElabHeader)
     (k : Array Expr → TermElabM α) : TermElabM α := do
-  let (_, used) ← collectUsed.run {}
+  let mut revSectionFVars : Std.HashMap FVarId Name := {}
+  for (uid, var) in (← read).sectionFVars do
+    revSectionFVars := revSectionFVars.insert var.fvarId! uid
+  let (_, used) ← collectUsed revSectionFVars |>.run {}
   let (lctx, localInsts, vars) ← removeUnused vars used
   withLCtx lctx localInsts <| k vars
 where
-  collectUsed : StateRefT CollectFVars.State MetaM Unit := do
+  collectUsed revSectionFVars : StateRefT CollectFVars.State MetaM Unit := do
     -- directly referenced in headers
     headers.forM (·.type.collectFVars)
     -- included by `include`
-    vars.forM fun var => do
-      let ldecl ← getFVarLocalDecl var
-      if includedVars.contains ldecl.userName then
-        modify (·.add ldecl.fvarId)
+    for var in vars do
+      if let some uid := revSectionFVars[var.fvarId!]? then
+        if sc.includedVars.contains uid then
+          modify (·.add var.fvarId!)
     -- transitively referenced
     get >>= (·.addDependencies) >>= set
+    for var in (← get).fvarIds do
+      if let some uid := revSectionFVars[var]? then
+        if sc.omittedVars.contains uid then
+          throwError "cannot omit referenced section variable '{Expr.fvar var}'"
     -- instances (`addDependencies` unnecessary as by definition they may only reference variables
     -- already included)
-    vars.forM fun var => do
+    for var in vars do
       let ldecl ← getFVarLocalDecl var
+      if let some uid := revSectionFVars[var.fvarId!]? then
+        if sc.omittedVars.contains uid then
+          continue
       let st ← get
       if ldecl.binderInfo.isInstImplicit && (← getFVars ldecl.type).all st.fvarSet.contains then
         modify (·.add ldecl.fvarId)
@@ -371,7 +383,7 @@ register_builtin_option deprecated.oldSectionVars : Bool := {
   descr    := "re-enable deprecated behavior of including exactly the section variables used in a declaration"
 }
 
-private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr) (includedVars : List Name) : TermElabM (Array Expr) :=
+private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr) (sc : Command.Scope) : TermElabM (Array Expr) :=
   headers.mapM fun header => do
     let mut reusableResult? := none
     if let some snap := header.bodySnap? then
@@ -386,7 +398,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
       withReuseContext header.value do
       withDeclName header.declName <| withLevelNames header.levelNames do
       let valStx ← liftMacroM <| declValToTerm header.value
-      (if header.kind.isTheorem && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars includedVars #[header] else fun x => x #[]) fun vars => do
+      (if header.kind.isTheorem && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc #[header] else fun x => x #[]) fun vars => do
       forallBoundedTelescope header.type header.numParams fun xs type => do
         -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
         for i in [0:header.binderIds.size] do
@@ -962,7 +974,7 @@ partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs :
     for preDef in preDefs do
       checkPreDef preDef
 
-def elabMutualDef (vars : Array Expr) (includedVars : List Name) (views : Array DefView) : TermElabM Unit :=
+def elabMutualDef (vars : Array Expr) (sc : Command.Scope) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv do
       -- save correct environment in info tree
@@ -983,7 +995,7 @@ where
           addLocalVarInfo view.declId funFVar
         let values ←
           try
-            let values ← elabFunValues headers vars includedVars
+            let values ← elabFunValues headers vars sc
             Term.synthesizeSyntheticMVarsNoPostponing
             values.mapM (instantiateMVarsProfiling ·)
           catch ex =>
@@ -993,7 +1005,7 @@ where
         let letRecsToLift ← getLetRecsToLift
         let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
         checkLetRecsToLiftTypes funFVars letRecsToLift
-        (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars includedVars headers else withUsed vars headers values letRecsToLift) fun vars => do
+        (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc headers else withUsed vars headers values letRecsToLift) fun vars => do
           let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
           for preDef in preDefs do
             trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
@@ -1064,8 +1076,8 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
     if let some snap := snap? then
       -- no non-fatal diagnostics at this point
       snap.new.resolve <| .ofTyped { defs, diagnostics := .empty : DefsParsedSnapshot }
-    let includedVars := (← getScope).includedVars
-    runTermElabM fun vars => Term.elabMutualDef vars includedVars views
+    let sc ← getScope
+    runTermElabM fun vars => Term.elabMutualDef vars sc views
 
 builtin_initialize
   registerTraceClass `Elab.definition.mkClosure

src/Lean/Linter.lean

@@ -10,3 +10,4 @@ import Lean.Linter.ConstructorAsVariable
 import Lean.Linter.Deprecated
 import Lean.Linter.UnusedVariables
 import Lean.Linter.MissingDocs
+import Lean.Linter.Omit

src/Lean/Linter/Omit.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+prelude
+import Lean.Elab.Command
+import Lean.Linter.Util
+
+namespace Lean.Linter
+open Elab.Command
+
+register_builtin_option linter.omit : Bool := {
+  defValue := false
+  descr := "enable the 'avoid omit' linter"
+}
+
+def «omit» : Linter where
+  run stx := do
+    unless linter.omit.get (← getOptions) do
+      return
+    if let some stx := stx.find? (·.isOfKind ``Lean.Parser.Command.«omit») then
+      logLint linter.omit stx m!"`omit` should be avoided in favor of restructuring your \
+        `variable` declarations"
+
+builtin_initialize addLinter «omit»

src/Lean/Parser/Command.lean

@@ -734,6 +734,15 @@ followed by the `in` combinator to limit the inclusion to the subsequent declara
 -/
 @[builtin_command_parser] def «include» := leading_parser "include " >> many1 ident
 
+/--
+`omit` instructs Lean to not include a variable previously `include`d. Apart from variable names, it
+can also refer to typeclass instance variables by type using the syntax `omit [TypeOfInst]`, in
+which case all instance variables that unify with the given type are omitted. `omit` should usually
+only be used in conjunction with `in` in order to keep the section structure simple.
+-/
+@[builtin_command_parser] def «omit» := leading_parser "omit " >>
+  many1 (ident <|> Term.instBinder)
+
 /-- No-op parser used as syntax kind for attaching remaining whitespace at the end of the input. -/
 @[run_builtin_parser_attribute_hooks] def eoi : Parser := leading_parser ""
 

stage0/src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);

tests/lean/run/variable.lean

@@ -60,3 +60,115 @@ theorem MulEquiv.decompositionMonoid (_b : β) : α = α :=
 /-- info: MulEquiv.decompositionMonoid {α β F : Type} [EquivLike F α β] (f : F) (_b : β) : α = α -/
 #guard_msgs in
 #check MulEquiv.decompositionMonoid
+
+section
+/-! `omit` -/
+variable [ToString α] [ToString β]
+
+/--
+error: failed to synthesize
+  ToString α
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+omit [ToString α] in
+theorem t8 (a : α) (b : β) : True :=
+  let _ := toString a; let _ := toString b; trivial
+
+/--
+error: failed to synthesize
+  ToString β
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+omit [ToString β] in
+theorem t9 (a : α) (b : β) : True :=
+  let _ := toString a; let _ := toString b; trivial
+
+/--
+error: failed to synthesize
+  ToString α
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+error: failed to synthesize
+  ToString β
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+omit [ToString _] in
+theorem t10 (a : α) (b : β) : True :=
+  let _ := toString a; let _ := toString b; trivial
+end
+
+/-! illegal `omit`s -/
+
+/-- error: invalid 'omit', 'α' has not been declared in the current scope -/
+#guard_msgs in
+variable (a : α) in
+omit α in
+theorem t11 (a : α) : True := trivial
+
+/--
+error: cannot omit referenced section variable 'α'
+---
+error: cannot omit referenced section variable 'α'
+-/
+#guard_msgs in
+variable (α : Type) in
+omit α in
+theorem t12 (a : α) : True := trivial
+
+/--
+error: cannot omit referenced section variable 'inst✝'
+---
+error: cannot omit referenced section variable 'inst✝'
+-/
+#guard_msgs in
+variable [ToString α] in
+omit [ToString α] in
+theorem t13 (a : α) : toString a = toString a := rfl
+
+/--
+error: application type mismatch
+  ToString True
+argument
+  True
+has type
+  Prop : Type
+but is expected to have type
+  Type ?u.1758 : Type (?u.1758 + 1)
+-/
+#guard_msgs in
+omit [ToString True]
+
+/-- error: '[ToString Nat]' did not match any variables in the current scope -/
+#guard_msgs in
+omit [ToString Nat]
+
+/-! `omit` can also be used to revert an `include` -/
+
+variable (α : Type) in
+include α in
+omit α in
+theorem t13 : True := trivial
+
+/-- warning: included section variable 'α' is not used in 't14', consider excluding it -/
+#guard_msgs in
+variable (α : Type) in
+include α in
+omit α in
+include α in
+theorem t14 : True := trivial
+
+/-! But you probably shouldn't use it -/
+
+set_option linter.omit true in
+/--
+warning: `omit` should be avoided in favor of restructuring your `variable` declarations
+note: this linter can be disabled with `set_option linter.omit false`
+-/
+#guard_msgs in
+variable (α : Type) in
+include α in
+omit α in
+theorem t15 : True := trivial