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

State before:
⊢ ∀ (e : TensorElem) (shape : List ℕ), inferredShape e = some shape → hasShape e shape = true
Tactic:
intro e
State after:
e : TensorElem
⊢ ∀ (shape : List ℕ), inferredShape e = some shape → hasShape e shape = true

State before:
e : TensorElem
⊢ ∀ (shape : List ℕ), inferredShape e = some shape → hasShape e shape = true
Tactic:
apply @TensorElem.recOn
  (motive_1 := fun e =>
    ∀s, e.inferredShape = some s → e.hasShape s)
  (motive_2 := fun l =>
    ∀s, l.all (TensorElem.inferredShape . = some s) →
      l.all (TensorElem.hasShape . s))
State after:
case int
e : TensorElem
⊢ ∀ (a : ℤ) (s : List ℕ), inferredShape (int a) = some s → hasShape (int a) s = true

case float
e : TensorElem
⊢ ∀ (a : Float) (s : List ℕ), inferredShape (float a) = some s → hasShape (float a) s = true

case bool
e : TensorElem
⊢ ∀ (a : Bool) (s : List ℕ), inferredShape (bool a) = some s → hasShape (bool a) s = true

case nested
e : TensorElem
⊢ ∀ (a : List TensorElem),
    (∀ (s : List ℕ),
        (List.all a fun x => decide (inferredShape x = some s)) = true → (List.all a fun x => hasShape x s) = true) →
      ∀ (s : List ℕ), inferredShape (nested a) = some s → hasShape (nested a) s = true

case empty
e : TensorElem
⊢ ∀ (s : List ℕ), inferredShape empty = some s → hasShape empty s = true

case nil
e : TensorElem
⊢ ∀ (s : List ℕ),
    (List.all [] fun x => decide (inferredShape x = some s)) = true → (List.all [] fun x => hasShape x s) = true

case cons
e : TensorElem
⊢ ∀ (head : TensorElem) (tail : List TensorElem),
    (∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true) →
      (∀ (s : List ℕ),
          (List.all tail fun x => decide (inferredShape x = some s)) = true →
            (List.all tail fun x => hasShape x s) = true) →
        ∀ (s : List ℕ),
          (List.all (head :: tail) fun x => decide (inferredShape x = some s)) = true →
            (List.all (head :: tail) fun x => hasShape x s) = true

State before:
e : TensorElem
⊢ ∀ (a : ℤ) (s : List ℕ), inferredShape (int a) = some s → hasShape (int a) s = true
Tactic:
case int =>
  intros _ s H; cases s <;> simp [inferredShape, hasShape] at *
State after:
no goals

State before:
e : TensorElem
⊢ ∀ (a : Bool) (s : List ℕ), inferredShape (bool a) = some s → hasShape (bool a) s = true
Tactic:
case bool =>
  intros _ s H; cases s <;> simp [inferredShape, hasShape] at *
State after:
no goals

State before:
e : TensorElem
⊢ ∀ (a : Float) (s : List ℕ), inferredShape (float a) = some s → hasShape (float a) s = true
Tactic:
case float =>
  intros _ s H; cases s <;> simp [inferredShape, hasShape] at *
State after:
no goals

State before:
e : TensorElem
⊢ ∀ (a : List TensorElem),
    (∀ (s : List ℕ),
        (List.all a fun x => decide (inferredShape x = some s)) = true → (List.all a fun x => hasShape x s) = true) →
      ∀ (s : List ℕ), inferredShape (nested a) = some s → hasShape (nested a) s = true
