intring

IntExpr

data IntExpr

Syntax of integer ring expressions reflected by the Int ring tactic: variables, numerals, negation, addition and multiplication.

intNth

def intNth (ρ : List Int) (i : Nat) : Int

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

intEval

def intEval (ρ : List Int) (e : IntExpr) : Int

Evaluates an integer ring expression under an environment of variable values.

monoEvalI

def monoEvalI (ρ : List Int) (m : List Nat) : Int

Evaluates a monomial, a list of variable indices, as the product of their values in Int.

polyEvalI

def polyEvalI (ρ : List Int) (p : List (List Nat)) : Int

Evaluates a polynomial, a list of monomials, as the sum of their values in Int.

mulIntSwap

def mulIntSwap (a : Int) (b : Int) (c : Int) : Int.mul b (Int.mul a c) = Int.mul a (Int.mul b c)

Swaps the two outer factors of a nested product: b * (a * c) = a * (b * c).

monoInsBSoundI

def monoInsBSoundI (ρ : List Int) (b : Bool) (i : Nat) (j : Nat) (t : List Nat) (rest : List Nat) (ih : monoEvalI ρ rest = Int.mul (intNth ρ i) (monoEvalI ρ t)) : monoEvalI ρ (monoInsB b i j t rest) = Int.mul (intNth ρ i) (Int.mul (intNth ρ j) (monoEvalI ρ t))

Inductive step for monoInsSoundI: one branch of inserting a variable into a sorted monomial preserves its Int value.

monoInsSoundI

def monoInsSoundI (ρ : List Int) (i : Nat) (m : List Nat) : monoEvalI ρ (monoIns i m) = Int.mul (intNth ρ i) (monoEvalI ρ m)

Inserting a variable into a monomial multiplies its Int value by that variable.

monoMulSoundI

def monoMulSoundI (ρ : List Int) (m : List Nat) (n : List Nat) : monoEvalI ρ (monoMul m n) = Int.mul (monoEvalI ρ m) (monoEvalI ρ n)

Multiplying monomials multiplies their Int values.

polyInsBSoundI

def polyInsBSoundI (ρ : List Int) (b : Bool) (m : List Nat) (n : List Nat) (t : List (List Nat)) (rest : List (List Nat)) (ih : polyEvalI ρ rest = Int.add (monoEvalI ρ m) (polyEvalI ρ t)) : polyEvalI ρ (polyInsB b m n t rest) = Int.add (monoEvalI ρ m) (Int.add (monoEvalI ρ n) (polyEvalI ρ t))

Inductive step for polyInsSoundI: one branch of inserting a monomial into a sorted polynomial preserves its Int value.

polyInsSoundI

def polyInsSoundI (ρ : List Int) (m : List Nat) (p : List (List Nat)) : polyEvalI ρ (polyIns m p) = Int.add (monoEvalI ρ m) (polyEvalI ρ p)

Inserting a monomial into a polynomial adds its Int value.

polyAddSoundI

def polyAddSoundI (ρ : List Int) (p : List (List Nat)) (q : List (List Nat)) : polyEvalI ρ (polyAdd p q) = Int.add (polyEvalI ρ p) (polyEvalI ρ q)

Polynomial addition is sound for evaluation in Int.

polyScaleSoundI

def polyScaleSoundI (ρ : List Int) (m : List Nat) (q : List (List Nat)) : polyEvalI ρ (polyScale m q) = Int.mul (monoEvalI ρ m) (polyEvalI ρ q)

Scaling a polynomial by a monomial multiplies its Int value by that monomial.

polyMulSoundI

def polyMulSoundI (ρ : List Int) (p : List (List Nat)) (q : List (List Nat)) : polyEvalI ρ (polyMul p q) = Int.mul (polyEvalI ρ p) (polyEvalI ρ q)

Polynomial multiplication is sound for evaluation in Int.

polyNumSoundI

def polyNumSoundI (ρ : List Int) (n : Nat) : polyEvalI ρ (polyNum n) = pos n

The polynomial for a numeral n evaluates to pos n.

addIntMiddle

def addIntMiddle (a : Int) (b : Int) (c : Int) (d : Int) : Int.add (Int.add a b) (Int.add c d) = Int.add (Int.add a c) (Int.add b d)

Rearranges a sum of two sums: (a + b) + (c + d) = (a + c) + (b + d).

mulIntNegR

def mulIntNegR (a : Int) (b : Int) : Int.mul a (Int.neg b) = Int.neg (Int.mul a b)

