Skip to content

wip: document the simp-all tactic in the simp guide #848

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
grunweg wants to merge 1 commit into
base: lean4
Choose a base branch
from
Open

wip: document the simp-all tactic in the simp guide #848

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 11 additions & 1 deletion templates/extras/simp.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)?
Expand Down
Loading