OAI/Combinatorics/BinaryEdit/TaggedExtraction.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TreeEdit.BinaryLower.TaggedExtraction.exists_maximum_matching line 16

   Source documentation

   Every canonical LCS is witnessed by a numerically indexed increasing matching.

   theorem exists_maximum_matching (x y : List α) :
       ∃ N : ℕ, N = lcs x y ∧ ∃ (u v : Fin N → ℕ)
         (hu : ∀ i, u i < x.length) (hv : ∀ i, v i < y.length),
         StrictMono u ∧ StrictMono v ∧
         (∀ i, x[u i]'(hu i) = y[v i]'(hv i)) := by
   …

   Mentions: OAI.TreeEdit.lcs

2. def OAI.TreeEdit.BinaryLower.TaggedExtraction.blocks line 28

   Source documentation

   A row obtained by concatenating equal-width blocks in increasing index order.

   def blocks {m B : ℕ} (X : Fin m → Word α B) : List α :=
   …

   Mentions: OAI.TreeEdit.Word

3. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.blocks_succ line 31
4. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.length_blocks line 35
5. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.block_index_lt line 44
6. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.getElem_blocks line 52

   Source documentation

   Indexing a concatenated row at block i and within-block position j.

   lemma getElem_blocks {m B : ℕ} (X : Fin m → Word α B) (i : Fin m) (j : Fin B) :
       (blocks X)[i.val * B + j.val]'(by rw [length_blocks]; exact block_index_lt i j) =
         (X i).val[j.val]'(by rw [(X i).property]; exact j.isLt) := by
   …

   Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.TaggedExtraction.blocks, OAI.TreeEdit.BinaryLower.TaggedExtraction.length_blocks, OAI.TreeEdit.BinaryLower.TaggedExtraction.block_index_lt

7. def OAI.TreeEdit.BinaryLower.TaggedExtraction.rows line 71

   Source documentation

   T rows of m blocks of width B.

   def rows {T m B : ℕ} (X : Fin T → Fin m → Word α B) : List α :=
   …

   Mentions: OAI.TreeEdit.Word

8. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.rows_eq_flatMap line 74
9. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.length_rows line 78
10. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.row_index_lt line 83
11. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.getElem_rows line 89

    Source documentation

    Indexed extraction of a cell from the literal concatenation of rows.

    lemma getElem_rows {T m B : ℕ} (X : Fin T → Fin m → Word α B)
        (a : Fin T) (i : Fin m) (j : Fin B) :
        (rows X)[a.val * (m * B) + (i.val * B + j.val)]'
          (by rw [length_rows]; exact row_index_lt a i j) =
          (X a i).val[j.val]'(by rw [(X a i).property]; exact j.isLt) := by
    …

    Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.TaggedExtraction.rows, OAI.TreeEdit.BinaryLower.TaggedExtraction.length_rows, OAI.TreeEdit.BinaryLower.TaggedExtraction.row_index_lt

12. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.row_quotient_lt line 99
13. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.row_quotient_decomposition line 104
14. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.getElem_rows_quotient line 113

    Source documentation

    Quotient/remainder form matching the numerical tagged-row geometric lemmas.

    lemma getElem_rows_quotient {T m B : ℕ} (X : Fin T → Fin m → Word α B)
        (hm : 0 < m) (hB : 0 < B) (p : ℕ) (hp : p < T * m * B) :
        (rows X)[p]'(by rw [length_rows]; exact hp) =
          (X ⟨p / B / m, row_quotient_lt hm hB hp⟩
             ⟨p / B % m, Nat.mod_lt _ hm⟩).val[p % B]'
            (by rw [(X _ _).property]; exact Nat.mod_lt _ hB) := by
    …

    Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.TaggedExtraction.rows, OAI.TreeEdit.BinaryLower.TaggedExtraction.length_rows, OAI.TreeEdit.BinaryLower.TaggedExtraction.row_quotient_lt

15. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.equal_symbols_same_tag line 126

    Source documentation

    Pairwise-disjoint letter tags force equal matched positions to have the same block index. The assumption is only cross-family disjointness; no row-boundary alignment is assumed.

    lemma equal_symbols_same_tag {T m B : ℕ}
        (X Y : Fin T → Fin m → Word α B) (hm : 0 < m) (hB : 0 < B)
        (hdisjoint : ∀ (a b : Fin T) (i j : Fin m) (s : α),
          s ∈ (X a i).val → s ∈ (Y b j).val → i = j)
        (p q : ℕ) (hp : p < T * m * B) (hq : q < T * m * B)
        (heq : (rows X)[p]'(by rw [length_rows]; exact hp) =
          (rows Y)[q]'(by rw [length_rows]; exact hq)) :
        p / B % m = q / B % m := by
    …

    Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.TaggedExtraction.rows, OAI.TreeEdit.BinaryLower.TaggedExtraction.length_rows

16. theorem OAI.TreeEdit.BinaryLower.TaggedExtraction.exists_maximum_row_matching line 149

    Source documentation

    A longest matching of tagged rows supplies the precise natural-coordinate interface used by the split-row gap bound, including the zero-match case.

    theorem exists_maximum_row_matching {T m B : ℕ}
        (X Y : Fin T → Fin m → Word α B) (hm : 0 < m) (hB : 0 < B)
        (hdisjoint : ∀ (a b : Fin T) (i j : Fin m) (s : α),
          s ∈ (X a i).val → s ∈ (Y b j).val → i = j) :
        ∃ N : ℕ, N = lcs (rows X) (rows Y) ∧
          ∃ (u v : Fin N → ℕ) (hu : ∀ i, u i < T * m * B)
            (hv : ∀ i, v i < T * m * B),
            StrictMono u ∧ StrictMono v ∧
            (∀ i, u i / B % m = v i / B % m) ∧
            (∀ i, (rows X)[u i]'(by rw [length_rows]; exact hu i) =
              (rows Y)[v i]'(by rw [length_rows]; exact hv i)) := by
    …

    Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.lcs, OAI.TreeEdit.BinaryLower.TaggedExtraction.rows, OAI.TreeEdit.BinaryLower.TaggedExtraction.length_rows

17. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.cross_disjoint_of_tags line 169

    Source documentation

    Ordered tags expressed as a single decoder imply the disjointness premise above.

    lemma cross_disjoint_of_tags {T m B : ℕ}
        (X Y : Fin T → Fin m → Word α B) (tag : α → Fin m)
        (hX : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (X a i).val → tag s = i)
        (hY : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (Y a i).val → tag s = i) :
        ∀ (a b : Fin T) (i j : Fin m) (s : α),
          s ∈ (X a i).val → s ∈ (Y b j).val → i = j := by
    …

    Mentions: OAI.TreeEdit.Word

18. lemma OAI.TreeEdit.BinaryLower.TaggedExtraction.equal_symbols_same_tag_of_decoder line 179

    Source documentation

    The global-symbol interface required by the tagged slice-alignment theorem.

    lemma equal_symbols_same_tag_of_decoder {T m B : ℕ}
        (X Y : Fin T → Fin m → Word α B) (tag : α → Fin m)
        (hX : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (X a i).val → tag s = i)
        (hY : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (Y a i).val → tag s = i)
        (hm : 0 < m) (hB : 0 < B)
        (p q : ℕ) (hp : p < T * m * B) (hq : q < T * m * B)
        (heq : (rows X)[p]'(by rw [length_rows]; exact hp) =
          (rows Y)[q]'(by rw [length_rows]; exact hq)) :
        p / B % m = q / B % m :=
    …

    Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.TaggedExtraction.rows, OAI.TreeEdit.BinaryLower.TaggedExtraction.length_rows