Edges of a word

An Edge is an end of a word, left for its beginning and right for its end. The same two values name a scan by the end it starts from, and a side of a position by the end it faces. This file gives the length-k part of a word at an edge, the positions within a distance of a target on one side, and the reverse conjugation that exchanges the two edges on string functions.

Main definitions

• Edge, Edge.swap: the left or right end of a word, and the other one.
• Edge.takeAt: the length-k prefix or suffix of a word.
• Edge.window: the positions not far from a target on one side.
• List.revConj: conjugation of a string function by reversal.

inductive Edge : Type

An Edge is an end of a word, left for its beginning and right for its end. A scan is named by the edge it starts from, so the left scan reads a word from its beginning and the right scan from its end. The two scans give function classes that are mirror images under reversal but differ as classes of functions on unreversed strings.

• left : Edge
• right : Edge

@[instance_reducible]

instance instDecidableEqEdge : DecidableEq Edge

Equations

• instDecidableEqEdge x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance instReprEdge : Repr Edge

Equations

• instReprEdge = { reprPrec := instReprEdge.repr }

def instReprEdge.repr : Edge → ℕ → Std.Format

Equations

• instReprEdge.repr Edge.left prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Edge.left")).group prec✝
• instReprEdge.repr Edge.right prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Edge.right")).group prec✝

@[instance_reducible]

instance instFintypeEdge : Fintype Edge

Equations

• instFintypeEdge = { elems := { val := ↑Edge.enumList, nodup := Edge.enumList_nodup }, complete := instFintypeEdge._proof_1 }

def Edge.swap : Edge → Edge

The other edge.

Equations

• Edge.left.swap = Edge.right
• Edge.right.swap = Edge.left

@[simp]

theorem Edge.swap_left : left.swap = right

@[simp]

theorem Edge.swap_right : right.swap = left

@[simp]

theorem Edge.swap_swap (e : Edge) : e.swap.swap = e

theorem Edge.swap_involutive : Function.Involutive swap

Edge substrings

def Edge.takeAt {α : Type u_1} (e : Edge) (k : ℕ) (xs : List α) : List α

The length-k part of xs at an edge, its prefix List.take at the left and its suffix List.rtake at the right. A word shorter than k is returned in full.

Equations

• Edge.left.takeAt k xs = List.take k xs
• Edge.right.takeAt k xs = xs.rtake k

@[simp]

theorem Edge.takeAt_left {α : Type u_1} (k : ℕ) (xs : List α) : left.takeAt k xs = List.take k xs

@[simp]

theorem Edge.takeAt_right {α : Type u_1} (k : ℕ) (xs : List α) : right.takeAt k xs = xs.rtake k

theorem Edge.length_takeAt {α : Type u_1} (e : Edge) (k : ℕ) (xs : List α) : (e.takeAt k xs).length = min k xs.length

An edge substring has length min k xs.length.

theorem Edge.takeAt_of_length_le {α : Type u_1} (e : Edge) {k : ℕ} {xs : List α} (h : xs.length ≤ k) : e.takeAt k xs = xs

For a short string the edge substring is the whole string.

theorem Edge.takeAt_left_append_of_le_length {α : Type u_1} {k : ℕ} (p rest : List α) (h : k ≤ p.length) : left.takeAt k (p ++ rest) = left.takeAt k p

The left-k-prefix of p ++ rest is that of p, when k ≤ p.length.

theorem Edge.takeAt_right_append_of_le_length {α : Type u_1} {k : ℕ} (x rest : List α) (h : k ≤ rest.length) : right.takeAt k (x ++ rest) = right.takeAt k rest

The right-k-suffix of x ++ rest is that of rest, when k ≤ rest.length.

theorem Edge.takeAt_idem {α : Type u_1} (e : Edge) (k : ℕ) (xs : List α) : e.takeAt k (e.takeAt k xs) = e.takeAt k xs

takeAt k is idempotent, since its output already has length at most k.

