EditMetric.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TreeEdit.BinaryLower.EditStep.length_le line 13
theorem OAI.TreeEdit.BinaryLower.EditScript.length_le line 21
theorem OAI.TreeEdit.BinaryLower.EditScript.replace_all line 29
Source documentation
Replace corresponding symbols, then insert or delete the leftover tail. This uses at most the larger word length, including the empty-word cases.
```
theorem replace_all (x y : List α) :
    EditScript x y (max x.length y.length) := by
…
```
Mentions: OAI.TreeEdit.EditScript
theorem OAI.TreeEdit.BinaryLower.length_le_length_add_editDistance line 45
theorem OAI.TreeEdit.BinaryLower.editDistance_pos_iff line 49
Source documentation
Positivity of ordinary edit distance does not require an inhabited alphabet.
```
theorem editDistance_pos_iff {x y : List α} : 0 < ed x y ↔ x ≠ y := by
…
```
Mentions: OAI.TreeEdit.ed
theorem OAI.TreeEdit.BinaryLower.editDistance_le_max_length line 52
theorem OAI.TreeEdit.BinaryLower.editDistance_nil_right line 55
theorem OAI.TreeEdit.BinaryLower.editDistance_nil_left line 60

inductive OAI.TreeEdit.BinaryLower.StrictEditScript line 65

Source documentation

Genuine changes only: this excludes the harmless identity substitutions permitted by EditStep.

inductive StrictEditScript : List α → List α → ℕ → Prop
  | nil (x : List α) : StrictEditScript x x 0
  | cons {x y z : List α} {n : ℕ} :
      EditStep x y → x ≠ y → StrictEditScript y z n → StrictEditScript x z (n + 1)

namespace StrictEditScript

Mentions: OAI.TreeEdit.EditStep

theorem OAI.TreeEdit.BinaryLower.StrictEditScript.toScript line 72
theorem OAI.TreeEdit.BinaryLower.EditScript.strict_of_optimal line 81
Source documentation
A minimum script never needs a redundant same-symbol substitution.
```
theorem EditScript.strict_of_optimal {x y : List α} {n : ℕ}
    (h : EditScript x y n) (hmin : ed x y = n) : StrictEditScript x y n := by
…
```
Mentions: OAI.TreeEdit.EditScript, OAI.TreeEdit.ed, OAI.TreeEdit.BinaryLower.StrictEditScript
theorem OAI.TreeEdit.BinaryLower.exists_optimal_strict_script line 96
theorem OAI.TreeEdit.BinaryLower.editDistance_eq_strict_minimum line 102
Source documentation
Thus the concrete definition is unchanged if substitutions are required to change their symbol, exactly as in the ordinary edit convention.
```
theorem editDistance_eq_strict_minimum (x y : List α) :
    ed x y = sInf {n : ℕ | StrictEditScript x y n} := by
…
```
Mentions: OAI.TreeEdit.ed, OAI.TreeEdit.BinaryLower.StrictEditScript