From 9f76cb9aa5ee503893308d94f255d67b8f4c2ca8 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 23 Jul 2024 18:35:37 +0200 Subject: [PATCH] feat: new `variable` command --- src/Lean/Elab/BuiltinCommand.lean | 10 +++++ src/Lean/Elab/Command.lean | 2 + src/Lean/Elab/MutualDef.lean | 65 ++++++++++++++++++++++++++++--- src/Lean/Parser/Command.lean | 64 +++++++++++++++++++++--------- stage0/src/stdlib_flags.h | 2 +- tests/lean/run/3807.lean | 18 ++++++--- tests/lean/run/calc.lean | 2 + tests/lean/run/variable.lean | 62 +++++++++++++++++++++++++++++ 8 files changed, 194 insertions(+), 31 deletions(-) create mode 100644 tests/lean/run/variable.lean diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index 8b18ec1fdb..ec81bb873c 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/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" diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index f41ef1dae9..f756f98a3c 100644 --- a/src/Lean/Elab/Command.lean +++ b/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 diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 2a9e6bb5b9..fb6f78d41f 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/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 diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index e1ba45e866..e457dc8703 100644 --- a/src/Lean/Parser/Command.lean +++ b/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 ` 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 ` 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,12 +274,12 @@ with `end `. 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 @@ -287,17 +287,22 @@ can be anonymous). This can be changed, for instance one can turn explicit varia 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 "" diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 0699845ba4..658ab0874e 100644 --- a/stage0/src/stdlib_flags.h +++ b/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); diff --git a/tests/lean/run/3807.lean b/tests/lean/run/3807.lean index 872c8e6839..d064fba38c 100644 --- a/tests/lean/run/3807.lean +++ b/tests/lean/run/3807.lean @@ -2085,9 +2085,10 @@ variable {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} section Semiring -variable [Semiring R] [Semiring A] [Semiring B] [Semiring C] -variable [Algebra R A] [Algebra R B] [Algebra R C] +variable [Semiring R] [Semiring A] [Semiring B] +variable [Algebra R A] [Algebra R B] +variable [Semiring C] [Algebra R C] in instance funLike : FunLike (A →ₐ[R] B) A B where coe f := f.toFun @@ -2101,6 +2102,7 @@ instance algHomClass : AlgHomClass (A →ₐ[R] B) R A B where @[ext] theorem ext {φ₁ φ₂ : A →ₐ[R] B} (H : ∀ x, φ₁ x = φ₂ x) : φ₁ = φ₂ := sorry +variable [Semiring C] [Algebra R C] in def comp (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) : A →ₐ[R] C := { φ₁.toRingHom.comp φ₂ with commutes' := sorry } @@ -2400,7 +2402,7 @@ end Mathlib.FieldTheory.Subfield section Mathlib.FieldTheory.IntermediateField -variable (K L L' : Type _) [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] +variable (K L L' : Type _) [Field K] [Field L] [Field L'] [Algebra K L] structure IntermediateField extends Subalgebra K L where inv_mem' : ∀ x ∈ carrier, x⁻¹ ∈ carrier @@ -2430,7 +2432,7 @@ end IntermediateField namespace AlgHom -variable (f : L →ₐ[K] L') +variable [Algebra K L'] (f : L →ₐ[K] L') def fieldRange : IntermediateField K L' := { f.range, (f : L →+* L').fieldRange with @@ -2446,8 +2448,9 @@ def inclusion {E F : IntermediateField K L} (hEF : E ≤ F) : E →ₐ[K] F := section RestrictScalars variable (K) -variable [Algebra L' L] [IsScalarTower K L' L] +variable [Algebra L' L] +variable [Algebra K L'] [IsScalarTower K L' L] in def restrictScalars (E : IntermediateField L' L) : IntermediateField K L := { E.toSubfield, E.toSubalgebra.restrictScalars K with carrier := E.carrier @@ -2470,17 +2473,20 @@ namespace IntermediateField section AdjoinDef -variable (F : Type _) [Field F] {E : Type _} [Field E] [Algebra F E] (S : Set E) +variable (F : Type _) {E : Type _} [Field E] (S : Set E) +variable [Field F] [Algebra F E] in def adjoin : IntermediateField F E := { Subfield.closure (Set.range (algebraMap F E) ∪ S) with inv_mem' := sorry } +variable [Field F] [Algebra F E] in theorem subset_adjoin : S ⊆ adjoin F S := sorry theorem subset_adjoin_of_subset_left {F : Subfield E} {T : Set E} (HT : T ⊆ F) : T ⊆ adjoin F S := sorry +variable [Field F] [Algebra F E] in theorem adjoin_subset_adjoin_iff {F' : Type _} [Field F'] [Algebra F' E] {S S' : Set E} : (adjoin F S : Set E) ⊆ adjoin F' S' ↔ Set.range (algebraMap F E) ⊆ adjoin F' S' ∧ S ⊆ adjoin F' S' := sorry diff --git a/tests/lean/run/calc.lean b/tests/lean/run/calc.lean index 7dcdc72803..598891a96c 100644 --- a/tests/lean/run/calc.lean +++ b/tests/lean/run/calc.lean @@ -1,5 +1,6 @@ variable (t1 t2 t3 t4 : Nat) variable (pf12 : t1 = t2) (pf23 : t2 = t3) (pf34 : t3 = t4) +include pf12 pf23 pf34 theorem foo : t1 = t4 := calc @@ -9,6 +10,7 @@ theorem foo : t1 = t4 := variable (t5 : Nat) variable (pf23' : t2 < t3) (pf45' : t4 < t5) +include pf23' pf45' instance [LT α] : Trans (α := α) (· < ·) (· < ·) (· < ·) where trans := sorry diff --git a/tests/lean/run/variable.lean b/tests/lean/run/variable.lean new file mode 100644 index 0000000000..5577d51650 --- /dev/null +++ b/tests/lean/run/variable.lean @@ -0,0 +1,62 @@ +/-! # Basic section variable tests -/ + +/-! Directly referenced variables should be included. -/ +variable {n : Nat} in +theorem t1 : n = n := by induction n <;> rfl + +/-! Variables mentioned only in the body should not be included. -/ +variable {n : Nat} in +/-- error: unknown identifier 'n' -/ +#guard_msgs in +theorem t2 : ∃ (n : Nat), n = n := by exists n + +/-! Variables transitively mentioned should be included. -/ +variable {n : Nat} (h : n = n) in +theorem t3 : h = h := rfl + +/-! Instance variables mentioning only included variables should be included. -/ +variable {α : Type} [ToString α] in +theorem t4 (a : α) : a = a := let _ := toString a; rfl + +/-! Instance variables not mentioning only included variables should not be included. -/ +variable {α β : Type} [Coe α β] in +/-- +error: don't know how to synthesize placeholder +context: +α : Type +a : α +⊢ a = a +-/ +#guard_msgs in +theorem t5 (a : α) : a = a := _ + +/-! Accidentally included variables should be warned for. -/ +variable {α : Type} [ToString α] in +/-- warning: included section variable '[ToString α]' is not used in 't6', consider excluding it -/ +#guard_msgs in +theorem t6 (a : α) : a = a := rfl + +/-! `include` should always include. -/ +variable {n : Nat} in +include n in +theorem t7 : ∃ (n : Nat), n = n := by exists n + +/-! traversal order bug broke instance inclusion -/ +variable {M N : Type} (r : N → N → Prop) +class IsTrans (N : Type) (r : N → N → Prop) : Prop +variable [IsTrans N r] {a b c d : N} +/-- +warning: included section variable '[IsTrans N r]' is not used in 'act_rel_of_rel_of_act_rel', consider excluding it +-/ +#guard_msgs in +theorem act_rel_of_rel_of_act_rel (ab : r a b) : r a b := ab + +/-! More complex include case, instance should be included via `f`. -/ +class EquivLike (F : Type) (α β : Type) : Type +variable {F : Type} [EquivLike F α β] (f : F) in +include f in +theorem MulEquiv.decompositionMonoid (_b : β) : α = α := + let _ : EquivLike F α β := inferInstance; let _ := f; rfl +/-- info: MulEquiv.decompositionMonoid {α β F : Type} [EquivLike F α β] (f : F) (_b : β) : α = α -/ +#guard_msgs in +#check MulEquiv.decompositionMonoid