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

State before:
l : List TensorElem
s : List ℕ
⊢ inferredShape (nested l) = some s → ∃ tail, s = List.length l :: tail
Tactic:
cases s <;> simp [inferredShape]
State after:
case nil
l : List TensorElem
⊢ inferredShape (nested l) = some [] → False

case cons
l : List TensorElem
head✝ : ℕ
tail✝ : List ℕ
⊢ inferredShape (nested l) = some (head✝ :: tail✝) → head✝ = List.length l

State before:
l : List TensorElem
⊢ inferredShape (nested l) = some [] → False
Tactic:
case nil =>
  cases l <;> simp [inferredShape]
  case cons head tail =>
    cases tail <;> simp [inferredShape]
    case nil =>
      cases inferredShape head <;> simp [bind, Option.bind]
    case cons mid tail =>
      cases inferredShape head <;> simp [bind, Option.bind]
      cases inferredShape (.nested (mid :: tail)) <;> simp [Option.bind]
      case some.some s1 s2 =>
        cases s2 <;> simp
        case cons s2_head s2_tail =>
          apply dite (s1 = s2_tail) <;> intros H <;> simp [H]
State after:
no goals

State before:
l : List TensorElem
s_head : ℕ
s_tail : List ℕ
⊢ inferredShape (nested l) = some (s_head :: s_tail) → s_head = List.length l
Tactic:
case cons s_head s_tail =>
  intro H
  let H' := inferredShape_list H
  exact H'.1
State after:
no goals

State before:
l : List TensorElem
⊢ inferredShape (nested l) = some [] → False
Tactic:
cases l <;> simp [inferredShape]
State after:
case cons
head✝ : TensorElem
tail✝ : List TensorElem
⊢ inferredShape (nested (head✝ :: tail✝)) = some [] → False

State before:
head : TensorElem
tail : List TensorElem
⊢ inferredShape (nested (head :: tail)) = some [] → False
Tactic:
case cons head tail =>
  cases tail <;> simp [inferredShape]
  case nil =>
    cases inferredShape head <;> simp [bind, Option.bind]
  case cons mid tail =>
    cases inferredShape head <;> simp [bind, Option.bind]
    cases inferredShape (.nested (mid :: tail)) <;> simp [Option.bind]
    case some.some s1 s2 =>
      cases s2 <;> simp
      case cons s2_head s2_tail =>
        apply dite (s1 = s2_tail) <;> intros H <;> simp [H]
State after:
no goals

State before:
head : TensorElem
tail : List TensorElem
⊢ inferredShape (nested (head :: tail)) = some [] → False
Tactic:
cases tail <;> simp [inferredShape]
State after:
case nil
head : TensorElem
⊢ (do
        let __do_lift ← inferredShape head
        some (1 :: __do_lift)) =
      some [] →
    False

case cons
head head✝ : TensorElem
tail✝ : List TensorElem
⊢ (do
        let s1 ← inferredShape head
        let s2 ← inferredShape (nested (head✝ :: tail✝))
        match s2 with
          | [] => none
          | head :: tail => if s1 = tail then some ((head + 1) :: tail) else none) =
      some [] →
    False

State before:
head : TensorElem
⊢ (do
        let __do_lift ← inferredShape head
        some (1 :: __do_lift)) =
      some [] →
    False
Tactic:
case nil =>
  cases inferredShape head <;> simp [bind, Option.bind]
State after:
no goals

State before:
head mid : TensorElem
tail : List TensorElem
⊢ (do
        let s1 ← inferredShape head
        let s2 ← inferredShape (nested (mid :: tail))
        match s2 with
          | [] => none
          | head :: tail => if s1 = tail then some ((head + 1) :: tail) else none) =
      some [] →
    False
Tactic:
case cons mid tail =>
  cases inferredShape head <;> simp [bind, Option.bind]
  cases inferredShape (.nested (mid :: tail)) <;> simp [Option.bind]
  case some.some s1 s2 =>
    cases s2 <;> simp
    case cons s2_head s2_tail =>
      apply dite (s1 = s2_tail) <;> intros H <;> simp [H]
State after:
no goals

State before:
head : TensorElem
⊢ (do
        let __do_lift ← inferredShape head
        some (1 :: __do_lift)) =
      some [] →
    False
