Theorem: List.splitOnListAux_r (One.lean)

State before:
α : Type u_1
acc : Array α
r rest : Array (Array α)
inst✝ : DecidableEq α
delim l : List α
h : delim ≠ []
⊢ splitOnListAux delim l acc (r ++ rest) h = r ++ splitOnListAux delim l acc rest h
Tactic:
induction l using List.induction_by_length_on generalizing acc r rest with
| h l ih =>
  unfold splitOnListAux
  split
  case h_1 =>
    simp only [Array.ext_iff, Array.push_data, Array.append_data, append_assoc]
  case h_2 head tail =>
    split
    case h_1 heq₂ =>
      simp only [length_cons, gt_iff_lt, Nat.lt_succ_self, ih]
    case h_2 rst heq₂ =>
      simp only
      have h₃: Array.push (r ++ rest) acc = r ++ (Array.push rest acc) := by
        simp only [Array.ext_iff, Array.push_data, Array.append_data, append_assoc]
      rw [h₃, ih]
      have h₄:= List.eq_append_of_getRest heq₂
      simp only [h₄, length_append, lt_add_iff_pos_left, zero_le, ge_iff_le, nonpos_iff_eq_zero,
        Nat.pos_iff_ne_zero, ne_eq, length_eq_zero, h, not_false_iff]
State after:
no goals

