feat: refined variable behavior in proofs

src/Init/Data/List/Erase.lean

@@ -354,7 +354,7 @@ theorem erase_eq_iff [LawfulBEq α] {a : α} {l : List α} :
   rw [erase_of_not_mem]
   simp_all
 
-theorem Nodup.erase_eq_filter [BEq α] [LawfulBEq α] {l} (d : Nodup l) (a : α) : l.erase a = l.filter (· != a) := by
+theorem Nodup.erase_eq_filter [LawfulBEq α] {l} (d : Nodup l) (a : α) : l.erase a = l.filter (· != a) := by
   induction d with
   | nil => rfl
   | cons m _n ih =>
@@ -367,13 +367,13 @@ theorem Nodup.erase_eq_filter [BEq α] [LawfulBEq α] {l} (d : Nodup l) (a : α)
       simpa [@eq_comm α] using m
     · simp [beq_false_of_ne h, ih, h]
 
-theorem Nodup.mem_erase_iff [BEq α] [LawfulBEq α] {a : α} (d : Nodup l) : a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l := by
+theorem Nodup.mem_erase_iff [LawfulBEq α] {a : α} (d : Nodup l) : a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l := by
   rw [Nodup.erase_eq_filter d, mem_filter, and_comm, bne_iff_ne]
 
-theorem Nodup.not_mem_erase [BEq α] [LawfulBEq α] {a : α} (h : Nodup l) : a ∉ l.erase a := fun H => by
+theorem Nodup.not_mem_erase [LawfulBEq α] {a : α} (h : Nodup l) : a ∉ l.erase a := fun H => by
   simpa using ((Nodup.mem_erase_iff h).mp H).left
 
-theorem Nodup.erase [BEq α] [LawfulBEq α] (a : α) : Nodup l → Nodup (l.erase a) :=
+theorem Nodup.erase [LawfulBEq α] (a : α) : Nodup l → Nodup (l.erase a) :=
   Nodup.sublist <| erase_sublist _ _
 
 end erase

src/Init/WF.lean

