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

State before:
⊢ ∀ {head mid : TensorElem} {tail : List TensorElem} {s_head : ℕ} {s_tail : List ℕ},
    inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail) →
      s_head > 0 ∧
        inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)
Tactic:
intros head mid tail s_head s_tail
State after:
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail : List ℕ
⊢ inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail) →
    s_head > 0 ∧ inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)

State before:
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail : List ℕ
⊢ inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail) →
    s_head > 0 ∧ inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)
Tactic:
simp [inferredShape, bind, Option.bind]
State after:
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail : List ℕ
⊢ (match inferredShape head, fun s1 =>
        match inferredShape (nested (mid :: tail)), fun s2 =>
          match s2 with
          | [] => none
          | head :: tail => if s1 = tail then some ((head + 1) :: tail) else none with
        | none, x => none
        | some a, b => b a with
      | none, x => none
      | some a, b => b a) =
      some (s_head :: s_tail) →
    0 < s_head ∧ inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)

State before:
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail : List ℕ
⊢ (match inferredShape head, fun s1 =>
        match inferredShape (nested (mid :: tail)), fun s2 =>
          match s2 with
          | [] => none
          | head :: tail => if s1 = tail then some ((head + 1) :: tail) else none with
        | none, x => none
        | some a, b => b a with
      | none, x => none
      | some a, b => b a) =
      some (s_head :: s_tail) →
    0 < s_head ∧ inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)
Tactic:
cases inferredShape head <;> simp
State after:
case some
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail val✝ : List ℕ
⊢ (match inferredShape (nested (mid :: tail)), fun s2 =>
        match s2 with
        | [] => none
        | head :: tail => if val✝ = tail then some ((head + 1) :: tail) else none with
      | none, x => none
      | some a, b => b a) =
      some (s_head :: s_tail) →
    0 < s_head ∧ val✝ = s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)

State before:
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
⊢ (match inferredShape (nested (mid :: tail)), fun s2 =>
        match s2 with
        | [] => none
        | head :: tail => if head_shape = tail then some ((head + 1) :: tail) else none with
      | none, x => none
      | some a, b => b a) =
      some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)
Tactic:
case some head_shape =>
cases inferredShape (.nested (mid :: tail)) <;> simp
case some tail_shape =>
cases tail_shape <;> simp
case cons s_head' s_tail' =>
apply dite (head_shape = s_tail')
. intros Heq; rw [Heq]; simp
  intros H H'; rw [←H, Nat.add_sub_self_right, ←H']
  exact ⟨by simp_arith, rfl, rfl, rfl⟩
. intros Hne; simp [Hne]
State after:
no goals

State before:
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
⊢ (match inferredShape (nested (mid :: tail)), fun s2 =>
        match s2 with
        | [] => none
        | head :: tail => if head_shape = tail then some ((head + 1) :: tail) else none with
      | none, x => none
      | some a, b => b a) =
      some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)
Tactic:
cases inferredShape (.nested (mid :: tail)) <;> simp
State after:
case some
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape val✝ : List ℕ
⊢ (match val✝ with
      | [] => none
      | head :: tail => if head_shape = tail then some ((head + 1) :: tail) else none) =
      some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ val✝ = (s_head - 1) :: s_tail

State before:
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape tail_shape : List ℕ
⊢ (match tail_shape with
      | [] => none
      | head :: tail => if head_shape = tail then some ((head + 1) :: tail) else none) =
      some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ tail_shape = (s_head - 1) :: s_tail
Tactic:
case some tail_shape =>
cases tail_shape <;> simp
case cons s_head' s_tail' =>
apply dite (head_shape = s_tail')
. intros Heq; rw [Heq]; simp
  intros H H'; rw [←H, Nat.add_sub_self_right, ←H']
  exact ⟨by simp_arith, rfl, rfl, rfl⟩
. intros Hne; simp [Hne]
State after:
no goals

State before:
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape tail_shape : List ℕ
⊢ (match tail_shape with
      | [] => none
      | head :: tail => if head_shape = tail then some ((head + 1) :: tail) else none) =
      some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ tail_shape = (s_head - 1) :: s_tail
