Reflection Tactics for Polynomials

def tacticPoly_rfl_rw : Lean.ParserDescr

Rewrites polynomials into forms with type-class instances in our reflection systems. This is typically rewriting polynomials that are synonyms for constants as those constants. Performing this step before the instance inference reduces the necessary breadth of the type-class instances.

Equations

• tacticPoly_rfl_rw = Lean.ParserDescr.node `tacticPoly_rfl_rw 1024 (Lean.ParserDescr.nonReservedSymbol "poly_rfl_rw" false)

def tacticPoly_rfl_dsimp : Lean.ParserDescr

Definitionally simplifies an expression in terms of values from inferred instances. This step is performed after instance inference transforms the goal in terms of instances. With a computable represenatation, the resulting goal should be autmatically verifiable with rfl, decide, simp, etc.

Equations

• tacticPoly_rfl_dsimp = Lean.ParserDescr.node `tacticPoly_rfl_dsimp 1024 (Lean.ParserDescr.nonReservedSymbol "poly_rfl_dsimp" false)

def «tacticPoly_rfl_with<:>_» : Lean.ParserDescr

Performs type-class reflection tactic t after rewriting the polynomial into a compatible form and before definitionally simplifying the resulting instanced values in the goal.

Equations

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

def tacticPoly_infer_try : Lean.ParserDescr

A standard tactic to resolve subgoals produced during infer_instance_trying

Equations

• tacticPoly_infer_try = Lean.ParserDescr.node `tacticPoly_infer_try 1024 (Lean.ParserDescr.nonReservedSymbol "poly_infer_try" false)

def tacticPoly_rfl_degree_le : Lean.ParserDescr

Automates goals of the form p.degree ≤ d

Equations

• tacticPoly_rfl_degree_le = Lean.ParserDescr.node `tacticPoly_rfl_degree_le 1024 (Lean.ParserDescr.nonReservedSymbol "poly_rfl_degree_le" false)

def tacticPoly_rfl_degree_eq : Lean.ParserDescr

Automates goals of the form p.degree = d

Equations

• tacticPoly_rfl_degree_eq = Lean.ParserDescr.node `tacticPoly_rfl_degree_eq 1024 (Lean.ParserDescr.nonReservedSymbol "poly_rfl_degree_eq" false)

def «tacticPoly_rfl_degree_eq_trying<:>_» : Lean.ParserDescr

Automates goals of the form p.degree = d using infer_instance_trying <:> t to handle more complex intermediate subgoals

Equations

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

def tacticPoly_rfl_degree_eq_of_coeffsVIA_ : Lean.ParserDescr

Automates goals of the form p.degree = d by constructing a coefficient represenatation t with a computable degree

Equations

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

def tacticPoly_rfl_leading_coeff : Lean.ParserDescr

Automates goals of the form p.leadingCoeff = c

Equations

• tacticPoly_rfl_leading_coeff = Lean.ParserDescr.node `tacticPoly_rfl_leading_coeff 1024 (Lean.ParserDescr.nonReservedSymbol "poly_rfl_leading_coeff" false)

def «tacticPoly_rfl_leading_coeff_trying<:>_» : Lean.ParserDescr

Automates goals of the form p.leadingCoeff = c using infer_instance_trying <:> t to handle more complex intermediate subgoals

Equations

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

def tacticPoly_rfl_leading_coeff_of_coeffsVIA_ : Lean.ParserDescr

Automates goals of the form p.leadingCoeff = c by constructing a coefficient represenatation t with a computable leading coefficient

Equations

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

def tacticPoly_rfl_coeffVIA_ : Lean.ParserDescr

Automates goals of the form p.coeff n = c using coefficient representation t

Equations

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

def tacticPoly_rfl_evalVIA_ : Lean.ParserDescr

Automates goals of the form p.eval x = y using evaluation representation t

Equations

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

def tacticPoly_rfl_expandVIA_ : Lean.ParserDescr

Automates goals of the form p = q by rewriting the p into a normal form determined by coefficient representation t

Equations

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