mathlib3 documentation

tactic.omega.coeffs

source
@[simp]
def omega.coeffs.val_between (v : ℕ → ℤ) (as : list ℤ) (l : ℕ) :
ℕ → ℤ

val_between v as l o is the value (under valuation v) of the term obtained taking the term represented by (0, as) and dropping all subterms that include variables outside the range [l,l+o)

Equations
source
@[simp]
theorem omega.coeffs.val_between_nil {v : ℕ → ℤ} {l : ℕ} (m : ℕ) :
omega.coeffs.val_between v list.nil l m = 0
source
def omega.coeffs.val (v : ℕ → ℤ) (as : list ℤ) :
ℤ

Evaluation of the nonconstant component of a normalized linear arithmetic term.

Equations
source
@[simp]
theorem omega.coeffs.val_nil {v : ℕ → ℤ} :
omega.coeffs.val v list.nil = 0
source
theorem omega.coeffs.val_between_eq_of_le {v : ℕ → ℤ} {as : list ℤ} {l : ℕ} (m : ℕ) :
as.length ≤ l + m → omega.coeffs.val_between v as l m = omega.coeffs.val_between v as l (as.length - l)
source
theorem omega.coeffs.val_eq_of_le {v : ℕ → ℤ} {as : list ℤ} {k : ℕ} :
as.length ≤ k → omega.coeffs.val v as = omega.coeffs.val_between v as 0 k
source
theorem omega.coeffs.val_between_eq_val_between {v w : ℕ → ℤ} {as bs : list ℤ} {l m : ℕ} :
(∀ (x : ℕ), l ≤ x → x < l + m → v x = w x) → (∀ (x : ℕ), l ≤ x → x < l + m → list.func.get x as = list.func.get x bs) → omega.coeffs.val_between v as l m = omega.coeffs.val_between w bs l m
source
theorem omega.coeffs.val_between_set {v : ℕ → ℤ} {a : ℤ} {l n m : ℕ} :
l ≤ n → n < l + m → omega.coeffs.val_between v (list.func.set a list.nil n) l m = a * v n
source
@[simp]
theorem omega.coeffs.val_set {v : ℕ → ℤ} {m : ℕ} {a : ℤ} :
omega.coeffs.val v (list.func.set a list.nil m) = a * v m
source
theorem omega.coeffs.val_between_neg {v : ℕ → ℤ} {as : list ℤ} {l o : ℕ} :
omega.coeffs.val_between v (list.func.neg as) l o = -omega.coeffs.val_between v as l o
source
@[simp]
theorem omega.coeffs.val_neg {v : ℕ → ℤ} {as : list ℤ} :
omega.coeffs.val v (list.func.neg as) = -omega.coeffs.val v as
source
theorem omega.coeffs.val_between_add {v : ℕ → ℤ} {is js : list ℤ} {l : ℕ} (m : ℕ) :
omega.coeffs.val_between v (list.func.add is js) l m = omega.coeffs.val_between v is l m + omega.coeffs.val_between v js l m
source
@[simp]
theorem omega.coeffs.val_add {v : ℕ → ℤ} {is js : list ℤ} :
omega.coeffs.val v (list.func.add is js) = omega.coeffs.val v is + omega.coeffs.val v js
source
theorem omega.coeffs.val_between_sub {v : ℕ → ℤ} {is js : list ℤ} {l : ℕ} (m : ℕ) :
omega.coeffs.val_between v (list.func.sub is js) l m = omega.coeffs.val_between v is l m - omega.coeffs.val_between v js l m
source
@[simp]
theorem omega.coeffs.val_sub {v : ℕ → ℤ} {is js : list ℤ} :
omega.coeffs.val v (list.func.sub is js) = omega.coeffs.val v is - omega.coeffs.val v js
source
def omega.coeffs.val_except (k : ℕ) (v : ℕ → ℤ) (as : list ℤ) :
ℤ

val_except k v as is the value (under valuation v) of the term obtained taking the term represented by (0, as) and dropping the subterm that includes the kth variable.

Equations
source
theorem omega.coeffs.val_except_eq_val_except {k : ℕ} {is js : list ℤ} {v w : ℕ → ℤ} :
(∀ (x : ℕ), x ≠ k → v x = w x) → (∀ (x : ℕ), x ≠ k → list.func.get x is = list.func.get x js) → omega.coeffs.val_except k v is = omega.coeffs.val_except k w js
source
theorem omega.coeffs.val_except_update_set {v : ℕ → ℤ} {n : ℕ} {as : list ℤ} {i j : ℤ} :
omega.coeffs.val_except n (omega.update n i v) (list.func.set j as n) = omega.coeffs.val_except n v as
source
theorem omega.coeffs.val_between_add_val_between {v : ℕ → ℤ} {as : list ℤ} {l m n : ℕ} :
omega.coeffs.val_between v as l m + omega.coeffs.val_between v as (l + m) n = omega.coeffs.val_between v as l (m + n)
source
theorem omega.coeffs.val_except_add_eq {v : ℕ → ℤ} (n : ℕ) {as : list ℤ} :
omega.coeffs.val_except n v as + list.func.get n as * v n = omega.coeffs.val v as
source
@[simp]
theorem omega.coeffs.val_between_map_mul {v : ℕ → ℤ} {i : ℤ} {as : list ℤ} {l m : ℕ} :
omega.coeffs.val_between v (list.map (has_mul.mul i) as) l m = i * omega.coeffs.val_between v as l m
source
theorem omega.coeffs.forall_val_dvd_of_forall_mem_dvd {i : ℤ} {as : list ℤ} :
(∀ (x : ℤ), x ∈ as → i ∣ x) → ∀ (n : ℕ), i ∣ list.func.get n as
source
theorem omega.coeffs.dvd_val_between {v : ℕ → ℤ} {i : ℤ} {as : list ℤ} {l m : ℕ} :
(∀ (x : ℤ), x ∈ as → i ∣ x) → i ∣ omega.coeffs.val_between v as l m
source
theorem omega.coeffs.dvd_val {v : ℕ → ℤ} {as : list ℤ} {i : ℤ} :
(∀ (x : ℤ), x ∈ as → i ∣ x) → i ∣ omega.coeffs.val v as
source
@[simp]
theorem omega.coeffs.val_between_map_div {v : ℕ → ℤ} {as : list ℤ} {i : ℤ} {l : ℕ} (h1 : ∀ (x : ℤ), x ∈ as → i ∣ x) {m : ℕ} :
omega.coeffs.val_between v (list.map (λ (x : ℤ), x / i) as) l m = omega.coeffs.val_between v as l m / i
source
@[simp]
theorem omega.coeffs.val_map_div {v : ℕ → ℤ} {as : list ℤ} {i : ℤ} :
(∀ (x : ℤ), x ∈ as → i ∣ x) → omega.coeffs.val v (list.map (λ (x : ℤ), x / i) as) = omega.coeffs.val v as / i
source
theorem omega.coeffs.val_between_eq_zero {v : ℕ → ℤ} {is : list ℤ} {l m : ℕ} :
(∀ (x : ℤ), x ∈ is → x = 0) → omega.coeffs.val_between v is l m = 0
source
theorem omega.coeffs.val_eq_zero {v : ℕ → ℤ} {is : list ℤ} :
(∀ (x : ℤ), x ∈ is → x = 0) → omega.coeffs.val v is = 0