def Tokens.ListHelpers.split_at_prim {α : Type} (n : Nat) (acc ls : List α) : Option (List α × α × List α)

Equations

• Tokens.ListHelpers.split_at_prim Nat.zero acc (x :: xs) = some (acc, x, xs)
• Tokens.ListHelpers.split_at_prim pn.succ acc (x :: xs) = Tokens.ListHelpers.split_at_prim pn (acc ++ [x]) xs
• Tokens.ListHelpers.split_at_prim n acc ls = none

theorem Tokens.ListHelpers.split_less_length {α : Type} {n : Nat} {ls : List α} (acc : List α) (HL : n < ls.length) : ∃ (pre : List α), ∃ (a : α), ∃ (pos : List α), split_at_prim n acc ls = some (pre, a, pos)

theorem Tokens.ListHelpers.split_less_length' {α : Type} {n : Nat} {pre pos ls : List α} {a : α} (acc : List α) (HSplit : split_at_prim n acc ls = some (pre, a, pos)) : n < ls.length

theorem Tokens.ListHelpers.split_at_prim_nil {α : Type} {n : Nat} {acc : List α} : split_at_prim n acc [] = none

theorem Tokens.ListHelpers.split_at_prim_head {α : Type} {acc : List α} {hd : α} {tl : List α} : split_at_prim 0 acc (hd :: tl) = some (acc, hd, tl)

theorem Tokens.ListHelpers.split_at_prime_correct {α : Type} {n : Nat} {ls : List α} {x : α} {acc pre pos : List α} (H : split_at_prim n acc ls = some (pre, x, pos)) : pre ++ x :: pos = acc ++ ls

theorem Tokens.ListHelpers.split_at_prim_greater_length {α : Type} {n : Nat} {ls : List α} (acc : List α) (gt : ls.length ≤ n) : split_at_prim n acc ls = none

theorem Tokens.ListHelpers.split_at_prim_greater_length' {α : Type} {n : Nat} {ls acc : List α} (HN : split_at_prim n acc ls = none) : ls.length ≤ n

theorem Tokens.ListHelpers.split_at_prim_plus_concat {α : Type} {ls acc acc' : List α} {x : α} : split_at_prim acc'.length acc (acc' ++ x :: ls) = some (acc ++ acc', x, ls)

theorem Tokens.ListHelpers.split_at_prim_concat {α : Type} {n : Nat} {ls acc acc' : List α} : split_at_prim n (acc ++ acc') ls = split_at_prim (n + acc'.length) acc (acc' ++ ls)

theorem Tokens.ListHelpers.split_at_prim_concat_zero {α : Type} {ls acc acc' : List α} : split_at_prim 0 (acc ++ acc') ls = split_at_prim acc'.length acc (acc' ++ ls)

theorem Tokens.ListHelpers.split_at_prim_concat' {α : Type} {n : Nat} {ls acc acc' : List α} : split_at_prim n (acc ++ acc') ls = split_at_prim (acc'.length + n) acc (acc' ++ ls)

theorem Tokens.ListHelpers.split_at_prim_pre_length {α : Type} {n : Nat} {ls pre pos acc : List α} {x : α} (HS : split_at_prim n acc ls = some (pre, x, pos)) : pre.length = n + acc.length

theorem Tokens.ListHelpers.split_at_focus {α : Type} {n : Nat} {acc pre pos : List α} {x : α} (Hpre : pre.length = n) : split_at_prim n acc (pre ++ x :: pos) = some (acc ++ pre, x, pos)

theorem Tokens.ListHelpers.split_at_focus' {α : Type} {n : Nat} {acc pre pos : List α} {x : α} (Hpre : pre.length = n) : split_at_prim n acc (pre ++ [x] ++ pos) = some (acc ++ pre, x, pos)

theorem Tokens.ListHelpers.split_at_acc_irrelevant {α : Type} {n : Nat} {acc ls : List α} : Option.map (fun (x : List α × α × List α) => x.snd.fst) (split_at_prim n acc ls) = Option.map (fun (x : List α × α × List α) => x.snd.fst) (split_at_prim n [] ls)

def Tokens.ListHelpers.split_at {α : Type} (n : Nat) (ls : List α) : Option (List α × α × List α)

Equations

• Tokens.ListHelpers.split_at n ls = Tokens.ListHelpers.split_at_prim n [] ls

theorem Tokens.ListHelpers.split_at_succ_head {α : Type} {n : Nat} {hd : α} {tl : List α} : (fun (x : List α × α × List α) => x.snd.fst) <$> split_at n.succ (hd :: tl) = (fun (x : List α × α × List α) => x.snd.fst) <$> split_at n tl

theorem Tokens.ListHelpers.split_at_correct {α : Type} {n : Nat} {ls : List α} {x : α} {pre pos : List α} (H : split_at n ls = some (pre, x, pos)) : pre ++ x :: pos = ls

theorem Tokens.ListHelpers.split_at_lt_length {α : Type} {n : Nat} {pre pos ls : List α} {a : α} (HSplit : split_at n ls = some (pre, a, pos)) : n < ls.length

theorem Tokens.ListHelpers.split_at_pre_length {α : Type} {n : Nat} {ls pre pos : List α} {x : α} (HS : split_at n ls = some (pre, x, pos)) : pre.length = n

theorem Tokens.ListHelpers.split_at_ext_concat {α : Type} {n : Nat} {ls pre pos : List α} {v : α} (H : split_at n ls = some (pre, v, pos)) (ext : List α) : split_at n (ls ++ ext) = some (pre, v, pos ++ ext)

theorem Tokens.ListHelpers.split_at_left_concat {α : Type} {n : Nat} {l r : List α} (HL : n < l.length) : Option.map (fun (x : List α × α × List α) => match x with | (fst, v, snd) => v) (split_at n (l ++ r)) = Option.map (fun (x : List α × α × List α) => match x with | (fst, v, snd) => v) (split_at n l)

theorem Tokens.ListHelpers.split_at_right_concat {α : Type} {n : Nat} {l r : List α} (HL : l.length ≤ n) : Option.map (fun (x : List α × α × List α) => match x with | (fst, v, snd) => v) (split_at n (l ++ r)) = Option.map (fun (x : List α × α × List α) => match x with | (fst, v, snd) => v) (split_at (n - l.length) r)