Theorem: Lean4Lean.VEnv.WF.ordered (Lean4Lean/Theory/Typing/EnvLemmas.lean)

State before:
case empty
ds : List VDecl
env : VEnv
⊢ Ordered VEnv.empty
Tactic:
exact .empty
State after:
no goals

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
State after:
no goals

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 _ ⟨⟩
State after:
no goals

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
State after:
no goals

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 _ ⟨⟩
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

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
State after:
no goals

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) ⟨?_, ?_⟩
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

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 _ ⟨⟩
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

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 ⟨⟩
State after:
no goals

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]
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

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]
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)

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)
State after:
no goals

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
State after:
no goals

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)
State after:
no goals

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
State after:
no goals

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 _ ⟨⟩
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

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 ⟨⟩
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals