hex

3.2. Monomials and storage order🔗

An Hex.Mono is a fixed-length vector of natural-number exponents. The operations below are the building blocks for divisibility, S-polynomials, variable maps, and evaluation.

🔗def
Hex.Mono (n : ℕ) : Type
Hex.Mono (n : ℕ) : Type

An exponent vector for n ordered variables.

🔗def
Hex.Mono.mul {n : ℕ} (a b : Hex.Mono n) : Hex.Mono n
Hex.Mono.mul {n : ℕ} (a b : Hex.Mono n) :
  Hex.Mono n

Monomial multiplication, represented by pointwise exponent addition.

🔗def
Hex.Mono.dvd {n : ℕ} (a b : Hex.Mono n) : Bool
Hex.Mono.dvd {n : ℕ} (a b : Hex.Mono n) :
  Bool

Whether a divides b, i.e. whether every exponent of a is at most the corresponding exponent of b.

🔗def
Hex.Mono.div {n : ℕ} (a b : Hex.Mono n) : Option (Hex.Mono n)
Hex.Mono.div {n : ℕ} (a b : Hex.Mono n) :
  Option (Hex.Mono n)

The exact quotient b / a, returning none when a does not divide b.

🔗def
Hex.Mono.splits {n : ℕ} : Hex.Mono n → List (Hex.Mono n × Hex.Mono n)
Hex.Mono.splits {n : ℕ} :
  Hex.Mono n →
    List (Hex.Mono n × Hex.Mono n)

All decompositions a * b = m. Each exponent is split independently, so the list has ∏ i, (m[i] + 1) entries.

🔗def
Hex.Mono.prod.{u_1} {R : Type u_1} {n : ℕ} [One R] [Mul R]
  (x : Fin n → R) (m : Hex.Mono n) : R
Hex.Mono.prod.{u_1} {R : Type u_1} {n : ℕ}
  [One R] [Mul R] (x : Fin n → R)
  (m : Hex.Mono n) : R

Evaluate a monomial at x, using logarithmic exponentiation for each variable.

The named comparators Hex.Mono.lex, Hex.Mono.grlex, and Hex.Mono.grevlex are faithful total orders. Each also satisfies Hex.IsMonomialOrder, which adds the least-monomial, multiplicative-compatibility, and well-foundedness laws needed by leading-term and reduction algorithms.

🔗type class
Hex.IsMonomialOrder {n : ℕ} (cmp : Hex.Mono n → Hex.Mono n → Ordering) :
  Prop
Hex.IsMonomialOrder {n : ℕ}
  (cmp :
    Hex.Mono n → Hex.Mono n → Ordering) :
  Prop

Laws needed of a comparator by leading-term and reduction algorithms. Storage itself uses the inherited TransCmp and LawfulEqCmp laws.

Instance Constructor

Hex.IsMonomialOrder.mk

Extends

Methods

eq_swap : ∀ {a b : Hex.Mono n}, cmp a b = (cmp b a).swap
Inherited from
  1. Std.TransCmp cmp
  2. Std.LawfulEqCmp cmp
isLE_trans : ∀ {a b c : Hex.Mono n}, (cmp a b).isLE = true → (cmp b c).isLE = true → (cmp a c).isLE = true
Inherited from
  1. Std.TransCmp cmp
  2. Std.LawfulEqCmp cmp
compare_self : ∀ {a : Hex.Mono n}, cmp a a = Ordering.eq
Inherited from
  1. Std.TransCmp cmp
  2. Std.LawfulEqCmp cmp
eq_of_compare : ∀ {a b : Hex.Mono n}, cmp a b = Ordering.eq → a = b
Inherited from
  1. Std.TransCmp cmp
  2. Std.LawfulEqCmp cmp
zero_le : ∀ (m : Hex.Mono n), cmp Hex.Mono.zero m ≠ Ordering.gt

The constant monomial is least.

mul_mono : ∀ (a b c : Hex.Mono n), cmp a b = cmp (a.mul c) (b.mul c)

Multiplying both sides by the same monomial preserves comparison.

wf : WellFounded fun a b => cmp a b = Ordering.lt

Strict comparison is well founded.