mathlib docs: tactic.ring2

(reflect' t u α) quasiquotes a tree (t: tree expr) of quoted values of type α at level u into an expr which reifies to a tree α containing the reifications of the exprs from the original t.

source

def tree.get_or_zero {α : Type u_1} [has_zero α] :

tree α → pos_num → α

Returns an element indexed by n, or zero if n isn't a valid index. See tree.get.

Equations

t.get_or_zero n = tree.get_or_else n t 0

source

inductive tactic.ring2.csring_expr :

Type

atom : pos_num → tactic.ring2.csring_expr
const : num → tactic.ring2.csring_expr
add : tactic.ring2.csring_expr → tactic.ring2.csring_expr → tactic.ring2.csring_expr
mul : tactic.ring2.csring_expr → tactic.ring2.csring_expr → tactic.ring2.csring_expr
pow : tactic.ring2.csring_expr → num → tactic.ring2.csring_expr

A reflected/meta representation of an expression in a commutative semiring. This representation is a direct translation of such expressions - see horner_expr for a normal form.

source

@[instance]

meta def tactic.ring2.csring_expr.has_reflect :

has_reflect tactic.ring2.csring_expr

source

@[instance]

def tactic.ring2.csring_expr.inhabited :

inhabited tactic.ring2.csring_expr

Equations

tactic.ring2.csring_expr.inhabited = {default := tactic.ring2.csring_expr.const 0}

source

def tactic.ring2.csring_expr.eval {α : Type u_1} [comm_semiring α] :

tree α → tactic.ring2.csring_expr → α

Evaluates a reflected csring_expr into an element of the original comm_semiring type α, retrieving opaque elements (atoms) from the tree t.

Equations

source

@[instance]

def tactic.ring2.horner_expr.decidable_eq :

decidable_eq tactic.ring2.horner_expr

source

inductive tactic.ring2.horner_expr :

Type

const : znum → tactic.ring2.horner_expr
horner : tactic.ring2.horner_expr → pos_num → num → tactic.ring2.horner_expr → tactic.ring2.horner_expr

An efficient representation of expressions in a commutative semiring using the sparse Horner normal form. This type admits non-optimal instantiations (e.g. P can be represented as P+0+0), so to get good performance out of it, care must be taken to maintain an optimal, canonical form.

source

def tactic.ring2.horner_expr.is_cs :

tactic.ring2.horner_expr → Prop

True iff the horner_expr argument is a valid csring_expr. For that to be the case, all its constants must be non-negative.

Equations

(a.horner x n b).is_cs = (a.is_cs ∧ b.is_cs)
(tactic.ring2.horner_expr.const n).is_cs = ∃ (m : num), n = m.to_znum

source

@[instance]

def tactic.ring2.horner_expr.has_zero :

has_zero tactic.ring2.horner_expr

Equations

tactic.ring2.horner_expr.has_zero = {zero := tactic.ring2.horner_expr.const 0}

source

@[instance]

def tactic.ring2.horner_expr.has_one :

has_one tactic.ring2.horner_expr

Equations

tactic.ring2.horner_expr.has_one = {one := tactic.ring2.horner_expr.const 1}

source

@[instance]

def tactic.ring2.horner_expr.inhabited :

inhabited tactic.ring2.horner_expr

Equations

tactic.ring2.horner_expr.inhabited = {default := 0}

source

def tactic.ring2.horner_expr.atom :

pos_num → tactic.ring2.horner_expr

Represent a csring_expr.atom in Horner form.

Equations

tactic.ring2.horner_expr.atom n = 1.horner n 1 0

source

def tactic.ring2.horner_expr.to_string :

tactic.ring2.horner_expr → string

Equations

(a.horner x n b).to_string = "(" ++ a.to_string ++ ") * x" ++ repr x ++ "^" ++ repr n ++ " + " ++ b.to_string
(tactic.ring2.horner_expr.const n).to_string = repr n

source

@[instance]

def tactic.ring2.horner_expr.has_to_string :

has_to_string tactic.ring2.horner_expr

Equations

tactic.ring2.horner_expr.has_to_string = {to_string := tactic.ring2.horner_expr.to_string}

source

def tactic.ring2.horner_expr.horner' :

tactic.ring2.horner_expr → pos_num → num → tactic.ring2.horner_expr → tactic.ring2.horner_expr

Alternative constructor for (horner a x n b) which maintains canonical form by simplifying special cases of a.

Equations

a.horner' x n b = tactic.ring2.horner_expr.horner'._match_1 a x n b a
tactic.ring2.horner_expr.horner'._match_1 a x n b (a₁.horner x₁ n₁ b₁) = ite (x₁ = x ∧ b₁ = 0) (a₁.horner x (n₁ + n) b) (a.horner x n b)
tactic.ring2.horner_expr.horner'._match_1 a x n b (tactic.ring2.horner_expr.const q) = ite (q = 0) b (a.horner x n b)

source

def tactic.ring2.horner_expr.add_const :

znum → tactic.ring2.horner_expr → tactic.ring2.horner_expr

Equations

tactic.ring2.horner_expr.add_const k e = ite (k = 0) e (tactic.ring2.horner_expr.rec (λ (n : znum), tactic.ring2.horner_expr.const (k + n)) (λ (a : tactic.ring2.horner_expr) (x : pos_num) (n : num) (b A B : tactic.ring2.horner_expr), a.horner x n B) e)

source

def tactic.ring2.horner_expr.add_aux :

tactic.ring2.horner_expr → (tactic.ring2.horner_expr → tactic.ring2.horner_expr) → pos_num → tactic.ring2.horner_expr → num → tactic.ring2.horner_expr → (tactic.ring2.horner_expr → tactic.ring2.horner_expr) → tactic.ring2.horner_expr

Equations

a₁.add_aux A₁ x₁ (a₂.horner x₂ n₂ b₂) n₁ b₁ B₁ = let e₂ : tactic.ring2.horner_expr := a₂.horner x₂ n₂ b₂ in tactic.ring2.horner_expr.add_aux._match_1 a₁ A₁ x₁ a₂ x₂ n₂ b₂ n₁ B₁ e₂ (a₁.add_aux A₁ x₁ b₂ n₁ b₁ B₁) (λ (k : pos_num), a₁.add_aux A₁ x₁ a₂ ↑k 0 id) (x₁.cmp x₂)
a₁.add_aux A₁ x₁ (tactic.ring2.horner_expr.const n₂) n₁ b₁ B₁ = tactic.ring2.horner_expr.add_const n₂ (a₁.horner x₁ n₁ b₁)
tactic.ring2.horner_expr.add_aux._match_1 a₁ A₁ x₁ a₂ x₂ n₂ b₂ n₁ B₁ e₂ _f_1 _f_2 ordering.gt = a₂.horner x₂ n₂ _f_1
tactic.ring2.horner_expr.add_aux._match_1 a₁ A₁ x₁ a₂ x₂ n₂ b₂ n₁ B₁ e₂ _f_1 _f_2 ordering.eq = tactic.ring2.horner_expr.add_aux._match_2 A₁ x₁ a₂ n₂ b₂ n₁ B₁ (λ (k : pos_num), _f_2 k) (n₁.sub' n₂)
tactic.ring2.horner_expr.add_aux._match_1 a₁ A₁ x₁ a₂ x₂ n₂ b₂ n₁ B₁ e₂ _f_1 _f_2 ordering.lt = a₁.horner x₁ n₁ (B₁ e₂)
tactic.ring2.horner_expr.add_aux._match_2 A₁ x₁ a₂ n₂ b₂ n₁ B₁ _f_1 (znum.neg k) = (A₁ (a₂.horner x₁ ↑k 0)).horner x₁ n₁ (B₁ b₂)
tactic.ring2.horner_expr.add_aux._match_2 A₁ x₁ a₂ n₂ b₂ n₁ B₁ _f_1 (znum.pos k) = (_f_1 k).horner x₁ n₂ (B₁ b₂)
tactic.ring2.horner_expr.add_aux._match_2 A₁ x₁ a₂ n₂ b₂ n₁ B₁ _f_1 znum.zero = (A₁ a₂).horner' x₁ n₁ (B₁ b₂)

source

def tactic.ring2.horner_expr.add :

tactic.ring2.horner_expr → tactic.ring2.horner_expr → tactic.ring2.horner_expr

Equations

(a₁.horner x₁ n₁ b₁).add e₂ = a₁.add_aux a₁.add x₁ e₂ n₁ b₁ b₁.add
(tactic.ring2.horner_expr.const n₁).add e₂ = tactic.ring2.horner_expr.add_const n₁ e₂

source

def tactic.ring2.horner_expr.neg :

tactic.ring2.horner_expr → tactic.ring2.horner_expr

Equations

e.neg = tactic.ring2.horner_expr.rec (λ (n : znum), tactic.ring2.horner_expr.const (-n)) (λ (a : tactic.ring2.horner_expr) (x : pos_num) (n : num) (b A B : tactic.ring2.horner_expr), A.horner x n B) e

source

def tactic.ring2.horner_expr.mul_const :

znum → tactic.ring2.horner_expr → tactic.ring2.horner_expr

Equations

tactic.ring2.horner_expr.mul_const k e = ite (k = 0) 0 (ite (k = 1) e (tactic.ring2.horner_expr.rec (λ (n : znum), tactic.ring2.horner_expr.const (n * k)) (λ (a : tactic.ring2.horner_expr) (x : pos_num) (n : num) (b A B : tactic.ring2.horner_expr), A.horner x n B) e))

source

def tactic.ring2.horner_expr.mul_aux :

tactic.ring2.horner_expr → pos_num → num → tactic.ring2.horner_expr → (tactic.ring2.horner_expr → tactic.ring2.horner_expr) → (tactic.ring2.horner_expr → tactic.ring2.horner_expr) → tactic.ring2.horner_expr → tactic.ring2.horner_expr

Equations

a₁.mul_aux x₁ n₁ b₁ A₁ B₁ (a₂.horner x₂ n₂ b₂) = tactic.ring2.horner_expr.mul_aux._match_1 x₁ n₁ A₁ B₁ a₂ x₂ n₂ b₂ (a₁.mul_aux x₁ n₁ b₁ A₁ B₁ a₂) (a₁.mul_aux x₁ n₁ b₁ A₁ B₁ b₂) (a₁.mul_aux x₁ n₁ b₁ A₁ B₁ a₂) (x₁.cmp x₂)
a₁.mul_aux x₁ n₁ b₁ A₁ B₁ (tactic.ring2.horner_expr.const n₂) = tactic.ring2.horner_expr.mul_const n₂ (a₁.horner x₁ n₁ b₁)
tactic.ring2.horner_expr.mul_aux._match_1 x₁ n₁ A₁ B₁ a₂ x₂ n₂ b₂ _f_1 _f_2 _f_3 ordering.gt = _f_1.horner x₂ n₂ _f_2
tactic.ring2.horner_expr.mul_aux._match_1 x₁ n₁ A₁ B₁ a₂ x₂ n₂ b₂ _f_1 _f_2 _f_3 ordering.eq = let haa : tactic.ring2.horner_expr := _f_3.horner' x₁ n₂ 0 in ite (b₂ = 0) haa (haa.add ((A₁ b₂).horner x₁ n₁ (B₁ b₂)))
tactic.ring2.horner_expr.mul_aux._match_1 x₁ n₁ A₁ B₁ a₂ x₂ n₂ b₂ _f_1 _f_2 _f_3 ordering.lt = (A₁ (a₂.horner x₂ n₂ b₂)).horner x₁ n₁ (B₁ (a₂.horner x₂ n₂ b₂))

source

def tactic.ring2.horner_expr.mul :

tactic.ring2.horner_expr → tactic.ring2.horner_expr → tactic.ring2.horner_expr

Equations

(a₁.horner x₁ n₁ b₁).mul = a₁.mul_aux x₁ n₁ b₁ a₁.mul b₁.mul
(tactic.ring2.horner_expr.const n₁).mul = tactic.ring2.horner_expr.mul_const n₁

source

@[instance]

def tactic.ring2.horner_expr.has_add :

has_add tactic.ring2.horner_expr

Equations

tactic.ring2.horner_expr.has_add = {add := tactic.ring2.horner_expr.add}

source

@[instance]

def tactic.ring2.horner_expr.has_neg :

has_neg tactic.ring2.horner_expr

Equations

tactic.ring2.horner_expr.has_neg = {neg := tactic.ring2.horner_expr.neg}

source

@[instance]

def tactic.ring2.horner_expr.has_mul :

has_mul tactic.ring2.horner_expr

Equations

tactic.ring2.horner_expr.has_mul = {mul := tactic.ring2.horner_expr.mul}

source

def tactic.ring2.horner_expr.pow :

tactic.ring2.horner_expr → num → tactic.ring2.horner_expr

Equations

e.pow (num.pos p) = pos_num.rec e (λ (p : pos_num) (ep : tactic.ring2.horner_expr), (ep.mul ep).mul e) (λ (p : pos_num) (ep : tactic.ring2.horner_expr), ep.mul ep) p
e.pow 0 = 1

source

def tactic.ring2.horner_expr.inv :

tactic.ring2.horner_expr → tactic.ring2.horner_expr

Equations

e.inv = 0

source

def tactic.ring2.horner_expr.of_csexpr :

tactic.ring2.csring_expr → tactic.ring2.horner_expr

Brings expressions into Horner normal form.

Equations

source

def tactic.ring2.horner_expr.cseval {α : Type u_1} [comm_semiring α] :

tree α → tactic.ring2.horner_expr → α

Evaluates a reflected horner_expr - see csring_expr.eval.

Equations

tactic.ring2.horner_expr.cseval t (a.horner x n b) = tactic.ring.horner (tactic.ring2.horner_expr.cseval t a) (t.get_or_zero x) ↑n (tactic.ring2.horner_expr.cseval t b)
tactic.ring2.horner_expr.cseval t (tactic.ring2.horner_expr.const n) = ↑(n.abs)

source

theorem tactic.ring2.horner_expr.cseval_atom {α : Type u_1} [comm_semiring α] (t : tree α) (n : pos_num) :

(tactic.ring2.horner_expr.atom n).is_cs ∧ tactic.ring2.horner_expr.cseval t (tactic.ring2.horner_expr.atom n) = t.get_or_zero n

source

theorem tactic.ring2.horner_expr.cseval_add_const {α : Type u_1} [comm_semiring α] (t : tree α) (k : num) {e : tactic.ring2.horner_expr} :

e.is_cs → (tactic.ring2.horner_expr.add_const k.to_znum e).is_cs ∧ tactic.ring2.horner_expr.cseval t (tactic.ring2.horner_expr.add_const k.to_znum e) = ↑k + tactic.ring2.horner_expr.cseval t e

source

theorem tactic.ring2.horner_expr.cseval_horner' {α : Type u_1} [comm_semiring α] (t : tree α) (a : tactic.ring2.horner_expr) (x : pos_num) (n : num) (b : tactic.ring2.horner_expr) :

a.is_cs → b.is_cs → (a.horner' x n b).is_cs ∧ tactic.ring2.horner_expr.cseval t (a.horner' x n b) = tactic.ring.horner (tactic.ring2.horner_expr.cseval t a) (t.get_or_zero x) ↑n (tactic.ring2.horner_expr.cseval t b)

source

theorem tactic.ring2.horner_expr.cseval_add {α : Type u_1} [comm_semiring α] (t : tree α) {e₁ e₂ : tactic.ring2.horner_expr} :

e₁.is_cs → e₂.is_cs → (e₁.add e₂).is_cs ∧ tactic.ring2.horner_expr.cseval t (e₁.add e₂) = tactic.ring2.horner_expr.cseval t e₁ + tactic.ring2.horner_expr.cseval t e₂

source

theorem tactic.ring2.horner_expr.cseval_mul_const {α : Type u_1} [comm_semiring α] (t : tree α) (k : num) {e : tactic.ring2.horner_expr} :

e.is_cs → (tactic.ring2.horner_expr.mul_const k.to_znum e).is_cs ∧ tactic.ring2.horner_expr.cseval t (tactic.ring2.horner_expr.mul_const k.to_znum e) = tactic.ring2.horner_expr.cseval t e * ↑k

source

theorem tactic.ring2.horner_expr.cseval_mul {α : Type u_1} [comm_semiring α] (t : tree α) {e₁ e₂ : tactic.ring2.horner_expr} :

e₁.is_cs → e₂.is_cs → (e₁.mul e₂).is_cs ∧ tactic.ring2.horner_expr.cseval t (e₁.mul e₂) = tactic.ring2.horner_expr.cseval t e₁ * tactic.ring2.horner_expr.cseval t e₂

source

theorem tactic.ring2.horner_expr.cseval_pow {α : Type u_1} [comm_semiring α] (t : tree α) {x : tactic.ring2.horner_expr} (cs : x.is_cs) (n : num) :

(x.pow n).is_cs ∧ tactic.ring2.horner_expr.cseval t (x.pow n) = tactic.ring2.horner_expr.cseval t x ^ ↑n

source

theorem tactic.ring2.horner_expr.cseval_of_csexpr {α : Type u_1} [comm_semiring α] (t : tree α) (r : tactic.ring2.csring_expr) :

(tactic.ring2.horner_expr.of_csexpr r).is_cs ∧ tactic.ring2.horner_expr.cseval t (tactic.ring2.horner_expr.of_csexpr r) = tactic.ring2.csring_expr.eval t r

For any given tree t of atoms and any reflected expression r, the Horner form of r is a valid csring expression, and under t, the Horner form evaluates to the same thing as r.

source

theorem tactic.ring2.correctness {α : Type u_1} [comm_semiring α] (t : tree α) (r₁ r₂ : tactic.ring2.csring_expr) :

tactic.ring2.horner_expr.of_csexpr r₁ = tactic.ring2.horner_expr.of_csexpr r₂ → tactic.ring2.csring_expr.eval t r₁ = tactic.ring2.csring_expr.eval t r₂

The main proof-by-reflection theorem. Given reflected csring expressions r₁ and r₂ plus a storage t of atoms, if both expressions go to the same Horner normal form, then the original non-reflected expressions are equal. H follows from kernel reduction and is therefore rfl.

source

meta def tactic.ring2.reflect_expr :

expr → tactic.ring2.csring_expr × dlist expr

Reflects a csring expression into a csring_expr, together with a dlist of atoms, i.e. opaque variables over which the expression is a polynomial.

source

meta def tactic.ring2.csring_expr.replace :

tree expr → tactic.ring2.csring_expr → state_t (list expr) option tactic.ring2.csring_expr

In the output of reflect_expr, atoms are initialized with incorrect indices. The indices cannot be computed until the whole tree is built, so another pass over the expressions is needed - this is what replace does. The computation (expressed in the state monad) fixes up atoms to match their positions in the atom tree. The initial state is a list of all atom occurrences in the goal, left-to-right.

source

meta def tactic.interactive.ring2 :

tactic unit

ring2 solves equations in the language of rings.

It supports only the commutative semiring operations, i.e. it does not normalize subtraction or division.

This variant on the ring tactic uses kernel computation instead of proof generation. In general, you should use ring instead of ring2.

source

meta def conv.interactive.ring2 :

conv unit