internlm/Lean-Github huggingface dataset:
Theorem: List.splitOnListAux_append
Proof state before:
case true.inr
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
have hzero: length l₁ + 1 - length delim - length l₁ = 0 := by
  simp only [tsub_le_iff_right, ge_iff_le, add_le_add_iff_left, zero_le, nonpos_iff_eq_zero,
    tsub_eq_zero_iff_le]
  apply Nat.succ_le_of_lt
  simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, h₂, not_false_iff, length_pos_of_ne_nil]
Proof state after:
case true.inr
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
hzero : length l₁ + 1 - length delim - length l₁ = 0
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Theorem: List.splitOnListAux_append
Proof state before:
case true.inr
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
hzero : length l₁ + 1 - length delim - length l₁ = 0
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
rw [List.drop_append_eq_append_drop, hzero, drop] at hinf
Proof state after:
case true.inr
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Theorem: List.splitOnListAux_append
Proof state before:
case true.inr
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
have ⟨t, hinf⟩ := hinf
Proof state after:
case true.inr
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Theorem: List.splitOnListAux_append
Proof state before:
case true.inr
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
unfold lastN at h
Proof state after:
case true.inr
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Theorem: List.splitOnListAux_append
Proof state before:
case true.inr
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
exfalso
Proof state after:
case true.inr.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ False
Theorem: List.splitOnListAux_append
Proof state before:
case true.inr.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ False
Tactic:
apply h
Proof state after:
case true.inr.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
Theorem: List.splitOnListAux_append
Proof state before:
case true.inr.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
Tactic:
exists drop (length l₁ + 1 - length delim) s, t
Proof state after:
case true.inr.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ - (length delim - 1)) l₁ ++ l₂
Theorem: List.splitOnListAux_append
Proof state before:
case true.inr.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ - (length delim - 1)) l₁ ++ l₂
Tactic:
convert hinf using 3
Proof state after:
case e_a.e_a.e_a
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ length l₁ - (length delim - 1) = length l₁ + 1 - length delim
Theorem: List.splitOnListAux_append
Proof state before:
case e_a.e_a.e_a
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ length l₁ - (length delim - 1) = length l₁ + 1 - length delim
Tactic:
rw [Nat.sub_sub_eq_add_sub_of_le]
Proof state after:
case e_a.e_a.e_a
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ 1 ≤ length delim
Theorem: List.splitOnListAux_append
Proof state before:
case e_a.e_a.e_a
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ 1 ≤ length delim
Tactic:
apply Nat.succ_le_of_lt
Proof state after:
case e_a.e_a.e_a.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ 0 < length delim
Theorem: List.splitOnListAux_append
Proof state before:
case e_a.e_a.e_a.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ 0 < length delim
Tactic:
apply Nat.zero_lt_of_ne_zero
Proof state after:
case e_a.e_a.e_a.h.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ length delim ≠ 0
Theorem: List.splitOnListAux_append
Proof state before:
case e_a.e_a.e_a.h.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ length delim ≠ 0
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, length_eq_zero, h₂, not_false_iff]
Proof state after:
no goals
Theorem: List.splitOnListAux_append
Proof state before:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
⊢ length l₁ + 1 - length delim - length l₁ = 0
Tactic:
simp only [tsub_le_iff_right, ge_iff_le, add_le_add_iff_left, zero_le, nonpos_iff_eq_zero,
  tsub_eq_zero_iff_le]
Proof state after:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
⊢ 1 ≤ length delim
Theorem: List.splitOnListAux_append
Proof state before:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
⊢ 1 ≤ length delim
Tactic:
apply Nat.succ_le_of_lt
Proof state after:
case h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
⊢ 0 < length delim
Theorem: List.splitOnListAux_append
Proof state before:
case h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
⊢ 0 < length delim
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, h₂, not_false_iff, length_pos_of_ne_nil]
Proof state after:
no goals
Theorem: List.splitOnListAux_append
Proof state before:
case false
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : isInfixOf delim (l₁ ++ l₂) = false
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
rw [← Bool.not_eq_true, isInfixOf_ext] at heq
Proof state after:
case false
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Theorem: List.splitOnListAux_append
Proof state before:
case false
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
have not_in_l₁: ¬ delim <:+: l₁  :=  by
  intro contr;
  apply heq
  apply List.isInfix_append_right_of_isInfix contr
