Numeral inverses as rational coefficients

In a field of characteristic zero, the inverse c⁻¹ of a numeral c ≠ 0 is not an atom of the polynomial normal form: a / 2 + a / 2 must normalize to a. The reflection language Expr denotes into any ring and has no inverse, so c⁻¹ is reified as a variable x and the InvVars list records x ↦ c. The integer polynomial of the term is then normalized into a PolyQ num / den: an integer polynomial num over the remaining variables and a denominator den, in lowest terms. Every x is eliminated with Poly.cancelVar, which is justified by c * x = 1; that equation holds because c ≠ 0 in characteristic zero.

The side condition InvVars.ok (each recorded variable denotes the inverse of its numeral) is an equation between two lists that the kernel checks by rfl, since the context holds the inverse terms themselves.

The inverse x⁻¹ of an atom x is a variable y as well. When x ≠ 0 is known, x * y = 1 and every monomial containing both x and y is reduced (Poly.cancelInv); InvAtoms records the pairs (y, x) and InvAtoms.ok holds their equations, which are proved from x ≠ 0. This needs no characteristic: Expr.eq_of_cancelInvs_eq and the normA relation certificates work in any CommRing, and toPolyQ combines both kinds of inverses.

@[reducible, inline]

abbrev Lean.Grind.CommRing.InvVars : Type

Variables that denote inverses of numerals: (x, c) records that x denotes (OfNat.ofNat c)⁻¹.

Equations

• Lean.Grind.CommRing.InvVars = List (Lean.Grind.CommRing.Var × Nat)

structure Lean.Grind.CommRing.PolyQ : Type

A polynomial with a denominator, denoting num.denote ctx * (den : α)⁻¹.

• num : Poly
• den : Nat

def Lean.Grind.CommRing.instBEqPolyQ.beq : PolyQ → PolyQ → Bool

Equations

• Lean.Grind.CommRing.instBEqPolyQ.beq { num := a, den := a_1 } { num := b, den := b_1 } = (a == b && a_1 == b_1)
• Lean.Grind.CommRing.instBEqPolyQ.beq x✝¹ x✝ = false

@[instance_reducible]

instance Lean.Grind.CommRing.instBEqPolyQ : BEq PolyQ

Equations

• Lean.Grind.CommRing.instBEqPolyQ = { beq := Lean.Grind.CommRing.instBEqPolyQ.beq }

instance Lean.Grind.CommRing.instReflBEqPolyQ : ReflBEq PolyQ

instance Lean.Grind.CommRing.instLawfulBEqPolyQ : LawfulBEq PolyQ

def Lean.Grind.CommRing.instReprPolyQ.repr : PolyQ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Lean.Grind.CommRing.instReprPolyQ : Repr PolyQ

Equations

• Lean.Grind.CommRing.instReprPolyQ = { reprPrec := Lean.Grind.CommRing.instReprPolyQ.repr }

@[instance_reducible]

instance Lean.Grind.CommRing.instInhabitedPolyQ : Inhabited PolyQ

Equations

• Lean.Grind.CommRing.instInhabitedPolyQ = { default := Lean.Grind.CommRing.instInhabitedPolyQ.default }

def Lean.Grind.CommRing.InvVars.denoteVars {α : Type u_1} (ctx : Context α) (invs : InvVars) : List α

Equations

• Lean.Grind.CommRing.InvVars.denoteVars ctx invs = List.map (fun (p : Lean.Grind.CommRing.Var × Nat) => Lean.Grind.CommRing.Var.denote ctx p.fst) invs

def Lean.Grind.CommRing.InvVars.denoteInvs {α : Type u_1} [Field α] (invs : InvVars) : List α

Equations

• invs.denoteInvs = List.map (fun (p : Lean.Grind.CommRing.Var × Nat) => (OfNat.ofNat p.snd)⁻¹) invs

def Lean.Grind.CommRing.InvVars.ok {α : Type u_1} [Field α] (ctx : Context α) (invs : InvVars) : Prop

Each variable recorded in invs denotes the inverse of its numeral.

Equations

• Lean.Grind.CommRing.InvVars.ok ctx invs = (Lean.Grind.CommRing.InvVars.denoteVars ctx invs = invs.denoteInvs)

theorem Lean.Grind.CommRing.InvVars.ok_cons {α : Type u_1} [Field α] (ctx : Context α) (x : Var) (c : Nat) (invs : InvVars) : ok ctx ((x, c) :: invs) ↔ Var.denote ctx x = (OfNat.ofNat c)⁻¹ ∧ ok ctx invs

