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

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 searches for the first hypothesis h : type where type matches the term p, and splits the main goal by cases on h. Use holes in p to indicate arbitrary subexpressions, for example casesm _ ∧ _ will match any conjunction. casesm p fails if no hypothesis type matches p.

• casesm p_1, ..., p_n searches for a hypothesis h : type where type matches one or more of the given patterns p_1, ... p_n, and splits the main goal by cases on h.
• casesm* p repeatedly performs case splits until no more hypothesis type matches p. This is a more efficient and compact version of · repeat casesm p. It is more efficient because the pattern is compiled once.
• casesm! p and casesm!* p skip a hypothesis if the main goal would be replaced with two or more subgoals.

Example:

example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
  -- The following tactic destructs all conjunctions and disjunctions in the current context.
  casesm* _∨_, _∧_
  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
  · clear ‹c› ‹d› ‹e› ‹f›; trivial

def Mathlib.Tactic.casesm! : Lean.ParserDescr

casesm p searches for the first hypothesis h : type where type matches the term p, and splits the main goal by cases on h. Use holes in p to indicate arbitrary subexpressions, for example casesm _ ∧ _ will match any conjunction. casesm p fails if no hypothesis type matches p.

• casesm p_1, ..., p_n searches for a hypothesis h : type where type matches one or more of the given patterns p_1, ... p_n, and splits the main goal by cases on h.
• casesm* p repeatedly performs case splits until no more hypothesis type matches p. This is a more efficient and compact version of · repeat casesm p. It is more efficient because the pattern is compiled once.
• casesm! p and casesm!* p skip a hypothesis if the main goal would be replaced with two or more subgoals.

Example:

example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
  -- The following tactic destructs all conjunctions and disjunctions in the current context.
  casesm* _∨_, _∧_
  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
  · clear ‹c› ‹d› ‹e› ‹f›; trivial

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 searches for a hypothesis h : type where I has the form (I ...), and splits the main goal by cases on h. cases_type p fails if no hypothesis type has the identifier I as its head symbol.

• cases_type I_1 ... I_n searches for a hypothesis h : type where type has one or more of I_1, ..., I_n as its head symbol, and splits the main goal by cases on h.
• cases_type* I repeatedly performs case splits until no more hypothesis type has I as its head symbol. This shorthand for · repeat cases_type I.
• cases_type! p and cases_type!* p skip a hypothesis if the main goal would be replaced with two or more subgoals.

Example:

example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
  -- The following tactic destructs all conjunctions and disjunctions in the current context.
  cases_type* Or And
  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
  · clear ‹c› ‹d› ‹e› ‹f›; trivial

def Mathlib.Tactic.casesType! : Lean.ParserDescr

cases_type I searches for a hypothesis h : type where I has the form (I ...), and splits the main goal by cases on h. cases_type p fails if no hypothesis type has the identifier I as its head symbol.

• cases_type I_1 ... I_n searches for a hypothesis h : type where type has one or more of I_1, ..., I_n as its head symbol, and splits the main goal by cases on h.
• cases_type* I repeatedly performs case splits until no more hypothesis type has I as its head symbol. This shorthand for · repeat cases_type I.
• cases_type! p and cases_type!* p skip a hypothesis if the main goal would be replaced with two or more subgoals.

Example:

example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
  -- The following tactic destructs all conjunctions and disjunctions in the current context.
  cases_type* Or And
  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
  · clear ‹c› ‹d› ‹e› ‹f›; trivial

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

def Mathlib.Tactic.constructorM : Lean.ParserDescr

constructorm p_1, ..., p_n, where the main goal has type type, applies the first matching constructor for type, if type matches one of the given patterns. If type does not match any of the patterns, constructorm fails.

• constructorm* p_1, ..., p_n repeatedly applies a constructor until the goal no longer matches p_1, ..., p_n. This is a more efficient and compact version of · repeat constructorm p_1, ..., p_n. It is more efficient because the pattern is compiled once.

Examples:

example : True ∧ (True ∨ True) := by
  constructorm* _ ∨ _, _ ∧ _, True