internlm/Lean-Github huggingface dataset:
Theorem: DimList.dim_known_prod_refines
Proof state before:
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
S : List ℕ
Hrefines : shapeRefines S (head :: tail) = true
⊢ shapeProd S = prod (head :: tail)
Tactic:
cases S
Proof state after:
case nil
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
Hrefines : shapeRefines [] (head :: tail) = true
⊢ shapeProd [] = prod (head :: tail)

case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ shapeProd (head✝ :: tail✝) = prod (head :: tail)
Theorem: DimList.dim_known_prod_refines
Proof state before:
case nil
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
Hrefines : shapeRefines [] (head :: tail) = true
⊢ shapeProd [] = prod (head :: tail)

case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ shapeProd (head✝ :: tail✝) = prod (head :: tail)
Tactic:
simp at Hrefines
Proof state after:
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ shapeProd (head✝ :: tail✝) = prod (head :: tail)
Theorem: DimList.dim_known_prod_refines
Proof state before:
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ shapeProd (head✝ :: tail✝) = prod (head :: tail)
Tactic:
cases head <;> simp at *
Proof state after:
case cons.Known
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
head✝ : ℕ
tail✝ : List ℕ
a✝ : ℕ
Hknown : known tail = true
Hrefines : head✝ = a✝ ∧ shapeRefines tail✝ tail = true
⊢ head✝ * shapeProd tail✝ = a✝ * prod tail
Theorem: DimList.dim_known_prod_refines
Proof state before:
case cons.Known
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
head✝ : ℕ
tail✝ : List ℕ
a✝ : ℕ
Hknown : known tail = true
Hrefines : head✝ = a✝ ∧ shapeRefines tail✝ tail = true
⊢ head✝ * shapeProd tail✝ = a✝ * prod tail
Tactic:
rw [←Hrefines.1, ←ih Hknown Hrefines.2]
Proof state after:
no goals
Theorem: DimList.defaultRefinement_refines
Proof state before:
D : DimList
⊢ shapeRefines (defaultRefinement D) D = true
Tactic:
induction D <;> simp
Proof state after:
case cons
head✝ : Dimension
tail✝ : List Dimension
tail_ih✝ : shapeRefines (defaultRefinement tail✝) tail✝ = true
⊢ shapeRefines (defaultRefinement (head✝ :: tail✝)) (head✝ :: tail✝) = true
Theorem: DimList.defaultRefinement_refines
Proof state before:
head : Dimension
tail✝ : List Dimension
ih : shapeRefines (defaultRefinement tail✝) tail✝ = true
⊢ shapeRefines (defaultRefinement (head :: tail✝)) (head :: tail✝) = true
Tactic:
case cons head _ ih =>
  cases head <;> simp <;> apply ih
Proof state after:
no goals
Theorem: DimList.defaultRefinement_refines
Proof state before:
head : Dimension
tail✝ : List Dimension
ih : shapeRefines (defaultRefinement tail✝) tail✝ = true
⊢ shapeRefines (defaultRefinement (head :: tail✝)) (head :: tail✝) = true
Tactic:
cases head <;> simp <;> apply ih
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_list
Proof state before:
τ : MLIRTy
l : List TensorElem
h : hasType (nested l) τ = true
⊢ flatten (nested l) h = List.join (mapWithType l flatten h)
Tactic:
revert h
Proof state after:
τ : MLIRTy
l : List TensorElem
⊢ ∀ (h : hasType (nested l) τ = true), flatten (nested l) h = List.join (mapWithType l flatten h)
Theorem: MLIR.AST.TensorElem.flatten_list
Proof state before:
τ : MLIRTy
l : List TensorElem
⊢ ∀ (h : hasType (nested l) τ = true), flatten (nested l) h = List.join (mapWithType l flatten h)
Tactic:
induction l <;> intros h
Proof state after:
case nil
τ : MLIRTy
h : hasType (nested []) τ = true
⊢ flatten (nested []) h = List.join (mapWithType [] flatten h)

case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ : ∀ (h : hasType (nested tail✝) τ = true), flatten (nested tail✝) h = List.join (mapWithType tail✝ flatten h)
h : hasType (nested (head✝ :: tail✝)) τ = true
⊢ flatten (nested (head✝ :: tail✝)) h = List.join (mapWithType (head✝ :: tail✝) flatten h)
Theorem: MLIR.AST.TensorElem.flatten_list
Proof state before:
τ : MLIRTy
h : hasType (nested []) τ = true
⊢ flatten (nested []) h = List.join (mapWithType [] flatten h)
Tactic:
case nil =>
  simp [flatten, mapWithType, List.join]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_list
