CheapTranslations.lean`

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Inexpensive translations

Elementary unrestricted edit scripts give the translation estimates in lem:finite-cost.

theorem OAI.TreeEdit.BinaryLower.CheapTranslations.unitEdit_prefix line 21
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.script_prefix line 31
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.unitEdit_suffix line 37
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.script_suffix line 50
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.script_trans line 56
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.script_delete_prefix line 65
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.script_insert_prefix line 72
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.script_insert_suffix line 79
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.editDistance_le_script line 83
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.editDistance_prefix_suffix line 89
Source documentation
Retain a common middle word, delete the initial segment and insert the terminal segment. Intermediate words are not subject to any length cap.
```
theorem editDistance_prefix_suffix (p x s : List α) :
    ed (p ++ x) (x ++ s) ≤ p.length + s.length := by
…
```
Mentions: OAI.TreeEdit.ed
def OAI.TreeEdit.BinaryLower.CheapTranslations.rowWindow line 95
Source documentation
A consecutive finite window of rows, concatenated in increasing order.
```
def rowWindow (rows : ℕ → List α) (start count : ℕ) : List α :=
…
```
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.rowWindow_add line 98
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.rowWindow_shift_index line 104
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.rowWindow_length line 114
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.script_rowWindow_shift line 128
Source documentation
An explicit script for sliding a fixed number of rows. Its exact cost is useful when the same local operation is repeated in a larger concatenation.
```
theorem script_rowWindow_shift (rows : ℕ → List α)
    (a T s B : ℕ) (hs : s ≤ T)
    (hlen : ∀ j, (rows j).length = B) :
    EditScript (rowWindow rows a T) (rowWindow rows (a + s) T)
      (2 * s * B) := by
…
```
Mentions: OAI.TreeEdit.EditScript, OAI.TreeEdit.BinaryLower.CheapTranslations.rowWindow
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.editDistance_rowWindow_shift line 153
Source documentation
Sliding T equally long rows by s ≤ T retains the middle T-s rows and costs at most 2*s*B edits.
```
theorem editDistance_rowWindow_shift (rows : ℕ → List α)
    (a T s B : ℕ) (hs : s ≤ T)
    (hlen : ∀ j, (rows j).length = B) :
    ed (rowWindow rows a T) (rowWindow rows (a + s) T) ≤
      2 * s * B :=
…
```
Mentions: OAI.TreeEdit.ed, OAI.TreeEdit.BinaryLower.CheapTranslations.rowWindow
def OAI.TreeEdit.BinaryLower.CheapTranslations.orbitRows line 162
Source documentation
The row word arising from repeated translation in an additive parameter space. This is the row operation in both tree constructions.
```
def orbitRows {A : Type v} [AddMonoid A] (row : A → List α)
    (x u : A) (T : ℕ) : List α :=
…
```
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.orbitRows_shift line 166
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.script_orbitRows_shift line 181
Source documentation
An additive state translation by s*u is the exact row-window script, also when x already includes offsets contributed by ancestor nodes.
```
theorem script_orbitRows_shift {A : Type v} [AddMonoid A]
    (row : A → List α) (x u : A) (T s B : ℕ) (hs : s ≤ T)
    (hlen : ∀ y, (row y).length = B) :
    EditScript (orbitRows row x u T) (orbitRows row (x + s • u) u T)
      (2 * s * B) := by
…
```
Mentions: OAI.TreeEdit.EditScript, OAI.TreeEdit.BinaryLower.CheapTranslations.orbitRows
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.editDistance_orbitRows_shift line 191
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.script_map_mismatches line 201
Source documentation
Substituting exactly the differing positions gives a script whose cost is the Hamming mismatch count; repeated positions in xs are counted with their multiplicity, as required for leaf occurrences in the tree words.
```
theorem script_map_mismatches {β : Type v} [DecidableEq β]
    (xs : List α) (f g : α → β) :
    EditScript (xs.map f) (xs.map g)
      (xs.countP fun a => decide (f a ≠ g a)) := by
…
```
Mentions: OAI.TreeEdit.EditScript
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.editDistance_map_le_mismatches line 214
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.script_map_supported line 224
Source documentation
If a change is supported on a Boolean predicate, one substitution at each supported occurrence suffices. No decidable equality on the output alphabet is needed, and harmless substitutions at unchanged supported occurrences are allowed by the ordinary-script definition.
```
theorem script_map_supported {β : Type v} (xs : List α)
    (f g : α → β) (p : α → Bool)
    (hfg : ∀ a ∈ xs, p a = false → f a = g a) :
    EditScript (xs.map f) (xs.map g) (xs.countP p) := by
…
```
Mentions: OAI.TreeEdit.EditScript
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.editDistance_map_le_support line 243
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.script_flatMap line 252
Source documentation
Scripts in corresponding concatenated blocks add their costs. This allows a local row translation to be performed separately at every copy of a descendant word, without altering the other blocks.
```
theorem script_flatMap {ι : Type v} (indices : List ι)
    (f g : ι → List α) (cost : ι → ℕ)
    (h : ∀ i ∈ indices, EditScript (f i) (g i) (cost i)) :
    EditScript (indices.flatMap f) (indices.flatMap g)
      ((indices.map cost).sum) := by
…
```
Mentions: OAI.TreeEdit.EditScript
theorem OAI.TreeEdit.BinaryLower.CheapTranslations.editDistance_flatMap_le_cost line 268