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)⁻¹.

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

@[instance_reducible]

instance Lean.Grind.CommRing.instBEqPolyQ : BEq PolyQ

instance Lean.Grind.CommRing.instReflBEqPolyQ : ReflBEq PolyQ

instance Lean.Grind.CommRing.instLawfulBEqPolyQ : LawfulBEq PolyQ

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

@[instance_reducible]

instance Lean.Grind.CommRing.instReprPolyQ : Repr PolyQ

@[instance_reducible]

instance Lean.Grind.CommRing.instInhabitedPolyQ : Inhabited PolyQ

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

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

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.

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.

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).

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

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.

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).

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

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) : α

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.

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

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.

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.

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

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

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

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

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.

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')