internlm/Lean-Github huggingface dataset:
Theorem: List.List.getF_implies_mem
Proof state before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i' : ℕ
INBOUND : Nat.succ i' < length (x' :: xs)
⊢ Mem (getF (x' :: xs) (Nat.succ i') INBOUND) (x' :: xs)
Tactic:
simp [List.getF]
Proof state after:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i' : ℕ
INBOUND : Nat.succ i' < length (x' :: xs)
⊢ Mem (getF xs i' (_ : i' < length xs)) (x' :: xs)
Theorem: List.List.getF_implies_mem
Proof state before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i' : ℕ
INBOUND : Nat.succ i' < length (x' :: xs)
⊢ Mem (getF xs i' (_ : i' < length xs)) (x' :: xs)
Tactic:
constructor
Proof state after:
case a
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i' : ℕ
INBOUND : Nat.succ i' < length (x' :: xs)
⊢ Mem (getF xs i' (_ : i' < length xs)) xs
Theorem: List.List.getF_implies_mem
Proof state before:
case a
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i' : ℕ
INBOUND : Nat.succ i' < length (x' :: xs)
⊢ Mem (getF xs i' (_ : i' < length xs)) xs
Tactic:
apply IH
Proof state after:
no goals
Theorem: List.length_uniform
Proof state before:
α : Type u_1
v : α
n : ℕ
⊢ length (uniform v n) = n
Tactic:
induction n <;> simp [uniform]
Proof state after:
case succ
α : Type u_1
v : α
n✝ : ℕ
n_ih✝ : length (uniform v n✝) = n✝
⊢ length (uniform v n✝) = n✝
Theorem: List.length_uniform
Proof state before:
case succ
α : Type u_1
v : α
n✝ : ℕ
n_ih✝ : length (uniform v n✝) = n✝
⊢ length (uniform v n✝) = n✝
Tactic:
assumption
Proof state after:
no goals
Theorem: List.length_rangeF
Proof state before:
n : ℕ
⊢ length (rangeF n) = n
Tactic:
induction n with
| zero => simp
| succ m ih => simp [rangeF, ih]
Proof state after:
no goals
Theorem: List.length_rangeF
Proof state before:
case zero

⊢ length (rangeF Nat.zero) = Nat.zero
Tactic:
simp
Proof state after:
no goals
Theorem: List.length_rangeF
Proof state before:
case succ
m : ℕ
ih : length (rangeF m) = m
⊢ length (rangeF (Nat.succ m)) = Nat.succ m
Tactic:
simp [rangeF, ih]
Proof state after:
no goals
Theorem: List.getF_rangeF
Proof state before:
n i : ℕ
h : i < length (rangeF n)
⊢ i < n
Tactic:
simp at h
Proof state after:
n i : ℕ
h : i < n
⊢ i < n
Theorem: List.getF_rangeF
Proof state before:
n i : ℕ
h : i < n
⊢ i < n
Tactic:
apply h
Proof state after:
no goals
Theorem: List.getF_rangeF
Proof state before:
n : ℕ
⊢ ∀ (i : ℕ) (h : i < length (rangeF n)), getF (rangeF n) i h = { val := i, isLt := (_ : i < n) }
Tactic:
induction n with
| zero =>
    intro i h;
    simp;
| succ m ih =>
    intro i
    exact match i with
    | 0 => by simp [getF]
    | j+1 => by simp [rangeF, getF, ih]
Proof state after:
no goals
Theorem: List.getF_rangeF
Proof state before:
case zero

⊢ ∀ (i : ℕ) (h : i < length (rangeF Nat.zero)), getF (rangeF Nat.zero) i h = { val := i, isLt := (_ : i < Nat.zero) }
Tactic:
intro i h
Proof state after:
case zero
i : ℕ
h : i < length (rangeF Nat.zero)
⊢ getF (rangeF Nat.zero) i h = { val := i, isLt := (_ : i < Nat.zero) }
Theorem: List.getF_rangeF
Proof state before:
case zero
i : ℕ
h : i < length (rangeF Nat.zero)
⊢ getF (rangeF Nat.zero) i h = { val := i, isLt := (_ : i < Nat.zero) }
Tactic:
simp
Proof state after:
no goals
Theorem: List.getF_rangeF
Proof state before:
case succ
m : ℕ
ih : ∀ (i : ℕ) (h : i < length (rangeF m)), getF (rangeF m) i h = { val := i, isLt := (_ : i < m) }
⊢ ∀ (i : ℕ) (h : i < length (rangeF (Nat.succ m))),
    getF (rangeF (Nat.succ m)) i h = { val := i, isLt := (_ : i < Nat.succ m) }
