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.Meta.FVarSubst.append (s : Lean.Meta.FVarSubst) (t : Lean.Meta.FVarSubst) : Lean.Meta.FVarSubst

Constructs a substitution consisting of s followed by t. This satisfies (s.append t).apply e = t.apply (s.apply e)

Equations

• Lean.Meta.FVarSubst.append s t = Lean.AssocList.foldl (fun s' k v => Lean.Meta.FVarSubst.insert s' k (Lean.Meta.FVarSubst.apply t v)) t s.map

opaque Std.Tactic.RCases.linter.unusedRCasesPattern : Lean.Option Bool

Enables the 'unused rcases pattern' linter. This will warn when a pattern is ignored by rcases, rintro, ext and similar tactics.

def Std.Tactic.RCases.rcasesPat.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.rcasesPat : Lean.Parser.Category

The syntax category of rcases patterns.

Equations

• Lean.Parser.Category.rcasesPat = { }

def Std.Tactic.RCases.rcasesPatMed : Lean.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 Std.Tactic.RCases.rcasesPatLo : Lean.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 Std.Tactic.RCases.rcasesPat.one : Lean.ParserDescr

x is a pattern which binds x

Equations

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

def Std.Tactic.RCases.rcasesPat.ignore : Lean.ParserDescr

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

Equations

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

def Std.Tactic.RCases.rcasesPat.clear : Lean.ParserDescr

- is a pattern which removes the value from the context

Equations

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

def Std.Tactic.RCases.rcasesPat.explicit : Lean.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 Std.Tactic.RCases.rcasesPat.tuple : Lean.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 Std.Tactic.RCases.rcasesPat.paren : Lean.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 Std.Tactic.RCases.rintroPat.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.rintroPat : Lean.Parser.Category

The syntax category of rintro patterns.

Equations

• Lean.Parser.Category.rintroPat = { }

def Std.Tactic.RCases.rintroPat.one : Lean.ParserDescr

An rcases pattern is an rintro pattern

Equations

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

def Std.Tactic.RCases.rintroPat.binder : Lean.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.

instance Std.Tactic.RCases.instCoeIdentTSyntaxConsSyntaxNodeKindMkStr1Nil : Coe Lean.Ident (Lean.TSyntax `rcasesPat)

Equations

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

instance Std.Tactic.RCases.instCoeTSyntaxConsSyntaxNodeKindMkStr1NilMkStr4 : Coe (Lean.TSyntax `rcasesPat) (Lean.TSyntax `Std.Tactic.RCases.rcasesPatMed)

Equations

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

instance Std.Tactic.RCases.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil : Coe (Lean.TSyntax `Std.Tactic.RCases.rcasesPatMed) (Lean.TSyntax `Std.Tactic.RCases.rcasesPatLo)

Equations

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

instance Std.Tactic.RCases.instCoeTSyntaxConsSyntaxNodeKindMkStr1Nil : Coe (Lean.TSyntax `rcasesPat) (Lean.TSyntax `rintroPat)

Equations

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

inductive Std.Tactic.RCases.RCasesPatt : Type

• paren: Lean.Syntax → Std.Tactic.RCases.RCasesPatt → Std.Tactic.RCases.RCasesPatt

  A parenthesized expression, used for hovers

• one: Lean.Syntax → Lean.Name → Std.Tactic.RCases.RCasesPatt

  A named pattern like foo

• clear: Lean.Syntax → Std.Tactic.RCases.RCasesPatt

  A hyphen -, which clears the active hypothesis and any dependents.

• explicit: Lean.Syntax → Std.Tactic.RCases.RCasesPatt → Std.Tactic.RCases.RCasesPatt

  An explicit pattern @pat.

• typed: Lean.Syntax → Std.Tactic.RCases.RCasesPatt → Lean.Term → Std.Tactic.RCases.RCasesPatt

  A type ascription like pat : ty (parentheses are optional)

• tuple: Lean.Syntax → List Std.Tactic.RCases.RCasesPatt → Std.Tactic.RCases.RCasesPatt

  A tuple constructor like ⟨p1, p2, p3⟩

• alts: Lean.Syntax → List Std.Tactic.RCases.RCasesPatt → Std.Tactic.RCases.RCasesPatt

  An alternation / variant pattern p1 | p2 | p3

An rcases pattern can be one of the following, in a nested combination:

• A name like foo
• The special keyword rfl (for pattern matching on equality using subst)
• A hyphen -, which clears the active hypothesis and any dependents.
• A type ascription like pat : ty (parentheses are optional)
• A tuple constructor like ⟨p1, p2, p3⟩
• An alternation / variant pattern p1 | p2 | p3

Parentheses can be used for grouping; alternation is higher precedence than type ascription, so p1 | p2 | p3 : ty means (p1 | p2 | p3) : ty.

N-ary alternations are treated as a group, so p1 | p2 | p3 is not the same as p1 | (p2 | p3), and similarly for tuples. However, note that an n-ary alternation or tuple can match an n-ary conjunction or disjunction, because if the number of patterns exceeds the number of constructors in the type being destructed, the extra patterns will match on the last element, meaning that p1 | p2 | p3 will act like p1 | (p2 | p3) when matching a1 ∨ a2 ∨ a3. If matching against a type with 3 constructors, p1 | (p2 | p3) will act like p1 | (p2 | p3) | _ instead.

instance Std.Tactic.RCases.instReprRCasesPatt : Repr Std.Tactic.RCases.RCasesPatt

Equations

• Std.Tactic.RCases.instReprRCasesPatt = { reprPrec := Std.Tactic.RCases.reprRCasesPatt✝ }

instance Std.Tactic.RCases.RCasesPatt.instInhabitedRCasesPatt : Inhabited Std.Tactic.RCases.RCasesPatt

Equations

• Std.Tactic.RCases.RCasesPatt.instInhabitedRCasesPatt = { default := Std.Tactic.RCases.RCasesPatt.one Lean.Syntax.missing `_ }

