internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.TrLCtx.find?_isSome
Proof state before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
l : List LocalDecl
this : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l) = Option.isSome (List.lookup (some fv) Δ)
Tactic:
clear H
Proof state after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
this : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l) = Option.isSome (List.lookup (some fv) Δ)
Theorem: Lean4Lean.TrLCtx.find?_isSome
Proof state before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
this : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l) = Option.isSome (List.lookup (some fv) Δ)
Tactic:
induction this with
| nil => rfl
| @cons d d' _ _ eq _ ih =>
  cases d'; cases eq
  simp [List.find?, List.lookup, show (some fv == some d.fvarId) = (fv == d.fvarId) from rfl]
  split <;> simp [*]
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.find?_isSome
Proof state before:
case nil
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) []) = Option.isSome (List.lookup (some fv) [])
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.find?_isSome
Proof state before:
case cons
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
d' : Option FVarId × VLocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
eq : d'.fst = some (LocalDecl.fvarId d)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (d :: l₁✝)) =
    Option.isSome (List.lookup (some fv) (d' :: l₂✝))
Tactic:
cases d'
Proof state after:
case cons.mk
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
fst✝ : Option FVarId
snd✝ : VLocalDecl
eq : (fst✝, snd✝).fst = some (LocalDecl.fvarId d)
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (d :: l₁✝)) =
    Option.isSome (List.lookup (some fv) ((fst✝, snd✝) :: l₂✝))
Theorem: Lean4Lean.TrLCtx.find?_isSome
Proof state before:
case cons.mk
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
fst✝ : Option FVarId
snd✝ : VLocalDecl
eq : (fst✝, snd✝).fst = some (LocalDecl.fvarId d)
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (d :: l₁✝)) =
    Option.isSome (List.lookup (some fv) ((fst✝, snd✝) :: l₂✝))
Tactic:
cases eq
Proof state after:
case cons.mk.refl
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
snd✝ : VLocalDecl
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (d :: l₁✝)) =
    Option.isSome (List.lookup (some fv) ((some (LocalDecl.fvarId d), snd✝) :: l₂✝))
Theorem: Lean4Lean.TrLCtx.find?_isSome
Proof state before:
case cons.mk.refl
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
snd✝ : VLocalDecl
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (d :: l₁✝)) =
    Option.isSome (List.lookup (some fv) ((some (LocalDecl.fvarId d), snd✝) :: l₂✝))
Tactic:
simp [List.find?, List.lookup, show (some fv == some d.fvarId) = (fv == d.fvarId) from rfl]
Proof state after:
case cons.mk.refl
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
snd✝ : VLocalDecl
⊢ Option.isSome
      (match fv == LocalDecl.fvarId d with
      | true => some d
      | false => List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) =
    Option.isSome
      (match fv == LocalDecl.fvarId d with
      | true => some snd✝
      | false => List.lookup (some fv) l₂✝)
Theorem: Lean4Lean.TrLCtx.find?_isSome
Proof state before:
case cons.mk.refl
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
snd✝ : VLocalDecl
⊢ Option.isSome
      (match fv == LocalDecl.fvarId d with
      | true => some d
      | false => List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) =
    Option.isSome
      (match fv == LocalDecl.fvarId d with
      | true => some snd✝
      | false => List.lookup (some fv) l₂✝)