State before:
case h
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
l : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length l →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
acc : Array α
r rest : Array (Array α)
⊢ splitOnListAux delim l acc (r ++ rest) h = r ++ splitOnListAux delim l acc rest h
Tactic:
unfold splitOnListAux
State after:
case h
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
l : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length l →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
acc : Array α
r rest : Array (Array α)
⊢ (match _h₀ : l with
    | [] => Array.push (r ++ rest) acc
    | head :: tail =>
      match h : getRest l delim with
      | none => splitOnListAux delim tail (Array.push acc head) (r ++ rest) h
      | some rest_1 =>
        let_fun x := (_ : sizeOf rest_1 < sizeOf l);
        splitOnListAux delim rest_1 #[] (Array.push (r ++ rest) acc) h) =
    r ++
      match _h₀ : l with
      | [] => Array.push rest acc
      | head :: tail =>
        match h : getRest l delim with
        | none => splitOnListAux delim tail (Array.push acc head) rest h
        | some rest_1 =>
          let_fun x := (_ : sizeOf rest_1 < sizeOf l);
          splitOnListAux delim rest_1 #[] (Array.push rest acc) h

State before:
case h
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
l : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length l →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
acc : Array α
r rest : Array (Array α)
⊢ (match _h₀ : l with
    | [] => Array.push (r ++ rest) acc
    | head :: tail =>
      match h : getRest l delim with
      | none => splitOnListAux delim tail (Array.push acc head) (r ++ rest) h
      | some rest_1 =>
        let_fun x := (_ : sizeOf rest_1 < sizeOf l);
        splitOnListAux delim rest_1 #[] (Array.push (r ++ rest) acc) h) =
    r ++
      match _h₀ : l with
      | [] => Array.push rest acc
      | head :: tail =>
        match h : getRest l delim with
        | none => splitOnListAux delim tail (Array.push acc head) rest h
        | some rest_1 =>
          let_fun x := (_ : sizeOf rest_1 < sizeOf l);
          splitOnListAux delim rest_1 #[] (Array.push rest acc) h
Tactic:
split
State after:
case h.h_1
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
ih :
  ∀ (l₂ : List α),
    length l₂ < length [] →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
⊢ Array.push (r ++ rest) acc = r ++ Array.push rest acc

case h.h_2
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head✝ : α
tail✝ : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head✝ :: tail✝) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
⊢ (match h : getRest (head✝ :: tail✝) delim with
    | none => splitOnListAux delim tail✝ (Array.push acc head✝) (r ++ rest) h
    | some rest_1 =>
      let_fun x := (_ : sizeOf rest_1 < sizeOf (head✝ :: tail✝));
      splitOnListAux delim rest_1 #[] (Array.push (r ++ rest) acc) h) =
    r ++
      match h : getRest (head✝ :: tail✝) delim with
      | none => splitOnListAux delim tail✝ (Array.push acc head✝) rest h
      | some rest_1 =>
        let_fun x := (_ : sizeOf rest_1 < sizeOf (head✝ :: tail✝));
        splitOnListAux delim rest_1 #[] (Array.push rest acc) h

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
ih :
  ∀ (l₂ : List α),
    length l₂ < length [] →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
⊢ Array.push (r ++ rest) acc = r ++ Array.push rest acc
Tactic:
case h_1 =>
  simp only [Array.ext_iff, Array.push_data, Array.append_data, append_assoc]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
⊢ (match h : getRest (head :: tail) delim with
    | none => splitOnListAux delim tail (Array.push acc head) (r ++ rest) h
    | some rest_1 =>
      let_fun x := (_ : sizeOf rest_1 < sizeOf (head :: tail));
      splitOnListAux delim rest_1 #[] (Array.push (r ++ rest) acc) h) =
    r ++
      match h : getRest (head :: tail) delim with
      | none => splitOnListAux delim tail (Array.push acc head) rest h
      | some rest_1 =>
        let_fun x := (_ : sizeOf rest_1 < sizeOf (head :: tail));
        splitOnListAux delim rest_1 #[] (Array.push rest acc) h
Tactic:
case h_2 head tail =>
  split
  case h_1 heq₂ =>
    simp only [length_cons, gt_iff_lt, Nat.lt_succ_self, ih]
  case h_2 rst heq₂ =>
    simp only
    have h₃: Array.push (r ++ rest) acc = r ++ (Array.push rest acc) := by
      simp only [Array.ext_iff, Array.push_data, Array.append_data, append_assoc]
    rw [h₃, ih]
    have h₄:= List.eq_append_of_getRest heq₂
    simp only [h₄, length_append, lt_add_iff_pos_left, zero_le, ge_iff_le, nonpos_iff_eq_zero,
      Nat.pos_iff_ne_zero, ne_eq, length_eq_zero, h, not_false_iff]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
ih :
  ∀ (l₂ : List α),
    length l₂ < length [] →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
⊢ Array.push (r ++ rest) acc = r ++ Array.push rest acc
Tactic:
simp only [Array.ext_iff, Array.push_data, Array.append_data, append_assoc]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
⊢ (match h : getRest (head :: tail) delim with
    | none => splitOnListAux delim tail (Array.push acc head) (r ++ rest) h
    | some rest_1 =>
      let_fun x := (_ : sizeOf rest_1 < sizeOf (head :: tail));
      splitOnListAux delim rest_1 #[] (Array.push (r ++ rest) acc) h) =
    r ++
      match h : getRest (head :: tail) delim with
      | none => splitOnListAux delim tail (Array.push acc head) rest h
      | some rest_1 =>
        let_fun x := (_ : sizeOf rest_1 < sizeOf (head :: tail));
        splitOnListAux delim rest_1 #[] (Array.push rest acc) h
Tactic:
split
State after:
case h_1
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
heq✝ : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push acc head) (r ++ rest) h =
    r ++ splitOnListAux delim tail (Array.push acc head) rest h

case h_2
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
rest✝ : List α
heq✝ : getRest (head :: tail) delim = some rest✝
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push (r ++ rest) acc) h) =
    r ++
      let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push rest acc) h

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
heq₂ : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push acc head) (r ++ rest) h =
    r ++ splitOnListAux delim tail (Array.push acc head) rest h
Tactic:
case h_1 heq₂ =>
  simp only [length_cons, gt_iff_lt, Nat.lt_succ_self, ih]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
rst : List α
heq₂ : getRest (head :: tail) delim = some rst
⊢ (let_fun x := (_ : sizeOf rst < sizeOf (head :: tail));
    splitOnListAux delim rst #[] (Array.push (r ++ rest) acc) h) =
    r ++
      let_fun x := (_ : sizeOf rst < sizeOf (head :: tail));
      splitOnListAux delim rst #[] (Array.push rest acc) h
Tactic:
case h_2 rst heq₂ =>
  simp only
  have h₃: Array.push (r ++ rest) acc = r ++ (Array.push rest acc) := by
    simp only [Array.ext_iff, Array.push_data, Array.append_data, append_assoc]
  rw [h₃, ih]
  have h₄:= List.eq_append_of_getRest heq₂
  simp only [h₄, length_append, lt_add_iff_pos_left, zero_le, ge_iff_le, nonpos_iff_eq_zero,
    Nat.pos_iff_ne_zero, ne_eq, length_eq_zero, h, not_false_iff]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
heq₂ : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push acc head) (r ++ rest) h =
    r ++ splitOnListAux delim tail (Array.push acc head) rest h
