@[reducible, inline]

abbrev AtCoder.Segtree.WF' {α : Type u_1} {n : ℕ} [Monoid α] (data : Vector α (n * 2)) (k : ℕ) (h' : 1 ≤ k := by get_elem_tactic) : Prop

Equations

• AtCoder.Segtree.WF' data k h' = ∀ (i : ℕ) (h : k ≤ i ∧ i < n), data[i] = data[i * 2] * data[i * 2 + 1]

@[reducible, inline]

abbrev AtCoder.Segtree.WF {α : Type u_1} {n : ℕ} [Monoid α] (data : Vector α (n * 2)) : Prop

Equations

• AtCoder.Segtree.WF data = AtCoder.Segtree.WF' data 1 AtCoder.Segtree.WF.proof_1

structure AtCoder.Segtree (α : Type) [Monoid α] (n : ℕ) : Type

• mk' :: (
• data : Vector α (n * 2)
• wf : WF self.data
• )

def AtCoder.Segtree.mk {α : Type} [Monoid α] (n : ℕ) : Segtree α n

Equations

• AtCoder.Segtree.mk n = { data := Vector.mkVector (n * 2) 1, wf := ⋯ }

theorem AtCoder.Segtree.updateAt_WF' {α : Type} [Monoid α] {n : ℕ} (data : Vector α (n * 2)) (k : ℕ) (hk : k < n) (hk' : 1 ≤ k) (h : WF' data (k + 1) ⋯) : WF' (AtCoder.Segtree.updateAt✝ k data hk) k hk'

def AtCoder.Segtree.build {α : Type} [Monoid α] {n : ℕ} (data : Vector α n) : Segtree α n

Equations

• AtCoder.Segtree.build data = AtCoder.Segtree.build'✝ (⋯ ▸ (Vector.mkVector n 1 ++ data))

def AtCoder.Segtree.get {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (i : Fin n) : α

Equations

• t.get i = t.data[↑i + n]

instance AtCoder.Segtree.instGetElemNatLt {α : Type} [Monoid α] {n : ℕ} : GetElem (Segtree α n) ℕ α fun (x : Segtree α n) (i : ℕ) => i < n

Equations

• AtCoder.Segtree.instGetElemNatLt = { getElem := fun (x : AtCoder.Segtree α n) (i : ℕ) (h : i < n) => x.get ⟨i, h⟩ }

theorem AtCoder.Segtree.get_eq_get' {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (i : ℕ) (h : i < n) : t[i] = t.data[i + n]

@[reducible, inline]

abbrev AtCoder.Segtree.WF_without {α : Type} [Monoid α] {n : ℕ} (data : Vector α (n * 2)) (i : ℕ) : Prop

Equations

• AtCoder.Segtree.WF_without data i = ∀ (j : ℕ), i ≠ j → ∀ (h : 1 ≤ j ∧ j < n), data[j] = data[j * 2] * data[j * 2 + 1]

theorem AtCoder.Segtree.WF_without_WF {α : Type} [Monoid α] {n i : ℕ} {data : Vector α (n * 2)} (hwf : WF data) : WF_without data i

theorem AtCoder.Segtree.WF_WF_without_zero {α : Type} [Monoid α] {n : ℕ} {data : Vector α (n * 2)} (hwf : WF_without data 0) : WF data

theorem AtCoder.Segtree.WF_without_set {α : Type} [Monoid α] {n : ℕ} (data : Vector α (n * 2)) (i : ℕ) (v : α) (h : i < n) (hwf : WF data) : WF_without (data.set (i + n) v ⋯) ((i + n) / 2)

theorem AtCoder.Segtree.WF_without_updateAt {α : Type} [Monoid α] {n : ℕ} (data : Vector α (n * 2)) (i : ℕ) (h : i < n) (hwf : WF_without data i) : WF_without (AtCoder.Segtree.updateAt✝ i data h) (i / 2)

def AtCoder.Segtree.set {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (i : ℕ) (v : α) (h : i < n := by get_elem_tactic) : Segtree α n

Equations

• t.set i v h = AtCoder.Segtree.Vector.buildAt✝ (t.data.set (i + n) v ⋯) ((i + n) / 2) ⋯ ⋯

def AtCoder.Segtree.modify {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (i : ℕ) (f : α → α) (h : i < n := by get_elem_tactic) : Segtree α n

Equations

• t.modify i f h = t.set i (f t[i]) h

@[simp]

theorem AtCoder.Segtree.get_updateAt_ne {α : Type} [Monoid α] {n : ℕ} (data : Vector α (n * 2)) (i j : ℕ) (h : i < n) (h' : j < n * 2) (h'' : i ≠ j) : (AtCoder.Segtree.updateAt✝ i data h)[j] = data[j]

@[simp]

theorem AtCoder.Segtree.buildAt_keep_larger {α : Type} [Monoid α] {n : ℕ} (data : Vector α (n * 2)) (i : ℕ) (hwf : WF_without data i) (h : i < n) (k : ℕ) (h' : i < k ∧ k < n * 2) : (AtCoder.Segtree.Vector.buildAt✝ data i hwf h).data[k] = data[k]

theorem AtCoder.Segtree.get_set_self {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (i : ℕ) (v : α) (h : i < n) : (t.set i v h)[i] = v

theorem AtCoder.Segtree.get_set_ne {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (i j : ℕ) (v : α) (hi : i < n) (hj : j < n) (h' : i ≠ j) : (t.set i v hi)[j] = t[j]

def AtCoder.Segtree.fold_all {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) : α

Equations

• t.fold_all = if x : n = 0 then 1 else t.data[1]

@[irreducible]

def AtCoder.Segtree.fold_aux {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (l r : ℕ) (p q : α) (h : 1 ≤ l ∧ l ≤ r ∧ r ≤ n * 2 := by get_elem_tactic) : α

Equations

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

def AtCoder.Segtree.fold {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (l r : ℕ) (h : 0 ≤ l ∧ l ≤ r ∧ r ≤ n := by get_elem_tactic) : α

Equations

• t.fold l r h = if x : n = 0 then 1 else t.fold_aux (l + n) (r + n) 1 1 ⋯

@[irreducible]

def AtCoder.Segtree.fold_naive {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (l r : ℕ) (h : 0 ≤ l ∧ l ≤ r ∧ r ≤ n := by get_elem_tactic) : α

Equations

• t.fold_naive l r h = if x : l = r then 1 else t[l] * t.fold_naive (l + 1) r ⋯

theorem AtCoder.Segtree.fold_naive'_def {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (l r : ℕ) (h : 1 ≤ l ∧ l < r ∧ r ≤ n * 2) : AtCoder.Segtree.fold_naive'✝ t l r ⋯ = t.data[l] * AtCoder.Segtree.fold_naive'✝ t (l + 1) r ⋯

@[simp]

theorem AtCoder.Segtree.fold_naive_one {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (i : ℕ) (h : 0 ≤ i ∧ i ≤ n) : t.fold_naive i i ⋯ = 1

@[simp]

theorem AtCoder.Segtree.fold_naive'_one {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (i : ℕ) (h : 1 ≤ i ∧ i ≤ n * 2) : AtCoder.Segtree.fold_naive'✝ t i i ⋯ = 1

@[irreducible]

def AtCoder.Segtree.leftmost {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (i : ℕ) (h : 1 ≤ i ∧ i < 2 * n := by get_elem_tactic) : ℕ

Equations

• t.leftmost i h = if x : i < n then t.leftmost (i * 2) ⋯ else i

@[irreducible]

theorem AtCoder.Segtree.leftmost_lower {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (i : ℕ) (h : 1 ≤ i ∧ i < 2 * n) : t.leftmost i h ≥ n

@[irreducible]

theorem AtCoder.Segtree.leftmost_upper {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (i : ℕ) (h : 1 ≤ i ∧ i < 2 * n) : t.leftmost i h < 2 * n

@[irreducible]

theorem AtCoder.Segtree.fold_naive_eq_fold_naive' {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (l r : ℕ) (h : 0 ≤ l ∧ l ≤ r ∧ r ≤ n) (h' : n ≥ 1) : t.fold_naive l r h = AtCoder.Segtree.fold_naive'✝ t (l + n) (r + n) ⋯

@[irreducible]

theorem AtCoder.Segtree.fold_naive'_double {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (l r : ℕ) (h : 1 ≤ l ∧ l ≤ r ∧ r ≤ n) : AtCoder.Segtree.fold_naive'✝ t l r ⋯ = AtCoder.Segtree.fold_naive'✝ t (l * 2) (r * 2) ⋯

@[simp, irreducible]

theorem AtCoder.Segtree.fold_naive'_r {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (l r : ℕ) (h : 1 ≤ l ∧ l ≤ r ∧ r < n * 2) : AtCoder.Segtree.fold_naive'✝ t l r ⋯ * t.data[r] = AtCoder.Segtree.fold_naive'✝ t l (r + 1) ⋯

@[irreducible]

theorem AtCoder.Segtree.fold_aux_eq_fold_naive' {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (l r : ℕ) (p q : α) (h' : 1 ≤ l ∧ l ≤ r ∧ r ≤ n * 2) : t.fold_aux l r p q h' = p * AtCoder.Segtree.fold_naive'✝ t l r h' * q

theorem AtCoder.Segtree.fold_eq_fold_naive {α : Type} [Monoid α] {n : ℕ} (t : Segtree α n) (l r : ℕ) (h : 0 ≤ l ∧ l ≤ r ∧ r ≤ n) : t.fold l r h = t.fold_naive l r h