Theorem: Array.modify_data (One.lean)

State before:
α : Type u_1
a : Array α
i : ℕ
f : α → α
⊢ (modify a i f).data = List.modifyNth f i a.data
Tactic:
unfold modify Id.run modifyM
State after:
α : Type u_1
a : Array α
i : ℕ
f : α → α
⊢ (if h : i < size a then
        let idx := { val := i, isLt := h };
        let v := get a idx;
        do
        let v ← f v
        pure (set a idx v)
      else pure a).data =
    List.modifyNth f i a.data

State before:
α : Type u_1
a : Array α
i : ℕ
f : α → α
⊢ (if h : i < size a then
        let idx := { val := i, isLt := h };
        let v := get a idx;
        do
        let v ← f v
        pure (set a idx v)
      else pure a).data =
    List.modifyNth f i a.data
Tactic:
split
State after:
case inl
α : Type u_1
a : Array α
i : ℕ
f : α → α
h✝ : i < size a
⊢ (let idx := { val := i, isLt := h✝ };
      let v := get a idx;
      do
      let v ← f v
      pure (set a idx v)).data =
    List.modifyNth f i a.data

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

State before:
case inl
α : Type u_1
a : Array α
i : ℕ
f : α → α
h✝ : i < size a
⊢ (let idx := { val := i, isLt := h✝ };
      let v := get a idx;
      do
      let v ← f v
      pure (set a idx v)).data =
    List.modifyNth f i a.data

case inr
α : Type u_1
a : Array α
i : ℕ
f : α → α
h✝ : ¬i < size a
⊢ (pure a).data = List.modifyNth f i a.data
Tactic:
. simp
  rw [List.modifyNth_eq_set_get]
  congr 1
State after:
case inr
α : Type u_1
a : Array α
i : ℕ
f : α → α
h✝ : ¬i < size a
⊢ (pure a).data = List.modifyNth f i a.data

State before:
α : Type u_1
a : Array α
i : ℕ
f : α → α
heq : ¬i < size a
⊢ (pure a).data = List.modifyNth f i a.data
Tactic:
case inr heq =>
  simp at heq
  rw [List.modifyNth_eq_set_get?]
  simp [List.get?_eq_none.2 heq]
State after:
no goals

State before:
α : Type u_1
a : Array α
i : ℕ
f : α → α
heq : ¬i < size a
⊢ (pure a).data = List.modifyNth f i a.data
Tactic:
simp at heq
State after:
α : Type u_1
a : Array α
i : ℕ
f : α → α
heq : size a ≤ i
⊢ (pure a).data = List.modifyNth f i a.data

State before:
α : Type u_1
a : Array α
i : ℕ
f : α → α
heq : size a ≤ i
⊢ (pure a).data = List.modifyNth f i a.data
Tactic:
rw [List.modifyNth_eq_set_get?]
State after:
α : Type u_1
a : Array α
i : ℕ
f : α → α
heq : size a ≤ i
⊢ (pure a).data = Option.getD ((fun a_1 => List.set a.data i (f a_1)) <$> List.get? a.data i) a.data

State before:
α : Type u_1
a : Array α
i : ℕ
f : α → α
heq : size a ≤ i
⊢ (pure a).data = Option.getD ((fun a_1 => List.set a.data i (f a_1)) <$> List.get? a.data i) a.data
Tactic:
simp [List.get?_eq_none.2 heq]
State after:
no goals