@@ -68,6 +68,7 @@ noncomputable def recursion {C : α → Sort v} (a : α) (h : ∀ x, (∀ y, r y
   induction (apply hwf a) with
   | intro x₁ _ ih => exact h x₁ ih
 
+include hwf in
 theorem induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a :=
   recursion hwf a h
 

src/Lean/Elab/BuiltinCommand.lean

@@ -502,6 +502,16 @@ def elabRunMeta : CommandElab := fun stx =>
     addDocString declName (← getDocStringText doc)
   | _ => throwUnsupportedSyntax
 
+@[builtin_command_elab Lean.Parser.Command.include] def elabInclude : CommandElab
+  | `(Lean.Parser.Command.include| include $ids*) => do
+    let vars := (← getScope).varDecls.concatMap getBracketedBinderIds
+    for id in ids do
+      unless vars.contains id.getId do
+        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) }
+  | _ => throwUnsupportedSyntax
+
 @[builtin_command_elab Parser.Command.exit] def elabExit : CommandElab := fun _ =>
   logWarning "using 'exit' to interrupt Lean"
 

src/Lean/Elab/Command.lean

@@ -51,6 +51,8 @@ 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

src/Lean/Elab/MutualDef.lean

@@ -327,7 +327,45 @@ def instantiateMVarsProfiling (e : Expr) : MetaM Expr := do
   profileitM Exception s!"instantiate metavars" (← getOptions) do
     instantiateMVars e
 
-private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array Expr) :=
+/--
+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 directly referenced in any variable included by these rules, OR
+* are instance-implicit variables that only reference section variables included by these rules.
+-/
+private def withHeaderSecVars {α} (vars : Array Expr) (includedVars : List Name) (headers : Array DefViewElabHeader)
+    (k : Array Expr → TermElabM α) : TermElabM α := do
+  let (_, used) ← collectUsed.run {}
+  let (lctx, localInsts, vars) ← removeUnused vars used
+  withLCtx lctx localInsts <| k vars
+where
+  collectUsed : 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)
+    -- transitively referenced
+    get >>= (·.addDependencies) >>= set
+    -- instances (`addDependencies` unnecessary as by definition they may only reference variables
+    -- already included)
+    vars.forM fun var => do
+      let ldecl ← getFVarLocalDecl var
+      let st ← get
+      if ldecl.binderInfo.isInstImplicit && (← getFVars ldecl.type).all st.fvarSet.contains then
+        modify (·.add ldecl.fvarId)
+  getFVars (e : Expr) : MetaM (Array FVarId) :=
+    (·.2.fvarIds) <$> e.collectFVars.run {}
+
+register_builtin_option deprecated.oldSectionVars : Bool := {
+  defValue := false
+  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) :=
   headers.mapM fun header => do
     let mut reusableResult? := none
     if let some snap := header.bodySnap? then
@@ -342,6 +380,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array
       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
       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
@@ -353,7 +392,20 @@ private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array
         -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
         -- leads to more section variables being included than necessary
         let val ← instantiateMVarsProfiling val
-        mkLambdaFVars xs val
+        let val ← mkLambdaFVars xs val
+        unless header.type.hasSorry || val.hasSorry do
+          for var in vars do
+            unless header.type.containsFVar var.fvarId! ||
+                val.containsFVar var.fvarId! ||
+                (← vars.anyM (fun v => return (← v.fvarId!.getType).containsFVar var.fvarId!)) do
+              let varDecl ← var.fvarId!.getDecl
+              let var := if varDecl.userName.hasMacroScopes && varDecl.binderInfo.isInstImplicit then
+                m!"[{varDecl.type}]".group
+              else
+                var
+              logWarningAt header.ref m!"included section variable '{var}' is not used in \
+                '{header.declName}', consider excluding it"
+        return val
     if let some snap := header.bodySnap? then
       snap.new.resolve <| some {
         diagnostics :=
@@ -904,7 +956,7 @@ partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs :
     for preDef in preDefs do
       checkPreDef preDef
 
-def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit :=
+def elabMutualDef (vars : Array Expr) (includedVars : List Name) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv do
       -- save correct environment in info tree
@@ -925,7 +977,7 @@ where
           addLocalVarInfo view.declId funFVar
         let values ←
           try
-            let values ← elabFunValues headers
+            let values ← elabFunValues headers vars includedVars
             Term.synthesizeSyntheticMVarsNoPostponing
             values.mapM (instantiateMVarsProfiling ·)
           catch ex =>
@@ -935,7 +987,7 @@ where
         let letRecsToLift ← getLetRecsToLift
         let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
         checkLetRecsToLiftTypes funFVars letRecsToLift
-        withUsed vars headers values letRecsToLift fun vars => do
+        (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars includedVars 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}"
@@ -1006,7 +1058,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 }
-    runTermElabM fun vars => Term.elabMutualDef vars views
+    let includedVars := (← getScope).includedVars
+    runTermElabM fun vars => Term.elabMutualDef vars includedVars views
 
 builtin_initialize
   registerTraceClass `Elab.definition.mkClosure

src/Lean/Parser/Command.lean

@@ -242,10 +242,10 @@ def «structure»          := leading_parser
 @[builtin_command_parser] def noncomputableSection := leading_parser
   "noncomputable " >> "section" >> optional (ppSpace >> checkColGt >> ident)
 /--
-A `section`/`end` pair delimits the scope of `variable`, `open`, `set_option`, and `local` commands.
-Sections can be nested. `section <id>` provides a label to the section that has to appear with the
-matching `end`. In either case, the `end` can be omitted, in which case the section is closed at the
-end of the file.
+A `section`/`end` pair delimits the scope of `variable`, `include, `open`, `set_option`, and `local`
+commands. Sections can be nested. `section <id>` provides a label to the section that has to appear
+with the matching `end`. In either case, the `end` can be omitted, in which case the section is
+closed at the end of the file.
 -/
 @[builtin_command_parser] def «section»      := leading_parser
   "section" >> optional (ppSpace >> checkColGt >> ident)
@@ -274,30 +274,35 @@ with `end <id>`. The `end` command is optional at the end of a file.
 @[builtin_command_parser] def «end»          := leading_parser
   "end" >> optional (ppSpace >> checkColGt >> ident)
 /-- Declares one or more typed variables, or modifies whether already-declared variables are
-implicit.
+  implicit.
 
 Introduces variables that can be used in definitions within the same `namespace` or `section` block.
-When a definition mentions a variable, Lean will add it as an argument of the definition. The
-`variable` command is also able to add typeclass parameters. This is useful in particular when
-writing many definitions that have parameters in common (see below for an example).
+When a definition mentions a variable, Lean will add it as an argument of the definition. This is
+useful in particular when writing many definitions that have parameters in common (see below for an
+example).
 
 Variable declarations have the same flexibility as regular function paramaters. In particular they
 can be [explicit, implicit][binder docs], or [instance implicit][tpil classes] (in which case they
 can be anonymous). This can be changed, for instance one can turn explicit variable `x` into an
 implicit one with `variable {x}`. Note that currently, you should avoid changing how variables are
 bound and declare new variables at the same time; see [issue 2789] for more on this topic.
 
+In *theorem bodies* (i.e. proofs), variables are not included based on usage in order to ensure that
+changes to the proof cannot change the statement of the overall theorem. Instead, variables are only
+available to the proof if they have been mentioned in the theorem header or in an `include` command
+or are instance implicit and depend only on such variables.
+
 See [*Variables and Sections* from Theorem Proving in Lean][tpil vars] for a more detailed
 discussion.
 
-[tpil vars]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#variables-and-sections
-(Variables and Sections on Theorem Proving in Lean)
-[tpil classes]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html
-(Type classes on Theorem Proving in Lean)
-[binder docs]: https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.BinderInfo
-(Documentation for the BinderInfo type)
-[issue 2789]: https://github.com/leanprover/lean4/issues/2789
-(Issue 2789 on github)
+[tpil vars]:
+https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#variables-and-sections
+(Variables and Sections on Theorem Proving in Lean) [tpil classes]:
+https://lean-lang.org/theorem_proving_in_lean4/type_classes.html (Type classes on Theorem Proving in
+Lean) [binder docs]:
+https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.BinderInfo (Documentation
+for the BinderInfo type) [issue 2789]: https://github.com/leanprover/lean4/issues/2789 (Issue 2789
+on github)
 
 ## Examples
 
@@ -368,6 +373,24 @@ namespace Logger
 end Logger
 ```
 
+The following example demonstrates availability of variables in proofs:
+```lean
+variable
+  {α : Type}    -- available in the proof as indirectly mentioned through `a`
+  [ToString α]  -- available in the proof as `α` is included
+  (a : α)       -- available in the proof as mentioned in the header
+  {β : Type}    -- not available in the proof
+  [ToString β]  -- not available in the proof
+
+theorem ex : a = a := rfl
+```
+After elaboration of the proof, the following warning will be generated to highlight the unused
+hypothesis:
+```
+included section variable '[ToString α]' is not used in 'ex', consider excluding it
+```
+In such cases, the offending variable declaration should be moved down or into a section so that
+only theorems that do depend on it follow it until the end of the section.
 -/
 @[builtin_command_parser] def «variable»     := leading_parser
   "variable" >> many1 (ppSpace >> checkColGt >> Term.bracketedBinder)
@@ -703,8 +726,13 @@ list, so it should be brief.
 @[builtin_command_parser] def genInjectiveTheorems := leading_parser
   "gen_injective_theorems% " >> ident
 
-/-- To be implemented. -/
-@[builtin_command_parser] def «include» := leading_parser "include " >> many1 (checkColGt >> ident)
+/--
+`include eeny meeny` instructs Lean to include the section `variable`s `eeny` and `meeny` in all
+declarations in the remainder of the current section, differing from the default behavior of
+conditionally including variables based on use in the declaration header. `include` is usually
+followed by the `in` combinator to limit the inclusion to the subsequent declaration.
+-/
+@[builtin_command_parser] def «include» := leading_parser "include " >> many1 ident
 
 /-- 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 ""

src/Std/Data/DHashMap/Internal/RawLemmas.lean

@@ -20,7 +20,7 @@ open Std.DHashMap.Internal.List
 
 universe u v
 
-variable {α : Type u} {β : α → Type v} [BEq α] [Hashable α]
+variable {α : Type u} {β : α → Type v}
 
 namespace Std.DHashMap.Internal
 
@@ -41,6 +41,8 @@ theorem Raw.buckets_emptyc {i : Nat} {h} :
     (∅ : Raw α β).buckets[i]'h = AssocList.nil :=
   buckets_empty
 
+variable [BEq α] [Hashable α]
+
 @[simp]
 theorem buckets_empty {c} {i : Nat} {h} :
     (empty c : DHashMap α β).1.buckets[i]'h = AssocList.nil := by
@@ -55,7 +57,9 @@ end empty
 
 namespace Raw₀
 
+variable [BEq α] [Hashable α]
 variable (m : Raw₀ α β) (h : m.1.WF)
+set_option deprecated.oldSectionVars true
 
 /-- Internal implementation detail of the hash map -/
 scoped macro "wf_trivial" : tactic => `(tactic|

src/Std/Data/DHashMap/RawLemmas.lean

@@ -75,6 +75,7 @@ namespace Raw
 open Internal.Raw₀ Internal.Raw
 
 variable {m : Raw α β} (h : m.WF)
+set_option deprecated.oldSectionVars true
 
 @[simp]
 theorem isEmpty_empty {c} : (empty c : Raw α β).isEmpty := by

src/Std/Data/HashMap/RawLemmas.lean

@@ -27,6 +27,7 @@ namespace Std.HashMap
 namespace Raw
 
 variable {m : Raw α β} (h : m.WF)
+set_option deprecated.oldSectionVars true
 
 private theorem ext {m m' : Raw α β} : m.inner = m'.inner → m = m' := by
   cases m; cases m'; rintro rfl; rfl

src/Std/Data/HashSet/Lemmas.lean

@@ -20,7 +20,7 @@ set_option autoImplicit false
 
 universe u v
 
-variable {α : Type u} {_ : BEq α} {_ : Hashable α} [EquivBEq α] [LawfulHashable α]
+variable {α : Type u} {_ : BEq α} {_ : Hashable α}
 
 namespace Std.HashSet
 

src/Std/Data/HashSet/RawLemmas.lean

@@ -27,6 +27,7 @@ namespace Std.HashSet
 namespace Raw
 
 variable {m : Raw α} (h : m.WF)
+set_option deprecated.oldSectionVars true
 
 private theorem ext {m m' : Raw α} : m.inner = m'.inner → m = m' := by
   cases m; cases m'; rintro rfl; rfl