1.8. Induction / case distinction

induction

Assuming x is a variable in the local context with an inductive type, induction x applies induction on x to the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor and an inductive hypothesis is added for each recursive argument to the constructor. If the type of an element in the local context depends on x, that element is reverted and reintroduced afterward, so that the inductive hypothesis incorporates that hypothesis as well.

For example, given n : Nat and a goal with a hypothesis h : P n and target Q n, induction n produces one goal with hypothesis h : P 0 and target Q 0, and one goal with hypotheses h : P (Nat.succ a) and ih₁ : P a → Q a and target Q (Nat.succ a). Here the names a and ih₁ are chosen automatically and are not accessible. You can use with to provide the variables names for each constructor.

• induction e, where e is an expression instead of a variable, generalizes e in the goal, and then performs induction on the resulting variable.

• induction e using r allows the user to specify the principle of induction that should be used. Here r should be a term whose result type must be of the form C t, where C is a bound variable and t is a (possibly empty) sequence of bound variables

• induction e generalizing z₁ ... zₙ, where z₁ ... zₙ are variables in the local context, generalizes over z₁ ... zₙ before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized.

• Given x : Nat, induction x with | zero => tac₁ | succ x' ih => tac₂ uses tactic tac₁ for the zero case, and tac₂ for the succ case.

cases

Assuming x is a variable in the local context with an inductive type, cases x splits the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor. If the type of an element in the local context depends on x, that element is reverted and reintroduced afterward, so that the case split affects that hypothesis as well. cases detects unreachable cases and closes them automatically.

For example, given n : Nat and a goal with a hypothesis h : P n and target Q n, cases n produces one goal with hypothesis h : P 0 and target Q 0, and one goal with hypothesis h : P (Nat.succ a) and target Q (Nat.succ a). Here the name a is chosen automatically and is not accessible. You can use with to provide the variables names for each constructor.

• cases e, where e is an expression instead of a variable, generalizes e in the goal, and then cases on the resulting variable.

• Given as : List α, cases as with | nil => tac₁ | cons a as' => tac₂, uses tactic tac₁ for the nil case, and tac₂ for the cons case, and a and as' are used as names for the new variables introduced.

• cases h : e, where e is a variable or an expression, performs cases on e as above, but also adds a hypothesis h : e = ... to each hypothesis, where ... is the constructor instance for that particular case.

rcases

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.

by_cases

by_cases (h :)? p splits the main goal into two cases, assuming h : p in the first branch, and h : ¬ p in the second branch.

fin_cases

fin_cases h performs case analysis on a hypothesis of the form h : A, where [Fintype A] is available, or h : a ∈ A, where A : Finset X, A : Multiset X or A : List X.

As an example, in

example (f : ℕ → Prop) (p : Fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val := byf:ℕ → Propp:Fin 3h0:f 0h1:f 1h2:f 2⊢ f ↑p fin_cases p«0»f:ℕ → Proph0:f 0h1:f 1h2:f 2⊢ f ↑((fun i => i) ⟨0, ⋯⟩)«1»f:ℕ → Proph0:f 0h1:f 1h2:f 2⊢ f ↑((fun i => i) ⟨1, ⋯⟩)«2»f:ℕ → Proph0:f 0h1:f 1h2:f 2⊢ f ↑((fun i => i) ⟨2, ⋯⟩); simp«0»f:ℕ → Proph0:f 0h1:f 1h2:f 2⊢ f 0«1»f:ℕ → Proph0:f 0h1:f 1h2:f 2⊢ f ↑((fun i => i) ⟨1, ⋯⟩)«2»f:ℕ → Proph0:f 0h1:f 1h2:f 2⊢ f ↑((fun i => i) ⟨2, ⋯⟩) all_goals assumptionAll goals completed! 🐙

after fin_cases p; simp, there are three goals, f 0, f 1, and f 2.

interval_cases

interval_cases n searches for upper and lower bounds on a variable n, and if bounds are found, splits into separate cases for each possible value of n.

As an example, in

example (n : ℕ) (w₁ : n ≥ 3) (w₂ : n < 5) : n = 3 ∨ n = 4 := byn:ℕw₁:n ≥ 3w₂:n < 5⊢ n = 3 ∨ n = 4 interval_cases n«3»n:ℕw₁:3 ≥ 3w₂:3 < 5⊢ 3 = 3 ∨ 3 = 4«4»n:ℕw₁:4 ≥ 3w₂:4 < 5⊢ 4 = 3 ∨ 4 = 4 all_goals simpAll goals completed! 🐙

after interval_cases n, the goals are 3 = 3 ∨ 3 = 4 and 4 = 3 ∨ 4 = 4.

You can also explicitly specify a lower and upper bound to use, as interval_cases using hl, hu. The hypotheses should be in the form hl : a ≤ n and hu : n < b, in which case interval_cases calls fin_cases on the resulting fact n ∈ Set.Ico a b.

You can specify a name h for the new hypothesis, as interval_cases h : n or interval_cases h : n using hl, hu.

split

The split tactic is useful for breaking nested if-then-else and match expressions into separate cases. For a match expression with n cases, the split tactic generates at most n subgoals.

For example, given n : Nat, and a target if n = 0 then Q else R, split will generate one goal with hypothesis n = 0 and target Q, and a second goal with hypothesis ¬n = 0 and target R. Note that the introduced hypothesis is unnamed, and is commonly renamed used the case or next tactics.

• split will split the goal (target).

• split at h will split the hypothesis h.

split_ifs

Splits all if-then-else-expressions into multiple goals. Given a goal of the form g (if p then x else y), split_ifs will produce two goals: p ⊢ g x and ¬p ⊢ g y. If there are multiple ite-expressions, then split_ifs will split them all, starting with a top-most one whose condition does not contain another ite-expression. split_ifs at * splits all ite-expressions in all hypotheses as well as the goal. split_ifs with h₁ h₂ h₃ overrides the default names for the hypotheses.