Documentation

Mathlib.Tactic.FinCases

The fin_cases tactic. #

Given a hypothesis of the form h : x ∈ (A : List α), x ∈ (A : Finset α), or 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.

source
def Lean.Elab.Tactic.getMemType {m : Type → Type} [Monad m] [Lean.MonadError m] (e : Lean.Expr) :
m (Option Lean.Expr)

If e is of the form x ∈ (A : List α), x ∈ (A : Finset α), or x ∈ (A : Multiset α), return some α, otherwise none.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    partial def Lean.Elab.Tactic.unfoldCases (g : Lean.MVarId) (h : Lean.FVarId) :
    Lean.MetaM (List Lean.MVarId)

    Recursively runs the cases tactic on a hypothesis h. 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.

    source
    partial def Lean.Elab.Tactic.finCasesAt (g : Lean.MVarId) (hyp : Lean.FVarId) :
    Lean.MetaM (List Lean.MVarId)

    Implementation of the fin_cases tactic.

    source
    def Lean.Elab.Tactic.finCases :
    Lean.ParserDescr

    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 := by
  fin_cases p; simp
  all_goals assumption

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

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

      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 h. These should be definitionally equal to and in the same order as the default enumeration of the cases.

      For example,

      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.

      When using fin_cases a on data a defined with let, the tactic will not be able to clear the variable a, and will instead produce hypotheses this : a = .... These hypotheses can be given a name using fin_cases a using ha.

      For example,

      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.