Documentation

Mathlib.Tactic.CasesM

casesm, cases_type, constructorm tactics #

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

source
def Lean.MVarId.casesMatching (matcher : Lean.Expr → Lean.MetaM Bool) (recursive : optParam Bool false) (allowSplit : optParam Bool true) (throwOnNoMatch : optParam Bool true) (g : Lean.MVarId) :
Lean.MetaM (List Lean.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
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.MVarId.casesMatching.go (matcher : Lean.Expr → Lean.MetaM Bool) (recursive : optParam Bool false) (allowSplit : optParam Bool true) (g : Lean.MVarId) (acc : optParam (Array Lean.MVarId) #[]) :
Lean.MetaM (Array Lean.MVarId)

Auxiliary for casesMatching. Accumulates generated subgoals in acc.

source
def Lean.MVarId.casesType (heads : Array Lean.Name) (recursive : optParam Bool false) (allowSplit : optParam Bool true) :
Lean.MVarId → Lean.MetaM (List Lean.MVarId)
Equations
  • One or more equations did not get rendered due to their size.
source
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.

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

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

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.
source
def Mathlib.Tactic.elabCasesType (heads : Array Lean.Ident) (recursive : optParam Bool false) (allowSplit : optParam Bool true) :
Lean.Elab.Tactic.TacticM Unit

Common implementation of cases_type and cases_type!.

Equations
  • One or more equations did not get rendered due to their size.
source
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
Equations
  • One or more equations did not get rendered due to their size.
source
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
Equations
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.constructorMatching (g : Lean.MVarId) (matcher : Lean.Expr → Lean.MetaM Bool) (recursive : optParam Bool false) (throwOnNoMatch : optParam 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
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Mathlib.Tactic.constructorMatching.go (matcher : Lean.Expr → Lean.MetaM Bool) (g : Lean.MVarId) (acc : optParam (Array Lean.MVarId) #[]) :
Lean.MetaM (Array Lean.MVarId)

Auxiliary for constructorMatching. Accumulates generated subgoals in acc.

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