internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.HasTypeU1.induction
Proof state before:
case sort
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
l✝ : VLevel
h : VLevel.WF U l✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ HasType env U Γ✝ (VExpr.sort l✝) (VExpr.sort (VLevel.succ l✝))
Tactic:
exact .sort h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.HasTypeU1.induction
Proof state before:
case app
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
f✝ A✝ B✝ a✝² : VExpr
a✝¹ : HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝)
a✝ : HasTypeU1 env U defEq Γ✝ a✝² A✝
ih1 : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ f✝ (VExpr.forallE A✝ B✝)
ih2 : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ a✝² A✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ HasType env U Γ✝ (VExpr.app f✝ a✝²) (inst B✝ a✝²)
Tactic:
exact .app (ih1 hΓ) (ih2 hΓ)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.HasTypeU1.induction
Proof state before:
case lam
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
body✝ B✝ : VExpr
a✝¹ : HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝)
a✝ : HasTypeU1 env U defEq (A✝ :: Γ✝) body✝ B✝
ih1 : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ A✝ (VExpr.sort u✝)
ih2 : OnCtx (A✝ :: Γ✝) (IsType env U) → HasType env U (A✝ :: Γ✝) body✝ B✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ HasType env U Γ✝ (VExpr.lam A✝ body✝) (VExpr.forallE A✝ B✝)
Tactic:
exact .lam (ih1 hΓ) (ih2 ⟨hΓ, _, ih1 hΓ⟩)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.HasTypeU1.induction
Proof state before:
case forallE
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
body✝ : VExpr
v✝ : VLevel
a✝¹ : HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝)
a✝ : HasTypeU1 env U defEq (A✝ :: Γ✝) body✝ (VExpr.sort v✝)
ih1 : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ A✝ (VExpr.sort u✝)
ih2 : OnCtx (A✝ :: Γ✝) (IsType env U) → HasType env U (A✝ :: Γ✝) body✝ (VExpr.sort v✝)
hΓ : OnCtx Γ✝ (IsType env U)
⊢ HasType env U Γ✝ (VExpr.forallE A✝ body✝) (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
exact .forallE (ih1 hΓ) (ih2 ⟨hΓ, _, ih1 hΓ⟩)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.HasTypeU1.induction
Proof state before:
case defeq
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
A✝ B✝ e✝ : VExpr
h1 : defEq Γ✝ A✝ B✝
a✝ : HasTypeU1 env U defEq Γ✝ e✝ A✝
ih : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ e✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ HasType env U Γ✝ e✝ B✝
Tactic:
let ⟨_, h⟩ := (ih hΓ).isType henv hΓ
Proof state after:
case defeq
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
A✝ B✝ e✝ : VExpr
h1 : defEq Γ✝ A✝ B✝
a✝ : HasTypeU1 env U defEq Γ✝ e✝ A✝
ih : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ e✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
w✝ : VLevel
h : HasType env U Γ✝ A✝ (VExpr.sort w✝)
⊢ HasType env U Γ✝ e✝ B✝
Theorem: Lean4Lean.VEnv.HasTypeU1.induction
Proof state before:
case defeq
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
A✝ B✝ e✝ : VExpr
h1 : defEq Γ✝ A✝ B✝
a✝ : HasTypeU1 env U defEq Γ✝ e✝ A✝
ih : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ e✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
w✝ : VLevel
h : HasType env U Γ✝ A✝ (VExpr.sort w✝)
⊢ HasType env U Γ✝ e✝ B✝
Tactic:
exact (IH h h1).defeq (ih hΓ)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case empty
ds : List VDecl
env : VEnv
⊢ Ordered VEnv.empty
Tactic:
exact .empty
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case decl.block
ds : List VDecl
env env'✝ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
n✝ : Name
h : addConst env✝ n✝ none = some env'✝
⊢ Ordered env'✝
Tactic:
exact .const ih (by rintro _ ⟨⟩) h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
ds : List VDecl
env env'✝ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
n✝ : Name
h : addConst env✝ n✝ none = some env'✝
⊢ ∀ (ci : VConstant), none = some ci → VConstant.WF env✝ ci
Tactic:
rintro _ ⟨⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case decl.axiom
ds : List VDecl
env env'✝ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
ci✝ : VConstVal
h1 : VConstant.WF env✝ ci✝.toVConstant
h2 : addConst env✝ ci✝.name (some ci✝.toVConstant) = some env'✝
⊢ Ordered env'✝
Tactic:
exact .const ih (by rintro _ ⟨⟩; exact h1) h2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
ds : List VDecl
env env'✝ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
ci✝ : VConstVal
h1 : VConstant.WF env✝ ci✝.toVConstant
h2 : addConst env✝ ci✝.name (some ci✝.toVConstant) = some env'✝
⊢ ∀ (ci : VConstant), some ci✝.toVConstant = some ci → VConstant.WF env✝ ci
Tactic:
rintro _ ⟨⟩
Proof state after:
case refl
ds : List VDecl
env env'✝ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
ci✝ : VConstVal
h1 : VConstant.WF env✝ ci✝.toVConstant
h2 : addConst env✝ ci✝.name (some ci✝.toVConstant) = some env'✝
⊢ VConstant.WF env✝ ci✝.toVConstant
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case refl
ds : List VDecl
env env'✝ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
ci✝ : VConstVal
h1 : VConstant.WF env✝ ci✝.toVConstant
h2 : addConst env✝ ci✝.name (some ci✝.toVConstant) = some env'✝
⊢ VConstant.WF env✝ ci✝.toVConstant
Tactic:
exact h1
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case decl.def
ds : List VDecl
env✝¹ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
env : VEnv
ci : VDefVal
h1 : VDefVal.WF env✝ ci
h2 : addConst env✝ ci.name (some ci.toVConstant) = some env
⊢ Ordered (addDefEq env (VDefVal.toDefEq ci))
Tactic:
refine .defeq (.const ih (by rintro _ ⟨⟩; exact h1.isType ih ⟨⟩) h2) ⟨?_, ?_⟩
Proof state after:
case decl.def.refine_1
ds : List VDecl
env✝¹ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
env : VEnv
ci : VDefVal
h1 : VDefVal.WF env✝ ci
h2 : addConst env✝ ci.name (some ci.toVConstant) = some env
⊢ HasType env (VDefVal.toDefEq ci).uvars [] (VDefVal.toDefEq ci).lhs (VDefVal.toDefEq ci).type

case decl.def.refine_2
ds : List VDecl
env✝¹ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
env : VEnv
ci : VDefVal
h1 : VDefVal.WF env✝ ci
h2 : addConst env✝ ci.name (some ci.toVConstant) = some env
⊢ HasType env (VDefVal.toDefEq ci).uvars [] (VDefVal.toDefEq ci).rhs (VDefVal.toDefEq ci).type
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
ds : List VDecl
env✝¹ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
env : VEnv
ci : VDefVal
h1 : VDefVal.WF env✝ ci
h2 : addConst env✝ ci.name (some ci.toVConstant) = some env
⊢ ∀ (ci_1 : VConstant), some ci.toVConstant = some ci_1 → VConstant.WF env✝ ci_1
Tactic:
rintro _ ⟨⟩
Proof state after:
case refl
ds : List VDecl
env✝¹ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
env : VEnv
ci : VDefVal
h1 : VDefVal.WF env✝ ci
h2 : addConst env✝ ci.name (some ci.toVConstant) = some env
⊢ VConstant.WF env✝ ci.toVConstant
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case refl
ds : List VDecl
env✝¹ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
env : VEnv
ci : VDefVal
h1 : VDefVal.WF env✝ ci
h2 : addConst env✝ ci.name (some ci.toVConstant) = some env
⊢ VConstant.WF env✝ ci.toVConstant
Tactic:
exact h1.isType ih ⟨⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case decl.def.refine_1
ds : List VDecl
env✝¹ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
env : VEnv
ci : VDefVal
h1 : VDefVal.WF env✝ ci
h2 : addConst env✝ ci.name (some ci.toVConstant) = some env
⊢ HasType env (VDefVal.toDefEq ci).uvars [] (VDefVal.toDefEq ci).lhs (VDefVal.toDefEq ci).type
Tactic:
simp [VDefVal.toDefEq]
Proof state after:
case decl.def.refine_1
ds : List VDecl
env✝¹ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
env : VEnv
ci : VDefVal
h1 : VDefVal.WF env✝ ci
h2 : addConst env✝ ci.name (some ci.toVConstant) = some env
⊢ HasType env ci.uvars [] (VExpr.const ci.name (List.map VLevel.param (List.range ci.uvars))) ci.type
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case decl.def.refine_1
ds : List VDecl
env✝¹ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
env : VEnv
ci : VDefVal
h1 : VDefVal.WF env✝ ci
h2 : addConst env✝ ci.name (some ci.toVConstant) = some env
⊢ HasType env ci.uvars [] (VExpr.const ci.name (List.map VLevel.param (List.range ci.uvars))) ci.type
Tactic:
rw [← (h1.levelWF ⟨⟩).2.2.instL_id]
Proof state after:
case decl.def.refine_1
ds : List VDecl
env✝¹ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
env : VEnv
ci : VDefVal
h1 : VDefVal.WF env✝ ci
h2 : addConst env✝ ci.name (some ci.toVConstant) = some env
⊢ HasType env ci.uvars [] (VExpr.const ci.name (List.map VLevel.param (List.range ci.uvars)))
    (VExpr.instL (List.map VLevel.param (List.range ci.uvars)) ci.type)
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case decl.def.refine_1
ds : List VDecl
env✝¹ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
env : VEnv
ci : VDefVal
h1 : VDefVal.WF env✝ ci
h2 : addConst env✝ ci.name (some ci.toVConstant) = some env
⊢ HasType env ci.uvars [] (VExpr.const ci.name (List.map VLevel.param (List.range ci.uvars)))
    (VExpr.instL (List.map VLevel.param (List.range ci.uvars)) ci.type)
Tactic:
exact .const (addConst_self h2) VLevel.id_WF (by simp)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
ds : List VDecl
env✝¹ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
env : VEnv
ci : VDefVal
h1 : VDefVal.WF env✝ ci
h2 : addConst env✝ ci.name (some ci.toVConstant) = some env
⊢ List.length (List.map VLevel.param (List.range ci.uvars)) = ci.uvars
Tactic:
simp
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case decl.def.refine_2
ds : List VDecl
env✝¹ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
env : VEnv
ci : VDefVal
h1 : VDefVal.WF env✝ ci
h2 : addConst env✝ ci.name (some ci.toVConstant) = some env
⊢ HasType env (VDefVal.toDefEq ci).uvars [] (VDefVal.toDefEq ci).rhs (VDefVal.toDefEq ci).type
Tactic:
exact h1.mono (addConst_le h2)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case decl.opaque
ds : List VDecl
env env'✝ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
ci✝ : VDefVal
h1 : VDefVal.WF env✝ ci✝
h2 : addConst env✝ ci✝.name (some ci✝.toVConstant) = some env'✝
⊢ Ordered env'✝
Tactic:
exact .const ih (by rintro _ ⟨⟩; exact h1.isType ih ⟨⟩) h2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
ds : List VDecl
env env'✝ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
ci✝ : VDefVal
h1 : VDefVal.WF env✝ ci✝
h2 : addConst env✝ ci✝.name (some ci✝.toVConstant) = some env'✝
⊢ ∀ (ci : VConstant), some ci✝.toVConstant = some ci → VConstant.WF env✝ ci
Tactic:
rintro _ ⟨⟩
Proof state after:
case refl
ds : List VDecl
env env'✝ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
ci✝ : VDefVal
h1 : VDefVal.WF env✝ ci✝
h2 : addConst env✝ ci✝.name (some ci✝.toVConstant) = some env'✝
⊢ VConstant.WF env✝ ci✝.toVConstant
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case refl
ds : List VDecl
env env'✝ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
ci✝ : VDefVal
h1 : VDefVal.WF env✝ ci✝
h2 : addConst env✝ ci✝.name (some ci✝.toVConstant) = some env'✝
⊢ VConstant.WF env✝ ci✝.toVConstant
Tactic:
exact h1.isType ih ⟨⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case decl.example
ds : List VDecl
env env'✝ : VEnv
ds✝ : List VDecl
ci✝ : VDefVal
a✝¹ : WF ds✝ env'✝
ih : Ordered env'✝
a✝ : VDefVal.WF env'✝ ci✝
⊢ Ordered env'✝
Tactic:
exact ih
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case decl.quot
ds : List VDecl
env env'✝ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
h1 : QuotReady env✝
h2 : addQuot env✝ = some env'✝
⊢ Ordered env'✝
Tactic:
exact addQuot_WF ih h1 h2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.WF.ordered
Proof state before:
case decl.induct
ds : List VDecl
env env'✝ : VEnv
ds✝ : List VDecl
env✝ : VEnv
a✝ : WF ds✝ env✝
ih : Ordered env✝
decl✝ : VInductDecl
h1 : VInductDecl.WF env✝ decl✝
h2 : addInduct env✝ decl✝ = some env'✝
⊢ Ordered env'✝
Tactic:
exact addInduct_WF ih h1 h2
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.succ_congr
Proof state before:
a b : VLevel
h : a ≈ b
⊢ succ a ≈ succ b
Tactic:
simpa [equiv_def, eval] using h
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.inst_inst
Proof state before:
ls ls' : List VLevel
l : VLevel
⊢ inst ls' (inst ls l) = inst (List.map (inst ls') ls) l
Tactic:
induction l <;> simp [inst, *, List.getD_eq_get?]
Proof state after:
case param
ls ls' : List VLevel
a✝ : Nat
⊢ inst ls' (Option.getD (List.get? ls a✝) zero) = Option.getD (Option.map (inst ls') (List.get? ls a✝)) zero
Theorem: Lean4Lean.VLevel.inst_inst
Proof state before:
ls ls' : List VLevel
n : Nat
⊢ inst ls' (Option.getD (List.get? ls n) zero) = Option.getD (Option.map (inst ls') (List.get? ls n)) zero
Tactic:
case param n => cases ls.get? n <;> simp [inst]
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.inst_inst
Proof state before:
ls ls' : List VLevel
n : Nat
⊢ inst ls' (Option.getD (List.get? ls n) zero) = Option.getD (Option.map (inst ls') (List.get? ls n)) zero
Tactic:
cases ls.get? n <;> simp [inst]
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.inst_id
Proof state before:
u : Nat
l : VLevel
h : WF u l
⊢ inst (List.map param (List.range u)) l = l
Tactic:
induction l <;> simp_all [inst, WF, List.getD_eq_get?, List.get?_range]
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.eval_inst
Proof state before:
ls : List VLevel
ns : List Nat
l : VLevel
⊢ eval ns (inst ls l) = eval (List.map (eval ns) ls) l
Tactic:
induction l <;> simp [eval, inst, *, List.getD_eq_get?]
Proof state after:
case param
ls : List VLevel
ns : List Nat
a✝ : Nat
⊢ eval ns (Option.getD (List.get? ls a✝) zero) = Option.getD (Option.map (eval ns) (List.get? ls a✝)) 0
Theorem: Lean4Lean.VLevel.eval_inst
Proof state before:
ls : List VLevel
ns : List Nat
n : Nat
⊢ eval ns (Option.getD (List.get? ls n) zero) = Option.getD (Option.map (eval ns) (List.get? ls n)) 0
Tactic:
case param n => cases ls.get? n <;> simp [eval]
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.eval_inst
Proof state before:
ls : List VLevel
ns : List Nat
n : Nat
⊢ eval ns (Option.getD (List.get? ls n) zero) = Option.getD (Option.map (eval ns) (List.get? ls n)) 0
Tactic:
cases ls.get? n <;> simp [eval]
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.WF.inst
Proof state before:
ls : List VLevel
n : Nat
l : VLevel
H : ∀ (l : VLevel), l ∈ ls → WF n l
⊢ WF n (VLevel.inst ls l)
Tactic:
induction l with
| zero => trivial
| succ _ ih => exact ih
| max _ _ ih1 ih2 | imax _ _ ih1 ih2 => exact ⟨ih1, ih2⟩
| param i =>
  simp [VLevel.inst, List.getD_eq_get?]
  cases e : ls.get? i with
  | none => trivial
  | some => exact H _ (List.get?_mem e)
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.WF.inst
Proof state before:
case zero
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
⊢ WF n (VLevel.inst ls zero)
Tactic:
trivial
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.WF.inst
Proof state before:
case succ
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
a✝ : VLevel
ih : WF n (VLevel.inst ls a✝)
⊢ WF n (VLevel.inst ls (succ a✝))
Tactic:
exact ih
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.WF.inst
Proof state before:
case imax
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
a✝¹ a✝ : VLevel
ih1 : WF n (VLevel.inst ls a✝¹)
ih2 : WF n (VLevel.inst ls a✝)
⊢ WF n (VLevel.inst ls (imax a✝¹ a✝))
Tactic:
exact ⟨ih1, ih2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.WF.inst
Proof state before:
case param
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
i : Nat
⊢ WF n (VLevel.inst ls (param i))
Tactic:
simp [VLevel.inst, List.getD_eq_get?]
Proof state after:
case param
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
i : Nat
⊢ WF n (Option.getD (List.get? ls i) zero)
Theorem: Lean4Lean.VLevel.WF.inst
Proof state before:
case param
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
i : Nat
⊢ WF n (Option.getD (List.get? ls i) zero)
Tactic:
cases e : ls.get? i with
| none => trivial
| some => exact H _ (List.get?_mem e)
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.WF.inst
Proof state before:
case param.none
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
i : Nat
e : List.get? ls i = none
⊢ WF n (Option.getD none zero)
Tactic:
trivial
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.WF.inst
Proof state before:
case param.some
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
i : Nat
val✝ : VLevel
e : List.get? ls i = some val✝
⊢ WF n (Option.getD (some val✝) zero)
Tactic:
exact H _ (List.get?_mem e)
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.id_WF
Proof state before:
u : Nat
⊢ ∀ (l : VLevel), l ∈ List.map param (List.range u) → WF u l
Tactic:
simp [WF]
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.inst_congr
Proof state before:
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
⊢ inst ls l ≈ inst ls' l'
Tactic:
simp [equiv_def, eval_inst, ← equiv_def.1 h1]
Proof state after:
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
⊢ ∀ (ls_1 : List Nat), eval (List.map (eval ls_1) ls) l = eval (List.map (eval ls_1) ls') l
Theorem: Lean4Lean.VLevel.inst_congr
Proof state before:
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
⊢ ∀ (ls_1 : List Nat), eval (List.map (eval ls_1) ls) l = eval (List.map (eval ls_1) ls') l
Tactic:
intro ns
Proof state after:
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
ns : List Nat
⊢ eval (List.map (eval ns) ls) l = eval (List.map (eval ns) ls') l
Theorem: Lean4Lean.VLevel.inst_congr
Proof state before:
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
ns : List Nat
⊢ eval (List.map (eval ns) ls) l = eval (List.map (eval ns) ls') l
Tactic:
congr 1
Proof state after:
case e_ls
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
ns : List Nat
⊢ List.map (eval ns) ls = List.map (eval ns) ls'
Theorem: Lean4Lean.VLevel.inst_congr
Proof state before:
case e_ls
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
ns : List Nat
⊢ List.map (eval ns) ls = List.map (eval ns) ls'
Tactic:
induction h2 with
| nil => rfl
| cons h2 => simp [*, equiv_def.1 h2]
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.inst_congr
Proof state before:
case e_ls.nil
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
ns : List Nat
⊢ List.map (eval ns) [] = List.map (eval ns) []
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.inst_congr
Proof state before:
case e_ls.cons
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
ns : List Nat
a✝¹ b✝ : VLevel
l₁✝ l₂✝ : List VLevel
h2 : a✝¹ ≈ b✝
a✝ : List.Forall₂ (fun x x_1 => x ≈ x_1) l₁✝ l₂✝
a_ih✝ : List.map (eval ns) l₁✝ = List.map (eval ns) l₂✝
⊢ List.map (eval ns) (a✝¹ :: l₁✝) = List.map (eval ns) (b✝ :: l₂✝)
Tactic:
simp [*, equiv_def.1 h2]
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.WF.of_ofLevel
Proof state before:
ls : List Name
l : Lean.Level
l' : VLevel
h : ofLevel ls l = some l'
⊢ WF (List.length ls) l'
Tactic:
induction l generalizing l' with simp [ofLevel, bind, Option.bind_eq_some] at h
| zero => cases h; trivial
| succ _ ih => obtain ⟨l', h, ⟨⟩⟩ := h; exact @ih l' h
| max _ _ ih1 ih2 | imax _ _ ih1 ih2 => obtain ⟨_, h1, _, h2, ⟨⟩⟩ := h; exact ⟨ih1 h1, ih2 h2⟩
| param n => exact h.2 ▸ h.1
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.WF.of_ofLevel
Proof state before:
case zero
ls : List Name
l' : VLevel
h : zero = l'
⊢ WF (List.length ls) l'
Tactic:
cases h
Proof state after:
case zero.refl
ls : List Name
⊢ WF (List.length ls) zero
Theorem: Lean4Lean.VLevel.WF.of_ofLevel
Proof state before:
case zero.refl
ls : List Name
⊢ WF (List.length ls) zero
Tactic:
trivial
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.WF.of_ofLevel
Proof state before:
case succ
ls : List Name
a✝ : Lean.Level
ih : ∀ {l' : VLevel}, ofLevel ls a✝ = some l' → WF (List.length ls) l'
l' : VLevel
h : ∃ a, ofLevel ls a✝ = some a ∧ succ a = l'
⊢ WF (List.length ls) l'
Tactic:
obtain ⟨l', h, ⟨⟩⟩ := h
Proof state after:
case succ.intro.intro.refl
ls : List Name
a✝ : Lean.Level
ih : ∀ {l' : VLevel}, ofLevel ls a✝ = some l' → WF (List.length ls) l'
l' : VLevel
h : ofLevel ls a✝ = some l'
⊢ WF (List.length ls) (succ l')
Theorem: Lean4Lean.VLevel.WF.of_ofLevel
Proof state before:
case succ.intro.intro.refl
ls : List Name
a✝ : Lean.Level
ih : ∀ {l' : VLevel}, ofLevel ls a✝ = some l' → WF (List.length ls) l'
l' : VLevel
h : ofLevel ls a✝ = some l'
⊢ WF (List.length ls) (succ l')
Tactic:
exact @ih l' h
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.WF.of_ofLevel
Proof state before:
case imax
ls : List Name
a✝¹ a✝ : Lean.Level
ih1 : ∀ {l' : VLevel}, ofLevel ls a✝¹ = some l' → WF (List.length ls) l'
ih2 : ∀ {l' : VLevel}, ofLevel ls a✝ = some l' → WF (List.length ls) l'
l' : VLevel
h : ∃ a, ofLevel ls a✝¹ = some a ∧ ∃ a_1, ofLevel ls a✝ = some a_1 ∧ imax a a_1 = l'
⊢ WF (List.length ls) l'
Tactic:
obtain ⟨_, h1, _, h2, ⟨⟩⟩ := h
Proof state after:
case imax.intro.intro.intro.intro.refl
ls : List Name
a✝¹ a✝ : Lean.Level
ih1 : ∀ {l' : VLevel}, ofLevel ls a✝¹ = some l' → WF (List.length ls) l'
ih2 : ∀ {l' : VLevel}, ofLevel ls a✝ = some l' → WF (List.length ls) l'
w✝¹ : VLevel
h1 : ofLevel ls a✝¹ = some w✝¹
w✝ : VLevel
h2 : ofLevel ls a✝ = some w✝
⊢ WF (List.length ls) (imax w✝¹ w✝)
Theorem: Lean4Lean.VLevel.WF.of_ofLevel
Proof state before:
case imax.intro.intro.intro.intro.refl
ls : List Name
a✝¹ a✝ : Lean.Level
ih1 : ∀ {l' : VLevel}, ofLevel ls a✝¹ = some l' → WF (List.length ls) l'
ih2 : ∀ {l' : VLevel}, ofLevel ls a✝ = some l' → WF (List.length ls) l'
w✝¹ : VLevel
h1 : ofLevel ls a✝¹ = some w✝¹
w✝ : VLevel
h2 : ofLevel ls a✝ = some w✝
⊢ WF (List.length ls) (imax w✝¹ w✝)
Tactic:
exact ⟨ih1 h1, ih2 h2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VLevel.WF.of_ofLevel
Proof state before:
case param
ls : List Name
n : Name
l' : VLevel
h : List.indexOf n ls < List.length ls ∧ param (List.indexOf n ls) = l'
⊢ WF (List.length ls) l'
Tactic:
exact h.2 ▸ h.1
Proof state after:
no goals