- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
Performs a depth-first search which, at each step, applies a provided helper tactic t then checks all instance declarations that match the current goal. Unlike Lean’s type-class inference, this procedure supports instance declarations that require assumptions that cannot be resolved by type-class instances, handling them with the helper tactic instead. The syntax is infer_instance_trying <:> t.
open Nat
class IsDouble (n : ℕ) where
m : ℕ
h : n = 2 * m
instance (h : n % 2 = 0) : IsDouble n :=
⟨n / 2, (Nat.mul_div_cancel' (dvd_of_mod_eq_zero h)).symm⟩
example : IsDouble 4 := by infer_instance_trying <:> decide
Resolves goals of the form \(\mathtt{nthCoefficient}_n(p) = c\) for univariate polynomials \(p\), natural numbers \(n\), and members of the relevant semiring \(c\). Note that we admit that the semiring is commutative.
section Coeffs
variable [CommSemiring R]
example : (0 : R[X]).coeff 1 = 0 := by poly_rfl_coeff VIA CoeffsList
example : (1 : R[X]).coeff 1 = 0 := by poly_rfl_coeff VIA CoeffsList; trivial
example : (X : R[X]).coeff 1 = 1 := by poly_rfl_coeff VIA CoeffsList; trivial
example : (X ^ 2 : R[X]).coeff 1 = 0 := by poly_rfl_coeff VIA CoeffsList; trivial
example : (X + 1 : R[X]).coeff 1 = 1 := by poly_rfl_coeff VIA CoeffsList; simp
end Coeffs
Resolves goals of the form \(\mathtt{degree}(p) = n\) for univariate polynomials \(p\) and some \(n\) which is either a natural number or the bottom member \(\bot \). In any case where we want \(\mathtt{degree}(p) \neq \bot \), we must admit that the the semiring is nontrivial, as in section DegreeEqNontrivial.
section DegreeEq
variable [Semiring R]
example : (0 : R[X]).degree = ⊥ := by poly_rfl_degree_eq
end DegreeEq
section DegreeEqNontrivial
variable [Semiring R] [Nontrivial R]
example : (1 : R[X]).degree = 0 := by poly_rfl_degree_eq
example : (X : R[X]).degree = 1 := by poly_rfl_degree_eq
example : (X ^ 2 : R[X]).degree = 2 := by poly_rfl_degree_eq
example : (X + 1 : R[X]).degree = 1 := by poly_rfl_degree_eq_trying <:> poly_infer_try
end DegreeEqNontrivial
section DegreeEqOfCoeffs
example : (X + 1 : ℕ[X]).degree = 1 := by poly_rfl_degree_eq_of_coeffs VIA CoeffsList; simp; trivial
end DegreeEqOfCoeffs
Resolves goals of the form \(\mathtt{degree}(p) \leq n\) for univariate polynomials \(p\) and some \(n\) which is either a natural number or the bottom member \(\bot \).
section DegreeLe
variable [Semiring R]
example : (0 : R[X]).degree ≤ ⊥ := by poly_rfl_degree_le; trivial
example : (1 : R[X]).degree ≤ 0 := by poly_rfl_degree_le; trivial
example : (X : R[X]).degree ≤ 1 := by poly_rfl_degree_le; trivial
example : (X ^ 2 : R[X]).degree ≤ 2 := by poly_rfl_degree_le; trivial
example : (X + 1 : R[X]).degree ≤ 1 := by poly_rfl_degree_le; trivial
end DegreeLe
Resolves goals of the form \(p(c) = c'\) for univariate polynomials \(p\) and members of the relevant semiring \(c\) and \(c'\). Note that we admit that the semiring is commutative.
section Eval
variable [CommSemiring R]
example : (0 : R[X]).eval 1 = 0 := by poly_rfl_eval VIA EvalArrow
example : (1 : R[X]).eval 1 = 1 := by poly_rfl_eval VIA EvalArrow
example : (X : R[X]).eval 1 = 1 := by poly_rfl_eval VIA EvalArrow
example : (X ^ 2 : R[X]).eval 1 = 1 := by poly_rfl_eval VIA EvalArrow; simp
example : (X + 1 : R[X]).eval 1 = 2 := by poly_rfl_eval VIA EvalArrow; norm_num
end Eval
Resolves goals of the form \(p = q\) for a univariate polynomial \(p\) and an equivalent polynomial \(q\) in expanded form. Note that we admit that the semiring is commutative.
section Expand
variable [CommSemiring R]
example : (C 2 + X : R[X]) = X + C 2 := by poly_rfl_expand VIA CoeffsList; simp; poly_unfold_expand; simp
example : (X * C 2 : R[X]) = C 2 * X := by poly_rfl_expand VIA CoeffsList; simp; poly_unfold_expand; simp
example : (X + X : R[X]) = C 2 * X := by poly_rfl_expand VIA CoeffsList; simp; poly_unfold_expand; norm_num
end Expand
Resolves goals of the form \(\mathtt{leadingCoefficient}(p) = c\) for univariate polynomials \(p\) and members of the relevant semiring \(c\). When the definition of \(p\) contains recursive cases such as +, *, or ^ (disregarding X ^ n which is handled separately), we must admit that the semiring is nontrivial, as in section LeadingCoeffNontrivial.
section LeadingCoeff
variable [Semiring R]
example : (0 : R[X]).leadingCoeff = 0 := by poly_rfl_leading_coeff
example : (1 : R[X]).leadingCoeff = 1 := by poly_rfl_leading_coeff
example : (X : R[X]).leadingCoeff = 1 := by poly_rfl_leading_coeff
example : (X ^ 2 : R[X]).leadingCoeff = 1 := by poly_rfl_leading_coeff
end LeadingCoeff
section LeadingCoeffNontrivial
variable [Semiring R] [Nontrivial R]
example : (X + 1 : R[X]).leadingCoeff = 1 := by poly_rfl_leading_coeff_trying <:> poly_infer_try
end LeadingCoeffNontrivial
section LeadingCoeffEqOfCoeffs
example : (X + 1 : ℕ[X]).leadingCoeff = 1 := by poly_rfl_leading_coeff_of_coeffs VIA CoeffsList; simp
end LeadingCoeffEqOfCoeffs