From 8185b6afe5ced0393020ca6d06cc773e5ae1e75e Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 22 May 2026 21:20:43 +0200 Subject: [PATCH] wip: document simp_all --- templates/extras/simp.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/templates/extras/simp.md b/templates/extras/simp.md index 2b5c199b9..24c1ac062 100644 --- a/templates/extras/simp.md +++ b/templates/extras/simp.md @@ -177,7 +177,7 @@ This generates the lemma `@[simp] lemma myFoo_n : myFoo.n = 37`. * `simp at h` tries to simplify `h` using all `simp` lemmas. -* `simp [h1] at h2 ⊢` tries to simplify both `h2` and the goal using `h1` and all `simp` lemmas (note: type `⊢` with `\|-` or `\vdash` in VS Code). +* `simp [h1] at h2 ⊢` tries to simplify both `h2` and the goal using `h1` and all `simp` lemmas (note: type `⊢` with `\|-`, `\goal` or `\vdash` in VS Code). * `simp [*] at *` : tries to simplify both the goal and all hypotheses, using all hypotheses and all `simp` lemmas. Sometimes worth a try. @@ -248,6 +248,13 @@ form. For example if `g 0` can be simplified, then `@[simp] lemma foo : f (g 0) Batteries' `simpNF` [linter](https://leanprover-community.github.io/mathlib4_docs/Batteries/Tactic/Lint/Frontend.html) checks for this (you can run mathlib's linters for a module yourself by putting `#lint` at the end of the file). +## `simp_all` + +`simp_all` is a stronger version of `simp [*] at *` where the hypotheses and target +are simplified multiple times until no simplification is applicable. +Only non-dependent propositional hypotheses are considered. +This can lead to unprovable goals if the local hypotheses were contradictory. + ## `simpa` The `simpa` tactic is a variation on `simp` for finishing a proof -- as a "finishing" tactic, it will fail @@ -399,6 +406,9 @@ This is the full syntax for the `simp` tactic: > `simp` (`?`)? (`!`)? (`(config :=` config `)`)? (`(disch :=` discharger `)`)? (`only`)? (`[`list of `*` and lemmas`]`)? (`at` locations)? +This is the full syntax for the `simp_all` tactic: +> `simp_all` config ( `disch := ` discharger `)`)? (&" only")? (`[`list of `*` and lemmas`]`)? + This is the full syntax for the `simpa` tactic: > `simpa` (`?`)? (`!`)? (`(config :=` config `)`)? (`(disch :=` discharger `)`)? (`only`)? (`[`list of `*` and lemmas`]`)? (`using` expr)?