partial def Std.Tactic.RCases.RCasesPatt.name? : Std.Tactic.RCases.RCasesPatt → Option Lean.Name

Get the name from a pattern, if provided

def Std.Tactic.RCases.RCasesPatt.ref : Std.Tactic.RCases.RCasesPatt → Lean.Syntax

Get the syntax node from which this pattern was parsed. Used for error messages

Equations

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

def Std.Tactic.RCases.RCasesPatt.asTuple : Std.Tactic.RCases.RCasesPatt → Bool × List Std.Tactic.RCases.RCasesPatt

Interpret an rcases pattern as a tuple, where p becomes ⟨p⟩ if p is not already a tuple.

Equations

• Std.Tactic.RCases.RCasesPatt.asTuple (Std.Tactic.RCases.RCasesPatt.paren ref p) = Std.Tactic.RCases.RCasesPatt.asTuple p
• Std.Tactic.RCases.RCasesPatt.asTuple (Std.Tactic.RCases.RCasesPatt.explicit ref p) = (true, (Std.Tactic.RCases.RCasesPatt.asTuple p).snd)
• Std.Tactic.RCases.RCasesPatt.asTuple (Std.Tactic.RCases.RCasesPatt.tuple ref ps) = (false, ps)
• Std.Tactic.RCases.RCasesPatt.asTuple x = (false, [x])

def Std.Tactic.RCases.RCasesPatt.asAlts : Std.Tactic.RCases.RCasesPatt → List Std.Tactic.RCases.RCasesPatt

Interpret an rcases pattern as an alternation, where non-alternations are treated as one alternative.

Equations

• Std.Tactic.RCases.RCasesPatt.asAlts (Std.Tactic.RCases.RCasesPatt.paren ref p) = Std.Tactic.RCases.RCasesPatt.asAlts p
• Std.Tactic.RCases.RCasesPatt.asAlts (Std.Tactic.RCases.RCasesPatt.alts ref ps) = ps
• Std.Tactic.RCases.RCasesPatt.asAlts x = [x]

def Std.Tactic.RCases.RCasesPatt.typed? (ref : Lean.Syntax) : Std.Tactic.RCases.RCasesPatt → Option Lean.Term → Std.Tactic.RCases.RCasesPatt

Convert a list of patterns to a tuple pattern, but mapping [p] to p instead of ⟨p⟩.

Equations

• Std.Tactic.RCases.RCasesPatt.typed? ref x x = match x, x with | p, none => p | p, some ty => Std.Tactic.RCases.RCasesPatt.typed ref p ty

def Std.Tactic.RCases.RCasesPatt.tuple' : List Std.Tactic.RCases.RCasesPatt → Std.Tactic.RCases.RCasesPatt

Convert a list of patterns to a tuple pattern, but mapping [p] to p instead of ⟨p⟩.

Equations

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

def Std.Tactic.RCases.RCasesPatt.alts' (ref : Lean.Syntax) : List Std.Tactic.RCases.RCasesPatt → Std.Tactic.RCases.RCasesPatt

Convert a list of patterns to an alternation pattern, but mapping [p] to p instead of a unary alternation |p.

Equations

• Std.Tactic.RCases.RCasesPatt.alts' ref x = match x with | [p] => p | ps => Std.Tactic.RCases.RCasesPatt.alts ref ps

