casesm, cases_type, constructorm tactics

These tactics implement repeated cases / constructor on anything satisfying a predicate.

def Lean.MVarId.casesMatching (matcher : Expr → MetaM Bool) (recursive : Bool := false) (allowSplit throwOnNoMatch : Bool := true) (g : MVarId) : MetaM (List MVarId)

Core tactic for casesm and cases_type. Calls cases on all fvars in g for which matcher ldecl.type returns true.

• recursive: if true, it calls itself repeatedly on the resulting subgoals
• allowSplit: if false, it will skip any hypotheses where cases returns more than one subgoal.
• throwOnNoMatch: if true, then throws an error if no match is found

partial def Lean.MVarId.casesMatching.go (matcher : Expr → MetaM Bool) (recursive : Bool := false) (allowSplit : Bool := true) (g : MVarId) (acc : Array MVarId := #[]) : MetaM (Array MVarId)

Auxiliary for casesMatching. Accumulates generated subgoals in acc.

def Lean.MVarId.casesType (heads : Array Name) (recursive : Bool := false) (allowSplit : Bool := true) : MVarId → MetaM (List MVarId)

def Mathlib.Tactic.elabPatterns (pats : Array Lean.Term) : Lean.Elab.TermElabM (Array Lean.Meta.AbstractMVarsResult)

Elaborate a list of terms with holes into a list of patterns.

def Mathlib.Tactic.matchPatterns (pats : Array Lean.Meta.AbstractMVarsResult) (e : Lean.Expr) : Lean.MetaM Bool

Returns true if any of the patterns match the expression.

def Mathlib.Tactic.elabCasesM (pats : Array Lean.Term) (recursive allowSplit : Bool) : Lean.Elab.Tactic.TacticM Unit

Common implementation of casesm and casesm!.

def Mathlib.Tactic.casesM : Lean.ParserDescr

• casesm p applies the cases tactic to a hypothesis h : type if type matches the pattern p.
• casesm p_1, ..., p_n applies the cases tactic to a hypothesis h : type if type matches one of the given patterns.
• casesm* p is a more efficient and compact version of · repeat casesm p. It is more efficient because the pattern is compiled once.
• casesm! p only applies cases if the number of resulting subgoals is <= 1.

Example: The following tactic destructs all conjunctions and disjunctions in the current context.

casesm* _ ∨ _, _ ∧ _

def Mathlib.Tactic.casesm! : Lean.ParserDescr

• casesm p applies the cases tactic to a hypothesis h : type if type matches the pattern p.
• casesm p_1, ..., p_n applies the cases tactic to a hypothesis h : type if type matches one of the given patterns.
• casesm* p is a more efficient and compact version of · repeat casesm p. It is more efficient because the pattern is compiled once.
• casesm! p only applies cases if the number of resulting subgoals is <= 1.

Example: The following tactic destructs all conjunctions and disjunctions in the current context.

casesm* _ ∨ _, _ ∧ _

def Mathlib.Tactic.elabCasesType (heads : Array Lean.Ident) (recursive : Bool := false) (allowSplit : Bool := true) : Lean.Elab.Tactic.TacticM Unit

Common implementation of cases_type and cases_type!.

def Mathlib.Tactic.casesType : Lean.ParserDescr

• cases_type I applies the cases tactic to a hypothesis h : (I ...)
• cases_type I_1 ... I_n applies the cases tactic to a hypothesis h : (I_1 ...) or ... or h : (I_n ...)
• cases_type* I is shorthand for · repeat cases_type I
• cases_type! I only applies cases if the number of resulting subgoals is <= 1.

Example: The following tactic destructs all conjunctions and disjunctions in the current goal.

cases_type* Or And

def Mathlib.Tactic.casesType! : Lean.ParserDescr

• cases_type I applies the cases tactic to a hypothesis h : (I ...)
• cases_type I_1 ... I_n applies the cases tactic to a hypothesis h : (I_1 ...) or ... or h : (I_n ...)
• cases_type* I is shorthand for · repeat cases_type I
• cases_type! I only applies cases if the number of resulting subgoals is <= 1.

Example: The following tactic destructs all conjunctions and disjunctions in the current goal.

cases_type* Or And

def Mathlib.Tactic.constructorMatching (g : Lean.MVarId) (matcher : Lean.Expr → Lean.MetaM Bool) (recursive : Bool := false) (throwOnNoMatch : Bool := true) : Lean.MetaM (List Lean.MVarId)

Core tactic for constructorm. Calls constructor on all subgoals for which matcher ldecl.type returns true.

• recursive: if true, it calls itself repeatedly on the resulting subgoals
• throwOnNoMatch: if true, throws an error if no match is found

partial def Mathlib.Tactic.constructorMatching.go (matcher : Lean.Expr → Lean.MetaM Bool) (g : Lean.MVarId) (acc : Array Lean.MVarId := #[]) : Lean.MetaM (Array Lean.MVarId)

Auxiliary for constructorMatching. Accumulates generated subgoals in acc.

def Mathlib.Tactic.constructorM : Lean.ParserDescr

• constructorm p_1, ..., p_n applies the constructor tactic to the main goal if type matches one of the given patterns.
• constructorm* p is a more efficient and compact version of · repeat constructorm p. It is more efficient because the pattern is compiled once.

Example: The following tactic proves any theorem like True ∧ (True ∨ True) consisting of and/or/true:

constructorm* _ ∨ _, _ ∧ _, True