Documentation

CharacteristicSet.TriangularSet

Triangular Set #

This file defines the structure of a Triangular Set of multivariate polynomials. A Triangular Set is a finite ordered sequence of non-zero polynomials [P₁, P₂, ..., Pₘ] such that their main (max) variables are strictly increasing: mainVar(P₁) < mainVar(P₂) < ... < mainVar(Pₘ).

Main Definitions #

TriangularSet: The structure definition. It bundles the list, the proofs of non-zero elements and ascending main variables.

Main Results #

TriangularSet.takeConcat_lt_of_reducedToSet: Appending a reduced element strictly decreases the order, used to prove termination of basic set algorithms.

structure TriangularSet (σ : Type u_1) (R : Type u_2) [CommSemiring R] [LinearOrder σ] :

Type (max u_1 u_2)

A Triangular Set is a list of polynomials with strictly increasing main variables.

toList : List (MvPolynomial σ R)
The underlying list of non-zero polynomials
zero_notMem' : 0 ∉ self.toList
No polynomial in the list is zero
isChain_max_vars' : List.IsChain (fun (x1 x2 : MvPolynomial σ R) => x1.vars.max < x2.vars.max) self.toList
The main variables of successive polynomials are strictly increasing

Instances For

def TriangularSet.mk' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {l : List (MvPolynomial σ R)} (hl1 : 0 ∉ l) (hl2 : List.IsChain (fun (x1 x2 : MvPolynomial σ R) => x1.vars.max < x2.vars.max) l) :

TriangularSet σ R

Construct an triangular set from a list.

Equations

TriangularSet.mk' hl1 hl2 = { toList := l, zero_notMem' := hl1, isChain_max_vars' := hl2 }

Instances For

@[implicit_reducible]

noncomputable instance TriangularSet.instFunLike {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

FunLike (TriangularSet σ R) ℕ (MvPolynomial σ R)

Equations

TriangularSet.instFunLike = { coe := fun (S : TriangularSet σ R) (n : ℕ) => S.toList[n]?.getD 0, coe_injective' := ⋯ }

theorem TriangularSet.ext {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} (h : ∀ (i : ℕ), S i = T i) :

S = T

theorem TriangularSet.ext_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} :

S = T ↔ ∀ (i : ℕ), S i = T i

def TriangularSet.length {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

The length of the triangular set.

Equations

S.length = S.toList.length

Instances For

theorem TriangularSet.ne_zero_iff_lt_length {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} :

n < S.length ↔ S n ≠ 0

theorem TriangularSet.eq_zero_iff_length_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} :

S.length ≤ n ↔ S n = 0

theorem TriangularSet.ext' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} (h1 : S.length = T.length) (h2 : ∀ i < S.length, S i = T i) :

S = T

@[simp]

theorem TriangularSet.apply_length_eq_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} :

S S.length = 0

theorem TriangularSet.toList_getElem?_getD {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} :

S.toList[n]?.getD 0 = S n

theorem TriangularSet.toList_getElem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} (h : n < S.length) :

S.toList[n] = S n

@[simp]

theorem TriangularSet.length_toList {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

S.toList.length = S.length

@[simp]

theorem TriangularSet.toList_eq_iff_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} :

S.toList = T.toList ↔ S = T

theorem TriangularSet.mem_toList_iff' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} :

p ∈ S.toList ↔ ∃ n < S.length, S n = p

theorem TriangularSet.zero_notMem_toList {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

0 ∉ S.toList

theorem TriangularSet.toList_non_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) ⦃p : MvPolynomial σ R⦄ :

p ∈ S.toList → p ≠ 0

theorem TriangularSet.toList_isChain {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

List.IsChain (fun (x1 x2 : MvPolynomial σ R) => x1.vars.max < x2.vars.max) S.toList

theorem TriangularSet.toList_pairwise {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

List.Pairwise (fun (x1 x2 : MvPolynomial σ R) => x1.vars.max < x2.vars.max) S.toList

@[implicit_reducible]

instance TriangularSet.instDecidableEqOfMvPolynomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq (MvPolynomial σ R)] :

DecidableEq (TriangularSet σ R)

Equations

x✝¹.instDecidableEqOfMvPolynomial x✝ = decidable_of_iff (x✝¹.toList = x✝.toList) ⋯

theorem TriangularSet.max_vars_lt_next {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} (h : n < S.length - 1) :

(S n).vars.max < (S (n + 1)).vars.max

theorem TriangularSet.max_vars_lt_next' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} :

n + 1 < S.length → (S n).vars.max < (S (n + 1)).vars.max

theorem TriangularSet.max_vars_lt_next'' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} :

0 < n → n < S.length → (S (n - 1)).vars.max < (S n).vars.max

