The goals in a proof state are displayed in order, with the main goal on top.
Goals may be either named or anonymous.
Named goals are indicated with case at the top (called a case label), while anonymous goals have no such indicator.
Tactics assign goal names, typically on the basis of constructor names, parameter names, structure field names, or the nature of the reasoning step implemented by the tactic.
Named goals
This proof state contains four goals, all of which are named.
This is part of a proof that the MonadOption instance is lawful (that is, to provide the LawfulMonadOption instance), and the case names (highlighted below) come from the names of the fields of LawfulMonad.
α:Type ?u.25β:Type ?u.25f:α → βx:Optionα⊢ (doleta ← xpure (fa)) =
f <$> xα:Type ?u.25β:Type ?u.25f:Option (α → β)x:Optionα⊢ (doletx_1 ← fx_1 <$> x) =
f <*> xα:Type ?u.25β:Type ?u.25x:αf:α → Optionβ⊢ purex >>= f = fxα:Type ?u.25β:Type ?u.25γ:Type ?u.25x:Optionαf:α → Optionβg:β → Optionγ⊢ x >>= f >>= g = x >>= funx => fx >>= g
Anonymous Goals
This proof state contains a single anonymous goal.
n:Natk:Nat⊢ n + k = k + n
The case and case' tactics can be used to select a new main goal using the desired goal's name.
When names are assigned in the context of a goal which itself has a name, the new goals's names are appended to the main goal's name with a dot ('.', Unicode FULL STOP (0x2e)) between them.
Hierarchical Goal Names
In the course of an attempt to prove ∀(nk:Nat),n+k=k+n, this proof state can occur:
k:Nat⊢ 0 + k = k + 0k:Natn✝:Nata✝:n✝ + k = k + n✝⊢ n✝ + 1 + k = k + (n✝ + 1)
After ⊢ 0 + 0 = 0 + 0n✝:Nata✝:0 + n✝ = n✝ + 0⊢ 0 + (n✝ + 1) = n✝ + 1 + 0k:Natn✝:Nata✝:n✝ + k = k + n✝⊢ n✝ + 1 + k = k + (n✝ + 1), the two new cases' names have zero as a prefix, because they were created in a goal named zero:
Each goal consists of a sequence of assumptions and a desired conclusion.
Each assumption has a name and a type; the conclusion is a type.
Assumptions are either arbitrary elements of some type or statements that are presumed true.
Assumption Names and Conclusion
This goal has four assumptions:
α:Type ?u.300x:αxs:Listαih:xs ++ [] = xs⊢ x :: xs ++ [] = x :: xs
They are:
α, an arbitrary type
x, an arbitrary α
xs, an arbitrary Listα
ih, an induction hypothesis that asserts that appending the empty list to xs is equal to xs.
The conclusion is the statement that prepending x to both sides of the equality in the induction hypothesis results in equal lists.
Some assumptions are inaccessible, which means that they cannot be referred to explicitly by name.
Inaccessible assumptions occur when an assumption is created without a specified name or when the assumption's name is shadowed by a later assumption.
Inaccessible assumptions should be regarded as anonymous; they are presented as if they had names because they may be referred to in later assumptions or in the conclusion, and displaying a name allows these references to be distinguished from one another.
In particular, inaccessible assumptions are presented with daggers (†) after their names.
Accessible Assumption Names
In this proof state, all assumptions are accessible.
α:Type ?u.438β:Type ?u.438f:α → βx:Optionα⊢ (doleta ← xpure (fa)) =
f <$> x
Inaccessible Assumption Names
In this proof state, only the first and third assumptions are accessible.
The second and fourth are inaccessible, and their names include a dagger to indicate that they cannot be referenced.
Inaccessible assumptions can still be used.
Tactics such as assumption or simp can scan the entire list of assumptions, finding one that is useful, and contradiction can eliminate the current goal by finding an impossible assumption without naming it.
Other tactics, such as rename_i and next, can be used to name inaccessible assumptions, making them accessible.
Additionally, assumptions can be referred to by their type, by writing the type in single guillemets.
syntax
Single guillemets around a term represent a reference to some term in scope with that type.
term::= ...
|`‹t›` resolves to an (arbitrary) hypothesis of type `t`.
It is useful for referring to hypotheses without accessible names.
`t` may contain holes that are solved by unification with the expected type;
in particular, `‹_›` is a shortcut for `by assumption`.
‹term›
This can be used to refer to local lemmas by their theorem statement rather than by name, or to refer to assumptions regardless of whether they have explicit names.
Assumptions by Typevariable(n:Nat)
In the following proof, cases is repeatedly used to analyze a number.
At the beginning of the proof, the number is named x, but cases generates an inaccessible name for subsequent numbers.
Rather than providing names, the proof takes advantage of the fact that there is a single assumption of type Nat at any given time and uses ‹Nat› to refer to it.
After the iteration, there is an assumption that n + 3 < 3, which contradiction can use to remove the goal from consideration.
Single-guillemet syntax also works outside of proofs:
2#evalletx:=1lety:=2‹Nat›
2
This is generally not a good idea for non-propositions, however—when it matters which element of a type is selected, it's better to select it explicitly.
Terms in proof states can be quite big, and there may be many assumptions.
Because of definitional proof irrelevance, proof terms typically give little useful information.
By default, they are not shown in goals in proof states unless they are atomic, meaning that they contain no subterms.
Hiding proofs is controlled by two options: pp.proofs turns the feature on and off, while pp.proofs.threshold determines a size threshold for proof hiding.
Hiding Proof Terms
In this proof state, the proof that 0 < n is hidden.
(pretty printer) when pp.proofs is false, controls the complexity of proofs at which they begin being replaced with ⋯
Additionally, non-proof terms may be hidden when they are too large.
In particular, Lean will hide terms that are below a configurable depth threshold, and it will hide the remainder of a term once a certain amount in total has been printed.
Showing deep terms can enabled or disabled with the option pp.deepTerms, and the depth threshold can be configured with the option pp.deepTerms.threshold.
The maximum number of pretty-printer steps can be configured with the option pp.maxSteps.
Printing very large terms can lead to slowdowns or even stack overflows in tooling; please be conservative when adjusting these options' values.
Terms that begin with a question mark are metavariables that correspond to an unknown value.
They may stand for either universe levels or for terms.
Some metavariables arise as part of Lean's elaboration process, when not enough information is yet available to determine a value.
These metavariables' names have a numeric component at the end, such as ?m.392 or ?u.498.
Other metavariables come into existence as a result of tactics or named holes.
These metavariables' names do not have a numeric component.
Metavariables that result from tactics frequently appear as goals whose case labels match the name of the metavariable.
Universe Level Metavariables
In this proof state, the universe level of α is unknown:
In this proof state, the type of list elements is unknown.
The metavariable is repeated because the unknown type must be the same in both positions.
x:?m.980xs:List ?m.980elem:x ∈ xs⊢ xs.length > 0
Metavariables in Proofs
In this proof state,
i:Natj:Natk:Nath1:i < jh2:j < k⊢ i < k
applying the tactic i:Natj:Natk:Nath1:i < jh2:j < k⊢ i < ?mi:Natj:Natk:Nath1:i < jh2:j < k⊢ ?m < ki:Natj:Natk:Nath1:i < jh2:j < k⊢ Nat results in the following proof state, in which the middle value of the transitivity step ?m is unknown:
Explicit named holes are represented by metavariables, and additionally give rise to proof goals.
In this proof state,
i:Natj:Natk:Nath1:i < jh2:j < k⊢ i < k
applying the tactic i:Natj:Natk:Nath1:i < jh2:j < k⊢ Nati:Natj:Natk:Nath1:i < jh2:j < k⊢ i < ?middlei:Natj:Natk:Nath1:i < jh2:j < k⊢ ?middle < k results in the following proof state, in which the middle value of the transitivity step ?middle is unknown and goals have been created for each of the named holes in the term:
i:Natj:Natk:Nath1:i < jh2:j < k⊢ Nati:Natj:Natk:Nath1:i < jh2:j < k⊢ i < ?middlei:Natj:Natk:Nath1:i < jh2:j < k⊢ ?middle < k
The display of metavariable numbers can be disabled using the pp.mvars.
This can be useful when using features such as Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd`
and checks that they match the contents of the docstring.
Basic example:
```lean
/--
error: unknown identifier 'x'
-/
#guard_msgs in
example : α := x
```
This checks that there is such an error and then consumes the message.
By default, the command captures all messages, but the filter condition can be adjusted.
For example, we can select only warnings:
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
or only errors
```lean
#guard_msgs(error) in
example : α := sorry
```
In the previous example, since warnings are not captured there is a warning on `sorry`.
We can drop the warning completely with
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses:
```
#guard_msgs (configElt,*) in cmd
```
By default, the configuration list is `(all, whitespace := normalized, ordering := exact)`.
Message filters (processed in left-to-right order):
- `info`, `warning`, `error`: capture messages with the given severity level.
- `all`: capture all messages (the default).
- `drop info`, `drop warning`, `drop error`: drop messages with the given severity level.
- `drop all`: drop every message.
Whitespace handling (after trimming leading and trailing whitespace):
- `whitespace := exact` requires an exact whitespace match.
- `whitespace := normalized` converts all newline characters to a space before matching
(the default). This allows breaking long lines.
- `whitespace := lax` collapses whitespace to a single space before matching.
Message ordering:
- `ordering := exact` uses the exact ordering of the messages (the default).
- `ordering := sorted` sorts the messages in lexicographic order.
This helps with testing commands that are non-deterministic in their ordering.
For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and drop
everything else.
The command elaborator has special support for `#guard_msgs` for linting.
The `#guard_msgs` itself wants to capture linter warnings,
so it elaborates the command it is attached to as if it were a top-level command.
However, the command elaborator runs linters for *all* top-level commands,
which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings.
The top-level command elaborator only runs the linters if `#guard_msgs` is not present.
#guard_msgs that match Lean's output against a desired string, which is very useful when writing tests for custom tactics.
(pretty printer) display names of metavariables when true, and otherwise display them as '?' (for expression metavariables) and as '' (for universe level metavariables)
Planned Content
Demonstrate and explain diff labels that show the difference between the steps of a proof state.