fin_cases tactic. #
Given a hypothesis of the form
h : x ∈ (A : List α),
x ∈ (A : Finset α),
x ∈ (A : Multiset α),
or a hypothesis of the form
h : A, where
[Fintype A] is available,
fin_cases h will repeatedly call
cases to split the goal into
separate cases for each possible value.
Recursively runs the
cases tactic on a hypothesis
As long as two goals are produced,
cases is called recursively on the second goal,
and we return a list of the first goals which appeared.
This is useful for hypotheses of the form
h : a ∈ [l₁, l₂, ...],
which will be transformed into a sequence of goals with hypotheses
h : a = l₁,
h : a = l₂,
and so on.
As an example, in
example (f : ℕ → Prop) (p : Fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val := by fin_cases p; simp all_goals assumption
fin_cases p; simp, there are three goals,
f 1, and
fin_cases used to also have two modifiers,
fin_cases ... with ... and
fin_cases ... using ....
With neither actually used in mathlib, they haven't been re-implemented here.
In case someone finds a need for them, and wants to re-implement, the relevant sections of the doc-string are preserved here:
fin_cases h with l takes a list of descriptions for the cases of
These should be definitionally equal to and in the same order as the
default enumeration of the cases.
example (x y : ℕ) (h : x ∈ [1, 2]) : x = y := by fin_cases h with 1, 1+1
produces two cases:
1 = y and
1 + 1 = y.
fin_cases a on data
a defined with
the tactic will not be able to clear the variable
and will instead produce hypotheses
this : a = ....
These hypotheses can be given a name using
fin_cases a using ha.
example (f : ℕ → Fin 3) : True := by let a := f 3 fin_cases a using ha
produces three goals with hypotheses
ha : a = 0,
ha : a = 1, and
ha : a = 2.