Tactic:
intro i
Proof state after:
case succ
m : ℕ
ih : ∀ (i : ℕ) (h : i < length (rangeF m)), getF (rangeF m) i h = { val := i, isLt := (_ : i < m) }
i : ℕ
⊢ ∀ (h : i < length (rangeF (Nat.succ m))), getF (rangeF (Nat.succ m)) i h = { val := i, isLt := (_ : i < Nat.succ m) }
Theorem: List.getF_rangeF
Proof state before:
case succ
m : ℕ
ih : ∀ (i : ℕ) (h : i < length (rangeF m)), getF (rangeF m) i h = { val := i, isLt := (_ : i < m) }
i : ℕ
⊢ ∀ (h : i < length (rangeF (Nat.succ m))), getF (rangeF (Nat.succ m)) i h = { val := i, isLt := (_ : i < Nat.succ m) }
Tactic:
exact match i with
| 0 => by simp [getF]
| j+1 => by simp [rangeF, getF, ih]
Proof state after:
no goals
Theorem: List.getF_rangeF
Proof state before:
m : ℕ
ih : ∀ (i : ℕ) (h : i < length (rangeF m)), getF (rangeF m) i h = { val := i, isLt := (_ : i < m) }
i : ℕ
⊢ ∀ (h : 0 < length (rangeF (Nat.succ m))), getF (rangeF (Nat.succ m)) 0 h = { val := 0, isLt := (_ : 0 < Nat.succ m) }
Tactic:
simp [getF]
Proof state after:
no goals
Theorem: List.getF_rangeF
Proof state before:
m : ℕ
ih : ∀ (i : ℕ) (h : i < length (rangeF m)), getF (rangeF m) i h = { val := i, isLt := (_ : i < m) }
i j : ℕ
⊢ ∀ (h : j + 1 < length (rangeF (Nat.succ m))),
    getF (rangeF (Nat.succ m)) (j + 1) h = { val := j + 1, isLt := (_ : j + 1 < Nat.succ m) }
Tactic:
simp [rangeF, getF, ih]
Proof state after:
no goals
Theorem: List.length_remap
Proof state before:
α : Type u_1
l : List α
f : ℕ → ℕ
h : ∀ (n : ℕ), n < length l → f n < length l
⊢ length (remap l f h) = length l
Tactic:
simp [remap]
Proof state after:
no goals
Theorem: List.getF_remap
Proof state before:
α : Type ?u.30674
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length (remap l f h_f)
⊢ f n < length l
Tactic:
apply h_f
Proof state after:
case a
α : Type ?u.30674
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length (remap l f h_f)
⊢ n < length l
Theorem: List.getF_remap
Proof state before:
case a
α : Type ?u.30674
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length (remap l f h_f)
⊢ n < length l
Tactic:
simp at h_n
Proof state after:
case a
α : Type ?u.30674
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length l
⊢ n < length l
Theorem: List.getF_remap
Proof state before:
case a
α : Type ?u.30674
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length l
⊢ n < length l
Tactic:
apply h_n
Proof state after:
no goals
Theorem: List.getF_remap
Proof state before:
α : Type u_1
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length (remap l f h_f)
⊢ getF (remap l f h_f) n h_n = getF l (f n) (_ : f n < length l)
Tactic:
simp [remap]
Proof state after:
no goals
Theorem: List.remap_remap
Proof state before:
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
h_g : ∀ (n : ℕ), n < length (remap l f h_f) → g n < length (remap l f h_f)
n : ℕ
h : n < length l
⊢ Function.comp f g n < length l
Tactic:
simp [Function.comp] at *
Proof state after:
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
n : ℕ
h : n < length l
h_g : ∀ (n : ℕ), n < length l → g n < length l
⊢ f (g n) < length l
Theorem: List.remap_remap
Proof state before:
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
n : ℕ
h : n < length l
h_g : ∀ (n : ℕ), n < length l → g n < length l
⊢ f (g n) < length l
Tactic:
apply h_f
Proof state after:
case a
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
n : ℕ
h : n < length l
h_g : ∀ (n : ℕ), n < length l → g n < length l
⊢ g n < length l
Theorem: List.remap_remap
Proof state before:
case a
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
n : ℕ
h : n < length l
h_g : ∀ (n : ℕ), n < length l → g n < length l
⊢ g n < length l
Tactic:
apply h_g
Proof state after:
case a.a
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
n : ℕ
h : n < length l
h_g : ∀ (n : ℕ), n < length l → g n < length l
⊢ n < length l
Theorem: List.remap_remap
Proof state before:
case a.a
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
n : ℕ
h : n < length l
h_g : ∀ (n : ℕ), n < length l → g n < length l
⊢ n < length l
Tactic:
apply h
Proof state after:
no goals
Theorem: List.remap_remap
Proof state before:
α : Type u_1
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
h_g : ∀ (n : ℕ), n < length (remap l f h_f) → g n < length (remap l f h_f)
⊢ remap (remap l f h_f) g h_g = remap l (f ∘ g) (_ : ∀ (n : ℕ), n < length l → Function.comp f g n < length l)
Tactic:
apply extF <;> simp
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasType_list_1
Proof state before:
l : List TensorElem
τ : MLIRTy
⊢ hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
Tactic:
induction l
Proof state after:
case nil
τ : MLIRTy
⊢ hasType (nested []) τ = true → (List.all [] fun x => hasType x τ) = true