Proof state before:
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
ih : ∀ (h : hasType (nested tail✝) τ = true), flatten (nested tail✝) h = List.join (mapWithType tail✝ flatten h)
h : hasType (nested (head✝ :: tail✝)) τ = true
⊢ flatten (nested (head✝ :: tail✝)) h = List.join (mapWithType (head✝ :: tail✝) flatten h)
Tactic:
case cons _ _ ih =>
  simp [flatten, mapWithType, List.join, ih]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_list
Proof state before:
τ : MLIRTy
h : hasType (nested []) τ = true
⊢ flatten (nested []) h = List.join (mapWithType [] flatten h)
Tactic:
simp [flatten, mapWithType, List.join]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_list
Proof state before:
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
ih : ∀ (h : hasType (nested tail✝) τ = true), flatten (nested tail✝) h = List.join (mapWithType tail✝ flatten h)
h : hasType (nested (head✝ :: tail✝)) τ = true
⊢ flatten (nested (head✝ :: tail✝)) h = List.join (mapWithType (head✝ :: tail✝) flatten h)
Tactic:
simp [flatten, mapWithType, List.join, ih]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
e : TensorElem
shape : List ℕ
⊢ hasShape e shape = true → ∀ (h : hasType e τ = true), List.length (flatten e h) = shapeProd shape
Tactic:
revert shape
Proof state after:
τ : MLIRTy
e : TensorElem
⊢ ∀ (shape : List ℕ), hasShape e shape = true → ∀ (h : hasType e τ = true), List.length (flatten e h) = shapeProd shape
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
e : TensorElem
⊢ ∀ (shape : List ℕ), hasShape e shape = true → ∀ (h : hasType e τ = true), List.length (flatten e h) = shapeProd shape
Tactic:
apply @TensorElem.recOn
  (motive_1 := fun e =>
    ∀s, e.hasShape s → (h: e.hasType τ) → (e.flatten h).length = shapeProd s)
  (motive_2 := fun l =>
    ∀s, l.all (TensorElem.hasShape . s) → (h: l.all (hasType . τ)) →
      (mapWithType l flatten (hasType_list_2 h)).join.length = l.length * shapeProd s)
  <;> simp <;> clear e
Proof state after:
case int
τ : MLIRTy
⊢ ∀ (a : ℤ) (s : List ℕ),
    hasShape (int a) s = true → ∀ (h : hasType (int a) τ = true), List.length (flatten (int a) h) = shapeProd s

case float
τ : MLIRTy
⊢ ∀ (a : Float) (s : List ℕ),
    hasShape (float a) s = true → ∀ (h : hasType (float a) τ = true), List.length (flatten (float a) h) = shapeProd s

case bool
τ : MLIRTy
⊢ (∀ (s : List ℕ),
      hasShape (bool false) s = true →
        ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s) ∧
    ∀ (s : List ℕ),
      hasShape (bool true) s = true →
        ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s

case nested
τ : MLIRTy
⊢ ∀ (a : List TensorElem),
    (∀ (s : List ℕ),
        (∀ (x : TensorElem), x ∈ a → hasShape x s = true) →
          ∀ (h : (List.all a fun x => hasType x τ) = true),
            List.length (List.join (mapWithType a flatten (_ : hasType (nested a) τ = true))) =
              List.length a * shapeProd s) →
      ∀ (s : List ℕ),
        hasShape (nested a) s = true →
          ∀ (h : hasType (nested a) τ = true), List.length (flatten (nested a) h) = shapeProd s

case empty
τ : MLIRTy
⊢ ∀ (s : List ℕ), hasShape empty s = true → ∀ (h : hasType empty τ = true), List.length (flatten empty h) = shapeProd s