Inverses of atoms

theorem Lean.Grind.CommRing.Mon.degreeOf_cancelVar (m : Mon) (x y : Var) (h : x ≠ y) : (m.cancelVar x).degreeOf y = m.degreeOf y

def Lean.Grind.CommRing.Mon.cancelInv (x y : Var) (m : Mon) : Mon

Cancels x ^ d * y ^ d from m, where d is the smaller of the degrees of x and y in m. Justified by x * y = 1; a no-op when x = y.

Equations

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

theorem Lean.Grind.CommRing.Mon.denote_cancelInv {α : Type u_1} [CommSemiring α] (ctx : Context α) (m : Mon) (x y : Var) (h : Var.denote ctx x * Var.denote ctx y = 1) : denote ctx (cancelInv x y m) = denote ctx m

def Lean.Grind.CommRing.Poly.cancelInv (x y : Var) (p : Poly) : Poly

Cancels x ^ d * y ^ d from every monomial of p (Mon.cancelInv).

Equations

• Lean.Grind.CommRing.Poly.cancelInv x y p = Lean.Grind.CommRing.Poly.cancelInv.go x y p (Lean.Grind.CommRing.Poly.num 0)

def Lean.Grind.CommRing.Poly.cancelInv.go (x y : Var) : Poly → Poly → Poly

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Poly.cancelInv.go x y (Lean.Grind.CommRing.Poly.num k) a✝ = a✝.addConst k

theorem Lean.Grind.CommRing.Poly.denote_cancelInv {α : Type u_1} [CommRing α] (ctx : Context α) (p : Poly) (x y : Var) (h : Var.denote ctx x * Var.denote ctx y = 1) : denote ctx (cancelInv x y p) = denote ctx p

@[reducible, inline]

abbrev Lean.Grind.CommRing.InvAtoms : Type

Variables that denote inverses of variables: (y, x) records that y denotes x⁻¹, for x ≠ 0.

Equations

• Lean.Grind.CommRing.InvAtoms = List (Lean.Grind.CommRing.Var × Lean.Grind.CommRing.Var)

def Lean.Grind.CommRing.InvAtoms.ok {α : Type u_1} [Ring α] (ctx : Context α) : InvAtoms → Prop

x.denote ctx * y.denote ctx = 1 for each (y, x).

Equations

• Lean.Grind.CommRing.InvAtoms.ok ctx [] = True
• Lean.Grind.CommRing.InvAtoms.ok ctx ((y, x_1) :: l) = (Lean.Grind.CommRing.Var.denote ctx x_1 * Lean.Grind.CommRing.Var.denote ctx y = 1 ∧ Lean.Grind.CommRing.InvAtoms.ok ctx l)

theorem Lean.Grind.CommRing.InvAtoms.ok_cons {α : Type u_1} [Ring α] (ctx : Context α) (y x : Var) (l : InvAtoms) (h₁ : Var.denote ctx x * Var.denote ctx y = 1) (h₂ : ok ctx l) : ok ctx ((y, x) :: l)

def Lean.Grind.CommRing.Poly.cancelInvs (p : Poly) (ainvs : InvAtoms) : Poly

Equations

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

theorem Lean.Grind.CommRing.Poly.denote_cancelInvs {α : Type u_1} [CommRing α] (ctx : Context α) (p : Poly) (ainvs : InvAtoms) (h : InvAtoms.ok ctx ainvs) : denote ctx (p.cancelInvs ainvs) = denote ctx p

Inverses of numerals

def Lean.Grind.CommRing.PolyQ.denote {α : Type u_1} [Field α] (ctx : Context α) (q : PolyQ) : α

Equations

• Lean.Grind.CommRing.PolyQ.denote ctx q = Lean.Grind.CommRing.Poly.denote ctx q.num * (↑q.den)⁻¹

def Lean.Grind.CommRing.Poly.substInv (p : Poly) (x : Var) (c : Nat) : PolyQ

Eliminates the variable x, which denotes c⁻¹, from p: the polynomial is multiplied by c ^ n, where n is the maximal degree of x in p, so that every power x ^ k can be cancelled against the coefficient (c ^ k * x ^ k = 1); the denominator is c ^ n. c = 0 is not an inverse and is left alone.

Equations

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

def Lean.Grind.CommRing.PolyQ.substInv (q : PolyQ) (x : Var) (c : Nat) : PolyQ

