ring

RingExpr

data RingExpr

Syntax of commutative-semiring expressions over Nat: variables by index, numerals, sums and products.

ringNth

def ringNth (ρ : List Nat) (i : Nat) : Nat

Looks up the i-th variable in an environment, defaulting to zero when the index is out of range.

ringEval

def ringEval (ρ : List Nat) (e : RingExpr) : Nat

Evaluates a ring expression in Nat under the given variable environment.

ringLeN

def ringLeN (m : Nat) (n : Nat) : Bool

Boolean less-or-equal on Nat, used to order variables inside monomials.

monoLe

def monoLe (a : List Nat) (b : List Nat) : Bool

Lexicographic comparison of monomials, used to keep polynomials sorted (affects completeness only).

monoEval

def monoEval (ρ : List Nat) (m : List Nat) : Nat

Evaluates a monomial (a list of variable indices) as the product of those variables.

monoInsB

def monoInsB (b : Bool) (i : Nat) (j : Nat) (t : List Nat) (rest : List Nat) : List Nat

Insertion step for monoIns: places i before j when the comparison flag is true, otherwise keeps j and uses the recursive result.

monoIns

def monoIns (i : Nat) (m : List Nat) : List Nat

Inserts a variable index into a sorted monomial.

ringMulSwap

def ringMulSwap (a : Nat) (b : Nat) (c : Nat) : mul b (mul a c) = mul a (mul b c)

Swapping the outer factors of a nested product: b * (a * c) equals a * (b * c).

monoInsBSound

def monoInsBSound (ρ : List Nat) (b : Bool) (i : Nat) (j : Nat) (t : List Nat) (rest : List Nat) (ih : monoEval ρ rest = mul (ringNth ρ i) (monoEval ρ t)) : monoEval ρ (monoInsB b i j t rest) = mul (ringNth ρ i) (mul (ringNth ρ j) (monoEval ρ t))

Soundness of one monoInsB step: the result evaluates to i’s value times j’s value times the tail.

monoInsSound

def monoInsSound (ρ : List Nat) (i : Nat) (m : List Nat) : monoEval ρ (monoIns i m) = mul (ringNth ρ i) (monoEval ρ m)

Soundness of monoIns: inserting i multiplies the monomial’s value by the value of variable i.

monoMul

def monoMul (m : List Nat) (n : List Nat) : List Nat

Multiplies two monomials by merging their sorted variable lists.

monoMulSound

def monoMulSound (ρ : List Nat) (m : List Nat) (n : List Nat) : monoEval ρ (monoMul m n) = mul (monoEval ρ m) (monoEval ρ n)

Soundness of monoMul: the product monomial evaluates to the product of the two values.

polyEval

def polyEval (ρ : List Nat) (p : List (List Nat)) : Nat

Evaluates a polynomial (a list of monomials) as the sum of its monomials.

ringAddSwap

def ringAddSwap (a : Nat) (b : Nat) (c : Nat) : add b (add a c) = add a (add b c)

Swapping the outer summands of a nested sum: b + (a + c) equals a + (b + c).

polyInsB

def polyInsB (b : Bool) (m : List Nat) (n : List Nat) (t : List (List Nat)) (rest : List (List Nat)) : List (List Nat)

Insertion step for polyIns: places m before n when the comparison flag is true, otherwise keeps n and uses the recursive result.

polyIns

def polyIns (m : List Nat) (p : List (List Nat)) : List (List Nat)

Inserts a monomial into a sorted polynomial.

polyInsBSound

def polyInsBSound (ρ : List Nat) (b : Bool) (m : List Nat) (n : List Nat) (t : List (List Nat)) (rest : List (List Nat)) (ih : polyEval ρ rest = add (monoEval ρ m) (polyEval ρ t)) : polyEval ρ (polyInsB b m n t rest) = add (monoEval ρ m) (add (monoEval ρ n) (polyEval ρ t))

Soundness of one polyInsB step: the result evaluates to m’s value plus n’s value plus the tail.

polyInsSound

def polyInsSound (ρ : List Nat) (m : List Nat) (p : List (List Nat)) : polyEval ρ (polyIns m p) = add (monoEval ρ m) (polyEval ρ p)

Soundness of polyIns: inserting a monomial adds its value to the polynomial’s value.

polyAdd

def polyAdd (p : List (List Nat)) (q : List (List Nat)) : List (List Nat)

Adds two polynomials by inserting the monomials of the first into the second.

polyAddSound

def polyAddSound (ρ : List Nat) (p : List (List Nat)) (q : List (List Nat)) : polyEval ρ (polyAdd p q) = add (polyEval ρ p) (polyEval ρ q)

Soundness of polyAdd: the sum polynomial evaluates to the sum of the two values.

polyScale

def polyScale (m : List Nat) (q : List (List Nat)) : List (List Nat)

Multiplies every monomial of a polynomial by a fixed monomial.

polyScaleSound

def polyScaleSound (ρ : List Nat) (m : List Nat) (q : List (List Nat)) : polyEval ρ (polyScale m q) = mul (monoEval ρ m) (polyEval ρ q)

Soundness of polyScale: scaling by a monomial multiplies the polynomial’s value by that monomial’s value.

polyMul

def polyMul (p : List (List Nat)) (q : List (List Nat)) : List (List Nat)

Multiplies two polynomials by distributing over the monomials of the first.

polyMulSound

def polyMulSound (ρ : List Nat) (p : List (List Nat)) (q : List (List Nat)) : polyEval ρ (polyMul p q) = mul (polyEval ρ p) (polyEval ρ q)

Soundness of polyMul: the product polynomial evaluates to the product of the two values.

polyNum

def polyNum (n : Nat) : List (List Nat)

Represents a numeral n as the polynomial with n copies of the empty (unit) monomial.

polyNumSound

def polyNumSound (ρ : List Nat) (n : Nat) : polyEval ρ (polyNum n) = n

Soundness of polyNum: the polynomial for n evaluates to n.

ringNorm

def ringNorm (e : RingExpr) : List (List Nat)

Normalizes a ring expression to a sorted polynomial; this is the computation the ring tactic relies on.

ringNormSound

def ringNormSound (ρ : List Nat) (e : RingExpr) : polyEval ρ (ringNorm e) = ringEval ρ e

Soundness of the ring normalizer: the normal form evaluates to the same value as the expression under every environment.

ringEq

def ringEq (ρ : List Nat) (a : RingExpr) (b : RingExpr) (h : ringNorm a = ringNorm b) : ringEval ρ a = ringEval ρ b

The certificate the ring tactic produces: equal normal forms imply equal values under every environment.

ringEqTestComm

def ringEqTestComm (x : Nat) (y : Nat) : mul x y = mul y x

Example of using ringEq directly to prove commutativity of multiplication without the tactic.