Theorem: Array.modifyHead_data (One.lean)

State before:
α : Type u_1
f : α → α
a : Array α
⊢ (modifyHead f a).data = List.modifyHead f a.data
Tactic:
unfold modifyHead modify modifyM Id.run
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

State before:
α : 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
Tactic:
split
State after:
case inl
α : Type u_1
f : α → α
a : Array α
h✝ : 0 < size a
⊢ (let idx := { val := 0, isLt := h✝ };
      let v := get a idx;
      do
      let v ← f v
      pure (set a idx v)).data =
    List.modifyHead f a.data

case inr
α : Type u_1
f : α → α
a : Array α
h✝ : ¬0 < size a
⊢ (pure a).data = List.modifyHead f a.data

State before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
⊢ (let idx := { val := 0, isLt := heq };
      let v := get a idx;
      do
      let v ← f v
      pure (set a idx v)).data =
    List.modifyHead f a.data
Tactic:
case inl heq =>
  simp [List.set_eq_take_cons_drop _ heq]
  split
  case h_1 heq₂ =>
    apply_fun (@List.toArray α) at heq₂
    simp only [toArray_data] at heq₂
    subst heq₂
    simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, size_toArray, List.length_nil, lt_self_iff_false] at heq
  case h_2 head tail heq₂ =>
    apply_fun (@List.toArray α) at heq₂
    simp only [toArray_data] at heq₂
    subst heq₂
    simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, data_toArray, List.tail_cons, List.cons.injEq, and_true]
    congr
    simp [Array.getElem_eq_data_get, Array.data_toArray (head::tail)] 
    simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, List.get_eq_iff, data_toArray, List.cons.injEq,
      forall_true_left, and_imp, forall_apply_eq_imp_iff', forall_eq', List.get?_zero, List.head?_cons]
State after:
no goals

State before:
α : Type u_1
f : α → α
a : Array α
heq : ¬0 < size a
⊢ (pure a).data = List.modifyHead f a.data
Tactic:
case inr heq =>
  simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, not_lt] at heq
  rw [← Array.toArray_data a, Array.size_toArray, List.length_eq_zero] at heq
  simp only [Id.pure_eq, heq, List.modifyHead]
State after:
no goals

State before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
⊢ (let idx := { val := 0, isLt := heq };
      let v := get a idx;
      do
      let v ← f v
      pure (set a idx v)).data =
    List.modifyHead f a.data
Tactic:
simp [List.set_eq_take_cons_drop _ heq]
State after:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
⊢ f a[0] :: List.tail a.data =
    match a.data with
    | [] => []
    | a :: l => f a :: l

State before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
⊢ f a[0] :: List.tail a.data =
    match a.data with
    | [] => []
    | a :: l => f a :: l
Tactic:
split
State after:
case h_1
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq✝ : a.data = []
⊢ f a[0] :: List.tail a.data = []

case h_2
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝¹ : List α
x✝ : α
xs✝ : List α
heq✝ : a.data = x✝ :: xs✝
⊢ f a[0] :: List.tail a.data = f x✝ :: xs✝

State before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq₂ : a.data = []
⊢ f a[0] :: List.tail a.data = []
Tactic:
case h_1 heq₂ =>
  apply_fun (@List.toArray α) at heq₂
  simp only [toArray_data] at heq₂
  subst heq₂
  simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, size_toArray, List.length_nil, lt_self_iff_false] at heq
State after:
no goals

State before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
head : α
tail : List α
heq₂ : a.data = head :: tail
⊢ f a[0] :: List.tail a.data = f head :: tail
Tactic:
case h_2 head tail heq₂ =>
  apply_fun (@List.toArray α) at heq₂
  simp only [toArray_data] at heq₂
  subst heq₂
  simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, data_toArray, List.tail_cons, List.cons.injEq, and_true]
  congr
  simp [Array.getElem_eq_data_get, Array.data_toArray (head::tail)] 
  simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, List.get_eq_iff, data_toArray, List.cons.injEq,
    forall_true_left, and_imp, forall_apply_eq_imp_iff', forall_eq', List.get?_zero, List.head?_cons]
State after:
no goals