case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ : hasType (nested tail✝) τ = true → (List.all tail✝ fun x => hasType x τ) = true
⊢ hasType (nested (head✝ :: tail✝)) τ = true → (List.all (head✝ :: tail✝) fun x => hasType x τ) = true
Theorem: MLIR.AST.TensorElem.hasType_list_1
Proof state before:
case nil
τ : MLIRTy
⊢ hasType (nested []) τ = true → (List.all [] fun x => hasType x τ) = true

case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ : hasType (nested tail✝) τ = true → (List.all tail✝ fun x => hasType x τ) = true
⊢ hasType (nested (head✝ :: tail✝)) τ = true → (List.all (head✝ :: tail✝) fun x => hasType x τ) = true
Tactic:
simp
Proof state after:
case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ : hasType (nested tail✝) τ = true → (List.all tail✝ fun x => hasType x τ) = true
⊢ hasType (nested (head✝ :: tail✝)) τ = true → (List.all (head✝ :: tail✝) fun x => hasType x τ) = true
Theorem: MLIR.AST.TensorElem.hasType_list_1
Proof state before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
⊢ hasType (nested (e :: l)) τ = true → (List.all (e :: l) fun x => hasType x τ) = true
Tactic:
case cons e l ih' =>
  simp [hasType, List.all_cons]
  intro h' h
  constructor <;> simp
  assumption
  simp[h, h']
  sorry
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasType_list_1
Proof state before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
⊢ hasType (nested (e :: l)) τ = true → (List.all (e :: l) fun x => hasType x τ) = true
Tactic:
simp [hasType, List.all_cons]
Proof state after:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
⊢ hasType e τ = true → hasType (nested l) τ = true → hasType e τ = true ∧ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Theorem: MLIR.AST.TensorElem.hasType_list_1
Proof state before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
⊢ hasType e τ = true → hasType (nested l) τ = true → hasType e τ = true ∧ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Tactic:
intro h' h
Proof state after:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ hasType e τ = true ∧ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Theorem: MLIR.AST.TensorElem.hasType_list_1
Proof state before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ hasType e τ = true ∧ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Tactic:
constructor <;> simp
Proof state after:
case left
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ hasType e τ = true

case right
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Theorem: MLIR.AST.TensorElem.hasType_list_1
Proof state before:
case left
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ hasType e τ = true

case right
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Tactic:
assumption
Proof state after:
case right
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Theorem: MLIR.AST.TensorElem.hasType_list_1
Proof state before:
case right
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Tactic:
sorry
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasType_list_2
Proof state before:
l : List TensorElem
τ : MLIRTy
⊢ (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
Tactic:
induction l
Proof state after:
case nil
τ : MLIRTy
⊢ (List.all [] fun x => hasType x τ) = true → hasType (nested []) τ = true

case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ : (List.all tail✝ fun x => hasType x τ) = true → hasType (nested tail✝) τ = true
⊢ (List.all (head✝ :: tail✝) fun x => hasType x τ) = true → hasType (nested (head✝ :: tail✝)) τ = true
Theorem: MLIR.AST.TensorElem.hasType_list_2
Proof state before:
case nil
τ : MLIRTy
⊢ (List.all [] fun x => hasType x τ) = true → hasType (nested []) τ = true

case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ : (List.all tail✝ fun x => hasType x τ) = true → hasType (nested tail✝) τ = true
⊢ (List.all (head✝ :: tail✝) fun x => hasType x τ) = true → hasType (nested (head✝ :: tail✝)) τ = true
Tactic:
simp [hasType]
Proof state after:
case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ : (List.all tail✝ fun x => hasType x τ) = true → hasType (nested tail✝) τ = true
⊢ (List.all (head✝ :: tail✝) fun x => hasType x τ) = true → hasType (nested (head✝ :: tail✝)) τ = true
Theorem: MLIR.AST.TensorElem.hasType_list_2
Proof state before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
⊢ (List.all (e :: l) fun x => hasType x τ) = true → hasType (nested (e :: l)) τ = true
Tactic:
case cons e l ih =>
  simp [hasType, List.all_cons]
  intro h2 h
  simp [h2]
  apply ih
  simp[h]
  assumption
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasType_list_2
Proof state before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
⊢ (List.all (e :: l) fun x => hasType x τ) = true → hasType (nested (e :: l)) τ = true
Tactic:
simp [hasType, List.all_cons]
Proof state after:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
⊢ hasType e τ = true →
    (∀ (x : TensorElem), x ∈ l → hasType x τ = true) → hasType e τ = true ∧ hasType (nested l) τ = true
Theorem: MLIR.AST.TensorElem.hasType_list_2
Proof state before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
⊢ hasType e τ = true →
    (∀ (x : TensorElem), x ∈ l → hasType x τ = true) → hasType e τ = true ∧ hasType (nested l) τ = true
Tactic:
intro h2 h
Proof state after:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
h2 : hasType e τ = true
h : ∀ (x : TensorElem), x ∈ l → hasType x τ = true
⊢ hasType e τ = true ∧ hasType (nested l) τ = true
Theorem: MLIR.AST.TensorElem.hasType_list_2
Proof state before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
h2 : hasType e τ = true
h : ∀ (x : TensorElem), x ∈ l → hasType x τ = true
⊢ hasType e τ = true ∧ hasType (nested l) τ = true
Tactic:
simp [h2]
Proof state after:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
h2 : hasType e τ = true
h : ∀ (x : TensorElem), x ∈ l → hasType x τ = true
⊢ hasType (nested l) τ = true
Theorem: MLIR.AST.TensorElem.hasType_list_2
Proof state before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
h2 : hasType e τ = true
h : ∀ (x : TensorElem), x ∈ l → hasType x τ = true
⊢ hasType (nested l) τ = true
Tactic:
apply ih
Proof state after:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
h2 : hasType e τ = true
h : ∀ (x : TensorElem), x ∈ l → hasType x τ = true
⊢ (List.all l fun x => hasType x τ) = true
Theorem: MLIR.AST.TensorElem.hasType_list_2
Proof state before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
h2 : hasType e τ = true
h : ∀ (x : TensorElem), x ∈ l → hasType x τ = true
⊢ (List.all l fun x => hasType x τ) = true
Tactic:
simp[h]
Proof state after:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
h2 : hasType e τ = true
h : ∀ (x : TensorElem), x ∈ l → hasType x τ = true
⊢ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Theorem: MLIR.AST.TensorElem.hasType_list_2
Proof state before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
h2 : hasType e τ = true
h : ∀ (x : TensorElem), x ∈ l → hasType x τ = true
⊢ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Tactic:
assumption
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.inferredShape_cons
Proof state before:
⊢ ∀ (head : TensorElem) (tail : List TensorElem) (s_head : ℕ) (s_tail : List ℕ),
    inferredShape (nested tail) = some (s_head :: s_tail) →
      inferredShape head = some s_tail → inferredShape (nested (head :: tail)) = some ((s_head + 1) :: s_tail)
Tactic:
intros head tail s_head s_tail H1 H2
Proof state after:
head : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail : List ℕ
H1 : inferredShape (nested tail) = some (s_head :: s_tail)
H2 : inferredShape head = some s_tail
⊢ inferredShape (nested (head :: tail)) = some ((s_head + 1) :: s_tail)
Theorem: MLIR.AST.TensorElem.inferredShape_cons
Proof state before:
head : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail : List ℕ
H1 : inferredShape (nested tail) = some (s_head :: s_tail)
H2 : inferredShape head = some s_tail
⊢ inferredShape (nested (head :: tail)) = some ((s_head + 1) :: s_tail)
Tactic:
cases tail
Proof state after:
case nil
head : TensorElem
s_head : ℕ
s_tail : List ℕ
H2 : inferredShape head = some s_tail
H1 : inferredShape (nested []) = some (s_head :: s_tail)
⊢ inferredShape (nested [head]) = some ((s_head + 1) :: s_tail)

case cons
head : TensorElem
s_head : ℕ
s_tail : List ℕ
H2 : inferredShape head = some s_tail
head✝ : TensorElem
tail✝ : List TensorElem
H1 : inferredShape (nested (head✝ :: tail✝)) = some (s_head :: s_tail)
⊢ inferredShape (nested (head :: head✝ :: tail✝)) = some ((s_head + 1) :: s_tail)
Theorem: MLIR.AST.TensorElem.inferredShape_cons
Proof state before:
case nil
head : TensorElem
s_head : ℕ
s_tail : List ℕ
H2 : inferredShape head = some s_tail
H1 : inferredShape (nested []) = some (s_head :: s_tail)
⊢ inferredShape (nested [head]) = some ((s_head + 1) :: s_tail)

case cons
head : TensorElem
s_head : ℕ
s_tail : List ℕ
H2 : inferredShape head = some s_tail
head✝ : TensorElem
tail✝ : List TensorElem
H1 : inferredShape (nested (head✝ :: tail✝)) = some (s_head :: s_tail)
⊢ inferredShape (nested (head :: head✝ :: tail✝)) = some ((s_head + 1) :: s_tail)
Tactic:
. simp [inferredShape, H2, bind, Option.bind] at *; simp[H1.1];
Proof state after:
case cons
head : TensorElem
s_head : ℕ
s_tail : List ℕ
H2 : inferredShape head = some s_tail
head✝ : TensorElem
tail✝ : List TensorElem
H1 : inferredShape (nested (head✝ :: tail✝)) = some (s_head :: s_tail)
⊢ inferredShape (nested (head :: head✝ :: tail✝)) = some ((s_head + 1) :: s_tail)
Theorem: MLIR.AST.TensorElem.inferredShape_cons
Proof state before:
case cons
head : TensorElem
s_head : ℕ
s_tail : List ℕ
H2 : inferredShape head = some s_tail
head✝ : TensorElem
tail✝ : List TensorElem
H1 : inferredShape (nested (head✝ :: tail✝)) = some (s_head :: s_tail)
⊢ inferredShape (nested (head :: head✝ :: tail✝)) = some ((s_head + 1) :: s_tail)
Tactic:
. simp [inferredShape, H2, bind, Option.bind, H1]
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 : List ℕ},
    inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail) →
      s_head > 0 ∧
        inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)
