OAI/Combinatorics/BinaryEdit/MatchingSublist.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TreeEdit.BinaryLower.ofFn_get_sublist line 10

   Source documentation

   Strictly increasing index selections produce sublists.

   theorem ofFn_get_sublist {α : Type*} (x : List α) {k : ℕ}
       (i : Fin k → Fin x.length) (hi : StrictMono i) :
       (List.ofFn (fun t => x.get (i t))).Sublist x := by
   …

2. theorem OAI.TreeEdit.BinaryLower.common_sublist_of_strict_matching line 23

   Source documentation

   A matching described by two increasing index maps is a common sublist with exactly as many symbols as matched index pairs.

   theorem common_sublist_of_strict_matching {α : 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)) :
       ∃ z : List α, z.Sublist x ∧ z.Sublist y ∧ z.length = k := by
   …

3. theorem OAI.TreeEdit.BinaryLower.matching_length_le_lcs line 35

   Source documentation

   Every increasing matching has size at most the longest common subsequence.

   theorem matching_length_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)) : k ≤ lcs x y := by
   …

   Mentions: OAI.TreeEdit.lcs