internlm/Lean-Github huggingface dataset:
Theorem: List.sizeOf_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq : head :: tail = x✝ :: l✝
h : (if x✝ = y✝ then getRest l✝ l₁✝ else none) = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)
Tactic:
split at h <;> try contradiction
Proof state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq : head :: tail = x✝ :: l✝
h✝ : x✝ = y✝
h : getRest l✝ l₁✝ = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)
Theorem: List.sizeOf_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq : head :: tail = x✝ :: l✝
heq₂ : x✝ = y✝
h : getRest l✝ l₁✝ = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)
Tactic:
case inl heq₂ =>
  injection heq
  subst_vars
  simp only [ih h, tsub_le_iff_right, ge_iff_le, cons.sizeOf_spec, sizeOf_default, add_zero, zero_le,
    nonpos_iff_eq_zero, Nat.add_sub_add_left, add_le_add_iff_left]
Proof state after:
no goals
Theorem: List.sizeOf_getRest
Proof state before:
case inr
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq : head :: tail = x✝ :: l✝
h✝ : ¬x✝ = y✝
h : False
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.sizeOf_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq : head :: tail = x✝ :: l✝
heq₂ : x✝ = y✝
h : getRest l✝ l₁✝ = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)
Tactic:
injection heq
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq₂ : x✝ = y✝
h : getRest l✝ l₁✝ = some l₂
head_eq✝ : head = x✝
tail_eq✝ : tail = l✝
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)
Theorem: List.sizeOf_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq₂ : x✝ = y✝
h : getRest l✝ l₁✝ = some l₂
head_eq✝ : head = x✝
tail_eq✝ : tail = l✝
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)
Tactic:
subst_vars
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
l₂ x✝¹ x✝ l✝ : List α
y✝ : α
l₁✝ : List α
h : getRest l✝ l₁✝ = some l₂
ih : ∀ {l₁ l₂ : List α}, getRest l✝ l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf l✝ - sizeOf l₁
⊢ sizeOf l₂ = 1 + sizeOf (y✝ :: l✝) - sizeOf (y✝ :: l₁✝)
Theorem: List.sizeOf_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
l₂ x✝¹ x✝ l✝ : List α
y✝ : α
l₁✝ : List α
h : getRest l✝ l₁✝ = some l₂
ih : ∀ {l₁ l₂ : List α}, getRest l✝ l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf l✝ - sizeOf l₁
⊢ sizeOf l₂ = 1 + sizeOf (y✝ :: l✝) - sizeOf (y✝ :: l₁✝)
Tactic:
simp only [ih h, tsub_le_iff_right, ge_iff_le, cons.sizeOf_spec, sizeOf_default, add_zero, zero_le,
  nonpos_iff_eq_zero, Nat.add_sub_add_left, add_le_add_iff_left]
Proof state after:
no goals
Theorem: List.sizeOf_pos
Proof state before:
α : Type u_1
l : List α
⊢ sizeOf l > 0
Tactic:
cases l <;> simp only [cons.sizeOf_spec, nil.sizeOf_spec, sizeOf_default, add_zero, zero_le, ge_iff_le, nonpos_iff_eq_zero, gt_iff_lt,
  add_pos_iff, true_or]
Proof state after:
no goals
Theorem: Array.data_injective
Proof state before:
α : Type u_1
⊢ Function.Injective data
Tactic:
unfold Function.Injective
Proof state after:
α : Type u_1
⊢ ∀ ⦃a₁ a₂ : Array α⦄, a₁.data = a₂.data → a₁ = a₂
Theorem: Array.data_injective
Proof state before:
α : Type u_1
⊢ ∀ ⦃a₁ a₂ : Array α⦄, a₁.data = a₂.data → a₁ = a₂
Tactic:
intro a₁ a₂ h
Proof state after:
α : Type u_1
a₁ a₂ : Array α
h : a₁.data = a₂.data
⊢ a₁ = a₂
Theorem: Array.data_injective
Proof state before:
α : Type u_1
a₁ a₂ : Array α
h : a₁.data = a₂.data
⊢ a₁ = a₂
Tactic:
rw [← Array.toArray_data a₁, ← Array.toArray_data a₂]
Proof state after:
α : Type u_1
a₁ a₂ : Array α
h : a₁.data = a₂.data
⊢ List.toArray a₁.data = List.toArray a₂.data
Theorem: Array.data_injective
Proof state before:
α : Type u_1
a₁ a₂ : Array α
h : a₁.data = a₂.data
⊢ List.toArray a₁.data = List.toArray a₂.data
Tactic:
congr
Proof state after:
no goals
Theorem: List.splitOnListAux_r
Proof 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]
Proof state after:
no goals
Theorem: List.splitOnListAux_r
Proof 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
Proof 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
Theorem: List.splitOnListAux_r
Proof 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
Proof 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
Theorem: List.splitOnListAux_r
Proof 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]
Proof state after:
no goals
Theorem: List.splitOnListAux_r
Proof 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]
Proof state after:
no goals
Theorem: List.splitOnListAux_r
Proof 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]
Proof state after:
no goals
Theorem: List.splitOnListAux_r
Proof 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
Proof 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
Theorem: List.splitOnListAux_r
Proof 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]
Proof state after:
no goals
Theorem: List.splitOnListAux_r
Proof 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]
Proof state after:
no goals
Theorem: List.splitOnListAux_r
Proof 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]
Proof state after:
no goals
Theorem: List.splitOnListAux_r
Proof 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
Proof 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
Theorem: List.splitOnListAux_r
Proof 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]
Proof 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
Theorem: List.splitOnListAux_r
Proof 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]
Proof 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)
Theorem: List.splitOnListAux_r
Proof 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₂
Proof 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)
Theorem: List.splitOnListAux_r
Proof 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]
Proof state after:
no goals
Theorem: List.splitOnListAux_r
Proof 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]
Proof state after:
no goals
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
⊢ (modifyHead f a).data = List.modifyHead f a.data
Tactic:
unfold modifyHead modify modifyM Id.run
Proof state after:
α : Type u_1
f : α → α
a : Array α
⊢ (if h : 0 < size a then
        let idx := { val := 0, isLt := h };
        let v := get a idx;
        do
        let v ← f v
        pure (set a idx v)
      else pure a).data =
    List.modifyHead f a.data