Tactic:
simp only [length_cons, gt_iff_lt, Nat.lt_succ_self, ih]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
rst : List α
heq₂ : getRest (head :: tail) delim = some rst
⊢ (let_fun x := (_ : sizeOf rst < sizeOf (head :: tail));
    splitOnListAux delim rst #[] (Array.push (r ++ rest) acc) h) =
    r ++
      let_fun x := (_ : sizeOf rst < sizeOf (head :: tail));
      splitOnListAux delim rst #[] (Array.push rest acc) h
Tactic:
simp only
State after:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
rst : List α
heq₂ : getRest (head :: tail) delim = some rst
⊢ splitOnListAux delim rst #[] (Array.push (r ++ rest) acc) h =
    r ++ splitOnListAux delim rst #[] (Array.push rest acc) h

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
rst : List α
heq₂ : getRest (head :: tail) delim = some rst
⊢ splitOnListAux delim rst #[] (Array.push (r ++ rest) acc) h =
    r ++ splitOnListAux delim rst #[] (Array.push rest acc) h
Tactic:
have h₃: Array.push (r ++ rest) acc = r ++ (Array.push rest acc) := by
  simp only [Array.ext_iff, Array.push_data, Array.append_data, append_assoc]
State after:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
rst : List α
heq₂ : getRest (head :: tail) delim = some rst
h₃ : Array.push (r ++ rest) acc = r ++ Array.push rest acc
⊢ splitOnListAux delim rst #[] (Array.push (r ++ rest) acc) h =
    r ++ splitOnListAux delim rst #[] (Array.push rest acc) h

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
rst : List α
heq₂ : getRest (head :: tail) delim = some rst
h₃ : Array.push (r ++ rest) acc = r ++ Array.push rest acc
⊢ splitOnListAux delim rst #[] (Array.push (r ++ rest) acc) h =
    r ++ splitOnListAux delim rst #[] (Array.push rest acc) h
Tactic:
rw [h₃, ih]
State after:
case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
rst : List α
heq₂ : getRest (head :: tail) delim = some rst
h₃ : Array.push (r ++ rest) acc = r ++ Array.push rest acc
⊢ length rst < length (head :: tail)

State before:
case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
rst : List α
heq₂ : getRest (head :: tail) delim = some rst
h₃ : Array.push (r ++ rest) acc = r ++ Array.push rest acc
⊢ length rst < length (head :: tail)
Tactic:
have h₄:= List.eq_append_of_getRest heq₂
State after:
case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
rst : List α
heq₂ : getRest (head :: tail) delim = some rst
h₃ : Array.push (r ++ rest) acc = r ++ Array.push rest acc
h₄ : head :: tail = delim ++ rst
⊢ length rst < length (head :: tail)

State before:
case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
rst : List α
heq₂ : getRest (head :: tail) delim = some rst
h₃ : Array.push (r ++ rest) acc = r ++ Array.push rest acc
h₄ : head :: tail = delim ++ rst
⊢ length rst < length (head :: tail)
Tactic:
simp only [h₄, length_append, lt_add_iff_pos_left, zero_le, ge_iff_le, nonpos_iff_eq_zero,
  Nat.pos_iff_ne_zero, ne_eq, length_eq_zero, h, not_false_iff]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
r rest : Array (Array α)
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ {acc : Array α} {r rest : Array (Array α)},
        splitOnListAux delim l₂ acc (r ++ rest) h = r ++ splitOnListAux delim l₂ acc rest h
rst : List α
heq₂ : getRest (head :: tail) delim = some rst
⊢ Array.push (r ++ rest) acc = r ++ Array.push rest acc
Tactic:
simp only [Array.ext_iff, Array.push_data, Array.append_data, append_assoc]
State after:
no goals