internlm/Lean-Github huggingface dataset:
Theorem: MLIR.AST.TensorElem.inferredShape_cons_inv
Proof 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]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_cons_inv
Proof 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
Proof 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
Theorem: MLIR.AST.TensorElem.inferredShape_cons_inv
Proof 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]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_cons_inv
Proof 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
Proof 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
Theorem: MLIR.AST.TensorElem.inferredShape_cons_inv
Proof 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]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_cons_inv
Proof 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')
Proof 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
Theorem: MLIR.AST.TensorElem.inferredShape_cons_inv
Proof 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⟩
Proof 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
Theorem: MLIR.AST.TensorElem.inferredShape_cons_inv
Proof 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]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_cons_inv
Proof 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
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
l : List TensorElem
head : ℕ
tail : List ℕ
⊢ inferredShape (nested l) = some (head :: tail) →
    head = List.length l ∧ (List.all l fun x => decide (inferredShape x = some tail)) = true
Tactic:
revert head tail
Proof state after:
l : List TensorElem
⊢ ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested l) = some (head :: tail) →
      head = List.length l ∧ (List.all l fun x => decide (inferredShape x = some tail)) = true
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
l : List TensorElem
⊢ ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested l) = some (head :: tail) →
      head = List.length l ∧ (List.all l fun x => decide (inferredShape x = some tail)) = true
Tactic:
induction l <;> simp
Proof state after:
case nil

⊢ ∀ {head : ℕ} {tail : List ℕ}, inferredShape (nested []) = some (head :: tail) → head = 0

case cons
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested tail✝) = some (head :: tail) →
      head = List.length tail✝ ∧ (List.all tail✝ fun x => decide (inferredShape x = some tail)) = true
⊢ ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested (head✝ :: tail✝)) = some (head :: tail) →
      head = Nat.succ (List.length tail✝) ∧
        inferredShape head✝ = some tail ∧ ∀ (x : TensorElem), x ∈ tail✝ → inferredShape x = some tail
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
⊢ ∀ {head : ℕ} {tail : List ℕ}, inferredShape (nested []) = some (head :: tail) → head = 0
Tactic:
case nil =>
  intros head tile H; simp [inferredShape, List.all_nil] at *; simp [H.1]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested tail) = some (head :: tail_1) →
      head = List.length tail ∧ (List.all tail fun x => decide (inferredShape x = some tail_1)) = true
⊢ ∀ {head_1 : ℕ} {tail_1 : List ℕ},
    inferredShape (nested (head :: tail)) = some (head_1 :: tail_1) →
      head_1 = Nat.succ (List.length tail) ∧
        inferredShape head = some tail_1 ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some tail_1
Tactic:
case cons head tail ih =>
  intros s_head s_tail H
  cases tail
  case nil =>
    simp [inferredShape, List.all_one]
    simp [inferredShape, bind, Option.bind, List.all_one] at H
    split at H; trivial; simp at H
    case h_2 _ s_mid H' =>
      simp [←H.1, H', H.2]
  case cons mid tail =>
    let H' := inferredShape_cons_inv H
    specialize (ih H'.2.2)
    constructor
    . have helper: forall {n m}, n > 0 → n - 1 = m → n = m + 1 := by
        sorry
      simp [helper H'.1 ih.1]
    . sorry
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
⊢ ∀ {head : ℕ} {tail : List ℕ}, inferredShape (nested []) = some (head :: tail) → head = 0
Tactic:
intros head tile H
Proof state after:
head : ℕ
tile : List ℕ
H : inferredShape (nested []) = some (head :: tile)
⊢ head = 0
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : ℕ
tile : List ℕ
H : inferredShape (nested []) = some (head :: tile)
⊢ head = 0
Tactic:
simp [inferredShape, List.all_nil] at *
Proof state after:
head : ℕ
tile : List ℕ
H : 0 = head ∧ [] = tile
⊢ head = 0
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : ℕ
tile : List ℕ
H : 0 = head ∧ [] = tile
⊢ head = 0
Tactic:
simp [H.1]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested tail) = some (head :: tail_1) →
      head = List.length tail ∧ (List.all tail fun x => decide (inferredShape x = some tail_1)) = true
⊢ ∀ {head_1 : ℕ} {tail_1 : List ℕ},
    inferredShape (nested (head :: tail)) = some (head_1 :: tail_1) →
      head_1 = Nat.succ (List.length tail) ∧
        inferredShape head = some tail_1 ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some tail_1
Tactic:
intros s_head s_tail H
Proof state after:
head : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested tail) = some (head :: tail_1) →
      head = List.length tail ∧ (List.all tail fun x => decide (inferredShape x = some tail_1)) = true
s_head : ℕ
s_tail : List ℕ
H : inferredShape (nested (head :: tail)) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length tail) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some s_tail
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested tail) = some (head :: tail_1) →
      head = List.length tail ∧ (List.all tail fun x => decide (inferredShape x = some tail_1)) = true
