internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
case h_2
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁ e₂ A₂ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv✝ v = some v✝
⊢ (do
        let __discr ← find? Δ₁✝ v✝
        match __discr with
          | (e, A) =>
            some
              (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) e,
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) A)) =
      some (e₁, A₁) →
    (do
          let __discr ← find? Δ₂✝ v✝
          match __discr with
            | (e, A) =>
              some
                (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) e,
                  VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) A)) =
        some (e₂, A₂) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) A₁ A₂ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) e₁ e₂ A₁
Tactic:
simp [bind, Option.bind_eq_some]
Proof state after:
case h_2
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁ e₂ A₂ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv✝ v = some v✝
⊢ ∀ (x : VExpr × VExpr),
    find? Δ₁✝ v✝ = some x →
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) x.fst = e₁ →
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) x.snd = A₁ →
          ∀ (x : VExpr × VExpr),
            find? Δ₂✝ v✝ = some x →
              VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) x.fst = e₂ →
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) x.snd = A₂ →
                  IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) A₁ A₂ ∧
                    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) e₁ e₂ A₁
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
case h_2
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁ e₂ A₂ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv✝ v = some v✝
⊢ ∀ (x : VExpr × VExpr),
    find? Δ₁✝ v✝ = some x →
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) x.fst = e₁ →
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) x.snd = A₁ →
          ∀ (x : VExpr × VExpr),
            find? Δ₂✝ v✝ = some x →
              VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) x.fst = e₂ →
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) x.snd = A₂ →
                  IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) A₁ A₂ ∧
                    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) e₁ e₂ A₁
Tactic:
rintro ⟨d₁', n₁'⟩ H1' rfl rfl ⟨d₂', n₂'⟩ H2' rfl rfl
Proof state after:
case h_2.mk.mk
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv✝ v = some v✝
d₁' n₁' : VExpr
H1' : find? Δ₁✝ v✝ = some (d₁', n₁')
d₂' n₂' : VExpr
H2' : find? Δ₂✝ v✝ = some (d₂', n₂')
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) (d₁', n₁').snd)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) (d₂', n₂').snd) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) (d₁', n₁').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) (d₂', n₂').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) (d₁', n₁').snd)
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
case h_2.mk.mk
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv✝ v = some v✝
d₁' n₁' : VExpr
H1' : find? Δ₁✝ v✝ = some (d₁', n₁')
d₂' n₂' : VExpr
H2' : find? Δ₂✝ v✝ = some (d₂', n₂')
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) (d₁', n₁').snd)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) (d₂', n₂').snd) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) (d₁', n₁').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) (d₂', n₂').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) (d₁', n₁').snd)
Tactic:
simpa [VLocalDecl.depth] using find?_uniq hΔ H1' H2'
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e : Expr
e' : VExpr
H : TrExpr env Us Δ e e'
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ) e (VLCtx.bvars Δ)
Tactic:
induction H with
| @bvar e A Δ i h1 =>
  simp [InScope]
  induction Δ generalizing i e A with
  | nil => cases h1
  | cons d Δ ih =>
    match d, i with
    | (none, _), 0 => exact Nat.succ_pos _
    | (none, _), _ + 1 =>
      simp [VLCtx.find?, VLCtx.next, bind] at h1
      obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
      exact Nat.succ_lt_succ (ih h1)
    | (some _, _), _ =>
      simp [VLCtx.find?, VLCtx.next, bind] at h1
      obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
      exact ih h1
| fvar h1 => exact VLCtx.find?_eq_some.1 ⟨_, h1⟩
| sort | const | lit | mdata => trivial
| app _ _ _ _ ih1 ih2
| lam _ _ _ ih1 ih2
| forallE _ _ _ _ ih1 ih2 => exact ⟨ih1, ih2⟩
| letE _ _ _ _ ih1 ih2 ih3 => exact ⟨ih1, ih2, ih3⟩
| proj _ _ ih => exact ih
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
case bvar
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' e A : VExpr
Δ : VLCtx
i : Nat
h1 : VLCtx.find? Δ (Sum.inl i) = some (e, A)
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.bvar i) (VLCtx.bvars Δ)
Tactic:
simp [InScope]
Proof state after:
case bvar
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' e A : VExpr
Δ : VLCtx
i : Nat
h1 : VLCtx.find? Δ (Sum.inl i) = some (e, A)
⊢ i < VLCtx.bvars Δ
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
case bvar
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' e A : VExpr
Δ : VLCtx
i : Nat
h1 : VLCtx.find? Δ (Sum.inl i) = some (e, A)
⊢ i < VLCtx.bvars Δ
Tactic:
induction Δ generalizing i e A with
| nil => cases h1
| cons d Δ ih =>
  match d, i with
  | (none, _), 0 => exact Nat.succ_pos _
  | (none, _), _ + 1 =>
    simp [VLCtx.find?, VLCtx.next, bind] at h1
    obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
    exact Nat.succ_lt_succ (ih h1)
  | (some _, _), _ =>
    simp [VLCtx.find?, VLCtx.next, bind] at h1
    obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
    exact ih h1
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
case bvar.nil
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e✝ : Expr
e' e A : VExpr
i : Nat
h1 : VLCtx.find? [] (Sum.inl i) = some (e, A)
⊢ i < VLCtx.bvars []
Tactic:
cases h1
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
case bvar.cons
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
h1 : VLCtx.find? (d :: Δ) (Sum.inl i) = some (e, A)
⊢ i < VLCtx.bvars (d :: Δ)
Tactic:
match d, i with
| (none, _), 0 => exact Nat.succ_pos _
| (none, _), _ + 1 =>
  simp [VLCtx.find?, VLCtx.next, bind] at h1
  obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
  exact Nat.succ_lt_succ (ih h1)
| (some _, _), _ =>
  simp [VLCtx.find?, VLCtx.next, bind] at h1
  obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
  exact ih h1
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
snd✝ : VLocalDecl
h1 : VLCtx.find? ((none, snd✝) :: Δ) (Sum.inl 0) = some (e, A)
⊢ 0 < VLCtx.bvars ((none, snd✝) :: Δ)
Tactic:
exact Nat.succ_pos _
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
snd✝ : VLocalDecl
n✝ : Nat
h1 : VLCtx.find? ((none, snd✝) :: Δ) (Sum.inl (n✝ + 1)) = some (e, A)
⊢ n✝ + 1 < VLCtx.bvars ((none, snd✝) :: Δ)
Tactic:
simp [VLCtx.find?, VLCtx.next, bind] at h1
Proof state after:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
snd✝ : VLocalDecl
n✝ : Nat
h1 :
  ∃ a,
    VLCtx.find? Δ (Sum.inl n✝) = some a ∧
      VExpr.liftN (VLocalDecl.depth snd✝) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth snd✝) a.snd = A
⊢ n✝ + 1 < VLCtx.bvars ((none, snd✝) :: Δ)
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
snd✝ : VLocalDecl
n✝ : Nat
h1 :
  ∃ a,
    VLCtx.find? Δ (Sum.inl n✝) = some a ∧
      VExpr.liftN (VLocalDecl.depth snd✝) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth snd✝) a.snd = A
⊢ n✝ + 1 < VLCtx.bvars ((none, snd✝) :: Δ)
Tactic:
obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
Proof state after:
case intro.mk.intro.intro
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
i : Nat
snd✝¹ : VLocalDecl
n✝ : Nat
fst✝ snd✝ : VExpr
h1 : VLCtx.find? Δ (Sum.inl n✝) = some (fst✝, snd✝)
⊢ n✝ + 1 < VLCtx.bvars ((none, snd✝¹) :: Δ)
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
case intro.mk.intro.intro
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
i : Nat
snd✝¹ : VLocalDecl
n✝ : Nat
fst✝ snd✝ : VExpr
h1 : VLCtx.find? Δ (Sum.inl n✝) = some (fst✝, snd✝)
⊢ n✝ + 1 < VLCtx.bvars ((none, snd✝¹) :: Δ)
Tactic:
exact Nat.succ_lt_succ (ih h1)
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
val✝ : FVarId
snd✝ : VLocalDecl
x✝ : Nat
h1 : VLCtx.find? ((some val✝, snd✝) :: Δ) (Sum.inl x✝) = some (e, A)
⊢ x✝ < VLCtx.bvars ((some val✝, snd✝) :: Δ)
Tactic:
simp [VLCtx.find?, VLCtx.next, bind] at h1
Proof state after:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
val✝ : FVarId
snd✝ : VLocalDecl
x✝ : Nat
h1 :
  ∃ a,
    VLCtx.find? Δ (Sum.inl x✝) = some a ∧
      VExpr.liftN (VLocalDecl.depth snd✝) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth snd✝) a.snd = A
⊢ x✝ < VLCtx.bvars ((some val✝, snd✝) :: Δ)
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
val✝ : FVarId
snd✝ : VLocalDecl
x✝ : Nat
h1 :
  ∃ a,
    VLCtx.find? Δ (Sum.inl x✝) = some a ∧
      VExpr.liftN (VLocalDecl.depth snd✝) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth snd✝) a.snd = A