def Std.Tactic.RCases.RCasesPatt.tuple₁Core : List Std.Tactic.RCases.RCasesPatt → List Std.Tactic.RCases.RCasesPatt

This function is used for producing rcases patterns based on a case tree. Suppose that we have a list of patterns ps that will match correctly against the branches of the case tree for one constructor. This function will merge tuples at the end of the list, so that [a, b, ⟨c, d⟩] becomes ⟨a, b, c, d⟩ instead of ⟨a, b, ⟨c, d⟩⟩.

We must be careful to turn [a, ⟨⟩] into ⟨a, ⟨⟩⟩ instead of ⟨a⟩ (which will not perform the nested match).

Equations

• Std.Tactic.RCases.RCasesPatt.tuple₁Core [] = []
• Std.Tactic.RCases.RCasesPatt.tuple₁Core [Std.Tactic.RCases.RCasesPatt.tuple ref []] = [Std.Tactic.RCases.RCasesPatt.tuple ref []]
• Std.Tactic.RCases.RCasesPatt.tuple₁Core [Std.Tactic.RCases.RCasesPatt.tuple ref ps] = ps
• Std.Tactic.RCases.RCasesPatt.tuple₁Core (p :: ps) = p :: Std.Tactic.RCases.RCasesPatt.tuple₁Core ps

def Std.Tactic.RCases.RCasesPatt.tuple₁ : List Std.Tactic.RCases.RCasesPatt → Std.Tactic.RCases.RCasesPatt

This function is used for producing rcases patterns based on a case tree. This is like tuple₁Core but it produces a pattern instead of a tuple pattern list, converting [n] to n instead of ⟨n⟩ and [] to _, and otherwise just converting [a, b, c] to ⟨a, b, c⟩.

Equations

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

def Std.Tactic.RCases.RCasesPatt.alts₁Core : List (List Std.Tactic.RCases.RCasesPatt) → List Std.Tactic.RCases.RCasesPatt

This function is used for producing rcases patterns based on a case tree. Here we are given the list of patterns to apply to each argument of each constructor after the main case, and must produce a list of alternatives with the same effect. This function calls tuple₁ to make the individual alternatives, and handles merging [a, b, c | d] to a | b | c | d instead of a | b | (c | d).

Equations

• Std.Tactic.RCases.RCasesPatt.alts₁Core [] = []
• Std.Tactic.RCases.RCasesPatt.alts₁Core [[Std.Tactic.RCases.RCasesPatt.alts ref ps]] = ps
• Std.Tactic.RCases.RCasesPatt.alts₁Core (p :: ps) = Std.Tactic.RCases.RCasesPatt.tuple₁ p :: Std.Tactic.RCases.RCasesPatt.alts₁Core ps

def Std.Tactic.RCases.RCasesPatt.alts₁ (ref : Lean.Syntax) : List (List Std.Tactic.RCases.RCasesPatt) → Std.Tactic.RCases.RCasesPatt