Tactic:
intros head mid tail s_head s_tail
Proof state after:
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail : List ℕ
⊢ inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail) →
    s_head > 0 ∧ inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((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 : List ℕ
⊢ inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail) →
    s_head > 0 ∧ inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)
Tactic:
simp [inferredShape, bind, Option.bind]
Proof state after:
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail : List ℕ
⊢ (match inferredShape head, fun s1 =>
        match inferredShape (nested (mid :: tail)), fun s2 =>
          match s2 with
          | [] => none
          | head :: tail => if s1 = tail then some ((head + 1) :: tail) else none with
        | none, x => none
        | some a, b => b a with
      | none, x => none
      | some a, b => b a) =
      some (s_head :: s_tail) →
    0 < s_head ∧ inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((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 : List ℕ
⊢ (match inferredShape head, fun s1 =>
        match inferredShape (nested (mid :: tail)), fun s2 =>
          match s2 with
          | [] => none
          | head :: tail => if s1 = tail then some ((head + 1) :: tail) else none with
        | none, x => none
        | some a, b => b a with
      | none, x => none
      | some a, b => b a) =
      some (s_head :: s_tail) →
    0 < s_head ∧ inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)
Tactic:
cases inferredShape head <;> simp
Proof state after:
case some
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail 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 (s_head :: s_tail) →
    0 < s_head ∧ val✝ = s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)