From 9148932e3de37a19bf62a8f7934192cfebc66a6c Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 25 Jan 2025 03:12:14 +0100 Subject: [PATCH] many updates --- Manual.lean | 11 +- Manual/Tactics.lean | 363 +++++++++++++++++++++++++++++++++++++------- README.md | 10 ++ 3 files changed, 323 insertions(+), 61 deletions(-) diff --git a/Manual.lean b/Manual.lean index fa73d713..cd2ce24c 100644 --- a/Manual.lean +++ b/Manual.lean @@ -18,11 +18,10 @@ tag := "mathlib-manual" This file has been created with Lean {versionString}[]. -The automatically generated -[Mathlib Documentation](https://leanprover-community.github.io/mathlib4_docs/index.html) -contains a systematic list of all declarations from Mathlib. - -The [Lean Language Reference](https://lean-lang.org/doc/reference/latest/) contains -detailed information about Lean Code. +**Other resources**: +- [Mathlib Documentation](https://leanprover-community.github.io/mathlib4_docs/index.html): + automatically generated collection of all declarations from Mathlib. +- The [Lean Language Reference](https://lean-lang.org/doc/reference/latest/) contains + detailed information about Lean Code. {include 0 Manual.Tactics} diff --git a/Manual/Tactics.lean b/Manual/Tactics.lean index 5dcf9c07..1fb8b408 100644 --- a/Manual/Tactics.lean +++ b/Manual/Tactics.lean @@ -14,23 +14,56 @@ set_option pp.rawOnError true set_option linter.unusedVariables false + +section + +open Lean.Elab.Tactic.Doc + +-- set_option pp.deepTerms.threshold 500 in +-- #eval do +-- let tacs ← allTacticDocs +-- return tacs.map (fun x => TacticDoc.userName x) + +-- set_option pp.deepTerms.threshold 500 in +-- #eval do +-- let tacs ← allTacticDocs +-- return tacs.map (fun x => TacticDoc.internalName x) + +-- #eval do +-- let tacs ← allTacticDocs +-- return tacs.map (fun x => TacticDoc.docString x) + +#eval do + let tacs ← allTacticDocs + return s!"There are {tacs.size} tactics" + +-- TODO: This could be used to generate a list of all tactics automatically +-- but I'm not sure this is desired... + +end + set_option maxHeartbeats 0 set_option maxRecDepth 100000000000000000 open Lean.Elab.Tactic + #doc (Manual) "Tactics" => %%% tag := "tactics" %%% -This lists of tactics if far from complete +This list of tactics attempts to be fairly complete but +does leave out slight variations of certain tactics, +such as `fconstructor` vs. `constructor`. -*Contribute*: Most information about tactics is directly from the docstring of the tactic In -mathlib. In order to improve this text, PR to the docstring of the tactic. +If a tactic is missing from this file, +please PR to [this repository](https://github.com/leanprover-community/mathlib-manual). -If a tactic is missing from this file, PR to this repository. +The displayed docstring and name are automatically extracted from the Lean code. +If the information about a tactic is wrong, you should directly change the tactic's docstring by +creating a [PR to mathlib](https://github.com/leanprover-community/mathlib4). @@ -41,40 +74,56 @@ These tactics help the user discover tactics or statements. :::tactic Mathlib.Tactic.LibrarySearch.observe ::: +:::tactic "exact?" +::: + +:::tactic "apply?" +::: + +:::tactic "rw?" +::: + :::tactic Mathlib.Tactic.Hint.hintStx ::: -# High level automation +# Automation -This section contains a few general-purpose tactics -that try to automatically solve a goal. :::tactic Aesop.Frontend.Parser.aesopTactic ::: -:::tactic Mathlib.Tactic.cc +:::tactic "omega" ::: -:::tactic Mathlib.Tactic.Tauto.tauto +:::tactic Lean.Parser.Tactic.decide show:="decide" ::: -:::example "polyrith" -TODO +:::tactic Lean.Parser.Tactic.simp ::: -:::tactic Mathlib.Tactic.Positivity.positivity +:::tactic "infer_instance" ::: -:::example "linarith" -TODO +:::tactic Mathlib.Tactic.Tauto.tauto ::: +:::tactic "trivial" +::: +:::tactic Mathlib.Tactic.cc +::: +:::example "polyrith" +TODO +::: +:::tactic linarith show:="linarith" +::: +:::tactic Mathlib.Tactic.Positivity.positivity +::: # Algebra @@ -83,38 +132,42 @@ These tactics deal with algebraic calculations. :::tactic Mathlib.Tactic.Abel.abel ::: -:::tactic Mathlib.Tactic.tacticAlgebraize__ +:::tactic Mathlib.Tactic.Group.group ::: -:::tactic Mathlib.Tactic.FieldSimp.fieldSimp +:::tactic Mathlib.Tactic.RingNF.ring ::: -:::tactic Mathlib.Tactic.Group.group +:::tactic Mathlib.Tactic.NoncommRing.noncomm_ring ::: :::tactic Mathlib.Tactic.Module.tacticModule ::: -:::tactic Mathlib.Tactic.NoncommRing.noncomm_ring +:::tactic Mathlib.Tactic.LinearCombination.linearCombination ::: -:::tactic Mathlib.Tactic.RingNF.ring +:::tactic Mathlib.Tactic.FieldSimp.fieldSimp ::: -:::tactic Mathlib.Tactic.LinearCombination.linearCombination +:::tactic cancelDenoms ::: -:::tactic cancelDenoms +:::tactic Mathlib.Tactic.tacticAlgebraize__ ::: :::tactic Tactic.ReduceModChar.reduce_mod_char ::: +:::tactic Mathlib.Tactic.ComputeDegree.computeDegree +::: +:::tactic Mathlib.Tactic.ComputeDegree.monicityMacro +::: -# Function Properties / Analysis +# Function Properties / Analysis / Measure Theory These tactics proof certain properties about functions. @@ -127,48 +180,75 @@ These tactics proof certain properties about functions. :::tactic tacticMeasurability ::: +:::tactic Mathlib.Tactic.Borelize.tacticBorelize___ +::: + :::example "bound" TODO ::: +:::tactic ArithmeticFunction.arith_mult +::: + + # Category Theory These tactics are explicitely written for category theory. -todo +TODO -# Coersions / type casting / definitional Equivalence +# Miscellaneous -These tactics are used for modifying the goal in a way that seems mathematically -trivial: handling coersions/casts, changing the goal to something definitionally -equivalent, etc. +:::tactic finiteness show:="finiteness" +::: -:::tactic Mathlib.Tactic.convert +:::tactic Mathlib.Tactic.Monotonicity.mono ::: -:::tactic Mathlib.Tactic.lift +:::tactic Mathlib.Tactic.Nontriviality.nontriviality ::: -:::tactic Mathlib.Tactic.normNum +:::tactic Mathlib.Tactic.subsingletonStx ::: -:::tactic Mathlib.Tactic.Rify.rify + + +# Induction / case distinction + +:::tactic "induction" ::: -:::tactic Mathlib.Tactic.Qify.qify +:::tactic "cases" ::: -:::tactic Mathlib.Tactic.Zify.zify +:::tactic "rcases" ::: +:::tactic "by_cases" +::: + +:::tactic Lean.Elab.Tactic.finCases +::: + +:::tactic Mathlib.Tactic.intervalCases +::: + +:::tactic "split" +::: + +:::tactic Mathlib.Tactic.splitIfs +::: + + # Logic -These tactics deal with statements in logic. +These tactics deal with statements in logic. Remember that +`tauto`, listed above, is also good a these. :::tactic Mathlib.Tactic.Contrapose.contrapose ::: @@ -176,9 +256,6 @@ These tactics deal with statements in logic. :::tactic Mathlib.Tactic.PushNeg.tacticPush_neg_ ::: -:::tactic Mathlib.Tactic.splitIfs -::: - :::tactic Mathlib.Tactic.TFAE.tfaeHave ::: @@ -197,70 +274,246 @@ These tactics deal with statements in logic. :::tactic Mathlib.Tactic.Peel.peel ::: +:::tactic "left" +::: + +:::tactic "right" +::: + +:::tactic "contradiction" +::: + +:::tactic "exfalso" +::: + -# Rewriting + +# Rewriting / `calc` These tactics are used for rewriting parts of a goal with something that is equal (or equivalent/etc.) +:::tactic "calc" +::: + +:::tactic "rw" +::: + :::tactic Mathlib.Tactic.nthRewriteSeq ::: :::tactic Mathlib.Tactic.tacticSimp_rw___ ::: +The following Tactic is avoided in Mathlib + +:::tactic "erw" +::: -# Unsorted +# Congr / ext These tactics have not made it into any other category yet, please move them. -:::tactic Mathlib.Tactic.tacticApply_At_ +:::tactic Mathlib.Tactic.subsingletonStx ::: -:::tactic Mathlib.Tactic.applyFun +:::tactic "congr" ::: -:::tactic ArithmeticFunction.arith_mult +:::tactic Mathlib.Tactic.GCongr.tacticGcongr__With__ ::: -:::tactic Mathlib.Tactic.ComputeDegree.computeDegree +:::tactic "ext" ::: -:::tactic Mathlib.Tactic.ComputeDegree.monicityMacro +:::tactic "funext" ::: -:::tactic Lean.Elab.Tactic.finCases + + +# Coersions + +These tactics deal with coersions/casts between different types. + +:::tactic Mathlib.Tactic.normNum ::: -:::example "finiteness" -TODO +:::tactic Lean.Parser.Tactic.tacticNorm_cast__ ::: -:::tactic Mathlib.Tactic.GCongr.tacticGcongr__With__ +:::tactic Lean.Parser.Tactic.pushCast ::: -:::tactic Mathlib.Tactic.intervalCases +:::tactic Lean.Parser.Tactic.tacticAssumption_mod_cast_ ::: -:::tactic Mathlib.Tactic.Monotonicity.mono +:::tactic Lean.Parser.Tactic.tacticExact_mod_cast_ ::: -:::tactic Mathlib.Tactic.Nontriviality.nontriviality +:::tactic Lean.Parser.Tactic.tacticApply_mod_cast_ ::: -:::example " Mathlib.Tactic.setTactic" -TODO +:::tactic Lean.Parser.Tactic.tacticRw_mod_cast___ ::: -:::tactic Mathlib.Tactic.subsingletonStx +:::tactic Mathlib.Tactic.lift +::: + +:::tactic Mathlib.Tactic.Zify.zify +::: + +:::tactic Mathlib.Tactic.Rify.rify +::: + +:::tactic Mathlib.Tactic.Qify.qify +::: + + + +# Definitional equality + +These tactics modify the goal or assumptions in a way that remains +definitionally equal. + +:::tactic Lean.Parser.Tactic.dsimp +::: + +:::tactic "change" +::: + +:::tactic "unfold" +::: + + + +# Basic tactics / assumptions + +:::tactic "rfl" +::: + +:::tactic "symm" +::: + +:::tactic Batteries.Tactic.tacticTrans___ +::: + +:::tactic Lean.Parser.Tactic.assumption +::: + +:::tactic "exact" ::: +:::tactic Lean.Parser.Tactic.apply +::: + +Note that `apply` and `apply at` are formally considered two distinct tactics +even though they appear to be one to the user. + +:::tactic Mathlib.Tactic.tacticApply_At_ show:="apply at" +::: + + +:::tactic "specialize" +::: + +:::tactic "generalize" +::: + +:::tactic Lean.Parser.Tactic.tacticHave_ +::: + +:::tactic Lean.Parser.Tactic.tacticLet_ +::: + +-- TODO: The `set` docstring ought to be on the `syntax`, not the `elab_rules` +-- remove the replace below once that's fixed +:::tactic Mathlib.Tactic.setTactic replace:=true +::: + +:::tactic "replace" +::: + + +:::tactic "suffices" +::: + +:::tactic Lean.Parser.Tactic.obtain +::: + + +:::tactic "refine" +::: + +:::tactic Mathlib.Tactic.convert +::: + +:::tactic "constructor" +::: + +:::tactic "injection" +::: + +:::tactic "intro" +::: + +:::tactic Lean.Parser.Tactic.revert +::: + + + # Conv mode :::tactic Lean.Parser.Tactic.Conv.conv ::: -TODO: This section should contain anything used in conv mode +TODO: a lot of tactics have a `conv`-equivalent. Add them here. +Meanwhile, try other tactics and see which work in `conv` mode. + + + +# Control flow + +These tactics should not appear in a final proof but might be +useful along the way. + +:::tactic "sorry" +::: + +:::tactic "done" +::: + +:::tactic "checkpoint" +::: + +:::tactic "save" +::: + +:::tactic "stop" +::: + + + +# For Tests + +These are particularly helpful for writing tests to the `MathlibTest` suite. + + +:::tactic Lean.Parser.Tactic.guardHyp +::: + +:::tactic Lean.Parser.Tactic.guardTarget +::: + +:::tactic Lean.Parser.Tactic.guardExpr +::: + +:::tactic Lean.Parser.Tactic.failIfSuccess +::: + +Finally, this is a command and not a tactic, but it is also essential for test files. + +:::tactic Lean.guardMsgsCmd +::: diff --git a/README.md b/README.md index 04d59bad..591350d9 100644 --- a/README.md +++ b/README.md @@ -28,6 +28,16 @@ python3 -m http.server 8880 --directory _out/html-multi & Then open in your browser. +## Development + +In theory, one should be able to update this by calling a simple + +``` +lake update +``` + +However, this requires Verso to be compatible with the Lean version Mathlib uses. + ## Contributing We happily accept content around Mathlib to this guide.