This function is used for producing rcases patterns based on a case tree. This is like alts₁Core, but it produces a cases pattern directly instead of a list of alternatives. We specially translate the empty alternation to ⟨⟩, and translate |(a | b) to ⟨a | b⟩ (because we don't have any syntax for unary alternation). Otherwise we can use the regular merging of alternations at the last argument so that a | b | (c | d) becomes a | b | c | d.

Equations

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

instance Std.Tactic.RCases.RCasesPatt.instToMessageDataRCasesPatt : Lean.ToMessageData Std.Tactic.RCases.RCasesPatt

Equations

• Std.Tactic.RCases.RCasesPatt.instToMessageDataRCasesPatt = { toMessageData := Std.Tactic.RCases.RCasesPatt.instToMessageDataRCasesPatt.fmt 0 }

def Std.Tactic.RCases.RCasesPatt.instToMessageDataRCasesPatt.parenAbove (tgt : Nat) (p : Nat) (m : Lean.MessageData) : Lean.MessageData

parenthesize the message if the precedence is above tgt

Equations

• Std.Tactic.RCases.RCasesPatt.instToMessageDataRCasesPatt.parenAbove tgt p m = if tgt < p then Lean.MessageData.paren m else m

partial def Std.Tactic.RCases.RCasesPatt.instToMessageDataRCasesPatt.fmt : Nat → Std.Tactic.RCases.RCasesPatt → Lean.MessageData

format an RCasesPatt with the given precedence: 0 = lo, 1 = med, 2 = hi

def Std.Tactic.RCases.processConstructor (ref : Lean.Syntax) (info : Array Lean.Meta.ParamInfo) (explicit : Bool) (idx : Nat) (ps : List Std.Tactic.RCases.RCasesPatt) : List Lean.Name × List Std.Tactic.RCases.RCasesPatt

Takes the number of fields of a single constructor and patterns to match its fields against (not necessarily the same number). The returned lists each contain one element per field of the constructor. The name is the name which will be used in the top-level cases tactic, and the rcases_patt is the pattern which the field will be matched against by subsequent cases tactics.

Equations

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

def Std.Tactic.RCases.processConstructors (ref : Lean.Syntax) (params : Nat) (altVarNames : optParam (Array Lean.Meta.AltVarNames) #[]) : List Lean.Name → List Std.Tactic.RCases.RCasesPatt → Lean.MetaM (Array Lean.Meta.AltVarNames × List (Lean.Name × List Std.Tactic.RCases.RCasesPatt))

Takes a list of constructor names, and an (alternation) list of patterns, and matches each pattern against its constructor. It returns the list of names that will be passed to cases, and the list of (constructor name, patterns) for each constructor, where patterns is the (conjunctive) list of patterns to apply to each constructor argument.

Equations

• One or more equations did not get rendered due to their size.
• Std.Tactic.RCases.processConstructors ref params altVarNames [] x = pure (altVarNames, [])

def Std.Tactic.RCases.subst' (goal : Lean.MVarId) (hFVarId : Lean.FVarId) (fvarSubst : optParam Lean.Meta.FVarSubst { map := ∅ }) : Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId)

Like Lean.Meta.subst, but preserves the FVarSubst.

Equations

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

partial def Std.Tactic.RCases.rcasesCore {α : Type} (g : Lean.MVarId) (fs : Lean.Meta.FVarSubst) (clears : Array Lean.FVarId) (e : Lean.Expr) (a : α) (pat : Std.Tactic.RCases.RCasesPatt) (cont : Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → α → Lean.Elab.TermElabM α) : Lean.Elab.TermElabM α

This will match a pattern pat against a local hypothesis e.

• g: The initial subgoal
• fs: A running variable substitution, the result of cases operations upstream. The variable e must be run through this map before locating it in the context of g, and the output variable substitutions will be end extensions of this one.
• clears: The list of variables to clear in all subgoals generated from this point on. We defer clear operations because clearing too early can cause cases to fail. The actual clearing happens in RCases.finish.
• e: a local hypothesis, the scrutinee to match against.
• a: opaque "user data" which is passed through all the goal calls at the end.
• pat: the pattern to match against
• cont: A continuation. This is called on every goal generated by the result of the pattern match, with updated values for g , fs, clears, and a.

partial def Std.Tactic.RCases.rcasesCore.align {α : Type} (fs : Lean.Meta.FVarSubst) (clears : Array Lean.FVarId) (cont : Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → α → Lean.Elab.TermElabM α) (a : α) (goal : Lean.Meta.InductionSubgoal) (ctorName : Lean.Name) : List (Lean.Name × List Std.Tactic.RCases.RCasesPatt) → Lean.Elab.TermElabM (List (Lean.Name × List Std.Tactic.RCases.RCasesPatt) × α)

Runs rcasesContinue on the first pattern in r with a matching ctorName. The unprocessed patterns (subsequent to the matching pattern) are returned.

partial def Std.Tactic.RCases.rcasesContinue {α : Type} (g : Lean.MVarId) (fs : Lean.Meta.FVarSubst) (clears : Array Lean.FVarId) (a : α) (pats : List (Std.Tactic.RCases.RCasesPatt × Lean.Expr)) (cont : Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → α → Lean.Elab.TermElabM α) : Lean.Elab.TermElabM α

This will match a list of patterns against a list of hypotheses e. The arguments are similar to rcasesCore, but the patterns and local variables are in pats. Because the calls are all nested in continuations, later arguments can be matched many times, once per goal produced by earlier arguments. For example ⟨a | b, ⟨c, d⟩⟩ performs the ⟨c, d⟩ match twice, once on the a branch and once on b.

def Std.Tactic.RCases.tryClearMany' (goal : Lean.MVarId) (fvarIds : Array Lean.FVarId) : Lean.MetaM Lean.MVarId

Like tryClearMany, but also clears dependent hypotheses if possible

Equations

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

def Std.Tactic.RCases.finish (g : Lean.MVarId) (fs : Lean.Meta.FVarSubst) (clears : Array Lean.FVarId) (gs : Array Lean.MVarId) : Lean.Elab.TermElabM (Array Lean.MVarId)

The terminating continuation used in rcasesCore and rcasesContinue. We specialize the type α to Array MVarId to collect the list of goals, and given the list of clears, it attempts to clear them from the goal and adds the goal to the list.

Equations

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

partial def Std.Tactic.RCases.RCasesPatt.parse (stx : Lean.Syntax) : Lean.MetaM Std.Tactic.RCases.RCasesPatt

Parses a Syntax into the RCasesPatt type used by the RCases tactic.

def Std.Tactic.RCases.generalizeExceptFVar (goal : Lean.MVarId) (args : Array Lean.Meta.GeneralizeArg) : Lean.MetaM (Array Lean.Expr × Lean.MVarId)

Generalize all the arguments as specified in args to fvars if they aren't already

Equations

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

def Std.Tactic.RCases.rcases (tgts : Array (Option Lean.Name × Lean.Syntax)) (pat : Std.Tactic.RCases.RCasesPatt) (g : Lean.MVarId) : Lean.Elab.TermElabM (List Lean.MVarId)

Given a list of targets of the form e or h : e, and a pattern, match all the targets against the pattern. Returns the list of produced subgoals.

Equations

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

def Std.Tactic.RCases.obtainNone (pat : Std.Tactic.RCases.RCasesPatt) (ty : Lean.Syntax) (g : Lean.MVarId) : Lean.Elab.TermElabM (List Lean.MVarId)

The obtain tactic in the no-target case. Given a type T, create a goal |- T and and pattern match T against the given pattern. Returns the list of goals, with the assumed goal first followed by the goals produced by the pattern match.

Equations

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

partial def Std.Tactic.RCases.expandRIntroPat (pat : Lean.TSyntax `rintroPat) (acc : optParam (Array (Lean.TSyntax `rcasesPat)) #[]) (ty? : optParam (Option Lean.Term) none) : Array (Lean.TSyntax `rcasesPat)

Expand a rintroPat into an equivalent list of rcasesPat patterns.

partial def Std.Tactic.RCases.expandRIntroPats (pats : Array (Lean.TSyntax `rintroPat)) (acc : optParam (Array (Lean.TSyntax `rcasesPat)) #[]) (ty? : optParam (Option Lean.Term) none) : Array (Lean.TSyntax `rcasesPat)

Expand a list of rintroPat into an equivalent list of rcasesPat patterns.

partial def Std.Tactic.RCases.rintroCore {α : Type} (g : Lean.MVarId) (fs : Lean.Meta.FVarSubst) (clears : Array Lean.FVarId) (a : α) (ref : Lean.Syntax) (pat : Lean.TSyntax `rintroPat) (ty? : Option Lean.Term) (cont : Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → α → Lean.Elab.TermElabM α) : Lean.Elab.TermElabM α

This introduces the pattern pat. It has the same arguments as rcasesCore, plus:

• ty?: the nearest enclosing type ascription on the current pattern

partial def Std.Tactic.RCases.rintroContinue {α : Type} (g : Lean.MVarId) (fs : Lean.Meta.FVarSubst) (clears : Array Lean.FVarId) (ref : Lean.Syntax) (pats : Lean.TSyntaxArray `rintroPat) (ty? : Option Lean.Term) (a : α) (cont : Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → α → Lean.Elab.TermElabM α) : Lean.Elab.TermElabM α

This introduces the list of patterns pats. It has the same arguments as rcasesCore, plus:

• ty?: the nearest enclosing type ascription on the current pattern

partial def Std.Tactic.RCases.rintroContinue.loop {α : Type} (ref : Lean.Syntax) (pats : Lean.TSyntaxArray `rintroPat) (ty? : Option Lean.Term) (cont : Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → α → Lean.Elab.TermElabM α) (i : Nat) (g : Lean.MVarId) (fs : Lean.Meta.FVarSubst) (clears : Array Lean.FVarId) (a : α) : Lean.Elab.TermElabM α

Runs rintroContinue on pats[i:]

def Std.Tactic.RCases.rintro (pats : Lean.TSyntaxArray `rintroPat) (ty? : Option Lean.Term) (g : Lean.MVarId) : Lean.Elab.TermElabM (List Lean.MVarId)

The implementation of the rintro tactic. It takes a list of patterns pats and an optional type ascription ty? and introduces the patterns, resulting in zero or more goals.

Equations

• Std.Tactic.RCases.rintro pats ty? g = (fun x => Array.toList x) <$> Std.Tactic.RCases.rintroContinue g { map := ∅ } #[] Lean.Syntax.missing pats ty? #[] Std.Tactic.RCases.finish

def Std.Tactic.rcases : Lean.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 alteration 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 Std.Tactic.obtain : Lean.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 Std.Tactic.rintro : Lean.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.