Positionwise agreement and dependence for lists

Two lists agree on a window of positions when their getElem? functions are Set.EqOn that window. Agreement on Set.Iic j transports truncations (Set.EqOn.take_eq), and agreement on Set.Ici j transports suffixes (Set.EqOn.drop_eq). List.DependsOn g K states that g : List α → γ is determined by the positions in K: equal-length inputs agreeing on K have equal images — the length-stratified sibling of Function.DependsOn, with the same congruence form as primary definition and the same factor-through characterization (List.dependsOn_iff_factorsThrough).

theorem List.take_eq_of_agree {α : Type u_1} {u v : List α} {i : ℕ} (h : ∀ (k : ℕ), k < i → u[k]? = v[k]?) : take i u = take i v

Prefixes agreeing below i have equal i-truncations.

theorem List.drop_eq_of_agree {α : Type u_1} {u v : List α} {i : ℕ} (h : ∀ (k : ℕ), i ≤ k → u[k]? = v[k]?) : drop i u = drop i v

Lists agreeing from i upward have equal i-suffixes.

def List.DependsOn {α : Type u_1} {γ : Type u_2} (g : List α → γ) (K : Set ℕ) : Prop

g is determined by the input positions in K: equal-length inputs agreeing on K have equal images. The length-stratified sibling of Function.DependsOn.

Equations

• List.DependsOn g K = ∀ ⦃u v : List α⦄, u.length = v.length → Set.EqOn (fun (x : ℕ) => u[x]?) (fun (x : ℕ) => v[x]?) K → g u = g v

theorem List.DependsOn.mono {α : Type u_1} {γ : Type u_2} {g : List α → γ} {K K' : Set ℕ} (hKK' : K ⊆ K') (h : DependsOn g K) : DependsOn g K'

def List.DependsAt {α : Type u_1} {γ : Type u_2} (g : List α → γ) (K : Set ℕ) (w : List α) : Prop

g is determined at w by the positions in K: any equal-length list agreeing with w on K has the same image. The pointwise form of List.DependsOn.

Equations

• List.DependsAt g K w = ∀ ⦃v : List α⦄, w.length = v.length → Set.EqOn (fun (x : ℕ) => w[x]?) (fun (x : ℕ) => v[x]?) K → g w = g v

theorem List.dependsOn_iff_forall_dependsAt {α : Type u_1} {γ : Type u_2} {g : List α → γ} {K : Set ℕ} : DependsOn g K ↔ ∀ (w : List α), DependsAt g K w

Window dependence is pointwise dependence everywhere.

theorem List.dependsOn_iff_factorsThrough {α : Type u_1} {γ : Type u_2} {g : List α → γ} {K : Set ℕ} : DependsOn g K ↔ Function.FactorsThrough g fun (u : List α) => (u.length, K.restrict fun (x : ℕ) => u[x]?)

g factors through the input's length and its restriction to K.

theorem Set.EqOn.getElem?_eq {α : Type u_1} {u v : List α} {s : Set ℕ} {k : ℕ} (h : EqOn (fun (x : ℕ) => u[x]?) (fun (x : ℕ) => v[x]?) s) (hk : k ∈ s) : u[k]? = v[k]?

The pointwise application of window agreement, stated in getElem? form so it rewrites cleanly.

theorem Set.EqOn.take_eq {α : Type u_1} {u v : List α} {i j : ℕ} (h : EqOn (fun (x : ℕ) => u[x]?) (fun (x : ℕ) => v[x]?) (Iic j)) (hij : i ≤ j + 1) : List.take i u = List.take i v

Agreement on positions up to j transports truncations: h.take_eq for h : Set.EqOn (u[·]?) (v[·]?) (Set.Iic j).

theorem Set.EqOn.drop_eq {α : Type u_1} {u v : List α} {i j : ℕ} (h : EqOn (fun (x : ℕ) => u[x]?) (fun (x : ℕ) => v[x]?) (Ici j)) (hij : j ≤ i) : List.drop i u = List.drop i v

Agreement on positions from j transports suffixes: h.drop_eq for h : Set.EqOn (u[·]?) (v[·]?) (Set.Ici j).