A list, with a disjunctive meaning (like a list of inductive constructors, or subgoals)

A list, with a conjunctive meaning (like a list of constructor arguments, or hypotheses)

A metavariable representing a subgoal, together with a list of local constants to clear.

Get the name from a pattern, if provided

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

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

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

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

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).

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⟩.

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).

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.

Formats an rcases pattern. If the bracket argument is true, then it will be printed at high precedence, i.e. it will have parentheses around it if it is not already a tuple or atomic name.

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.

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.

Given a list of uncleared_goals, each of which is a goal metavariable and a list of variables to clear, actually perform the clear and set the goals with the result.

rcases h e pat performs case distinction on e using pat to name the arising new variables and assumptions. If h is some name, a new assumption h : e = pat will relate the expression e with the current pattern. See the module comment for the syntax of pat.

rintro pat₁ pat₂ ... patₙ introduces n arguments, then pattern matches on the patᵢ using the same syntax as rcases.

Like zip_with, but if the lists don't match in length, the excess elements will be put at the end of the result.

Merge two rcases patterns. This is used to underapproximate a case tree by an rcases pattern. The two patterns come from cases in two branches, that due to the syntax of rcases patterns are forced to overlap. The rule here is that we take only the case splits that are in common between both branches. For example if one branch does ⟨a, b⟩ and the other does c, then we return c because we don't know that a case on c would be safe to do.

• rcases? e is like rcases e with ..., except it generates ... by matching on everything it can, and it outputs an rcases invocation that should have the same effect.
• rcases? e : n can be used to control the depth of case splits (especially important for recursive types like nat, which can be cased as many times as you like).

• rintro? is like rintro ..., except it generates ... by introducing and matching on everything it can, and it outputs an rintro invocation that should have the same effect.
• rintro? : n can be used to control the depth of case splits (especially important for recursive types like nat, which can be cased as many times as you like).

Parse the optional depth argument (: n)? of rcases? and rintro?, with default depth 5.

Syntax for a rcases pattern:

• rcases? expr (: n)?
• rcases (h :)? expr (with patt_list (: expr)?)?.

Syntax for a rintro pattern: ('?' (: n)?) | patt*.

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.
• 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.

rcases? e will perform case splits on e in the same way as rcases e, but rather than accepting a pattern, it does a maximal cases and prints the pattern that would produce this case splitting. The default maximum depth is 5, but this can be modified with rcases? e : n.

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? will introduce and case split on variables in the same way as rintro, but will also print the rintro invocation that would have the same result. Like rcases?, rintro? : n allows for modifying the depth of splitting; the default is 5.

rintros is an alias for rintro.

Alias for rintro.

Parses patt? (: expr)?. (This is almost the same as `

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

obtain ⟨patt⟩ : type,
{ ... }

is equivalent to

have h : type,
{ ... },
rcases h with ⟨patt⟩

The syntax obtain ⟨patt⟩ : type := proof is also supported.

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

If type is omitted, := proof is required.