Tactic:
split <;> simp [*]
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.find?_eq_some
Proof state before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ (∃ d, LocalContext.find? lctx fv = some d) ↔ fv ∈ VLCtx.fvars Δ
Tactic:
rw [← Option.isSome_iff_exists, H.find?_isSome, Option.isSome_iff_exists, VLCtx.find?_eq_some]
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.contains
Proof state before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ LocalContext.contains lctx fv = true ↔ fv ∈ VLCtx.fvars Δ
Tactic:
rw [LocalContext.contains, PersistentHashMap.find?_isSome, Option.isSome_iff_exists]
Proof state after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ (∃ a, PersistentHashMap.find? lctx.fvarIdToDecl fv = some a) ↔ fv ∈ VLCtx.fvars Δ
Theorem: Lean4Lean.TrLCtx.contains
Proof state before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ (∃ a, PersistentHashMap.find? lctx.fvarIdToDecl fv = some a) ↔ fv ∈ VLCtx.fvars Δ
Tactic:
exact H.find?_eq_some
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.wf
Proof state before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv✝ : FVarId
map✝ : PersistentHashMap FVarId LocalDecl
arr✝ : PersistentArray (Option LocalDecl)
Δ✝ : VLCtx
d✝ : LocalDecl
d'✝ : VLocalDecl
a✝¹ : LocalDecl.fvarId d✝ = fv✝
h2 : PersistentHashMap.find? map✝ fv✝ = none
a✝ : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
h5 : TrLocalDecl env Us Δ✝ d✝ d'✝
⊢ ∀ (fv : FVarId), some fv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ✝
Tactic:
simpa [← h4.find?_eq_some]
Proof state after:
no goals
Theorem: Lean4Lean.ConditionallyTyped.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyTyped ngen env Us ((some fv, d) :: Δ) e
⊢ ConditionallyTyped ngen env Us Δ e
Tactic:
refine H.imp_right fun H1 H2 => ?_
Proof state after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyTyped ngen env Us ((some fv, d) :: Δ) e
H1 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → ∃ e', TrExpr env Us ((some fv, d) :: Δ) e e'
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
⊢ ∃ e', TrExpr env Us Δ e e'
Theorem: Lean4Lean.ConditionallyTyped.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyTyped ngen env Us ((some fv, d) :: Δ) e
H1 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → ∃ e', TrExpr env Us ((some fv, d) :: Δ) e e'
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
⊢ ∃ e', TrExpr env Us Δ e e'
Tactic:
have ⟨e', H⟩ := H1 H2.fvars_cons
Proof state after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H✝ : ConditionallyTyped ngen env Us ((some fv, d) :: Δ) e
H1 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → ∃ e', TrExpr env Us ((some fv, d) :: Δ) e e'
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
e' : VExpr
H : TrExpr env Us ((some fv, d) :: Δ) e e'
⊢ ∃ e', TrExpr env Us Δ e e'
Theorem: Lean4Lean.ConditionallyTyped.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H✝ : ConditionallyTyped ngen env Us ((some fv, d) :: Δ) e
H1 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → ∃ e', TrExpr env Us ((some fv, d) :: Δ) e e'
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
e' : VExpr
H : TrExpr env Us ((some fv, d) :: Δ) e e'
⊢ ∃ e', TrExpr env Us Δ e e'
Tactic:
exact TrExpr.weakN_inv henv (.skip_fvar _ _ .refl) (.refl henv hΔ) H H2
Proof state after:
no goals
Theorem: Lean4Lean.ConditionallyTyped.fresh
Proof state before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
⊢ ConditionallyTyped ngen env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e
Tactic:
refine have ⟨H1, H2⟩ := H; ⟨H1, fun H3 => ?_⟩
Proof state after:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ ∃ e', TrExpr env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e e'
Theorem: Lean4Lean.ConditionallyTyped.fresh
Proof state before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ ∃ e', TrExpr env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e e'
Tactic:
refine have ⟨_, h⟩ := H2 (H3.mp ?_ H1); ⟨_, h.weakN henv (.skip_fvar _ _ .refl) hΔ⟩
Proof state after:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : 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 Δ
Theorem: Lean4Lean.ConditionallyTyped.fresh
Proof state before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : 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
Proof state after:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : 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 Δ
Theorem: Lean4Lean.ConditionallyTyped.fresh
Proof state before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : 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
Proof state after:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : 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 Δ
Theorem: Lean4Lean.ConditionallyTyped.fresh
Proof state before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : 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
Proof state after:
case inl
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : 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 inr
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : 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 Δ
Theorem: Lean4Lean.ConditionallyTyped.fresh
Proof state before:
case inl
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : 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)
Proof state after:
no goals
Theorem: Lean4Lean.ConditionallyTyped.fresh
Proof state before:
case inr
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : 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
Proof state after:
no goals
Theorem: Lean4Lean.ConditionallyHasType.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
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 fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
⊢ ConditionallyHasType ngen env Us Δ e A
Tactic:
have ⟨H1, H2, H3⟩ := H
Proof state after:
env : VEnv
fv : FVarId
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 fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
⊢ ConditionallyHasType ngen env Us Δ e A
Theorem: Lean4Lean.ConditionallyHasType.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
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 fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
⊢ ConditionallyHasType ngen env Us Δ e A
Tactic:
refine ⟨H1, H2, fun H4 => ?_⟩
Proof state after:
env : VEnv
fv : FVarId
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 fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
⊢ TrHasType env Us Δ e A
Theorem: Lean4Lean.ConditionallyHasType.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
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 fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
⊢ TrHasType env Us Δ e A
Tactic:
have ⟨h1, e', A', h2, h3, h4⟩ := H3 H4.fvars_cons
Proof state after:
env : VEnv
fv : FVarId
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 fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
⊢ TrHasType env Us Δ e A
Theorem: Lean4Lean.ConditionallyHasType.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
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 fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
⊢ TrHasType env Us Δ e A
Tactic:
have W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + d.depth) 0 := .skip_fvar _ _ .refl
Proof state after:
env : VEnv
fv : FVarId
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 fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
⊢ TrHasType env Us Δ e A