Standard Ascending Set (Ritt's Definition)

This file implements the theory and algorithm for Standard Ascending Set. In this context, a "Standard Ascending Set" requires that every element is reduced with respect to preceding elements.

Main declarations

• AscendingSetTheory: Implements the theory using reducedTo (strong reduction).
• HasBasicSet: Provides the basicSet algorithm that computes a minimal standard ascending set from a list of polynomials.

References

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

theorem StandardAscendingSet.isAscendingSet_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangularSet σ R} : IsAscendingSet S ↔ ∀ ⦃i j : ℕ⦄, i < j → j < S.length → (S j).reducedTo (S i)

theorem StandardAscendingSet.isAscendingSet_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangularSet σ R} : IsAscendingSet S ↔ ∀ ⦃i j : ℕ⦄, i < j → i < S.length → (S j).reducedTo (S i)

theorem StandardAscendingSet.reducedTo_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangularSet σ R} {i j : ℕ} (h : IsAscendingSet S) : i ≠ j → j < S.length → (S i).reducedTo (S j)

@[implicit_reducible]

noncomputable def StandardAscendingSet.instAscendingSetTheory {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] : AscendingSetTheory σ R

The standard ascending set theory uses strong reduction reducedTo.

Equations

• StandardAscendingSet.instAscendingSetTheory = { reducedTo' := MvPolynomial.reducedTo, decidableReducedTo := inferInstance, initial_reducedToSet_of_max_vars_ne_bot := ⋯ }

theorem StandardAscendingSet.isAscendingSet_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) (hp : p.reducedToSet S) : S.IsAscendingSet → (S.concat p h).IsAscendingSet

theorem StandardAscendingSet.isAscendingSet_takeConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (hp : p.reducedToSet S) : S.IsAscendingSet → (S.takeConcat p).IsAscendingSet

@[irreducible]

noncomputable def StandardAscendingSet.basicSet.go {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) : TriangularSet σ R

The recursive algorithm for computing the Standard Basic Set.

Equations

• One or more equations did not get rendered due to their size.
• StandardAscendingSet.basicSet.go [] BS hl1_2 = BS

noncomputable def StandardAscendingSet.basicSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) : TriangularSet σ R

Computes the Standard Basic Set of a list of polynomials. The algorithm works by:

1. Sort the list and let BS = ∅.
2. Pick the first (minimal) element B in the list.
3. Update the current basic set BS with B using takeConcat (which handles replacements).
4. Filter the remaining list to keep only elements reduced w.r.t. the new BS and go to step 2.

Equations

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

theorem StandardAscendingSet.basicSetGo_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (h : l ≠ []) (hl2 : (l.head h).reducedToSet BS) : basicSet.go l BS hl1 < BS

theorem StandardAscendingSet.basicSetGo_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : Option.all (fun (p : MvPolynomial σ R) => decide (p.reducedToSet BS)) l.head? = true) : basicSet.go l BS hl1 ≤ BS

theorem StandardAscendingSet.mem_of_mem_basicSetGo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (p : MvPolynomial σ R) : p ∉ BS → p ∈ basicSet.go l BS hl1 → p ∈ l

theorem StandardAscendingSet.basicSetGo_isAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) : Option.all (fun (p : MvPolynomial σ R) => decide (p.reducedToSet BS)) l.head? = true → BS.IsAscendingSet → (basicSet.go l BS hl1).IsAscendingSet

theorem StandardAscendingSet.basicSetGo_le_ascendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) : List.Pairwise (fun (x1 x2 : MvPolynomial σ R) => x1 ≤ x2) l → (∀ p ∈ l, BS.CanConcat p) → Option.all (fun (x : MvPolynomial σ R) => decide (x.reducedToSet BS)) l.head? = true → ∀ (T : TriangularSet σ R), T.IsAscendingSet → (BS.length ≤ T.length ∧ ∀ i < BS.length, BS i ≈ T i) → (∀ p ∈ T, (∀ i < BS.length, ¬BS i ≈ p) → p ∈ l) → basicSet.go l BS hl1 ≤ T

The core lemma proving that the computed Basic Set is indeed minimal among all ascending sets contained in l.

theorem StandardAscendingSet.basicSet_isAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) : (basicSet l).IsAscendingSet

theorem StandardAscendingSet.basicSet_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) ⦃p : MvPolynomial σ R⦄ : p ∈ basicSet l → p ∈ l

theorem StandardAscendingSet.basicSet_minimal {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) ⦃S : TriangularSet σ R⦄ : S.IsAscendingSet → (∀ ⦃p : MvPolynomial σ R⦄, p ∈ S → p ∈ l) → basicSet l ≤ S

@[implicit_reducible]

noncomputable def StandardAscendingSet.instHasBasicSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] : HasBasicSet σ R

The Standard Basic Set algorithm satisfies the abstract HasBasicSet interface.

Equations

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