theorem TriangularSet.max_vars_lt_of_index_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {m n : ℕ} (h : n < S.length) :

m < n → (S m).vars.max < (S n).vars.max

theorem TriangularSet.index_lt_of_max_vars_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {m n : ℕ} (h : m < S.length) :

(S m).vars.max < (S n).vars.max → m < n

theorem TriangularSet.false_of_max_vars_ge_of_index_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {m n : ℕ} :

m < n → n < S.length → (S n).vars.max ≤ (S m).vars.max → False

theorem TriangularSet.max_vars_le_of_index_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {m n : ℕ} :

m ≤ n → n < S.length → (S m).vars.max ≤ (S n).vars.max

theorem TriangularSet.index_eq_of_max_vars_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {m n : ℕ} :

m < S.length → n < S.length → (S m).vars.max = (S n).vars.max → m = n

theorem TriangularSet.index_eq_of_apply_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {m n : ℕ} :

m < S.length → n < S.length → S m = S n → m = n

theorem TriangularSet.index_eq_zero_of_max_vars_eq_bot {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} :

n < S.length → (S n).vars.max = ⊥ → n = 0

theorem TriangularSet.exists_index_max_vars_between_of_max_vars_first_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : (S 0).vars.max < p.vars.max) :

∃ k ≤ S.length, (S (k - 1)).vars.max < p.vars.max ∧ (p.vars.max ≤ (S k).vars.max ∨ k = S.length)

theorem TriangularSet.toList_nodup {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

Set-like behavior #

@[implicit_reducible]

instance TriangularSet.instSetLike {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

SetLike (TriangularSet σ R) (MvPolynomial σ R)

Equations

TriangularSet.instSetLike = { coe := fun (S : TriangularSet σ R) => {p : MvPolynomial σ R | ∃ n < S.length, S n = p}, coe_injective' := ⋯ }

theorem TriangularSet.mem_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} :

p ∈ S ↔ ∃ n < S.length, S n = p

@[simp]

theorem TriangularSet.mem_toList_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} :

p ∈ S.toList ↔ p ∈ S

@[simp]

theorem TriangularSet.zero_notMem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

0 ∉ S

theorem TriangularSet.ne_zero_of_mem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} :

p ∈ S → p ≠ 0

theorem TriangularSet.apply_mem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} :

n < S.length → S n ∈ S

theorem TriangularSet.forall_mem_iff_forall_index {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {a : MvPolynomial σ R → Prop} :

(∀ p ∈ S, a p) ↔ ∀ i < S.length, a (S i)

theorem TriangularSet.forall_mem_iff_forall_index' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {a : MvPolynomial σ R → Prop} {n : ℕ} (h : n = S.length) :

(∀ p ∈ S, a p) ↔ ∀ (i : Fin n), a (S ↑i)

theorem TriangularSet.exists_mem_iff_exists_index {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {a : MvPolynomial σ R → Prop} :

(∃ p ∈ S, a p) ↔ ∃ i < S.length, a (S i)

theorem TriangularSet.exists_mem_iff_exists_index' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {a : MvPolynomial σ R → Prop} {n : ℕ} (h : n = S.length) :

(∃ p ∈ S, a p) ↔ ∃ (i : Fin n), a (S ↑i)

@[implicit_reducible]

instance TriangularSet.instHasSubset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

HasSubset (TriangularSet σ R)

Equations

TriangularSet.instHasSubset = { Subset := fun (S T : TriangularSet σ R) => ∀ ⦃x : MvPolynomial σ R⦄, x ∈ S → x ∈ T }

@[implicit_reducible]

instance TriangularSet.instHasSSubset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

HasSSubset (TriangularSet σ R)

Equations

TriangularSet.instHasSSubset = { SSubset := fun (S T : TriangularSet σ R) => S ⊆ T ∧ ¬T ⊆ S }

@[simp]

theorem TriangularSet.Subset.refl {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

S ⊆ S

theorem TriangularSet.Subset.trans {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T U : TriangularSet σ R} :

S ⊆ T → T ⊆ U → S ⊆ U

theorem TriangularSet.subset_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} :

S ⊆ T ↔ ∀ ⦃x : MvPolynomial σ R⦄, x ∈ S → x ∈ T

theorem TriangularSet.mem_of_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} (p : MvPolynomial σ R) (h : S ⊆ T) :

p ∈ S → p ∈ T

theorem TriangularSet.ssubset_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} :

S ⊂ T ↔ S ⊆ T ∧ ¬T ⊆ S

def TriangularSet.toFinset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

Finset (MvPolynomial σ R)

Converts a triangular set to a finite set.

Equations

