Documentation

Mathlib.Tactic.CasesM

casesm, cases_type, constructorm tactics #

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

def Mathlib.Tactic.casesMatching (g : Lean.MVarId) (matcher : Lean.ExprLean.MetaM Bool) (recursive : optParam Bool false) (allowSplit : optParam Bool true) (throwOnNoMatch : optParam Bool !recursive) :

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
Equations
  • One or more equations did not get rendered due to their size.

Auxiliary for casesMatching. Accumulates generated subgoals in acc.

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

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

Returns true if any of the patterns match the expression.

Equations
  • One or more equations did not get rendered due to their size.
  • 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.

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

casesm* _ ∨ _, _ ∧ _
Equations
  • One or more equations did not get rendered due to their size.

Common implementation of cases_type and cases_type!.

Equations
  • One or more equations did not get rendered due to their size.
  • 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
Equations
  • One or more equations did not get rendered due to their size.
  • 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
Equations
  • One or more equations did not get rendered due to their size.
def Mathlib.Tactic.constructorMatching (g : Lean.MVarId) (matcher : Lean.ExprLean.MetaM Bool) (recursive : optParam Bool false) (throwOnNoMatch : optParam Bool !recursive) :

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
Equations
  • One or more equations did not get rendered due to their size.

Auxiliary for constructorMatching. Accumulates generated subgoals in acc.

  • 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
Equations
  • One or more equations did not get rendered due to their size.