s_head : ℕ
s_tail : List ℕ
H : inferredShape (nested (head :: tail)) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length tail) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some s_tail
Tactic:
cases tail
Proof state after:
case nil
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested [head]) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length []) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ [] → inferredShape x = some s_tail

case cons
head : TensorElem
s_head : ℕ
s_tail : List ℕ
head✝ : TensorElem
tail✝ : List TensorElem
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested (head✝ :: tail✝)) = some (head :: tail) →
      head = List.length (head✝ :: tail✝) ∧
        (List.all (head✝ :: tail✝) fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested (head :: head✝ :: tail✝)) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length (head✝ :: tail✝)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ head✝ :: tail✝ → inferredShape x = some s_tail
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested [head]) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length []) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ [] → inferredShape x = some s_tail
Tactic:
case nil =>
  simp [inferredShape, List.all_one]
  simp [inferredShape, bind, Option.bind, List.all_one] at H
  split at H; trivial; simp at H
  case h_2 _ s_mid H' =>
    simp [←H.1, H', H.2]
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
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)
⊢ s_head = Nat.succ (List.length (mid :: tail)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Tactic:
case cons mid tail =>
  let H' := inferredShape_cons_inv H
  specialize (ih H'.2.2)
  constructor
  . have helper: forall {n m}, n > 0 → n - 1 = m → n = m + 1 := by
      sorry
    simp [helper H'.1 ih.1]
  . sorry
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested [head]) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length []) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ [] → inferredShape x = some s_tail
Tactic:
simp [inferredShape, List.all_one]
Proof state after:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested [head]) = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested [head]) = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Tactic:
simp [inferredShape, bind, Option.bind, List.all_one] at H
Proof state after:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H :
  (match inferredShape head, fun __do_lift => some (1 :: __do_lift) with
    | none, x => none
    | some a, b => b a) =
    some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H :
  (match inferredShape head, fun __do_lift => some (1 :: __do_lift) with
    | none, x => none
    | some a, b => b a) =
    some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Tactic:
split at H
Proof state after:
case h_1
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
heq✝ : inferredShape head = none
H : none = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail

case h_2
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
a✝ : List ℕ
heq✝ : inferredShape head = some a✝
H : (fun __do_lift => some (1 :: __do_lift)) a✝ = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
case h_1
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
heq✝ : inferredShape head = none
H : none = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail

case h_2
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
a✝ : List ℕ
heq✝ : inferredShape head = some a✝
H : (fun __do_lift => some (1 :: __do_lift)) a✝ = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Tactic:
trivial
Proof state after:
case h_2
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
a✝ : List ℕ
heq✝ : inferredShape head = some a✝
H : (fun __do_lift => some (1 :: __do_lift)) a✝ = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
case h_2
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
a✝ : List ℕ
heq✝ : inferredShape head = some a✝
H : (fun __do_lift => some (1 :: __do_lift)) a✝ = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Tactic:
simp at H
Proof state after:
case h_2
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
a✝ : List ℕ
heq✝ : inferredShape head = some a✝
H : 1 = s_head ∧ a✝ = s_tail
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
s_mid : List ℕ
H' : inferredShape head = some s_mid
H : 1 = s_head ∧ s_mid = s_tail
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Tactic:
case h_2 _ s_mid H' =>
  simp [←H.1, H', H.2]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_list
Proof state before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
s_mid : List ℕ
H' : inferredShape head = some s_mid
H : 1 = s_head ∧ s_mid = s_tail
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Tactic:
simp [←H.1, H', H.2]
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
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)
⊢ s_head = Nat.succ (List.length (mid :: tail)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Tactic:
let H' := inferredShape_cons_inv H
Proof state after:
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