⊢ x✝ < VLCtx.bvars ((some val✝, snd✝) :: Δ)
Tactic:
obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
Proof state after:
case intro.mk.intro.intro
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
i : Nat
val✝ : FVarId
snd✝¹ : VLocalDecl
x✝ : Nat
fst✝ snd✝ : VExpr
h1 : VLCtx.find? Δ (Sum.inl x✝) = some (fst✝, snd✝)
⊢ x✝ < VLCtx.bvars ((some val✝, snd✝¹) :: Δ)
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
case intro.mk.intro.intro
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
i : Nat
val✝ : FVarId
snd✝¹ : VLocalDecl
x✝ : Nat
fst✝ snd✝ : VExpr
h1 : VLCtx.find? Δ (Sum.inl x✝) = some (fst✝, snd✝)
⊢ x✝ < VLCtx.bvars ((some val✝, snd✝¹) :: Δ)
Tactic:
exact ih h1
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
case fvar
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e : Expr
e' e✝ A✝ : VExpr
Δ✝ : VLCtx
fv✝ : FVarId
h1 : VLCtx.find? Δ✝ (Sum.inr fv✝) = some (e✝, A✝)
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ✝) (Expr.fvar fv✝) (VLCtx.bvars Δ✝)
Tactic:
exact VLCtx.find?_eq_some.1 ⟨_, h1⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
case mdata
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e : Expr
e' : VExpr
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
d✝ : MData
a✝ : TrExpr env Us Δ✝ e✝ e'✝
a_ih✝ : InScope (fun x => x ∈ VLCtx.fvars Δ✝) e✝ (VLCtx.bvars Δ✝)
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ✝) (Expr.mdata d✝ e✝) (VLCtx.bvars Δ✝)
Tactic:
trivial
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
case forallE
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
a✝³ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝² : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 : InScope (fun x => x ∈ VLCtx.fvars Δ✝) ty✝ (VLCtx.bvars Δ✝)
ih2 :
  InScope (fun x => x ∈ VLCtx.fvars ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body✝
    (VLCtx.bvars ((none, VLocalDecl.vlam ty'✝) :: Δ✝))
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ✝) (Expr.forallE name✝ ty✝ body✝ bi✝) (VLCtx.bvars Δ✝)
Tactic:
exact ⟨ih1, ih2⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
case letE
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e : Expr
e' val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
a✝³ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
a✝² : TrExpr env Us Δ✝ ty✝ ty'✝
a✝¹ : TrExpr env Us Δ✝ val✝ val'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) body✝ body'✝
ih1 : InScope (fun x => x ∈ VLCtx.fvars Δ✝) ty✝ (VLCtx.bvars Δ✝)
ih2 : InScope (fun x => x ∈ VLCtx.fvars Δ✝) val✝ (VLCtx.bvars Δ✝)
ih3 :
  InScope (fun x => x ∈ VLCtx.fvars ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝)) body✝
    (VLCtx.bvars ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝))
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ✝) (Expr.letE name✝ ty✝ val✝ body✝ bi✝) (VLCtx.bvars Δ✝)
Tactic:
exact ⟨ih1, ih2, ih3⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.inScope
Proof state before:
case proj
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e : Expr
e' : VExpr
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
a✝¹ : TrExpr env Us Δ✝ e✝ e'✝
a✝ : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih : InScope (fun x => x ∈ VLCtx.fvars Δ✝) e✝ (VLCtx.bvars Δ✝)
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ✝) (Expr.proj s✝ i✝ e✝) (VLCtx.bvars Δ✝)
Tactic:
exact ih
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
hΔ : VLCtx.WF env (List.length Us) Δ
e : Expr
e' : VExpr
H : TrExpr env Us Δ e e'
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ) e'
Tactic:
induction H with
| bvar h1 | fvar h1 => exact ⟨_, hΔ.find?_wf henv h1⟩
| sort h1 => exact ⟨_, .sort (.of_ofLevel h1)⟩
| const h1 h2 h3 =>
  simp [List.mapM_eq_some] at h2
  refine ⟨_, .const h1 (fun l hl => ?_) (h2.length_eq.symm.trans h3)⟩
  have ⟨_, _, h⟩ := h2.forall_exists_r _ hl; exact .of_ofLevel h
| app h1 h2 => exact ⟨_, h1.app h2⟩
| lam h1 _ _ _ ih2 =>
  have ⟨_, h1'⟩ := h1
  have ⟨_, h2'⟩ := ih2 ⟨hΔ, nofun, h1⟩
  refine ⟨_, h1'.lam h2'⟩
