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 x.
• A blank _, which does nothing (letting the automatic naming system used by cases name 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 subst on the hypothesis (which has the effect of replacing b with a everywhere or vice versa).
• A type ascription p : ty, which sets the type of the hypothesis to ty and then matches it against p. (Of course, ty must unify with the actual type of h for 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 p1 will be matched against a, p2 against b and so on.
• A @ before a tuple pattern as in @⟨p1, p2, p3⟩ will bind all arguments in the constructor, while leaving the @ off will only use the patterns on the explicit arguments.
• An alternation 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 obtain and rintro tactics, which use the same syntax of rcases patterns but with a slightly different use case:

• rintro (or rintros) is used like rintro x ⟨y, z⟩ and is the same as intros followed by rcases on the newly introduced arguments.
• obtain is the same as rcases but with a syntax styled after have rather than cases. obtain ⟨hx, hy⟩ | hz := foo is equivalent to rcases foo with ⟨hx, hy⟩ | hz. Unlike rcases, obtain also 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 ∨ c in addition to the subgoals hx : a, hy : b |- goal and hz : c |- goal.

Tags

rcases, rintro, obtain, destructuring, cases, pattern matching, match

def Lean.Parser.Category.rcasesPat : Category

The syntax category of rcases patterns.

Equations

• Lean.Parser.Category.rcasesPat = { }

def Lean.Parser.Tactic.rcasesPat.quot : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.rcasesPatMed : ParserDescr

A medium precedence rcases pattern is a list of rcasesPat separated by |

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.rcasesPatLo : ParserDescr

A low precedence rcases pattern is a rcasesPatMed optionally followed by : ty

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.rcasesPat.one : ParserDescr

x is a pattern which binds x

Equations

• Lean.Parser.Tactic.rcasesPat.one = Lean.ParserDescr.node `Lean.Parser.Tactic.rcasesPat.one 1022 (Lean.ParserDescr.const `ident)

def Lean.Parser.Tactic.rcasesPat.ignore : ParserDescr

_ is a pattern which ignores the value and gives it an inaccessible name

Equations

• Lean.Parser.Tactic.rcasesPat.ignore = Lean.ParserDescr.node `Lean.Parser.Tactic.rcasesPat.ignore 1024 (Lean.ParserDescr.symbol "_")

def Lean.Parser.Tactic.rcasesPat.clear : ParserDescr

- is a pattern which removes the value from the context

Equations

• Lean.Parser.Tactic.rcasesPat.clear = Lean.ParserDescr.node `Lean.Parser.Tactic.rcasesPat.clear 1024 (Lean.ParserDescr.symbol "-")

def Lean.Parser.Tactic.rcasesPat.explicit : ParserDescr

A @ before a tuple pattern as in @⟨p1, p2, p3⟩ will bind all arguments in the constructor, while leaving the @ off will only use the patterns on the explicit arguments.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.rcasesPat.tuple : ParserDescr

⟨pat, ...⟩ is a pattern which matches on a tuple-like constructor or multi-argument inductive constructor

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.rcasesPat.paren : ParserDescr

(pat) is a pattern which resets the precedence to low

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.rintroPat.quot : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.rintroPat : Category

The syntax category of rintro patterns.

Equations

• Lean.Parser.Category.rintroPat = { }

def Lean.Parser.Tactic.rintroPat.one : ParserDescr

An rcases pattern is an rintro pattern

Equations

• Lean.Parser.Tactic.rintroPat.one = Lean.ParserDescr.node `Lean.Parser.Tactic.rintroPat.one 1022 (Lean.ParserDescr.cat `rcasesPat 0)

def Lean.Parser.Tactic.rintroPat.binder : ParserDescr

A multi argument binder (pat1 pat2 : ty) binds a list of patterns and gives them all type ty.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.rcases : ParserDescr

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 x.
• A blank _, which does nothing (letting the automatic naming system used by cases name 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 subst on the hypothesis (which has the effect of replacing b with a everywhere or vice versa).
• A type ascription p : ty, which sets the type of the hypothesis to ty and then matches it against p. (Of course, ty must unify with the actual type of h for 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 p1 will be matched against a, p2 against b and so on.
• A @ before a tuple pattern as in @⟨p1, p2, p3⟩ will bind all arguments in the constructor, while leaving the @ off will only use the patterns on the explicit arguments.
• An alternation pattern p1 | p2 | p3, which matches an inductive type with multiple constructors, or a nested disjunction like a ∨ b ∨ c.

A pattern like ⟨a, b, c⟩ | ⟨d, e⟩ will do a split over the inductive datatype, naming the first three parameters of the first constructor as a,b,c and the first two of the second constructor d,e. If the list is not as long as the number of arguments to the constructor or the number of constructors, the remaining variables will be automatically named. If there are nested brackets such as ⟨⟨a⟩, b | c⟩ | d then these will cause more case splits as necessary. If there are too many arguments, such as ⟨a, b, c⟩ for splitting on ∃ x, ∃ y, p x, then it will be treated as ⟨a, ⟨b, c⟩⟩, splitting the last parameter as necessary.

rcases also has special support for quotient types: quotient induction into Prop works like matching on the constructor quot.mk.

rcases h : e with PAT will do the same as rcases e with PAT with the exception that an assumption h : e = PAT will be added to the context.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.obtain : ParserDescr

The obtain tactic is a combination of have and rcases. See rcases for a description of supported patterns.

obtain ⟨patt⟩ : type := proof

is equivalent to

have h : type := proof
rcases h with ⟨patt⟩

If ⟨patt⟩ is omitted, rcases will try to infer the pattern.

If type is omitted, := proof is required.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.rintro : ParserDescr

The rintro tactic is a combination of the intros tactic with rcases to allow for destructuring patterns while introducing variables. See rcases for a description of supported patterns. For example, rintro (a | ⟨b, c⟩) ⟨d, e⟩ will introduce two variables, and then do case splits on both of them producing two subgoals, one with variables a d e and the other with b c d e.

rintro, unlike rcases, also supports the form (x y : ty) for introducing and type-ascripting multiple variables at once, similar to binders.

Equations

• One or more equations did not get rendered due to their size.