Tactic:
cases tail_shape <;> simp
State after:
case cons
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
head✝ : ℕ
tail✝ : List ℕ
⊢ (if head_shape = tail✝ then some ((head✝ + 1) :: tail✝) else none) = some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ head✝ = s_head - 1 ∧ tail✝ = s_tail

State before:
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
s_head' : ℕ
s_tail' : List ℕ
⊢ (if head_shape = s_tail' then some ((s_head' + 1) :: s_tail') else none) = some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ s_head' = s_head - 1 ∧ s_tail' = s_tail
Tactic:
case cons s_head' s_tail' =>
apply dite (head_shape = s_tail')
. intros Heq; rw [Heq]; simp
  intros H H'; rw [←H, Nat.add_sub_self_right, ←H']
  exact ⟨by simp_arith, rfl, rfl, rfl⟩
. intros Hne; simp [Hne]
State after:
no goals

State before:
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
s_head' : ℕ
s_tail' : List ℕ
⊢ (if head_shape = s_tail' then some ((s_head' + 1) :: s_tail') else none) = some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ s_head' = s_head - 1 ∧ s_tail' = s_tail
Tactic:
apply dite (head_shape = s_tail')
State after:
case t
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
s_head' : ℕ
s_tail' : List ℕ
⊢ head_shape = s_tail' →
    (if head_shape = s_tail' then some ((s_head' + 1) :: s_tail') else none) = some (s_head :: s_tail) →
      0 < s_head ∧ head_shape = s_tail ∧ s_head' = s_head - 1 ∧ s_tail' = s_tail

case e
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
s_head' : ℕ
s_tail' : List ℕ
⊢ ¬head_shape = s_tail' →
    (if head_shape = s_tail' then some ((s_head' + 1) :: s_tail') else none) = some (s_head :: s_tail) →
      0 < s_head ∧ head_shape = s_tail ∧ s_head' = s_head - 1 ∧ s_tail' = s_tail

State before:
case t
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
s_head' : ℕ
s_tail' : List ℕ
⊢ head_shape = s_tail' →
    (if head_shape = s_tail' then some ((s_head' + 1) :: s_tail') else none) = some (s_head :: s_tail) →
      0 < s_head ∧ head_shape = s_tail ∧ s_head' = s_head - 1 ∧ s_tail' = s_tail

case e
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
s_head' : ℕ
s_tail' : List ℕ
⊢ ¬head_shape = s_tail' →
    (if head_shape = s_tail' then some ((s_head' + 1) :: s_tail') else none) = some (s_head :: s_tail) →
      0 < s_head ∧ head_shape = s_tail ∧ s_head' = s_head - 1 ∧ s_tail' = s_tail
Tactic:
. intros Heq; rw [Heq]; simp
  intros H H'; rw [←H, Nat.add_sub_self_right, ←H']
  exact ⟨by simp_arith, rfl, rfl, rfl⟩
State after:
case e
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
s_head' : ℕ
s_tail' : List ℕ
⊢ ¬head_shape = s_tail' →
    (if head_shape = s_tail' then some ((s_head' + 1) :: s_tail') else none) = some (s_head :: s_tail) →
      0 < s_head ∧ head_shape = s_tail ∧ s_head' = s_head - 1 ∧ s_tail' = s_tail

State before:
case e
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
s_head' : ℕ
s_tail' : List ℕ
⊢ ¬head_shape = s_tail' →
    (if head_shape = s_tail' then some ((s_head' + 1) :: s_tail') else none) = some (s_head :: s_tail) →
      0 < s_head ∧ head_shape = s_tail ∧ s_head' = s_head - 1 ∧ s_tail' = s_tail
Tactic:
. intros Hne; simp [Hne]
State after:
no goals

State before:
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
s_head' : ℕ
s_tail' : List ℕ
Heq : head_shape = s_tail'
H : s_head' + 1 = s_head
H' : s_tail' = s_tail
⊢ 0 < s_head' + 1
Tactic:
simp_arith
State after:
no goals