case cons
τ : MLIRTy
⊢ ∀ (head : TensorElem) (tail : List TensorElem),
    (∀ (s : List ℕ),
        hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s) →
      (∀ (s : List ℕ),
          (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
            ∀ (h : (List.all tail fun x => hasType x τ) = true),
              List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
                List.length tail * shapeProd s) →
        ∀ (s : List ℕ),
          hasShape head s = true →
            (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
              ∀ (h : (List.all (head :: tail) fun x => hasType x τ) = true),
                List.length (flatten head (_ : hasType head τ = true)) +
                    List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
                  Nat.succ (List.length tail) * shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
⊢ ∀ (a : ℤ) (s : List ℕ),
    hasShape (int a) s = true → ∀ (h : hasType (int a) τ = true), List.length (flatten (int a) h) = shapeProd s
Tactic:
case int =>
  intros i s Hshape Htype;
  cases τ <;> simp [hasType] at Htype
  cases s <;> simp [flatten, hasShape] at *
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
⊢ ∀ (a : Float) (s : List ℕ),
    hasShape (float a) s = true → ∀ (h : hasType (float a) τ = true), List.length (flatten (float a) h) = shapeProd s
Tactic:
case float =>
  intros i s Hshape Htype;
  cases τ <;> simp [hasType] at Htype
  cases s <;> simp [flatten, hasShape] at *
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
⊢ (∀ (s : List ℕ),
      hasShape (bool false) s = true →
        ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s) ∧
    ∀ (s : List ℕ),
      hasShape (bool true) s = true →
        ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
case bool =>
  constructor;
  intros s;
  intros Hshape;
  intros Htype;
  cases τ <;> simp [hasType] at Htype
  cases s <;> simp [flatten, hasShape] at *
  sorry
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
⊢ ∀ (a : List TensorElem),
    (∀ (s : List ℕ),
        (∀ (x : TensorElem), x ∈ a → hasShape x s = true) →
          ∀ (h : (List.all a fun x => hasType x τ) = true),
            List.length (List.join (mapWithType a flatten (_ : hasType (nested a) τ = true))) =
              List.length a * shapeProd s) →
      ∀ (s : List ℕ),
        hasShape (nested a) s = true →
          ∀ (h : hasType (nested a) τ = true), List.length (flatten (nested a) h) = shapeProd s
Tactic:
case nested =>
  intros l motive_2 s Hshape Htype
  cases s <;> simp [hasShape] at Hshape
  case cons s_head s_tail =>
  simp [TensorElem.flatten_list, shapeProd, List.foldr]
  simp [motive_2 s_tail Hshape.2 (hasType_list_1 Htype)]
  simp [shapeProd, Nat.mul_comm, Hshape.1]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
⊢ ∀ (s : List ℕ), hasShape empty s = true → ∀ (h : hasType empty τ = true), List.length (flatten empty h) = shapeProd s
Tactic:
case empty =>
  intros s Hshape Htype
  simp [hasType] at Htype
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
⊢ ∀ (head : TensorElem) (tail : List TensorElem),
    (∀ (s : List ℕ),
        hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s) →
      (∀ (s : List ℕ),
          (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
            ∀ (h : (List.all tail fun x => hasType x τ) = true),
              List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
                List.length tail * shapeProd s) →
        ∀ (s : List ℕ),
          hasShape head s = true →
            (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
              ∀ (h : (List.all (head :: tail) fun x => hasType x τ) = true),
                List.length (flatten head (_ : hasType head τ = true)) +
                    List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
                  Nat.succ (List.length tail) * shapeProd s
Tactic:
case cons =>
  intros head tail motive_1 IH2 s Hshape1 Hshape2 Htype1
  simp [List.map, List.join]
  rw [Nat.add_comm]
  simp [Nat.succ_eq_add_one, Nat.right_distrib]
  simp [List.all_cons] at Hshape1
  simp [List.all_cons] at Htype1
  sorry
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
⊢ ∀ (a : ℤ) (s : List ℕ),
    hasShape (int a) s = true → ∀ (h : hasType (int a) τ = true), List.length (flatten (int a) h) = shapeProd s
Tactic:
intros i s Hshape Htype
Proof state after:
τ : MLIRTy
i : ℤ
s : List ℕ
Hshape : hasShape (int i) s = true
Htype : hasType (int i) τ = true
⊢ List.length (flatten (int i) Htype) = shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
i : ℤ
s : List ℕ
Hshape : hasShape (int i) s = true
Htype : hasType (int i) τ = true
⊢ List.length (flatten (int i) Htype) = shapeProd s
Tactic:
cases τ <;> simp [hasType] at Htype
Proof state after:
case int
i : ℤ
s : List ℕ
Hshape : hasShape (int i) s = true
a✝¹ : Signedness
a✝ : ℕ
Htype✝ : hasType (int i) (MLIRType.int a✝¹ a✝) = true
Htype : FinInt.isInBounds a✝¹ a✝ i = true
⊢ List.length (flatten (int i) Htype✝) = shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
case int
i : ℤ
s : List ℕ
Hshape : hasShape (int i) s = true
a✝¹ : Signedness
a✝ : ℕ
Htype✝ : hasType (int i) (MLIRType.int a✝¹ a✝) = true
Htype : FinInt.isInBounds a✝¹ a✝ i = true
⊢ List.length (flatten (int i) Htype✝) = shapeProd s
Tactic:
cases s <;> simp [flatten, hasShape] at *
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
⊢ ∀ (a : Float) (s : List ℕ),
    hasShape (float a) s = true → ∀ (h : hasType (float a) τ = true), List.length (flatten (float a) h) = shapeProd s
Tactic:
intros i s Hshape Htype
Proof state after:
τ : MLIRTy
i : Float
s : List ℕ
Hshape : hasShape (float i) s = true
Htype : hasType (float i) τ = true
⊢ List.length (flatten (float i) Htype) = shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
i : Float
s : List ℕ
Hshape : hasShape (float i) s = true
Htype : hasType (float i) τ = true
⊢ List.length (flatten (float i) Htype) = shapeProd s
Tactic:
cases τ <;> simp [hasType] at Htype
Proof state after:
case float
i : Float
s : List ℕ
Hshape : hasShape (float i) s = true
a✝ : ℕ
Htype✝ : hasType (float i) (MLIRType.float a✝) = true
Htype : True
⊢ List.length (flatten (float i) Htype✝) = shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
case float
i : Float
s : List ℕ
Hshape : hasShape (float i) s = true
a✝ : ℕ
Htype✝ : hasType (float i) (MLIRType.float a✝) = true
Htype : True
⊢ List.length (flatten (float i) Htype✝) = shapeProd s
Tactic:
cases s <;> simp [flatten, hasShape] at *
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
⊢ (∀ (s : List ℕ),
      hasShape (bool false) s = true →
        ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s) ∧
    ∀ (s : List ℕ),
      hasShape (bool true) s = true →
        ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
constructor
Proof state after:
case left
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool false) s = true →
      ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
case left
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool false) s = true →
      ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
intros s
Proof state after:
case left
τ : MLIRTy
s : List ℕ
⊢ hasShape (bool false) s = true →
    ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
case left
τ : MLIRTy
s : List ℕ
⊢ hasShape (bool false) s = true →
    ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
intros Hshape
Proof state after:
case left
τ : MLIRTy
s : List ℕ
Hshape : hasShape (bool false) s = true
⊢ ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
case left
τ : MLIRTy
s : List ℕ
Hshape : hasShape (bool false) s = true
⊢ ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
intros Htype
Proof state after:
case left
τ : MLIRTy
s : List ℕ
Hshape : hasShape (bool false) s = true
Htype : hasType (bool false) τ = true
⊢ List.length (flatten (bool false) Htype) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
case left
τ : MLIRTy
s : List ℕ
Hshape : hasShape (bool false) s = true
Htype : hasType (bool false) τ = true
⊢ List.length (flatten (bool false) Htype) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
cases τ <;> simp [hasType] at Htype
Proof state after:
case left.int
s : List ℕ
Hshape : hasShape (bool false) s = true
a✝¹ : Signedness
a✝ : ℕ
Htype : hasType (bool false) (MLIRType.int a✝¹ a✝) = true
⊢ List.length (flatten (bool false) Htype) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
case left.int
s : List ℕ
Hshape : hasShape (bool false) s = true
a✝¹ : Signedness
a✝ : ℕ
Htype : hasType (bool false) (MLIRType.int a✝¹ a✝) = true
⊢ List.length (flatten (bool false) Htype) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
cases s <;> simp [flatten, hasShape] at *
Proof state after:
case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
sorry
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
⊢ ∀ (a : List TensorElem),
    (∀ (s : List ℕ),
        (∀ (x : TensorElem), x ∈ a → hasShape x s = true) →
          ∀ (h : (List.all a fun x => hasType x τ) = true),
            List.length (List.join (mapWithType a flatten (_ : hasType (nested a) τ = true))) =
              List.length a * shapeProd s) →
      ∀ (s : List ℕ),
        hasShape (nested a) s = true →
          ∀ (h : hasType (nested a) τ = true), List.length (flatten (nested a) h) = shapeProd s
Tactic:
intros l motive_2 s Hshape Htype
Proof state after:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
s : List ℕ
Hshape : hasShape (nested l) s = true
Htype : hasType (nested l) τ = true
⊢ List.length (flatten (nested l) Htype) = shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
s : List ℕ
Hshape : hasShape (nested l) s = true
Htype : hasType (nested l) τ = true
⊢ List.length (flatten (nested l) Htype) = shapeProd s
Tactic:
cases s <;> simp [hasShape] at Hshape
Proof state after:
case cons
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
head✝ : ℕ
tail✝ : List ℕ
Hshape : List.length l = head✝ ∧ ∀ (x : TensorElem), x ∈ l → hasShape x tail✝ = true
⊢ List.length (flatten (nested l) Htype) = shapeProd (head✝ :: tail✝)
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
s_head : ℕ
s_tail : List ℕ
Hshape : List.length l = s_head ∧ ∀ (x : TensorElem), x ∈ l → hasShape x s_tail = true
⊢ List.length (flatten (nested l) Htype) = shapeProd (s_head :: s_tail)
Tactic:
case cons s_head s_tail =>
simp [TensorElem.flatten_list, shapeProd, List.foldr]
simp [motive_2 s_tail Hshape.2 (hasType_list_1 Htype)]
simp [shapeProd, Nat.mul_comm, Hshape.1]
Proof state after:
no goals