Theorem: MLIR.AST.TensorElem.inferredShape_cons (MLIR/Semantics/TensorElem.lean)

State before:
⊢ ∀ (head : TensorElem) (tail : List TensorElem) (s_head : ℕ) (s_tail : List ℕ),
    inferredShape (nested tail) = some (s_head :: s_tail) →
      inferredShape head = some s_tail → inferredShape (nested (head :: tail)) = some ((s_head + 1) :: s_tail)
Tactic:
intros head tail s_head s_tail H1 H2
State after:
head : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail : List ℕ
H1 : inferredShape (nested tail) = some (s_head :: s_tail)
H2 : inferredShape head = some s_tail
⊢ inferredShape (nested (head :: tail)) = some ((s_head + 1) :: s_tail)

State before:
head : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail : List ℕ
H1 : inferredShape (nested tail) = some (s_head :: s_tail)
H2 : inferredShape head = some s_tail
⊢ inferredShape (nested (head :: tail)) = some ((s_head + 1) :: s_tail)
Tactic:
cases tail
State after:
case nil
head : TensorElem
s_head : ℕ
s_tail : List ℕ
H2 : inferredShape head = some s_tail
H1 : inferredShape (nested []) = some (s_head :: s_tail)
⊢ inferredShape (nested [head]) = some ((s_head + 1) :: s_tail)

case cons
head : TensorElem
s_head : ℕ
s_tail : List ℕ
H2 : inferredShape head = some s_tail
head✝ : TensorElem
tail✝ : List TensorElem
H1 : inferredShape (nested (head✝ :: tail✝)) = some (s_head :: s_tail)
⊢ inferredShape (nested (head :: head✝ :: tail✝)) = some ((s_head + 1) :: s_tail)

State before:
case nil
head : TensorElem
s_head : ℕ
s_tail : List ℕ
H2 : inferredShape head = some s_tail
H1 : inferredShape (nested []) = some (s_head :: s_tail)
⊢ inferredShape (nested [head]) = some ((s_head + 1) :: s_tail)

case cons
head : TensorElem
s_head : ℕ
s_tail : List ℕ
H2 : inferredShape head = some s_tail
head✝ : TensorElem
tail✝ : List TensorElem
H1 : inferredShape (nested (head✝ :: tail✝)) = some (s_head :: s_tail)
⊢ inferredShape (nested (head :: head✝ :: tail✝)) = some ((s_head + 1) :: s_tail)
Tactic:
. simp [inferredShape, H2, bind, Option.bind] at *; simp[H1.1];
State after:
case cons
head : TensorElem
s_head : ℕ
s_tail : List ℕ
H2 : inferredShape head = some s_tail
head✝ : TensorElem
tail✝ : List TensorElem
H1 : inferredShape (nested (head✝ :: tail✝)) = some (s_head :: s_tail)
⊢ inferredShape (nested (head :: head✝ :: tail✝)) = some ((s_head + 1) :: s_tail)

State before:
case cons
head : TensorElem
s_head : ℕ
s_tail : List ℕ
H2 : inferredShape head = some s_tail
head✝ : TensorElem
tail✝ : List TensorElem
H1 : inferredShape (nested (head✝ :: tail✝)) = some (s_head :: s_tail)
⊢ inferredShape (nested (head :: head✝ :: tail✝)) = some ((s_head + 1) :: s_tail)
Tactic:
. simp [inferredShape, H2, bind, Option.bind, H1]
State after:
no goals