Theorem: Lean4Lean.ConditionallyHasType.fresh (Lean4Lean/Verify/Typing/ConditionallyTyped.lean)

State before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
⊢ ConditionallyHasType ngen env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A
Tactic:
refine have ⟨H1, H2, H3⟩ := H; ⟨H1, H2, fun H4 => ?_⟩
State after:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ TrHasType env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A

State before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ TrHasType env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A
Tactic:
have ⟨h1, _, _, h2, h3, h4⟩ := H3 (H4.mp ?_ H1)
State after:
case refine_2
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P Δ → InScope P e → InScope P A
w✝¹ w✝ : VExpr
h2 : TrExpr env Us Δ e w✝¹
h3 : TrExpr env Us Δ A w✝
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) w✝¹ w✝
⊢ TrHasType env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A

case refine_1
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ ∀ (fv : FVarId),
    fv ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ) →
      NameGenerator.Reserves ngen fv → fv ∈ VLCtx.fvars Δ

State before:
case refine_2
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P Δ → InScope P e → InScope P A
w✝¹ w✝ : VExpr
h2 : TrExpr env Us Δ e w✝¹
h3 : TrExpr env Us Δ A w✝
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) w✝¹ w✝
⊢ TrHasType env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A
Tactic:
have W : VLCtx.LiftN Δ ((some ⟨ngen.curr⟩, d) :: Δ) 0 (0 + d.depth) 0 := .skip_fvar _ _ .refl
State after:
case refine_2
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P Δ → InScope P e → InScope P A
w✝¹ w✝ : VExpr
h2 : TrExpr env Us Δ e w✝¹
h3 : TrExpr env Us Δ A w✝
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) w✝¹ w✝
W : VLCtx.LiftN Δ ((some { name := NameGenerator.curr ngen }, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
⊢ TrHasType env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A

State before:
case refine_2
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P Δ → InScope P e → InScope P A
w✝¹ w✝ : VExpr
h2 : TrExpr env Us Δ e w✝¹
h3 : TrExpr env Us Δ A w✝
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) w✝¹ w✝
W : VLCtx.LiftN Δ ((some { name := NameGenerator.curr ngen }, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
⊢ TrHasType env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A
Tactic:
refine ⟨fun P hP => h1 _ hP.2, ?_⟩
State after:
case refine_2
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P Δ → InScope P e → InScope P A
w✝¹ w✝ : VExpr
h2 : TrExpr env Us Δ e w✝¹
h3 : TrExpr env Us Δ A w✝
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) w✝¹ w✝
W : VLCtx.LiftN Δ ((some { name := NameGenerator.curr ngen }, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
⊢ ∃ e' A',
    TrExpr env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e e' ∧
      TrExpr env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) A A' ∧
        HasType env (List.length Us) (VLCtx.toCtx ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e' A'

State before:
case refine_2
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P Δ → InScope P e → InScope P A
w✝¹ w✝ : VExpr
h2 : TrExpr env Us Δ e w✝¹
h3 : TrExpr env Us Δ A w✝
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) w✝¹ w✝
W : VLCtx.LiftN Δ ((some { name := NameGenerator.curr ngen }, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
⊢ ∃ e' A',
    TrExpr env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e e' ∧
      TrExpr env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) A A' ∧
        HasType env (List.length Us) (VLCtx.toCtx ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e' A'
Tactic:
exact ⟨_, _, h2.weakN henv W hΔ, h3.weakN henv W hΔ, h4.weakN henv W.toCtx⟩
State after:
no goals

State before:
case refine_1
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ ∀ (fv : FVarId),
    fv ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ) →
      NameGenerator.Reserves ngen fv → fv ∈ VLCtx.fvars Δ
Tactic:
intro _ h1 h2
State after:
case refine_1
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h1 : fv✝ ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)
h2 : NameGenerator.Reserves ngen fv✝
⊢ fv✝ ∈ VLCtx.fvars Δ

State before:
case refine_1
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h1 : fv✝ ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)
h2 : NameGenerator.Reserves ngen fv✝
⊢ fv✝ ∈ VLCtx.fvars Δ
Tactic:
simp at h1
State after:
case refine_1
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h2 : NameGenerator.Reserves ngen fv✝
h1 : fv✝ = { name := NameGenerator.curr ngen } ∨ fv✝ ∈ VLCtx.fvars Δ
⊢ fv✝ ∈ VLCtx.fvars Δ

State before:
case refine_1
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h2 : NameGenerator.Reserves ngen fv✝
h1 : fv✝ = { name := NameGenerator.curr ngen } ∨ fv✝ ∈ VLCtx.fvars Δ
⊢ fv✝ ∈ VLCtx.fvars Δ
Tactic:
rcases h1 with rfl | h1
State after:
case refine_1.inl
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h2 : NameGenerator.Reserves ngen { name := NameGenerator.curr ngen }
⊢ { name := NameGenerator.curr ngen } ∈ VLCtx.fvars Δ

case refine_1.inr
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h2 : NameGenerator.Reserves ngen fv✝
h1 : fv✝ ∈ VLCtx.fvars Δ
⊢ fv✝ ∈ VLCtx.fvars Δ

State before:
case refine_1.inl
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h2 : NameGenerator.Reserves ngen { name := NameGenerator.curr ngen }
⊢ { name := NameGenerator.curr ngen } ∈ VLCtx.fvars Δ
Tactic:
cases Nat.lt_irrefl _ (h2 _ rfl)
State after:
no goals

State before:
case refine_1.inr
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h2 : NameGenerator.Reserves ngen fv✝
h1 : fv✝ ∈ VLCtx.fvars Δ
⊢ fv✝ ∈ VLCtx.fvars Δ
Tactic:
exact h1
State after:
no goals