Equations

• q.substInv x c = { num := (q.num.substInv x c).num, den := q.den * (q.num.substInv x c).den }

def Lean.Grind.CommRing.PolyQ.reduce (q : PolyQ) : PolyQ

Lowest terms: divides num and den by their greatest common factor. The divisions are checked by multiplying back, so the correctness proof needs no divisibility reasoning.

Equations

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

def Lean.Grind.CommRing.Poly.toPolyQ (p : Poly) (invs : InvVars) (ainvs : InvAtoms) : PolyQ

Cancels the inverse pairs of ainvs, eliminates the numeral inverses of invs, and reduces the result to lowest terms.

Equations

• p.toPolyQ invs ainvs = (List.foldl (fun (q : Lean.Grind.CommRing.PolyQ) (xc : Lean.Grind.CommRing.Var × Nat) => q.substInv xc.fst xc.snd) { num := p.cancelInvs ainvs, den := 1 } invs).reduce

def Lean.Grind.CommRing.Expr.toPolyQ (e : Expr) (invs : InvVars) (ainvs : InvAtoms) : PolyQ

Equations

• e.toPolyQ invs ainvs = e.toPoly.toPolyQ invs ainvs

theorem Lean.Grind.CommRing.Poly.denote_substInv {α : Type u_1} [Field α] [IsCharP α 0] (ctx : Context α) (p : Poly) (x : Var) (c : Nat) (h : Var.denote ctx x = (OfNat.ofNat c)⁻¹) : PolyQ.denote ctx (p.substInv x c) = denote ctx p

theorem Lean.Grind.CommRing.PolyQ.denote_substInv {α : Type u_1} [Field α] [IsCharP α 0] (ctx : Context α) (q : PolyQ) (x : Var) (c : Nat) (h : Var.denote ctx x = (OfNat.ofNat c)⁻¹) : denote ctx (q.substInv x c) = denote ctx q

theorem Lean.Grind.CommRing.PolyQ.denote_reduce {α : Type u_1} [Field α] [IsCharP α 0] (ctx : Context α) (q : PolyQ) : denote ctx q.reduce = denote ctx q