theorem Edge.takeAt_takeAt_of_le {α : Type u_1} (e : Edge) {k k' : ℕ} (h : k ≤ k') (xs : List α) : e.takeAt k (e.takeAt k' xs) = e.takeAt k xs

A shorter edge substring of a longer one is the shorter edge substring.

theorem Edge.takeAt_eq_of_le {α : Type u_1} (e : Edge) {k k' : ℕ} (h : k ≤ k') {xs xs' : List α} (hxs : e.takeAt k' xs = e.takeAt k' xs') : e.takeAt k xs = e.takeAt k xs'

Words with the same edge substring of some length have the same shorter ones.

theorem Edge.takeAt_takeAt_append {α : Type u_1} (e : Edge) (k : ℕ) (xs ys : List α) : e.takeAt k (e.takeAt k xs ++ ys) = e.takeAt k (xs ++ ys)

Truncating the first factor of a concatenation to its edge substring leaves the edge substring of the whole unchanged.

theorem Edge.takeAt_append_congr {α : Type u_1} (e : Edge) {k : ℕ} {xs xs' : List α} (h : e.takeAt k xs = e.takeAt k xs') (ys : List α) : e.takeAt k (xs ++ ys) = e.takeAt k (xs' ++ ys)

Words with the same edge substring keep the same one after appending a word.

theorem Edge.takeAt_append_takeAt {α : Type u_1} (e : Edge) (k : ℕ) (xs ys : List α) : e.takeAt k (xs ++ e.takeAt k ys) = e.takeAt k (xs ++ ys)

Truncating the second factor of a concatenation to its edge substring leaves the edge substring of the whole unchanged.

theorem Edge.takeAt_append_congr_right {α : Type u_1} (e : Edge) {k : ℕ} {ys ys' : List α} (h : e.takeAt k ys = e.takeAt k ys') (xs : List α) : e.takeAt k (xs ++ ys) = e.takeAt k (xs ++ ys')

Words with the same edge substring keep the same one after prepending a word.

theorem Edge.takeAt_map {α : Type u_1} (e : Edge) (k : ℕ) (xs : List α) {β : Type u_2} (g : α → β) : e.takeAt k (List.map g xs) = List.map g (e.takeAt k xs)

Mapping a function over a word maps it over the edge substring.

theorem Edge.finite_range_takeAt {α : Type u_1} (e : Edge) (k : ℕ) [Finite α] : (Set.range (e.takeAt k)).Finite

Over a finite alphabet there are finitely many edge substrings of a given length.

Windows

def Edge.window : Edge → ℕ → ℕ → Set ℕ

The input positions not d-far from the target i on the side of an edge.

Equations

• Edge.left.window x✝¹ x✝ = Set.Ici (x✝¹ - x✝)
• Edge.right.window x✝¹ x✝ = Set.Iic (x✝¹ + x✝)

@[simp]

theorem Edge.window_left {i d : ℕ} : left.window i d = Set.Ici (i - d)

@[simp]

theorem Edge.window_right {i d : ℕ} : right.window i d = Set.Iic (i + d)

Reverse conjugation

Exchanging the two edges acts on string functions by reverse conjugation. The right-scan function classes are the List.revConj-images of the left-scan ones, so their theory transports along the involution.

def List.revConj {α : Type u_2} {β : Type u_3} (f : List α → List β) : List α → List β

Conjugation by List.reverse computes on the reversed input and reverses the result.

Equations

• List.revConj f xs = (f xs.reverse).reverse

@[simp]

theorem List.revConj_revConj {α : Type u_2} {β : Type u_3} (f : List α → List β) : revConj (revConj f) = f

theorem List.revConj_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : List β → List γ) (f : List α → List β) : revConj (g ∘ f) = revConj g ∘ revConj f

@[simp]

theorem List.revConj_id {α : Type u_2} : revConj id = id

@[simp]

theorem List.revConj_map {α : Type u_2} {β : Type u_3} (h : α → β) : revConj (map h) = map h

theorem List.preimage_revConj {α : Type u_2} {β : Type u_3} (f : List α → List β) (L : Language β) : revConj f ⁻¹' L = Language.reverse (f ⁻¹' L.reverse)

Pulling a language back along a reverse-conjugate reverses the pullback of the reversed language.

theorem List.revConj_eq_iff {α : Type u_2} {β : Type u_3} {h f : List α → List β} : revConj h = f ↔ h = revConj f