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.

References

• [Wen-Tsun Wu, Basic principles of mechanical theorem proving in elementary geometries] [WT86]

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

@[instance_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

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

@[instance_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) : S.toList.Nodup

Set-like behavior

@[instance_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)

@[instance_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 }

@[instance_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

@[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' := ⋯ }

@[instance_reducible]

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

Equations

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

@[instance_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 σ] : ∅ = default

@[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 σ] : ∅.length = 0

@[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' := ⋯ }

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' := ⋯ }

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) : S.take 0 = ∅

@[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' := ⋯ }

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

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

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' := ⋯ }

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

@[simp]

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

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.

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