Theorem: Array.size_modifyM (Algdata/Data/Array/Lemmas.lean)

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
⊢ SatisfiesM (fun y => size y = size x) (modifyM x n f)
Tactic:
unfold modifyM
State after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
⊢ SatisfiesM (fun y => size y = size x)
    (if h : n < size x then
      let idx := { val := n, isLt := h };
      let v := get x idx;
      do
      let v ← f v
      pure (set x idx v)
    else pure x)

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
⊢ SatisfiesM (fun y => size y = size x)
    (if h : n < size x then
      let idx := { val := n, isLt := h };
      let v := get x idx;
      do
      let v ← f v
      pure (set x idx v)
    else pure x)
Tactic:
if h : n < x.size
then
  rw [dif_pos h]; dsimp
  exists (f x[n] >>= λ v => pure ⟨x.set ⟨n,h⟩ v, x.size_set ⟨n,h⟩ v⟩)
  rw [map_eq_pure_bind, bind_assoc]
  apply bind_congr; intro a
  exact pure_bind ..
else rw [dif_neg h]; exact ⟨pure ⟨x,rfl⟩, map_pure Subtype.val _⟩
State after:
no goals

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ SatisfiesM (fun y => size y = size x)
    (if h : n < size x then
      let idx := { val := n, isLt := h };
      let v := get x idx;
      do
      let v ← f v
      pure (set x idx v)
    else pure x)
Tactic:
rw [dif_pos h]
State after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ SatisfiesM (fun y => size y = size x)
    (let idx := { val := n, isLt := h };
    let v := get x idx;
    do
    let v ← f v
    pure (set x idx v))

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ SatisfiesM (fun y => size y = size x)
    (let idx := { val := n, isLt := h };
    let v := get x idx;
    do
    let v ← f v
    pure (set x idx v))
Tactic:
dsimp
State after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ SatisfiesM (fun y => size y = size x) do
    let v ← f x[n]
    pure (set x { val := n, isLt := h } v)

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ SatisfiesM (fun y => size y = size x) do
    let v ← f x[n]
    pure (set x { val := n, isLt := h } v)
Tactic:
exists (f x[n] >>= λ v => pure ⟨x.set ⟨n,h⟩ v, x.size_set ⟨n,h⟩ v⟩)
State after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ (Subtype.val <$> do
      let v ← f x[n]
      pure
          { val := set x { val := n, isLt := h } v,
            property := (_ : size (set x { val := n, isLt := h } v) = size x) }) =
    do
    let v ← f x[n]
    pure (set x { val := n, isLt := h } v)

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ (Subtype.val <$> do
      let v ← f x[n]
      pure
          { val := set x { val := n, isLt := h } v,
            property := (_ : size (set x { val := n, isLt := h } v) = size x) }) =
    do
    let v ← f x[n]
    pure (set x { val := n, isLt := h } v)
Tactic:
rw [map_eq_pure_bind, bind_assoc]
State after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ (do
      let x_1 ← f x[n]
      let a ←
        pure
            { val := set x { val := n, isLt := h } x_1,
              property := (_ : size (set x { val := n, isLt := h } x_1) = size x) }
      pure a.val) =
    do
    let v ← f x[n]
    pure (set x { val := n, isLt := h } v)

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ (do
      let x_1 ← f x[n]
      let a ←
        pure
            { val := set x { val := n, isLt := h } x_1,
              property := (_ : size (set x { val := n, isLt := h } x_1) = size x) }
      pure a.val) =
    do
    let v ← f x[n]
    pure (set x { val := n, isLt := h } v)
Tactic:
apply bind_congr
State after:
case h
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ ∀ (a : α),
    (do
        let a ←
          pure
              { val := set x { val := n, isLt := h } a,
                property := (_ : size (set x { val := n, isLt := h } a) = size x) }
        pure a.val) =
      pure (set x { val := n, isLt := h } a)

State before:
case h
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ ∀ (a : α),
    (do
        let a ←
          pure
              { val := set x { val := n, isLt := h } a,
                property := (_ : size (set x { val := n, isLt := h } a) = size x) }
        pure a.val) =
      pure (set x { val := n, isLt := h } a)
Tactic:
intro a
State after:
case h
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
a : α
⊢ (do
      let a ←
        pure
            { val := set x { val := n, isLt := h } a,
              property := (_ : size (set x { val := n, isLt := h } a) = size x) }
      pure a.val) =
    pure (set x { val := n, isLt := h } a)

State before:
case h
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
a : α
⊢ (do
      let a ←
        pure
            { val := set x { val := n, isLt := h } a,
              property := (_ : size (set x { val := n, isLt := h } a) = size x) }
      pure a.val) =
    pure (set x { val := n, isLt := h } a)
Tactic:
exact pure_bind ..
State after:
no goals

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : ¬n < size x
⊢ SatisfiesM (fun y => size y = size x)
    (if h : n < size x then
      let idx := { val := n, isLt := h };
      let v := get x idx;
      do
      let v ← f v
      pure (set x idx v)
    else pure x)
Tactic:
rw [dif_neg h]
State after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : ¬n < size x
⊢ SatisfiesM (fun y => size y = size x) (pure x)

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : ¬n < size x
⊢ SatisfiesM (fun y => size y = size x) (pure x)
Tactic:
exact ⟨pure ⟨x,rfl⟩, map_pure Subtype.val _⟩
State after:
no goals