S.toFinset = Finset.map { toFun := fun (i : Fin S.toList.length) => S.toList[i], inj' := ⋯ } Finset.univ

Instances For

@[simp]

theorem TriangularSet.card_toFinset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

S.toFinset.card = S.length

@[simp]

theorem TriangularSet.mem_toFinset_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} :

p ∈ S.toFinset ↔ p ∈ S

@[simp]

theorem TriangularSet.toFinset_eq_iff_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} :

S.toFinset = T.toFinset ↔ S = T

theorem TriangularSet.toFinset_eq_coe_set {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

↑S.toFinset = ↑S

theorem TriangularSet.length_le_of_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} :

S ⊆ T → S.length ≤ T.length

theorem TriangularSet.length_lt_of_ssubset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} :

S ⊂ T → S.length < T.length

def TriangularSet.empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

TriangularSet σ R

The empty triangular set.

Equations

TriangularSet.empty = { toList := [], zero_notMem' := ⋯, isChain_max_vars' := ⋯ }

Instances For

@[implicit_reducible]

instance TriangularSet.instEmptyCollection {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

EmptyCollection (TriangularSet σ R)

Equations

TriangularSet.instEmptyCollection = { emptyCollection := TriangularSet.empty }

@[implicit_reducible]

instance TriangularSet.instInhabited {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

Inhabited (TriangularSet σ R)

Equations

TriangularSet.instInhabited = { default := ∅ }

theorem TriangularSet.empty_eq_default {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

@[simp]

theorem TriangularSet.toList_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

∅.toList = []

@[simp]

theorem TriangularSet.length_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :

@[simp]

theorem TriangularSet.empty_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {n : ℕ} :

∅ n = 0

theorem TriangularSet.length_eq_zero_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} :

S.length = 0 ↔ S = ∅

theorem TriangularSet.length_gt_zero_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} :

0 < S.length ↔ S ≠ ∅

theorem TriangularSet.length_ge_one_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} :

1 ≤ S.length ↔ S ≠ ∅

theorem TriangularSet.notMem_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (p : MvPolynomial σ R) :

p ∉ ∅

theorem TriangularSet.eq_empty_of_forall_notMem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} :

(∀ (p : MvPolynomial σ R), p ∉ S) → S = ∅

def TriangularSet.single' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} (hp : p ≠ 0) :

TriangularSet σ R

A triangular set with exactly one non-zero element.

Equations

TriangularSet.single' hp = { toList := [p], zero_notMem' := ⋯, isChain_max_vars' := ⋯ }

Instances For

theorem TriangularSet.toList_single' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} (hp : p ≠ 0) :

(single' hp).toList = [p]

theorem TriangularSet.single'_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} {n : ℕ} (hp : p ≠ 0) :

(single' hp) n = if n = 0 then p else 0

theorem TriangularSet.length_single' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} (hp : p ≠ 0) :

(single' hp).length = 1

def TriangularSet.take {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) (n : ℕ) :

TriangularSet σ R

Takes the first n elements of a triangular set.

Equations

S.take n = { toList := List.take n S.toList, zero_notMem' := ⋯, isChain_max_vars' := ⋯ }

Instances For

theorem TriangularSet.toList_take {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) (n : ℕ) :

(S.take n).toList = List.take n S.toList

@[simp]

theorem TriangularSet.length_take {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) (n : ℕ) :

(S.take n).length = min n S.length

theorem TriangularSet.take_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) (n m : ℕ) :

(S.take n) m = if m < n then S m else 0

theorem TriangularSet.take_apply' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n m : ℕ} (h : m < min n S.length) :

(S.take n) m = S m

@[simp]

theorem TriangularSet.take_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

@[simp]

theorem TriangularSet.take_length {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

S.take S.length = S

theorem TriangularSet.take_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) (n : ℕ) :

S.take n ⊆ S

def TriangularSet.drop {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) (n : ℕ) :

TriangularSet σ R

Drops the first n elements of a triangular set.

Equations

S.drop n = { toList := List.drop n S.toList, zero_notMem' := ⋯, isChain_max_vars' := ⋯ }

Instances For

theorem TriangularSet.toList_drop {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) (n : ℕ) :

(S.drop n).toList = List.drop n S.toList

@[simp]

theorem TriangularSet.length_drop {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) (n : ℕ) :

(S.drop n).length = S.length - n

@[simp]

theorem TriangularSet.drop_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) (n m : ℕ) :

(S.drop n) m = S (n + m)

@[simp]

theorem TriangularSet.drop_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

S.drop 0 = S

theorem TriangularSet.drop_eq_empty_of_ge_length {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} :

S.length ≤ n → S.drop n = ∅

@[simp]

theorem TriangularSet.drop_length {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) :

S.drop S.length = ∅

@[reducible, inline]

abbrev TriangularSet.CanConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) (p : MvPolynomial σ R) :

