Theorem: Tensor1D.mapM_map (MLIR/Util/KDTensor.lean)

State before:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
⊢ (∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)) →
    mapMWithFlatIndex v fM = pure (mapWithFlatIndex v f)
Tactic:
intros h
State after:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ mapMWithFlatIndex v fM = pure (mapWithFlatIndex v f)

State before:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ mapMWithFlatIndex v fM = pure (mapWithFlatIndex v f)
Tactic:
unfold mapWithFlatIndex
State after:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ mapMWithFlatIndex v fM =
    pure
      { size0 := v.size0,
        data :=
          List.map
            (fun x =>
              match x with
              | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data),
        h_data_size :=
          (_ :
            List.length
                (List.map
                  (fun x =>
                    match x with
                    | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
                  (List.zipFlatIndex v.data)) =
              v.size0) }

State before:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ mapMWithFlatIndex v fM =
    pure
      { size0 := v.size0,
        data :=
          List.map
            (fun x =>
              match x with
              | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data),
        h_data_size :=
          (_ :
            List.length
                (List.map
                  (fun x =>
                    match x with
                    | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
                  (List.zipFlatIndex v.data)) =
              v.size0) }
Tactic:
unfold mapMWithFlatIndex
State after:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ (do
      let data ←
        List.mapM
            (fun x =>
              match x with
              | (val, ix) => fM ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data)
      let temp : Tensor1D :=
        { size0 := List.length data, data := data, h_data_size := (_ : List.length data = List.length data) }
      pure temp) =
    pure
      { size0 := v.size0,
        data :=
          List.map
            (fun x =>
              match x with
              | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data),
        h_data_size :=
          (_ :
            List.length
                (List.map
                  (fun x =>
                    match x with
                    | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
                  (List.zipFlatIndex v.data)) =
              v.size0) }

State before:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ (do
      let data ←
        List.mapM
            (fun x =>
              match x with
              | (val, ix) => fM ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data)
      let temp : Tensor1D :=
        { size0 := List.length data, data := data, h_data_size := (_ : List.length data = List.length data) }
      pure temp) =
    pure
      { size0 := v.size0,
        data :=
          List.map
            (fun x =>
              match x with
              | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data),
        h_data_size :=
          (_ :
            List.length
                (List.map
                  (fun x =>
                    match x with
                    | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
                  (List.zipFlatIndex v.data)) =
              v.size0) }
Tactic:
rw [List.mapM_map]
State after:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ (do
      let data ← pure (List.map ?f (List.zipFlatIndex v.data))
      let temp : Tensor1D :=
        { size0 := List.length data, data := data, h_data_size := (_ : List.length data = List.length data) }
      pure temp) =
    pure
      { size0 := v.size0,
        data :=
          List.map
            (fun x =>
              match x with
              | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data),
        h_data_size :=
          (_ :
            List.length
                (List.map
                  (fun x =>
                    match x with
                    | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
                  (List.zipFlatIndex v.data)) =
              v.size0) }

case f
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ FinInt 32 × TensorFlatIndex (List.length v.data) → FinInt 32

case a
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ ∀ (a : FinInt 32 × TensorFlatIndex (List.length v.data)),
    (match a with
      | (val, ix) => fM ((_ : List.length v.data = v.size0) ▸ ix) val) =
      pure (?f a)

State before:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ (do
      let data ← pure (List.map ?f (List.zipFlatIndex v.data))
      let temp : Tensor1D :=
        { size0 := List.length data, data := data, h_data_size := (_ : List.length data = List.length data) }
      pure temp) =
    pure
      { size0 := v.size0,
        data :=
          List.map
            (fun x =>
              match x with
              | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data),
        h_data_size :=
          (_ :
            List.length
                (List.map
                  (fun x =>
                    match x with
                    | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
                  (List.zipFlatIndex v.data)) =
              v.size0) }

case f
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ FinInt 32 × TensorFlatIndex (List.length v.data) → FinInt 32

case a
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ ∀ (a : FinInt 32 × TensorFlatIndex (List.length v.data)),
    (match a with
      | (val, ix) => fM ((_ : List.length v.data = v.size0) ▸ ix) val) =
      pure (?f a)
Tactic:
. simp [v.h_data_size]; rfl
State after:
case a
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ ∀ (a : FinInt 32 × TensorFlatIndex (List.length v.data)),
    (match a with
      | (val, ix) => fM ((_ : List.length v.data = v.size0) ▸ ix) val) =
      pure (f ((_ : List.length v.data = v.size0) ▸ a.snd) a.fst)

State before:
case a
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ ∀ (a : FinInt 32 × TensorFlatIndex (List.length v.data)),
    (match a with
      | (val, ix) => fM ((_ : List.length v.data = v.size0) ▸ ix) val) =
      pure (f ((_ : List.length v.data = v.size0) ▸ a.snd) a.fst)
Tactic:
. intros a; cases a; simp [h]
State after:
no goals