theorem Lean.Grind.CommRing.Poly.denote_toPolyQ {α : Type u_1} [Field α] [IsCharP α 0] (ctx : Context α) (p : Poly) (invs : InvVars) (ainvs : InvAtoms) (h : InvVars.ok ctx invs) (h' : InvAtoms.ok ctx ainvs) : PolyQ.denote ctx (p.toPolyQ invs ainvs) = denote ctx p

theorem Lean.Grind.CommRing.Expr.denote_toPolyQ {α : Type u_1} [Field α] [IsCharP α 0] (ctx : Context α) (e : Expr) (invs : InvVars) (ainvs : InvAtoms) (h : InvVars.ok ctx invs) (h' : InvAtoms.ok ctx ainvs) : PolyQ.denote ctx (e.toPolyQ invs ainvs) = denote ctx e

theorem Lean.Grind.CommRing.Poly.substInv_den_ne_zero (p : Poly) (x : Var) (c : Nat) : (p.substInv x c).den ≠ 0

theorem Lean.Grind.CommRing.PolyQ.reduce_den_ne_zero (q : PolyQ) (h : q.den ≠ 0) : q.reduce.den ≠ 0

theorem Lean.Grind.CommRing.Poly.toPolyQ_den_ne_zero (p : Poly) (invs : InvVars) (ainvs : InvAtoms) : (p.toPolyQ invs ainvs).den ≠ 0

theorem Lean.Grind.CommRing.Expr.toPolyQ_den_ne_zero (e : Expr) (invs : InvVars) (ainvs : InvAtoms) : (e.toPolyQ invs ainvs).den ≠ 0

Certificates for inverses of atoms only

def Lean.Grind.CommRing.Expr.cancelInvs_cert (ainvs : InvAtoms) (a b : Expr) : Bool

Equations

• Lean.Grind.CommRing.Expr.cancelInvs_cert ainvs a b = (a.toPoly.cancelInvs ainvs == b.toPoly.cancelInvs ainvs)

theorem Lean.Grind.CommRing.Expr.eq_of_cancelInvs_eq {α : Type u_1} [CommRing α] (ctx : Context α) (ainvs : InvAtoms) (hok : InvAtoms.ok ctx ainvs) (a b : Expr) (h : cancelInvs_cert ainvs a b = true) : denote ctx a = denote ctx b

def Lean.Grind.CommRing.normA_cert (ainvs : InvAtoms) (lhs rhs lhs' rhs' : Expr) : Bool

Equations

• Lean.Grind.CommRing.normA_cert ainvs lhs rhs lhs' rhs' = ((lhs.sub rhs).toPoly.cancelInvs ainvs == (lhs'.sub rhs').toPoly)

theorem Lean.Grind.CommRing.eq_normA_expr {α : Type u_1} [CommRing α] (ctx : Context α) (ainvs : InvAtoms) (hok : InvAtoms.ok ctx ainvs) (lhs rhs lhs' rhs' : Expr) : normA_cert ainvs lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs = Expr.denote ctx rhs) = (Expr.denote ctx lhs' = Expr.denote ctx rhs')

theorem Lean.Grind.CommRing.le_normA_expr {α : Type u_1} [CommRing α] [LE α] [LT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (ainvs : InvAtoms) (hok : InvAtoms.ok ctx ainvs) (lhs rhs lhs' rhs' : Expr) : normA_cert ainvs lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs ≤ Expr.denote ctx rhs) = (Expr.denote ctx lhs' ≤ Expr.denote ctx rhs')

theorem Lean.Grind.CommRing.lt_normA_expr {α : Type u_1} [CommRing α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (ainvs : InvAtoms) (hok : InvAtoms.ok ctx ainvs) (lhs rhs lhs' rhs' : Expr) : normA_cert ainvs lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs < Expr.denote ctx rhs) = (Expr.denote ctx lhs' < Expr.denote ctx rhs')

Certificates for rational coefficients

def Lean.Grind.CommRing.Expr.toPolyQ_cert (invs : InvVars) (ainvs : InvAtoms) (a b : Expr) : Bool

Equations

• Lean.Grind.CommRing.Expr.toPolyQ_cert invs ainvs a b = (a.toPolyQ invs ainvs == b.toPolyQ invs ainvs)

theorem Lean.Grind.CommRing.Expr.eq_of_toPolyQ_eq {α : Type u_1} [Field α] [IsCharP α 0] (ctx : Context α) (invs : InvVars) (hok : InvVars.ok ctx invs) (ainvs : InvAtoms) (hoka : InvAtoms.ok ctx ainvs) (a b : Expr) (h : toPolyQ_cert invs ainvs a b = true) : denote ctx a = denote ctx b

def Lean.Grind.CommRing.normQ_cert (invs : InvVars) (ainvs : InvAtoms) (lhs rhs lhs' rhs' : Expr) : Bool

lhs' - rhs' is the numerator of lhs - rhs; the relation between lhs' and rhs' is denominator-free.

Equations

• Lean.Grind.CommRing.normQ_cert invs ainvs lhs rhs lhs' rhs' = (((lhs.sub rhs).toPolyQ invs ainvs).num == (lhs'.sub rhs').toPoly)

theorem Lean.Grind.CommRing.eq_normQ_expr {α : Type u_1} [Field α] [IsCharP α 0] (ctx : Context α) (invs : InvVars) (hok : InvVars.ok ctx invs) (ainvs : InvAtoms) (hoka : InvAtoms.ok ctx ainvs) (lhs rhs lhs' rhs' : Expr) : normQ_cert invs ainvs lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs = Expr.denote ctx rhs) = (Expr.denote ctx lhs' = Expr.denote ctx rhs')

theorem Lean.Grind.CommRing.le_normQ_expr {α : Type u} [Field α] [IsCharP α 0] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] [OrderedRing α] (ctx : Context α) (invs : InvVars) (hok : InvVars.ok ctx invs) (ainvs : InvAtoms) (hoka : InvAtoms.ok ctx ainvs) (lhs rhs lhs' rhs' : Expr) : normQ_cert invs ainvs lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs ≤ Expr.denote ctx rhs) = (Expr.denote ctx lhs' ≤ Expr.denote ctx rhs')

theorem Lean.Grind.CommRing.lt_normQ_expr {α : Type u} [Field α] [IsCharP α 0] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] [OrderedRing α] (ctx : Context α) (invs : InvVars) (hok : InvVars.ok ctx invs) (ainvs : InvAtoms) (hoka : InvAtoms.ok ctx ainvs) (lhs rhs lhs' rhs' : Expr) : normQ_cert invs ainvs lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs < Expr.denote ctx rhs) = (Expr.denote ctx lhs' < Expr.denote ctx rhs')