Recursive cases (
rcases) tactic and related tactics #
rcases is a tactic that will perform
cases recursively, according to a pattern. It is used to
destructure hypotheses or expressions composed of inductive types like
h1 : a ∧ b ∧ c ∨ d or
h2 : ∃ x y, trans_rel R x y. Usual usage might be
rcases h1 with ⟨ha, hb, hc⟩ | hd or
rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩ for these examples.
Each element of an
rcases pattern is matched against a particular local hypothesis (most of which
are generated during the execution of
rcases and represent individual elements destructured from
the input expression). An
rcases pattern has the following grammar:
- A name like
x, which names the active hypothesis as
- A blank
_, which does nothing (letting the automatic naming system used by
casesname the hypothesis).
- A hyphen
-, which clears the active hypothesis and any dependents.
- The keyword
rfl, which expects the hypothesis to be
h : a = b, and calls
subston the hypothesis (which has the effect of replacing
aeverywhere or vice versa).
- A type ascription
p : ty, which sets the type of the hypothesis to
tyand then matches it against
p. (Of course,
tymust unify with the actual type of
hfor this to work.)
- A tuple pattern
⟨p1, p2, p3⟩, which matches a constructor with many arguments, or a series of nested conjunctions or existentials. For example if the active hypothesis is
a ∧ b ∧ c, then the conjunction will be destructured, and
p1will be matched against
band so on.
- An alteration pattern
p1 | p2 | p3, which matches an inductive type with multiple constructors, or a nested disjunction like
a ∨ b ∨ c.
The patterns are fairly liberal about the exact shape of the constructors, and will insert additional alternation branches and tuple arguments if there are not enough arguments provided, and reuse the tail for further matches if there are too many arguments provided to alternation and tuple patterns.
This file also contains the
rintro tactics, which use the same syntax of
patterns but with a slightly different use case:
rintros) is used like
rintro x ⟨y, z⟩and is the same as
rcaseson the newly introduced arguments.
obtainis the same as
rcasesbut with a syntax styled after
obtain ⟨hx, hy⟩ | hz := foois equivalent to
rcases foo with ⟨hx, hy⟩ | hz. Unlike
obtainalso allows one to omit
:= foo, although a type must be provided in this case, as in
obtain ⟨hx, hy⟩ | hz : a ∧ b ∨ c, in which case it produces a subgoal for proving
a ∧ b ∨ cin addition to the subgoals
hx : a, hy : b |- goaland
hz : c |- goal.
rcases, rintro, obtain, destructuring, cases, pattern matching, match
These synonyms for
list are used to clarify the meanings of the many
usages of lists in this module.
listΣis used where a list represents a disjunction, such as the list of possible constructors of an inductive type.
listΠis used where a list represents a conjunction, such as the list of arguments of an individual constructor.
These are merely type synonyms, and so are not checked for consistency by the compiler.
local notation combination makes Lean retain these
annotations in reported types.
zip_with, but if the lists don't match in length, the excess elements will be put at the
end of the result.