Multiplying by a negation on the right negates the product.

diffNeg

def diffNeg (p : Int) (n : Int) : Int.add n (Int.neg p) = Int.neg (Int.add p (Int.neg n))

Negating the difference p - n gives n - p.

diffAdd

def diffAdd (p1 : Int) (n1 : Int) (p2 : Int) (n2 : Int) : Int.add (Int.add p1 p2) (Int.neg (Int.add n1 n2)) = Int.add (Int.add p1 (Int.neg n1)) (Int.add p2 (Int.neg n2))

The difference of two sums is the sum of the componentwise differences.

diffMul

def diffMul (p1 : Int) (n1 : Int) (p2 : Int) (n2 : Int) : Int.add (Int.add (Int.mul p1 p2) (Int.mul n1 n2)) (Int.neg (Int.add (Int.mul p1 n2) (Int.mul n1 p2))) = Int.mul (Int.add p1 (Int.neg n1)) (Int.add p2 (Int.neg n2))

The difference form of a product: (p1 p2 + n1 n2) - (p1 n2 + n1 p2) equals (p1 - n1)(p2 - n2).

diffEq

def diffEq (p : Int) (n : Int) (p2 : Int) (n2 : Int) (h : Int.add p n2 = Int.add p2 n) : Int.add p (Int.neg n) = Int.add p2 (Int.neg n2)

If p + n2 = p2 + n then the differences p - n and p2 - n2 are equal.

intNormNeg

def intNormNeg (pa : Pair (List (List Nat)) (List (List Nat))) : Pair (List (List Nat)) (List (List Nat))

Normal form of a negation: swaps the positive and negative parts.

intNormAdd

def intNormAdd (pa : Pair (List (List Nat)) (List (List Nat))) (pb : Pair (List (List Nat)) (List (List Nat))) : Pair (List (List Nat)) (List (List Nat))

Normal form of a sum from the already computed normal forms of its summands.

intNormMul

def intNormMul (pa : Pair (List (List Nat)) (List (List Nat))) (pb : Pair (List (List Nat)) (List (List Nat))) : Pair (List (List Nat)) (List (List Nat))

Normal form of a product from the already computed normal forms of its factors.

intNorm

def intNorm (e : IntExpr) : Pair (List (List Nat)) (List (List Nat))

Normalizes an integer expression into a pair (P, N) of nonnegative-coefficient polynomials meaning P - N.

intDiff

def intDiff (ρ : List Int) (pn : Pair (List (List Nat)) (List (List Nat))) : Int

Evaluates a normal-form pair (P, N) as the integer P - N.

intNormMulP

def intNormMulP (ρ : List Int) (a : IntExpr) (b : IntExpr) : polyEvalI ρ (fstPair (intNorm (imul a b))) = Int.add (Int.mul (polyEvalI ρ (fstPair (intNorm a))) (polyEvalI ρ (fstPair (intNorm b)))) (Int.mul (polyEvalI ρ (sndPair (intNorm a))) (polyEvalI ρ (sndPair (intNorm b))))

The positive part of a product’s normal form evaluates to PaPb + NaNb.

intNormMulN

def intNormMulN (ρ : List Int) (a : IntExpr) (b : IntExpr) : polyEvalI ρ (sndPair (intNorm (imul a b))) = Int.add (Int.mul (polyEvalI ρ (fstPair (intNorm a))) (polyEvalI ρ (sndPair (intNorm b)))) (Int.mul (polyEvalI ρ (sndPair (intNorm a))) (polyEvalI ρ (fstPair (intNorm b))))

The negative part of a product’s normal form evaluates to PaNb + NaPb.

intNormSound

def intNormSound (ρ : List Int) (e : IntExpr) : intDiff ρ (intNorm e) = intEval ρ e

Soundness of Int normalization: the normal form evaluates to the same value as the expression.

intCheckL

def intCheckL (a : IntExpr) (b : IntExpr) : List (List Nat)

Left side of the Int ring check for a = b: the polynomial P_a + N_b.

intCheckR

def intCheckR (a : IntExpr) (b : IntExpr) : List (List Nat)

Right side of the Int ring check for a = b: the polynomial P_b + N_a.

intRingEq

def intRingEq (ρ : List Int) (a : IntExpr) (b : IntExpr) (h : intCheckL a b = intCheckR a b) : intEval ρ a = intEval ρ b

Soundness of the Int ring checker: if the two check polynomials coincide, both expressions evaluate equally under every environment.