The condition required to append p to S while maintaining the Triangular Set property. p must be non-zero and its main variable must be strictly greater than the main variable of the last element of S.

Equations

S.CanConcat p = (p ≠ 0 ∧ (0 < S.length → (S (S.length - 1)).vars.max < p.vars.max))

Instances For

theorem TriangularSet.canConcat_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} :

S.CanConcat p ↔ p ≠ 0 ∧ (0 < S.length → (S (S.length - 1)).vars.max < p.vars.max)

theorem TriangularSet.empty_canConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} :

p ≠ 0 → ∅.CanConcat p

theorem TriangularSet.not_canConcat_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} :

¬S.CanConcat 0

def TriangularSet.concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) (p : MvPolynomial σ R) (h : S.CanConcat p := by assumption) :

TriangularSet σ R

Appends a polynomial p to the end of S. Requires S.canConcat p.

Equations

S.concat p h = { toList := S.toList.concat p, zero_notMem' := ⋯, isChain_max_vars' := ⋯ }

Instances For

theorem TriangularSet.toList_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) :

(S.concat p h).toList = S.toList.concat p

@[simp]

theorem TriangularSet.length_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) :

(S.concat p h).length = S.length + 1

theorem TriangularSet.concat_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) (n : ℕ) :

(S.concat p h) n = if n < S.length then S n else if n = S.length then p else 0

theorem TriangularSet.concat_apply_length {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) :

(S.concat p h) S.length = p

theorem TriangularSet.mem_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) :

p ∈ S.concat p h

theorem TriangularSet.subset_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) :

S ⊆ S.concat p h

theorem TriangularSet.mem_concat_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p q : MvPolynomial σ R} (h : S.CanConcat p) :

q ∈ S.concat p h ↔ q = p ∨ q ∈ S

theorem TriangularSet.coe_concat_eq_insert {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) :

↑(S.concat p h) = Set.insert p ↑S

noncomputable def TriangularSet.single {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (p : MvPolynomial σ R) :

TriangularSet σ R

A triangular set with exactly one element.

Equations

TriangularSet.single p = if h : p = 0 then ∅ else TriangularSet.single' h

Instances For

@[simp]

theorem TriangularSet.single_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] :

theorem TriangularSet.length_single {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {p : MvPolynomial σ R} :

p ≠ 0 → (single p).length = 1

theorem TriangularSet.single_eq_zero_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {p : MvPolynomial σ R} :

p = 0 ↔ single p = ∅

theorem TriangularSet.length_single_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {p : MvPolynomial σ R} :

p = 0 → (single p).length = 0

theorem TriangularSet.length_single_le_one {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {p : MvPolynomial σ R} :

(single p).length ≤ 1

theorem TriangularSet.single_apply_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (p : MvPolynomial σ R) :

(single p) 0 = p

theorem TriangularSet.single_apply_nonzero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {n : ℕ} [DecidableEq R] (p : MvPolynomial σ R) :

n ≠ 0 → (single p) n = 0

theorem TriangularSet.mem_single_of_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {p : MvPolynomial σ R} :

p ≠ 0 → p ∈ single p

theorem TriangularSet.notMem_single_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {p q : MvPolynomial σ R} :

q ≠ p → q ∉ single p

theorem TriangularSet.single_of_length_le_one {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} :

S.length ≤ 1 → S = single (S 0)

theorem TriangularSet.single_of_last_max_vars_eq_bot {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} :

(S (S.length - 1)).vars.max = ⊥ → S = single (S 0)

noncomputable def TriangularSet.takeConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (S : TriangularSet σ R) (p : MvPolynomial σ R) :

TriangularSet σ R

takeConcat S p tries to construct a new Triangular Set by taking a prefix of S and appending p. This is a key operation in constructing the Characteristic Set. If p fits naturally at the end of S, it behaves like S.concat p. If p conflicts with some element in S (in terms of main variable order), takeConcat finds the first element in S that has a higher or equal main variable than p, truncates S before that element, and appends p.

Equations

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

Instances For

theorem TriangularSet.takeConcat_eq_concat_of_canConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) :

S.takeConcat p = S.concat p h

theorem TriangularSet.takeConcat_zero_eq_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (S : TriangularSet σ R) :

S.takeConcat 0 = ∅

theorem TriangularSet.mem_takeConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (S : TriangularSet σ R) {p : MvPolynomial σ R} (h : p ≠ 0) :

p ∈ S.takeConcat p

theorem TriangularSet.takeConcat_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} {p : MvPolynomial σ R} (q : MvPolynomial σ R) :

q ∈ S.takeConcat p → q ≠ p → q ∈ S