Tactic:
case nested =>
  intros l motive_2 s H
  let H' := inferredShape_list_to_cons H
  cases H'; case intro s_tail Hs =>
    rw [Hs]; rw [Hs] at H; clear Hs H'
    let H' := inferredShape_list H
    simp [hasShape, motive_2 _ H'.2]
State after:
no goals

State before:
e : TensorElem
⊢ ∀ (s : List ℕ), inferredShape empty = some s → hasShape empty s = true
Tactic:
case empty =>
  simp [inferredShape]
State after:
no goals

State before:
e : TensorElem
⊢ ∀ (s : List ℕ),
    (List.all [] fun x => decide (inferredShape x = some s)) = true → (List.all [] fun x => hasShape x s) = true
Tactic:
case nil =>
  intros s H; simp [List.all_nil]
State after:
no goals

State before:
e : TensorElem
⊢ ∀ (head : TensorElem) (tail : List TensorElem),
    (∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true) →
      (∀ (s : List ℕ),
          (List.all tail fun x => decide (inferredShape x = some s)) = true →
            (List.all tail fun x => hasShape x s) = true) →
        ∀ (s : List ℕ),
          (List.all (head :: tail) fun x => decide (inferredShape x = some s)) = true →
            (List.all (head :: tail) fun x => hasShape x s) = true
Tactic:
case cons =>
  intros head tail motive_1 ih s H; simp [List.all_cons] at *
  simp [motive_1 _ H.1, ih _ H.2]
  sorry
State after:
no goals

State before:
e : TensorElem
⊢ ∀ (a : ℤ) (s : List ℕ), inferredShape (int a) = some s → hasShape (int a) s = true
Tactic:
intros _ s H
State after:
e : TensorElem
a✝ : ℤ
s : List ℕ
H : inferredShape (int a✝) = some s
⊢ hasShape (int a✝) s = true

State before:
e : TensorElem
a✝ : ℤ
s : List ℕ
H : inferredShape (int a✝) = some s
⊢ hasShape (int a✝) s = true
Tactic:
cases s <;> simp [inferredShape, hasShape] at *
State after:
no goals

State before:
e : TensorElem
⊢ ∀ (a : Bool) (s : List ℕ), inferredShape (bool a) = some s → hasShape (bool a) s = true
Tactic:
intros _ s H
State after:
e : TensorElem
a✝ : Bool
s : List ℕ
H : inferredShape (bool a✝) = some s
⊢ hasShape (bool a✝) s = true

State before:
e : TensorElem
a✝ : Bool
s : List ℕ
H : inferredShape (bool a✝) = some s
⊢ hasShape (bool a✝) s = true
Tactic:
cases s <;> simp [inferredShape, hasShape] at *
State after:
no goals

State before:
e : TensorElem
⊢ ∀ (a : Float) (s : List ℕ), inferredShape (float a) = some s → hasShape (float a) s = true
Tactic:
intros _ s H
State after:
e : TensorElem
a✝ : Float
s : List ℕ
H : inferredShape (float a✝) = some s
⊢ hasShape (float a✝) s = true

State before:
e : TensorElem
a✝ : Float
s : List ℕ
H : inferredShape (float a✝) = some s
⊢ hasShape (float a✝) s = true
Tactic:
cases s <;> simp [inferredShape, hasShape] at *
State after:
no goals

State before:
e : TensorElem
⊢ ∀ (a : List TensorElem),
    (∀ (s : List ℕ),
        (List.all a fun x => decide (inferredShape x = some s)) = true → (List.all a fun x => hasShape x s) = true) →
      ∀ (s : List ℕ), inferredShape (nested a) = some s → hasShape (nested a) s = true
Tactic:
intros l motive_2 s H
State after:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
⊢ hasShape (nested l) s = true

State before:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
⊢ hasShape (nested l) s = true
Tactic:
let H' := inferredShape_list_to_cons H
State after:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H
⊢ hasShape (nested l) s = true

State before:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H
⊢ hasShape (nested l) s = true
Tactic:
cases H'
State after:
case intro
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H
w✝ : List ℕ
h✝ : s = List.length l :: w✝
⊢ hasShape (nested l) s = true

State before:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H
s_tail : List ℕ
Hs : s = List.length l :: s_tail
⊢ hasShape (nested l) s = true
Tactic:
case intro s_tail Hs =>
rw [Hs]; rw [Hs] at H; clear Hs H'
let H' := inferredShape_list H
simp [hasShape, motive_2 _ H'.2]
State after:
no goals

State before:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H
s_tail : List ℕ
Hs : s = List.length l :: s_tail
⊢ hasShape (nested l) s = true
Tactic:
rw [Hs]
State after:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H
s_tail : List ℕ
Hs : s = List.length l :: s_tail
⊢ hasShape (nested l) (List.length l :: s_tail) = true

State before:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H
s_tail : List ℕ
Hs : s = List.length l :: s_tail
⊢ hasShape (nested l) (List.length l :: s_tail) = true
Tactic:
rw [Hs] at H
State after:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H✝ : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H✝
s_tail : List ℕ
H : inferredShape (nested l) = some (List.length l :: s_tail)
Hs : s = List.length l :: s_tail
⊢ hasShape (nested l) (List.length l :: s_tail) = true

State before:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H✝ : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H✝
s_tail : List ℕ
H : inferredShape (nested l) = some (List.length l :: s_tail)
Hs : s = List.length l :: s_tail
⊢ hasShape (nested l) (List.length l :: s_tail) = true
Tactic:
clear Hs H'
State after:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H✝ : inferredShape (nested l) = some s
s_tail : List ℕ
H : inferredShape (nested l) = some (List.length l :: s_tail)
⊢ hasShape (nested l) (List.length l :: s_tail) = true

State before:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H✝ : inferredShape (nested l) = some s
s_tail : List ℕ
H : inferredShape (nested l) = some (List.length l :: s_tail)
⊢ hasShape (nested l) (List.length l :: s_tail) = true
Tactic:
let H' := inferredShape_list H
State after:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H✝ : inferredShape (nested l) = some s
s_tail : List ℕ
H : inferredShape (nested l) = some (List.length l :: s_tail)
H' : List.length l = List.length l ∧ (List.all l fun x => decide (inferredShape x = some s_tail)) = true :=
  inferredShape_list H
⊢ hasShape (nested l) (List.length l :: s_tail) = true

State before:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H✝ : inferredShape (nested l) = some s
s_tail : List ℕ
H : inferredShape (nested l) = some (List.length l :: s_tail)
H' : List.length l = List.length l ∧ (List.all l fun x => decide (inferredShape x = some s_tail)) = true :=
  inferredShape_list H
⊢ hasShape (nested l) (List.length l :: s_tail) = true
Tactic:
simp [hasShape, motive_2 _ H'.2]
State after:
no goals

State before:
e : TensorElem
⊢ ∀ (s : List ℕ), inferredShape empty = some s → hasShape empty s = true
Tactic:
simp [inferredShape]
State after:
no goals

State before:
e : TensorElem
⊢ ∀ (s : List ℕ),
    (List.all [] fun x => decide (inferredShape x = some s)) = true → (List.all [] fun x => hasShape x s) = true
Tactic:
intros s H
State after:
e : TensorElem
s : List ℕ
H : (List.all [] fun x => decide (inferredShape x = some s)) = true
⊢ (List.all [] fun x => hasShape x s) = true

State before:
e : TensorElem
s : List ℕ
H : (List.all [] fun x => decide (inferredShape x = some s)) = true
⊢ (List.all [] fun x => hasShape x s) = true
Tactic:
simp [List.all_nil]
State after:
no goals

State before:
e : TensorElem
⊢ ∀ (head : TensorElem) (tail : List TensorElem),
    (∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true) →
      (∀ (s : List ℕ),
          (List.all tail fun x => decide (inferredShape x = some s)) = true →
            (List.all tail fun x => hasShape x s) = true) →
        ∀ (s : List ℕ),
          (List.all (head :: tail) fun x => decide (inferredShape x = some s)) = true →
            (List.all (head :: tail) fun x => hasShape x s) = true
Tactic:
intros head tail motive_1 ih s H
State after:
e head : TensorElem
tail : List TensorElem
motive_1 : ∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true
ih :
  ∀ (s : List ℕ),
    (List.all tail fun x => decide (inferredShape x = some s)) = true → (List.all tail fun x => hasShape x s) = true
s : List ℕ
H : (List.all (head :: tail) fun x => decide (inferredShape x = some s)) = true
⊢ (List.all (head :: tail) fun x => hasShape x s) = true

State before:
e head : TensorElem
tail : List TensorElem
motive_1 : ∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true
ih :
  ∀ (s : List ℕ),
    (List.all tail fun x => decide (inferredShape x = some s)) = true → (List.all tail fun x => hasShape x s) = true
s : List ℕ
H : (List.all (head :: tail) fun x => decide (inferredShape x = some s)) = true
⊢ (List.all (head :: tail) fun x => hasShape x s) = true
Tactic:
simp [List.all_cons] at *
State after:
e head : TensorElem
tail : List TensorElem
motive_1 : ∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true
s : List ℕ
ih :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → inferredShape x = some s) → ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
H : inferredShape head = some s ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some s
⊢ hasShape head s = true ∧ ∀ (x : TensorElem), x ∈ tail → hasShape x s = true

State before:
e head : TensorElem
tail : List TensorElem
motive_1 : ∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true
s : List ℕ
ih :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → inferredShape x = some s) → ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
H : inferredShape head = some s ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some s
⊢ hasShape head s = true ∧ ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Tactic:
simp [motive_1 _ H.1, ih _ H.2]
State after:
e head : TensorElem
tail : List TensorElem
motive_1 : ∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true
s : List ℕ
ih :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → inferredShape x = some s) → ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
H : inferredShape head = some s ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some s
⊢ ∀ (x : TensorElem), x ∈ tail → hasShape x s = true

State before:
e head : TensorElem
tail : List TensorElem
motive_1 : ∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true
s : List ℕ
ih :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → inferredShape x = some s) → ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
H : inferredShape head = some s ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some s
⊢ ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Tactic:
sorry
State after:
no goals