84e46162b5
This is the groundwork for a tactic index in generated documentation, as there was in Lean 3. There are a few challenges to getting this to work well in Lean 4: * There's no natural notion of *tactic identity* - a tactic may be specified by multiple syntax rules (e.g. the pattern-matching version of `intro` is specified apart from the default version, but both are the same from a user perspective) * There's no natural notion of *tactic name* - here, we take the pragmatic choice of using the first keyword atom in the tactic's syntax specification, but this may need to be overridable someday. * Tactics are extensible, but we don't want to allow arbitrary imports to clobber existing tactic docstrings, which could become unpredictable in practice. For tactic identity, this PR introduces the notion of a *tactic alternative*, which is a `syntax` specification that is really "the same as" an existing tactic, but needs to be separate for technical reasons. This provides a notion of tactic identity, which we can use as the basis of a tactic index in generated documentation. Alternative forms of tactics are specified using a new `@[tactic_alt IDENT]` attribute, applied to the new tactic syntax. It is an error to declare a tactic syntax rule to be an alternative of another one that is itself an alternative. Documentation hovers now take alternatives into account, and display the docs for the canonical name. *Tactic tags*, created with the `register_tactic_tag` command, specify tags that may be applied to tactics. This is intended to be used by doc-gen and Verso. Tags may be applied using the `@[tactic_tag TAG1 TAG2 ...]` attribute on a canonical tactic parser, which may be used in any module to facilitate downstream projects introducing tags that apply to pre-existing tactics. Tags may not be removed, but it's fine to redundantly add them. The collection of tags, and the tactics to which they're applied, can be seen using the `#print tactic tags` command. *Extension documentation* provides a structured way to document extensions to tactics. The resulting documentation is gathered into a bulleted list at the bottom of the tactic's docstring. Extensions are added using the `tactic_extension TAC` command. This can be used when adding new interpretations of a tactic via `macro_rules`, when extending some table or search index used by the tactic, or in any other way. It is a command to facilitate its flexible use with various extension mechanisms.
149 lines
4.5 KiB
Text
149 lines
4.5 KiB
Text
/-
|
|
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura, Sebastian Ullrich
|
|
-/
|
|
prelude
|
|
import Lean.Parser.Term
|
|
import Lean.Parser.Tactic.Doc
|
|
|
|
namespace Lean
|
|
namespace Parser
|
|
namespace Tactic
|
|
|
|
builtin_initialize
|
|
register_parser_alias tacticSeq
|
|
register_parser_alias tacticSeqIndentGt
|
|
|
|
/- This is a fallback tactic parser for any identifier which exists only
|
|
to improve syntax error messages.
|
|
```
|
|
example : True := by foo -- unknown tactic
|
|
```
|
|
-/
|
|
@[builtin_tactic_parser] def «unknown» := leading_parser
|
|
withPosition (ident >> errorAtSavedPos "unknown tactic" true)
|
|
|
|
@[builtin_tactic_parser] def nestedTactic := tacticSeqBracketed
|
|
|
|
def matchRhs := Term.hole <|> Term.syntheticHole <|> tacticSeq
|
|
def matchAlts := Term.matchAlts (rhsParser := matchRhs)
|
|
|
|
/-- `match` performs case analysis on one or more expressions.
|
|
See [Induction and Recursion][tpil4].
|
|
The syntax for the `match` tactic is the same as term-mode `match`, except that
|
|
the match arms are tactics instead of expressions.
|
|
```
|
|
example (n : Nat) : n = n := by
|
|
match n with
|
|
| 0 => rfl
|
|
| i+1 => simp
|
|
```
|
|
|
|
[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html
|
|
-/
|
|
@[builtin_tactic_parser] def «match» := leading_parser:leadPrec
|
|
"match " >> optional Term.generalizingParam >>
|
|
optional Term.motive >> sepBy1 Term.matchDiscr ", " >>
|
|
" with " >> ppDedent matchAlts
|
|
|
|
/--
|
|
The tactic
|
|
```
|
|
intro
|
|
| pat1 => tac1
|
|
| pat2 => tac2
|
|
```
|
|
is the same as:
|
|
```
|
|
intro x
|
|
match x with
|
|
| pat1 => tac1
|
|
| pat2 => tac2
|
|
```
|
|
That is, `intro` can be followed by match arms and it introduces the values while
|
|
doing a pattern match. This is equivalent to `fun` with match arms in term mode.
|
|
-/
|
|
@[builtin_tactic_parser] def introMatch := leading_parser
|
|
nonReservedSymbol "intro" >> matchAlts
|
|
|
|
/--
|
|
`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`
|
|
and then reducing that instance to evaluate the truth value of `p`.
|
|
If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.
|
|
|
|
Limitations:
|
|
- The target is not allowed to contain local variables or metavariables.
|
|
If there are local variables, you can try first using the `revert` tactic with these local variables
|
|
to move them into the target, which may allow `decide` to succeed.
|
|
- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined
|
|
by well-founded recursion might not work, because evaluating them requires reducing proofs.
|
|
The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.
|
|
These can appear for instances defined using tactics (such as `rw` and `simp`).
|
|
To avoid this, use definitions such as `decidable_of_iff` instead.
|
|
|
|
## Examples
|
|
|
|
Proving inequalities:
|
|
```lean
|
|
example : 2 + 2 ≠ 5 := by decide
|
|
```
|
|
|
|
Trying to prove a false proposition:
|
|
```lean
|
|
example : 1 ≠ 1 := by decide
|
|
/-
|
|
tactic 'decide' proved that the proposition
|
|
1 ≠ 1
|
|
is false
|
|
-/
|
|
```
|
|
|
|
Trying to prove a proposition whose `Decidable` instance fails to reduce
|
|
```lean
|
|
opaque unknownProp : Prop
|
|
|
|
open scoped Classical in
|
|
example : unknownProp := by decide
|
|
/-
|
|
tactic 'decide' failed for proposition
|
|
unknownProp
|
|
since its 'Decidable' instance reduced to
|
|
Classical.choice ⋯
|
|
rather than to the 'isTrue' constructor.
|
|
-/
|
|
```
|
|
|
|
## Properties and relations
|
|
|
|
For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.
|
|
```lean
|
|
example : 1 + 1 = 2 := by decide
|
|
example : 1 + 1 = 2 := by rfl
|
|
```
|
|
-/
|
|
@[builtin_tactic_parser] def decide := leading_parser
|
|
nonReservedSymbol "decide"
|
|
|
|
/-- `native_decide` will attempt to prove a goal of type `p` by synthesizing an instance
|
|
of `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this
|
|
uses `#eval` to evaluate the decidability instance.
|
|
|
|
This should be used with care because it adds the entire lean compiler to the trusted
|
|
part, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using
|
|
this method or anything that transitively depends on them. Nevertheless, because it is
|
|
compiled, this can be significantly more efficient than using `decide`, and for very
|
|
large computations this is one way to run external programs and trust the result.
|
|
```
|
|
example : (List.range 1000).length = 1000 := by native_decide
|
|
```
|
|
-/
|
|
@[builtin_tactic_parser] def nativeDecide := leading_parser
|
|
nonReservedSymbol "native_decide"
|
|
|
|
builtin_initialize
|
|
register_parser_alias "matchRhsTacticSeq" matchRhs
|
|
|
|
end Tactic
|
|
end Parser
|
|
end Lean
|