State before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq₂ : a.data = []
⊢ f a[0] :: List.tail a.data = []
Tactic:
apply_fun (@List.toArray α) at heq₂
State after:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq₂ : List.toArray a.data = #[]
⊢ f a[0] :: List.tail a.data = []

State before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq₂ : List.toArray a.data = #[]
⊢ f a[0] :: List.tail a.data = []
Tactic:
simp only [toArray_data] at heq₂
State after:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq₂ : a = #[]
⊢ f a[0] :: List.tail a.data = []

State before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq₂ : a = #[]
⊢ f a[0] :: List.tail a.data = []
Tactic:
subst heq₂
State after:
α : Type u_1
f : α → α
x✝ : List α
heq : 0 < size #[]
⊢ f #[][0] :: List.tail #[].data = []

State before:
α : Type u_1
f : α → α
x✝ : List α
heq : 0 < size #[]
⊢ f #[][0] :: List.tail #[].data = []
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, size_toArray, List.length_nil, lt_self_iff_false] at heq
State after:
no goals

State before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
head : α
tail : List α
heq₂ : a.data = head :: tail
⊢ f a[0] :: List.tail a.data = f head :: tail
Tactic:
apply_fun (@List.toArray α) at heq₂
State after:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
head : α
tail : List α
heq₂ : List.toArray a.data = List.toArray (head :: tail)
⊢ f a[0] :: List.tail a.data = f head :: tail

State before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
head : α
tail : List α
heq₂ : List.toArray a.data = List.toArray (head :: tail)
⊢ f a[0] :: List.tail a.data = f head :: tail
Tactic:
simp only [toArray_data] at heq₂
State after:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
head : α
tail : List α
heq₂ : a = List.toArray (head :: tail)
⊢ f a[0] :: List.tail a.data = f head :: tail

State before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
head : α
tail : List α
heq₂ : a = List.toArray (head :: tail)
⊢ f a[0] :: List.tail a.data = f head :: tail
Tactic:
subst heq₂
State after:
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ f (List.toArray (head :: tail))[0] :: List.tail (List.toArray (head :: tail)).data = f head :: tail

State before:
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ f (List.toArray (head :: tail))[0] :: List.tail (List.toArray (head :: tail)).data = f head :: tail
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, data_toArray, List.tail_cons, List.cons.injEq, and_true]
State after:
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ f (List.toArray (head :: tail))[0] = f head

State before:
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ f (List.toArray (head :: tail))[0] = f head
Tactic:
congr
State after:
case e_a
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ (List.toArray (head :: tail))[0] = head

State before:
case e_a
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ (List.toArray (head :: tail))[0] = head
Tactic:
simp [Array.getElem_eq_data_get, Array.data_toArray (head::tail)]
State after:
case e_a
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ List.get (List.toArray (head :: tail)).data
      { val := 0, isLt := (_ : ↑{ val := 0, isLt := heq } < size (List.toArray (head :: tail))) } =
    head

State before:
case e_a
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ List.get (List.toArray (head :: tail)).data
      { val := 0, isLt := (_ : ↑{ val := 0, isLt := heq } < size (List.toArray (head :: tail))) } =
    head
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, List.get_eq_iff, data_toArray, List.cons.injEq,
  forall_true_left, and_imp, forall_apply_eq_imp_iff', forall_eq', List.get?_zero, List.head?_cons]
State after:
no goals

State before:
α : Type u_1
f : α → α
a : Array α
heq : ¬0 < size a
⊢ (pure a).data = List.modifyHead f a.data
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, not_lt] at heq
State after:
α : Type u_1
f : α → α
a : Array α
heq : size a = 0
⊢ (pure a).data = List.modifyHead f a.data

State before:
α : Type u_1
f : α → α
a : Array α
heq : size a = 0
⊢ (pure a).data = List.modifyHead f a.data
Tactic:
rw [← Array.toArray_data a, Array.size_toArray, List.length_eq_zero] at heq
State after:
α : Type u_1
f : α → α
a : Array α
heq : a.data = []
⊢ (pure a).data = List.modifyHead f a.data

State before:
α : Type u_1
f : α → α
a : Array α
heq : a.data = []
⊢ (pure a).data = List.modifyHead f a.data
Tactic:
simp only [Id.pure_eq, heq, List.modifyHead]
State after:
no goals