internlm/Lean-Github huggingface dataset:
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested (mid :: tail)) = some (head :: tail_1) →
      head = List.length (mid :: tail) ∧ (List.all (mid :: tail) fun x => decide (inferredShape x = some tail_1)) = true
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
⊢ s_head = Nat.succ (List.length (mid :: tail)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Tactic:
specialize (ih H'.2.2)
Proof state after:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ s_head = Nat.succ (List.length (mid :: tail)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ s_head = Nat.succ (List.length (mid :: tail)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Tactic:
constructor
Proof state after:
case left
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ s_head = Nat.succ (List.length (mid :: tail))

case right
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
case left
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ s_head = Nat.succ (List.length (mid :: tail))

case right
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Tactic:
. have helper: forall {n m}, n > 0 → n - 1 = m → n = m + 1 := by
    sorry
  simp [helper H'.1 ih.1]
Proof state after:
case right
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
case right
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Tactic:
. sorry
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ ∀ {n m : ℕ}, n > 0 → n - 1 = m → n = m + 1
Tactic:
sorry
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof state before:
l : List TensorElem
s : List ℕ
⊢ inferredShape (nested l) = some s → ∃ tail, s = List.length l :: tail
Tactic:
cases s <;> simp [inferredShape]
Proof 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
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof state before:
l : List TensorElem
⊢ inferredShape (nested l) = some [] → False
Tactic:
cases l <;> simp [inferredShape]
Proof state after:
case cons
head✝ : TensorElem
tail✝ : List TensorElem
⊢ inferredShape (nested (head✝ :: tail✝)) = some [] → False
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof state before:
head : TensorElem
tail : List TensorElem
⊢ inferredShape (nested (head :: tail)) = some [] → False
Tactic:
cases tail <;> simp [inferredShape]
Proof 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
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof state before:
head : TensorElem
⊢ (do
        let __do_lift ← inferredShape head
        some (1 :: __do_lift)) =
      some [] →
    False
Tactic:
cases inferredShape head <;> simp [bind, Option.bind]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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]
Proof 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
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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]
Proof 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
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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
Proof 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
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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
Proof state after:
l : List TensorElem
s_head : ℕ
s_tail : List ℕ
H : inferredShape (nested l) = some (s_head :: s_tail)
⊢ s_head = List.length l
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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
Proof 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
Theorem: MLIR.AST.TensorElem.inferredShape_list_to_cons
Proof 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
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
⊢ ∀ (e : TensorElem) (shape : List ℕ), inferredShape e = some shape → hasShape e shape = true
Tactic:
intro e
Proof state after:
e : TensorElem
⊢ ∀ (shape : List ℕ), inferredShape e = some shape → hasShape e shape = true
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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))
Proof 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
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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 *
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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 *
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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 *
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e : TensorElem
⊢ ∀ (s : List ℕ), inferredShape empty = some s → hasShape empty s = true
Tactic:
case empty =>
  simp [inferredShape]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e : TensorElem
⊢ ∀ (a : ℤ) (s : List ℕ), inferredShape (int a) = some s → hasShape (int a) s = true
Tactic:
intros _ s H
Proof state after:
e : TensorElem
a✝ : ℤ
s : List ℕ
H : inferredShape (int a✝) = some s
⊢ hasShape (int a✝) s = true
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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 *
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e : TensorElem
⊢ ∀ (a : Bool) (s : List ℕ), inferredShape (bool a) = some s → hasShape (bool a) s = true
Tactic:
intros _ s H
Proof state after:
e : TensorElem
a✝ : Bool
s : List ℕ
H : inferredShape (bool a✝) = some s
⊢ hasShape (bool a✝) s = true
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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 *
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e : TensorElem
⊢ ∀ (a : Float) (s : List ℕ), inferredShape (float a) = some s → hasShape (float a) s = true
Tactic:
intros _ s H
Proof state after:
e : TensorElem
a✝ : Float
s : List ℕ
H : inferredShape (float a✝) = some s
⊢ hasShape (float a✝) s = true
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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 *
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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
Proof 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
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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
Proof 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
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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'
Proof 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
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof 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]
Proof state after:
no goals