| forallE h1 h2 => have ⟨_, h1'⟩ := h1; have ⟨_, h2'⟩ := h2; exact ⟨_, .forallE h1' h2'⟩
| letE h1 _ _ _ _ _ ih3 => exact ih3 ⟨hΔ, nofun, h1⟩
| lit _ ih | mdata _ ih => exact ih hΔ
| proj _ h2 ih => exact h2.wf (ih hΔ)
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case fvar
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' e✝ A✝ : VExpr
Δ✝ : VLCtx
fv✝ : FVarId
h1 : VLCtx.find? Δ✝ (Sum.inr fv✝) = some (e✝, A✝)
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) e✝
Tactic:
exact ⟨_, hΔ.find?_wf henv h1⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case sort
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' : VExpr
u✝ : Level
u'✝ : VLevel
Δ✝ : VLCtx
h1 : VLevel.ofLevel Us u✝ = some u'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.sort u'✝)
Tactic:
exact ⟨_, .sort (.of_ofLevel h1)⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' : VExpr
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
h1 : env.constants c✝ = some (some ci✝)
h2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
h3 : List.length us✝ = ci✝.uvars
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝)
Tactic:
simp [List.mapM_eq_some] at h2
Proof state after:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' : VExpr
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
h1 : env.constants c✝ = some (some ci✝)
h3 : List.length us✝ = ci✝.uvars
hΔ : VLCtx.WF env (List.length Us) Δ✝
h2 : List.Forall₂ (fun x x_1 => VLevel.ofLevel Us x = some x_1) us✝ us'✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝)
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' : VExpr
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
h1 : env.constants c✝ = some (some ci✝)
h3 : List.length us✝ = ci✝.uvars
hΔ : VLCtx.WF env (List.length Us) Δ✝
h2 : List.Forall₂ (fun x x_1 => VLevel.ofLevel Us x = some x_1) us✝ us'✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝)
Tactic:
refine ⟨_, .const h1 (fun l hl => ?_) (h2.length_eq.symm.trans h3)⟩
Proof state after:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' : VExpr
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
h1 : env.constants c✝ = some (some ci✝)
h3 : List.length us✝ = ci✝.uvars
hΔ : VLCtx.WF env (List.length Us) Δ✝
h2 : List.Forall₂ (fun x x_1 => VLevel.ofLevel Us x = some x_1) us✝ us'✝
l : VLevel
hl : l ∈ us'✝
⊢ VLevel.WF (List.length Us) l
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' : VExpr
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
h1 : env.constants c✝ = some (some ci✝)
h3 : List.length us✝ = ci✝.uvars
hΔ : VLCtx.WF env (List.length Us) Δ✝
h2 : List.Forall₂ (fun x x_1 => VLevel.ofLevel Us x = some x_1) us✝ us'✝
l : VLevel
hl : l ∈ us'✝
⊢ VLevel.WF (List.length Us) l
Tactic:
have ⟨_, _, h⟩ := h2.forall_exists_r _ hl
Proof state after:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' : VExpr
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
h1 : env.constants c✝ = some (some ci✝)
h3 : List.length us✝ = ci✝.uvars
hΔ : VLCtx.WF env (List.length Us) Δ✝
h2 : List.Forall₂ (fun x x_1 => VLevel.ofLevel Us x = some x_1) us✝ us'✝
l : VLevel
hl : l ∈ us'✝
w✝ : Level
left✝ : w✝ ∈ us✝
h : VLevel.ofLevel Us w✝ = some l
⊢ VLevel.WF (List.length Us) l
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case const
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' : VExpr
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
h1 : env.constants c✝ = some (some ci✝)
h3 : List.length us✝ = ci✝.uvars
hΔ : VLCtx.WF env (List.length Us) Δ✝
h2 : List.Forall₂ (fun x x_1 => VLevel.ofLevel Us x = some x_1) us✝ us'✝
l : VLevel
hl : l ∈ us'✝
w✝ : Level
left✝ : w✝ ∈ us✝
h : VLevel.ofLevel Us w✝ = some l
⊢ VLevel.WF (List.length Us) l
Tactic:
exact .of_ofLevel h
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case app
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' f'✝ A✝ B✝ a'✝ : VExpr
Δ✝ : VLCtx
f✝ a✝² : Expr
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ (VExpr.forallE A✝ B✝)
h2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ A✝
a✝¹ : TrExpr env Us Δ✝ f✝ f'✝
a✝ : TrExpr env Us Δ✝ a✝² a'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) f'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) a'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.app f'✝ a'✝)
Tactic:
exact ⟨_, h1.app h2⟩
Proof state after:
no goals