Theorem: ExtractSliceGenericCommute1D.equiv (MLIR/Dialects/LinalgSemantics.lean)

State before:
r✝ : Region linalg
t : Tensor1D
r : Region linalg
rSpec : ℤ → FinInt 32 → FinInt 32
⊢ validGenericRegion r rSpec →
    run ⟦ LHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })]) =
      run ⟦ RHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })])
Tactic:
intros valid_r
State after:
r✝ : Region linalg
t : Tensor1D
r : Region linalg
rSpec : ℤ → FinInt 32 → FinInt 32
valid_r : validGenericRegion r rSpec
⊢ run ⟦ LHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })]) =
    run ⟦ RHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })])

State before:
r✝ : Region linalg
t : Tensor1D
r : Region linalg
rSpec : ℤ → FinInt 32 → FinInt 32
valid_r : validGenericRegion r rSpec
⊢ run ⟦ LHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })]) =
    run ⟦ RHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })])
Tactic:
simp[LHS, RHS]
State after:
r✝ : Region linalg
t : Tensor1D
r : Region linalg
rSpec : ℤ → FinInt 32 → FinInt 32
valid_r : validGenericRegion r rSpec
⊢ run
      (denoteRegion linalg
        (Region.mk "entry" []
          [Op.mk "linalg.generic1d" [(SSAVal.SSAVal "x", MLIRType.tensor1d)] [(SSAVal.SSAVal "t", MLIRType.tensor1d)]
              [r] (AttrDict.mk [AttrEntry.mk "len" (AttrValue.int 10 MLIRType.index)]),
            Op.mk "linalg.fill1d" [(SSAVal.SSAVal "out", MLIRType.tensor1d)] [(SSAVal.SSAVal "x", MLIRType.tensor1d)] []
              (AttrDict.mk [AttrEntry.mk "cst" (AttrValue.int 42 MLIRType.index)])])
        [])
      (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })]) =
    run
      (denoteRegion linalg
        (Region.mk "entry" []
          [Op.mk "linalg.generic1d" [(SSAVal.SSAVal "x", MLIRType.tensor1d)] [(SSAVal.SSAVal "t", MLIRType.tensor1d)]
              [r] (AttrDict.mk [AttrEntry.mk "cst" (AttrValue.int 42 MLIRType.index)]),
            Op.mk "linalg.extractslice1d" [(SSAVal.SSAVal "out", MLIRType.tensor1d)]
              [(SSAVal.SSAVal "x", MLIRType.tensor1d)] []
              (AttrDict.mk [AttrEntry.mk "len" (AttrValue.int 10 MLIRType.index)])])
        [])
      (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })])

State before:
r✝ : Region linalg
t : Tensor1D
r : Region linalg
rSpec : ℤ → FinInt 32 → FinInt 32
valid_r : validGenericRegion r rSpec
⊢ run
      (denoteRegion linalg
        (Region.mk "entry" []
          [Op.mk "linalg.generic1d" [(SSAVal.SSAVal "x", MLIRType.tensor1d)] [(SSAVal.SSAVal "t", MLIRType.tensor1d)]
              [r] (AttrDict.mk [AttrEntry.mk "len" (AttrValue.int 10 MLIRType.index)]),
            Op.mk "linalg.fill1d" [(SSAVal.SSAVal "out", MLIRType.tensor1d)] [(SSAVal.SSAVal "x", MLIRType.tensor1d)] []
              (AttrDict.mk [AttrEntry.mk "cst" (AttrValue.int 42 MLIRType.index)])])
        [])
      (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })]) =
    run
      (denoteRegion linalg
        (Region.mk "entry" []
          [Op.mk "linalg.generic1d" [(SSAVal.SSAVal "x", MLIRType.tensor1d)] [(SSAVal.SSAVal "t", MLIRType.tensor1d)]
              [r] (AttrDict.mk [AttrEntry.mk "cst" (AttrValue.int 42 MLIRType.index)]),
            Op.mk "linalg.extractslice1d" [(SSAVal.SSAVal "out", MLIRType.tensor1d)]
              [(SSAVal.SSAVal "x", MLIRType.tensor1d)] []
              (AttrDict.mk [AttrEntry.mk "len" (AttrValue.int 10 MLIRType.index)])])
        [])
      (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })])
Tactic:
sorry
State after:
no goals