OAI/Combinatorics/BinaryEdit/MatchingSegments.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TreeEdit.BinaryLower.segmentIndex line 8

   Source documentation

   Shift an index known to lie in a segment into that segment's index type.

   def segmentIndex {α : Type*} (x : List α) (start width : ℕ)
       (i : Fin x.length) (hlo : start ≤ (i : ℕ)) (hhi : (i : ℕ) < start + width) :
       Fin ((x.drop start).take width).length :=
   …

2. theorem OAI.TreeEdit.BinaryLower.get_segmentIndex line 18

   Source documentation

   Shifting indices into a list segment preserves the selected letter.

   theorem get_segmentIndex {α : Type*} (x : List α) (start width : ℕ)
       (i : Fin x.length) (hlo : start ≤ (i : ℕ)) (hhi : (i : ℕ) < start + width) :
       ((x.drop start).take width).get (segmentIndex x start width i hlo hhi) =
         x.get i := by
   …

   Mentions: OAI.TreeEdit.BinaryLower.segmentIndex

3. theorem OAI.TreeEdit.BinaryLower.matching_in_segments_le_lcs line 28

   Source documentation

   An increasing matching confined to two intervals is a common subsequence of the corresponding contiguous segments.

   theorem matching_in_segments_le_lcs {α : Type*} (x y : List α) {k : ℕ}
       (i : Fin k → Fin x.length) (j : Fin k → Fin y.length)
       (hi : StrictMono i) (hj : StrictMono j)
       (hlabel : ∀ t, x.get (i t) = y.get (j t))
       (a b p q : ℕ)
       (hi_lo : ∀ t, a ≤ (i t : ℕ)) (hi_hi : ∀ t, (i t : ℕ) < a + p)
       (hj_lo : ∀ t, b ≤ (j t : ℕ)) (hj_hi : ∀ t, (j t : ℕ) < b + q) :
       k ≤ lcs ((x.drop a).take p) ((y.drop b).take q) := by
   …

   Mentions: OAI.TreeEdit.lcs

4. theorem OAI.TreeEdit.BinaryLower.matching_subset_in_segments_le_lcs line 59

   Source documentation

   Restricting a matching to any finite collection of edges lying in two segments gives the same bound for the cardinality of that collection.

   theorem matching_subset_in_segments_le_lcs {α : Type*} (x y : List α) {k : ℕ}
       (i : Fin k → Fin x.length) (j : Fin k → Fin y.length)
       (hi : StrictMono i) (hj : StrictMono j)
       (hlabel : ∀ t, x.get (i t) = y.get (j t))
       (S : Finset (Fin k)) (a b p q : ℕ)
       (hi_lo : ∀ t ∈ S, a ≤ (i t : ℕ)) (hi_hi : ∀ t ∈ S, (i t : ℕ) < a + p)
       (hj_lo : ∀ t ∈ S, b ≤ (j t : ℕ)) (hj_hi : ∀ t ∈ S, (j t : ℕ) < b + q) :
       S.card ≤ lcs ((x.drop a).take p) ((y.drop b).take q) := by
   …

   Mentions: OAI.TreeEdit.lcs

5. theorem OAI.TreeEdit.BinaryLower.matching_subset_in_segments_le_lcs_nat line 77

   Source documentation

   Natural-index interface for span-counting arguments.

   theorem matching_subset_in_segments_le_lcs_nat {α : Type*} (x y : List α) {k : ℕ}
       (i j : Fin k → ℕ) (hi : StrictMono i) (hj : StrictMono j)
       (hix : ∀ t, i t < x.length) (hjy : ∀ t, j t < y.length)
       (hlabel : ∀ t, x.get ⟨i t, hix t⟩ = y.get ⟨j t, hjy t⟩)
       (S : Finset (Fin k)) (a b p q : ℕ)
       (hi_lo : ∀ t ∈ S, a ≤ i t) (hi_hi : ∀ t ∈ S, i t < a + p)
       (hj_lo : ∀ t ∈ S, b ≤ j t) (hj_hi : ∀ t ∈ S, j t < b + q) :
       S.card ≤ lcs ((x.drop a).take p) ((y.drop b).take q) := by
   …

   Mentions: OAI.TreeEdit.lcs

6. theorem OAI.TreeEdit.BinaryLower.common_sublist_in_segments line 91

   Source documentation

   An increasing matching confined to two intervals is a common subsequence of the corresponding contiguous segments.

   theorem common_sublist_in_segments {α : Type*} (x y : List α) {k : ℕ}
       (i : Fin k → Fin x.length) (j : Fin k → Fin y.length)
       (hi : StrictMono i) (hj : StrictMono j)
       (hlabel : ∀ t, x.get (i t) = y.get (j t))
       (a b p q : ℕ)
       (hi_lo : ∀ t, a ≤ (i t : ℕ)) (hi_hi : ∀ t, (i t : ℕ) < a + p)
       (hj_lo : ∀ t, b ≤ (j t : ℕ)) (hj_hi : ∀ t, (j t : ℕ) < b + q) :
       ∃ z : List α, z.Sublist ((x.drop a).take p) ∧
         z.Sublist ((y.drop b).take q) ∧ z.length = k := by
   …

7. theorem OAI.TreeEdit.BinaryLower.common_sublist_subset_in_segments line 122

   Source documentation

   Witness form of the restricted matching-to-segment bound.

   theorem common_sublist_subset_in_segments {α : Type*} (x y : List α) {k : ℕ}
       (i : Fin k → Fin x.length) (j : Fin k → Fin y.length)
       (hi : StrictMono i) (hj : StrictMono j)
       (hlabel : ∀ t, x.get (i t) = y.get (j t))
       (S : Finset (Fin k)) (a b p q : ℕ)
       (hi_lo : ∀ t ∈ S, a ≤ (i t : ℕ)) (hi_hi : ∀ t ∈ S, (i t : ℕ) < a + p)
       (hj_lo : ∀ t ∈ S, b ≤ (j t : ℕ)) (hj_hi : ∀ t ∈ S, (j t : ℕ) < b + q) :
       ∃ z : List α, z.Sublist ((x.drop a).take p) ∧
         z.Sublist ((y.drop b).take q) ∧ z.length = S.card := by
   …

8. theorem OAI.TreeEdit.BinaryLower.common_sublist_subset_ofFn_segments line 141

   Source documentation

   Raw fixed-length function interface for the segment witness.

   theorem common_sublist_subset_ofFn_segments {α : Type*} {n m k : ℕ}
       (x : Fin n → α) (y : Fin m → α)
       (i : Fin k → Fin n) (j : Fin k → Fin m)
       (hi : StrictMono i) (hj : StrictMono j)
       (hlabel : ∀ t, x (i t) = y (j t))
       (S : Finset (Fin k)) (a b p q : ℕ)
       (hi_lo : ∀ t ∈ S, a ≤ (i t : ℕ)) (hi_hi : ∀ t ∈ S, (i t : ℕ) < a + p)
       (hj_lo : ∀ t ∈ S, b ≤ (j t : ℕ)) (hj_hi : ∀ t ∈ S, (j t : ℕ) < b + q) :
       ∃ z : List α, z.Sublist (((List.ofFn x).drop a).take p) ∧
         z.Sublist (((List.ofFn y).drop b).take q) ∧ z.length = S.card := by
   …