internlm/Lean-Github huggingface dataset:
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ Array.modifyHead (Array.append (Array.push acc head)) (splitOnListAux delim tail #[] #[] h) =
    Array.modifyHead (Array.append acc)
      (Array.modifyHead (Array.append (Array.push #[] head)) (splitOnListAux delim tail #[] #[] h))

case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)

case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)
Tactic:
. simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.append_eq_append]
  cases (splitOnListAux delim tail #[] #[] h).data with
  | nil => simp only
  | cons => 
    simp only [cons.injEq, Array.ext_iff, Array.append_data, Array.push_data, append_assoc, singleton_append,
      Array.data_toArray, nil_append, and_self]
Proof state after:
case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)

case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)
Theorem: List.splitOnListAux_acc
Proof state before:
case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)

case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)
Tactic:
. simp only [length_cons, Nat.lt_succ_self]
Proof state after:
case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)
Theorem: List.splitOnListAux_acc
Proof state before:
case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)
Tactic:
. simp only [length_cons, Nat.lt_succ_self]
Proof state after:
no goals
Theorem: List.splitOnListAux_acc
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ (match [] with
    | [] => []
    | a :: l => (Array.push acc head ++ a) :: l) =
    match
      match [] with
      | [] => []
      | a :: l => (Array.push #[] head ++ a) :: l with
    | [] => []
    | a :: l => (acc ++ a) :: l
Tactic:
simp only
Proof state after:
no goals
Theorem: List.splitOnListAux_acc
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
head✝ : Array α
tail✝ : List (Array α)
⊢ (match head✝ :: tail✝ with
    | [] => []
    | a :: l => (Array.push acc head ++ a) :: l) =
    match
      match head✝ :: tail✝ with
      | [] => []
      | a :: l => (Array.push #[] head ++ a) :: l with
    | [] => []
    | a :: l => (acc ++ a) :: l
Tactic:
simp only [cons.injEq, Array.ext_iff, Array.append_data, Array.push_data, append_assoc, singleton_append,
  Array.data_toArray, nil_append, and_self]
Proof state after:
no goals
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)
Tactic:
have h₁: (Array.push #[] acc) = (Array.push #[] acc) ++ #[] := by simp [Array.ext_iff]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)
Tactic:
have h₂: (Array.push #[] #[]) = (Array.push #[] (#[]:Array α)) ++ #[] := by simp [Array.ext_iff]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
h₂ : Array.push #[] #[] = Array.push #[] #[] ++ #[]
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
h₂ : Array.push #[] #[] = Array.push #[] #[] ++ #[]
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)
Tactic:
rw [h₁,h₂,List.splitOnListAux_r, List.splitOnListAux_r]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
h₂ : Array.push #[] #[] = Array.push #[] #[] ++ #[]
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    Array.push #[] acc ++ splitOnListAux delim rest✝ #[] #[] h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      Array.push #[] #[] ++ splitOnListAux delim rest✝ #[] #[] h)
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
h₂ : Array.push #[] #[] = Array.push #[] #[] ++ #[]
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    Array.push #[] acc ++ splitOnListAux delim rest✝ #[] #[] h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      Array.push #[] #[] ++ splitOnListAux delim rest✝ #[] #[] h)
Tactic:
simp [Array.ext_iff]
Proof state after:
no goals
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
⊢ Array.push #[] acc = Array.push #[] acc ++ #[]
Tactic:
simp [Array.ext_iff]
Proof state after:
no goals
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
⊢ Array.push #[] #[] = Array.push #[] #[] ++ #[]
Tactic:
simp [Array.ext_iff]
Proof state after:
no goals
Theorem: List.splitOnListAux_delim
Proof state before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
delim l : List α
h : delim ≠ []
⊢ splitOnListAux delim (delim ++ l) acc r h = r ++ #[acc] ++ splitOnListAux delim l #[] #[] h
Tactic:
conv => left; unfold splitOnListAux
Proof state after:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
delim l : List α
h : delim ≠ []
⊢ (match _h₀ : delim ++ l with
    | [] => Array.push r acc
    | head :: tail =>
      match h : getRest (delim ++ l) delim with
      | none => splitOnListAux delim tail (Array.push acc head) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf (delim ++ l));
        splitOnListAux delim rest #[] (Array.push r acc) h) =
    r ++ #[acc] ++ splitOnListAux delim l #[] #[] h
Theorem: List.splitOnListAux_delim
Proof state before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
delim l : List α
h : delim ≠ []
⊢ (match _h₀ : delim ++ l with
    | [] => Array.push r acc
    | head :: tail =>
      match h : getRest (delim ++ l) delim with
      | none => splitOnListAux delim tail (Array.push acc head) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf (delim ++ l));
        splitOnListAux delim rest #[] (Array.push r acc) h) =
    r ++ #[acc] ++ splitOnListAux delim l #[] #[] h
Tactic:
have ⟨head, tail, heq⟩ :=List.exists_cons_of_ne_nil h
Proof state after:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
delim l : List α
h : delim ≠ []
head : α
tail : List α
heq : delim = head :: tail
⊢ (match _h₀ : delim ++ l with
    | [] => Array.push r acc
    | head :: tail =>
      match h : getRest (delim ++ l) delim with
      | none => splitOnListAux delim tail (Array.push acc head) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf (delim ++ l));
        splitOnListAux delim rest #[] (Array.push r acc) h) =
    r ++ #[acc] ++ splitOnListAux delim l #[] #[] h
Theorem: List.splitOnListAux_delim
Proof state before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
delim l : List α
h : delim ≠ []
head : α
tail : List α
heq : delim = head :: tail
⊢ (match _h₀ : delim ++ l with
    | [] => Array.push r acc
    | head :: tail =>
      match h : getRest (delim ++ l) delim with
      | none => splitOnListAux delim tail (Array.push acc head) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf (delim ++ l));
        splitOnListAux delim rest #[] (Array.push r acc) h) =
    r ++ #[acc] ++ splitOnListAux delim l #[] #[] h
Tactic:
subst heq
Proof state after:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
⊢ (match _h₀ : head :: tail ++ l with
    | [] => Array.push r acc
    | head_1 :: tail_1 =>
      match h : getRest (head :: tail ++ l) (head :: tail) with
      | none => splitOnListAux (head :: tail) tail_1 (Array.push acc head_1) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf (head :: tail ++ l));
        splitOnListAux (head :: tail) rest #[] (Array.push r acc) h) =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Theorem: List.splitOnListAux_delim
Proof state before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
⊢ (match _h₀ : head :: tail ++ l with
    | [] => Array.push r acc
    | head_1 :: tail_1 =>
      match h : getRest (head :: tail ++ l) (head :: tail) with
      | none => splitOnListAux (head :: tail) tail_1 (Array.push acc head_1) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf (head :: tail ++ l));
        splitOnListAux (head :: tail) rest #[] (Array.push r acc) h) =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
simp only [cons_append]
Proof state after:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
⊢ (match h : getRest (head :: (tail ++ l)) (head :: tail) with
    | none => splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h
    | some rest => splitOnListAux (head :: tail) rest #[] (Array.push r acc) h) =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Theorem: List.splitOnListAux_delim
Proof state before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
⊢ (match h : getRest (head :: (tail ++ l)) (head :: tail) with
    | none => splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h
    | some rest => splitOnListAux (head :: tail) rest #[] (Array.push r acc) h) =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
split
Proof state after:
case h_1
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
heq✝ : getRest (head :: (tail ++ l)) (head :: tail) = none
⊢ splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h

case h_2
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest✝ : List α
heq✝ : getRest (head :: (tail ++ l)) (head :: tail) = some rest✝
⊢ splitOnListAux (head :: tail) rest✝ #[] (Array.push r acc) h =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Theorem: List.splitOnListAux_delim
Proof state before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
heq : getRest (head :: (tail ++ l)) (head :: tail) = none
⊢ splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
case h_1 heq =>
  unfold getRest at heq
  simp at heq
Proof state after:
no goals
Theorem: List.splitOnListAux_delim
Proof state before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
⊢ splitOnListAux (head :: tail) rest #[] (Array.push r acc) h = r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
case h_2 rest heq =>
  have h₂ : (Array.push r acc) = r ++ #[acc] ++ #[] := by simp only [Array.ext_iff, Array.push_data, Array.append_data, Array.data_toArray, append_nil]
  rw [h₂, List.splitOnListAux_r]
  congr
  have h₃ := List.eq_append_of_getRest heq
  simp_all only [ne_eq, not_false_iff, cons_append, cons.injEq, append_cancel_left_eq, true_and]
Proof state after:
no goals
Theorem: List.splitOnListAux_delim
Proof state before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
heq : getRest (head :: (tail ++ l)) (head :: tail) = none
⊢ splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
unfold getRest at heq
Proof state after:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
heq : (if head = head then getRest (tail ++ l) tail else none) = none
⊢ splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Theorem: List.splitOnListAux_delim
Proof state before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
heq : (if head = head then getRest (tail ++ l) tail else none) = none
⊢ splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
simp at heq
Proof state after:
no goals
Theorem: List.splitOnListAux_delim
Proof state before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
⊢ splitOnListAux (head :: tail) rest #[] (Array.push r acc) h = r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
have h₂ : (Array.push r acc) = r ++ #[acc] ++ #[] := by simp only [Array.ext_iff, Array.push_data, Array.append_data, Array.data_toArray, append_nil]
Proof state after:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
⊢ splitOnListAux (head :: tail) rest #[] (Array.push r acc) h = r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Theorem: List.splitOnListAux_delim
Proof state before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
⊢ splitOnListAux (head :: tail) rest #[] (Array.push r acc) h = r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
rw [h₂, List.splitOnListAux_r]
Proof state after:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
⊢ r ++ #[acc] ++ splitOnListAux (head :: tail) rest #[] #[] h = r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Theorem: List.splitOnListAux_delim
Proof state before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
⊢ r ++ #[acc] ++ splitOnListAux (head :: tail) rest #[] #[] h = r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
congr
Proof state after:
case e_a.e_l
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
⊢ rest = l
Theorem: List.splitOnListAux_delim
Proof state before:
case e_a.e_l
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
⊢ rest = l
Tactic:
have h₃ := List.eq_append_of_getRest heq
Proof state after:
case e_a.e_l
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
h₃ : head :: (tail ++ l) = head :: tail ++ rest
⊢ rest = l
Theorem: List.splitOnListAux_delim
Proof state before:
case e_a.e_l
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
h₃ : head :: (tail ++ l) = head :: tail ++ rest
⊢ rest = l
Tactic:
simp_all only [ne_eq, not_false_iff, cons_append, cons.injEq, append_cancel_left_eq, true_and]
Proof state after:
no goals