Proof state after:
case false
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Theorem: List.splitOnListAux_append
Proof state before:
case false
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
rw [splitOnListAux_nonmatching _ heq, splitOnListAux_nonmatching _ not_in_l₁]
Proof state after:
case false
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ #[toArray (l₁ ++ l₂)] = Array.modifyLast (fun x => x ++ toArray l₂) #[toArray l₁]
Theorem: List.splitOnListAux_append
Proof state before:
case false
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ #[toArray (l₁ ++ l₂)] = Array.modifyLast (fun x => x ++ toArray l₂) #[toArray l₁]
Tactic:
apply Array.ext'
Proof state after:
case false.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ #[toArray (l₁ ++ l₂)].data = (Array.modifyLast (fun x => x ++ toArray l₂) #[toArray l₁]).data
Theorem: List.splitOnListAux_append
Proof state before:
case false.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ #[toArray (l₁ ++ l₂)].data = (Array.modifyLast (fun x => x ++ toArray l₂) #[toArray l₁]).data
Tactic:
simp only [Array.data_toArray, Array.modifyLast_data, modifyLast_singleton, cons.injEq, and_true]
Proof state after:
case false.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ toArray (l₁ ++ l₂) = toArray l₁ ++ toArray l₂
Theorem: List.splitOnListAux_append
Proof state before:
case false.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ toArray (l₁ ++ l₂) = toArray l₁ ++ toArray l₂
Tactic:
apply Array.ext'
Proof state after:
case false.h.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ (toArray (l₁ ++ l₂)).data = (toArray l₁ ++ toArray l₂).data
Theorem: List.splitOnListAux_append
Proof state before:
case false.h.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ (toArray (l₁ ++ l₂)).data = (toArray l₁ ++ toArray l₂).data
Tactic:
simp only [Array.data_toArray, Array.append_data]
Proof state after:
no goals
Theorem: List.splitOnListAux_append
Proof state before:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
⊢ ¬delim <:+: l₁
Tactic:
intro contr
Proof state after:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
contr : delim <:+: l₁
⊢ False
Theorem: List.splitOnListAux_append
Proof state before:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
contr : delim <:+: l₁
⊢ False
Tactic:
apply heq
Proof state after:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
contr : delim <:+: l₁
⊢ delim <:+: l₁ ++ l₂
Theorem: List.splitOnListAux_append
Proof state before:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
contr : delim <:+: l₁
⊢ delim <:+: l₁ ++ l₂
Tactic:
apply List.isInfix_append_right_of_isInfix contr
Proof state after:
no goals
Theorem: List.map_modifyLast
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
f : α✝ → β✝
h : α✝ → α✝
g : β✝ → β✝
l : List α✝
P : Function.Semiconj f h g
⊢ map f (modifyLast h l) = modifyLast g (map f l)
Tactic:
if heq: l = [] then
  simp only [heq, map, modifyLast_nil]
else
  rw [← List.dropLast_append_getLast heq, List.modifyLast_append_one, map_append, map_append,
    map_singleton, map_singleton,List.modifyLast_append_one, P.eq]
Proof state after:
no goals
Theorem: List.map_modifyLast
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
f : α✝ → β✝
h : α✝ → α✝
g : β✝ → β✝
l : List α✝
P : Function.Semiconj f h g
heq : l = []
⊢ map f (modifyLast h l) = modifyLast g (map f l)
Tactic:
simp only [heq, map, modifyLast_nil]
Proof state after:
no goals