Tactic:
cases inferredShape head <;> simp [bind, Option.bind]
State after:
no goals

State before:
head mid : TensorElem
tail : List TensorElem
⊢ (do
        let s1 ← inferredShape head
        let s2 ← inferredShape (nested (mid :: tail))
        match s2 with
          | [] => none
          | head :: tail => if s1 = tail then some ((head + 1) :: tail) else none) =
      some [] →
    False
Tactic:
cases inferredShape head <;> simp [bind, Option.bind]
State after:
case some
head mid : TensorElem
tail : List TensorElem
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 [] →
    False

State before:
case some
head mid : TensorElem
tail : List TensorElem
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 [] →
    False
Tactic:
cases inferredShape (.nested (mid :: tail)) <;> simp [Option.bind]
State after:
case some.some
head mid : TensorElem
tail : List TensorElem
val✝¹ val✝ : List ℕ
⊢ (match val✝ with
      | [] => none
      | head :: tail => if val✝¹ = tail then some ((head + 1) :: tail) else none) =
      some [] →
    False

State before:
head mid : TensorElem
tail : List TensorElem
s1 s2 : List ℕ
⊢ (match s2 with
      | [] => none
      | head :: tail => if s1 = tail then some ((head + 1) :: tail) else none) =
      some [] →
    False
Tactic:
case some.some s1 s2 =>
  cases s2 <;> simp
  case cons s2_head s2_tail =>
    apply dite (s1 = s2_tail) <;> intros H <;> simp [H]
State after:
no goals

State before:
head mid : TensorElem
tail : List TensorElem
s1 s2 : List ℕ
⊢ (match s2 with
      | [] => none
      | head :: tail => if s1 = tail then some ((head + 1) :: tail) else none) =
      some [] →
    False
Tactic:
cases s2 <;> simp
State after:
case cons
head mid : TensorElem
tail : List TensorElem
s1 : List ℕ
head✝ : ℕ
tail✝ : List ℕ
⊢ (if s1 = tail✝ then some ((head✝ + 1) :: tail✝) else none) = some [] → False

State before:
head mid : TensorElem
tail : List TensorElem
s1 : List ℕ
s2_head : ℕ
s2_tail : List ℕ
⊢ (if s1 = s2_tail then some ((s2_head + 1) :: s2_tail) else none) = some [] → False
Tactic:
case cons s2_head s2_tail =>
  apply dite (s1 = s2_tail) <;> intros H <;> simp [H]
State after:
no goals

State before:
head mid : TensorElem
tail : List TensorElem
s1 : List ℕ
s2_head : ℕ
s2_tail : List ℕ
⊢ (if s1 = s2_tail then some ((s2_head + 1) :: s2_tail) else none) = some [] → False
Tactic:
apply dite (s1 = s2_tail) <;> intros H <;> simp [H]
State after:
no goals

State before:
l : List TensorElem
s_head : ℕ
s_tail : List ℕ
⊢ inferredShape (nested l) = some (s_head :: s_tail) → s_head = List.length l
Tactic:
intro H
State after:
l : List TensorElem
s_head : ℕ
s_tail : List ℕ
H : inferredShape (nested l) = some (s_head :: s_tail)
⊢ s_head = List.length l

State before:
l : List TensorElem
s_head : ℕ
s_tail : List ℕ
H : inferredShape (nested l) = some (s_head :: s_tail)
⊢ s_head = List.length l
Tactic:
let H' := inferredShape_list H
State after:
l : List TensorElem
s_head : ℕ
s_tail : List ℕ
H : inferredShape (nested l) = some (s_head :: s_tail)
H' : s_head = List.length l ∧ (List.all l fun x => decide (inferredShape x = some s_tail)) = true :=
  inferredShape_list H
⊢ s_head = List.length l

State before:
l : List TensorElem
s_head : ℕ
s_tail : List ℕ
H : inferredShape (nested l) = some (s_head :: s_tail)
H' : s_head = List.length l ∧ (List.all l fun x => decide (inferredShape x = some s_tail)) = true :=
  inferredShape_list H
⊢ s_head = List.length l
Tactic:
exact H'.1
State after:
no goals