internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case lam
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ih2 :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝ body'✝)
Tactic:
have ⟨_, h1'⟩ := h1
Proof state after:
case lam
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ih2 :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝ body'✝)
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case lam
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ih2 :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝ body'✝)
Tactic:
have ⟨_, h2'⟩ := ih2 ⟨hΔ, nofun, h1⟩
Proof state after:
case lam
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ih2 :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝¹ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝¹)
w✝ : VExpr
h2' : IsDefEq env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝ body'✝ w✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝ body'✝)
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case lam
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ih2 :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝¹ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝¹)
w✝ : VExpr
h2' : IsDefEq env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝ body'✝ w✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.lam ty'✝ body'✝)
Tactic:
refine ⟨_, h1'.lam h2'⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case forallE
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2 : 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'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a_ih✝ :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝)
Tactic:
have ⟨_, h1'⟩ := h1
Proof state after:
case forallE
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2 : 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'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a_ih✝ :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝)
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case forallE
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2 : 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'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a_ih✝ :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝)
Tactic:
have ⟨_, h2'⟩ := h2
Proof state after:
case forallE
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2 : 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'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a_ih✝ :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝¹ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝¹)
w✝ : VLevel
h2' : HasType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝ (VExpr.sort w✝)
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝)
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case forallE
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2 : 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'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a_ih✝ :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
w✝¹ : VLevel
h1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝¹)
w✝ : VLevel
h2' : HasType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝ (VExpr.sort w✝)
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝ body'✝)
Tactic:
exact ⟨_, .forallE h1' h2'⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case letE
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1 : 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'✝
a_ih✝¹ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a_ih✝ : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) val'✝
ih3 :
  VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) →
    VExpr.WF env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝)) body'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) body'✝
Tactic:
exact ih3 ⟨hΔ, nofun, h1⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case mdata
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' : VExpr
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
d✝ : MData
a✝ : TrExpr env Us Δ✝ e✝ e'✝
ih : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) e'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) e'✝
Tactic:
exact ih hΔ
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.wf
Proof state before:
case proj
env : VEnv
Δ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e' : VExpr
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
a✝ : TrExpr env Us Δ✝ e✝ e'✝
h2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih : VLCtx.WF env (List.length Us) Δ✝ → VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) e'✝
hΔ : VLCtx.WF env (List.length Us) Δ✝
⊢ VExpr.WF env (List.length Us) (VLCtx.toCtx Δ✝) e''✝
Tactic:
exact h2.wf (ih hΔ)
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.uniq
Proof state before:
env : VEnv
Δ₁ Δ₂ : VLCtx
henv : Ordered env
Us : List Name
hΔ : VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂
e : Expr
e₁ e₂ : VExpr
H1 : TrExpr env Us Δ₁ e e₁
H2 : TrExpr env Us Δ₂ e e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ₁) e₁ e₂
Tactic:
induction H1 generalizing Δ₂ e₂ with
| bvar l1 => let .bvar r1 := H2; exact ⟨_, (hΔ.find?_uniq henv l1 r1).2⟩
| fvar l1 => let .fvar r1 := H2; exact ⟨_, (hΔ.find?_uniq henv l1 r1).2⟩
| sort l1 => let .sort r1 := H2; cases l1.symm.trans r1; exact ⟨_, .sort (.of_ofLevel l1)⟩
| const l1 l2 l3 =>
  let .const r1 r2 r3 := H2; cases l1.symm.trans r1; cases l2.symm.trans r2
  exact (TrExpr.const l1 l2 l3).wf henv hΔ.wf
| app l1 l2 _ _ ih3 ih4 =>
  let .app _ _ r3 r4 := H2
  exact ⟨_, .appDF
    (ih3 hΔ r3 |>.of_l henv hΔ.wf.toCtx l1)
    (ih4 hΔ r4 |>.of_l henv hΔ.wf.toCtx l2)⟩
| lam l1 _ _ ih2 ih3 =>
  let ⟨_, l1⟩ := l1; let .lam _ r2 r3 := H2
  have hA := ih2 hΔ r2 |>.of_l henv hΔ.wf.toCtx l1
  have ⟨_, hb⟩ := ih3 (hΔ.cons nofun <| .vlam hA) r3
  exact ⟨_, .lamDF hA hb⟩
| forallE l1 l2 _ _ ih3 ih4 =>
  let ⟨_, l1'⟩ := l1; let ⟨_, l2⟩ := l2; let .forallE _ _ r3 r4 := H2
  have hA := ih3 hΔ r3 |>.of_l henv hΔ.wf.toCtx l1'
  have hB := ih4 (hΔ.cons nofun <| .vlam hA) r4 |>.of_l (Γ := _::_) henv ⟨hΔ.wf.toCtx, l1⟩ l2
  exact ⟨_, .forallEDF hA hB⟩
| letE l1 _ _ _ ih2 ih3 ih4 =>
  have hΓ := hΔ.wf.toCtx
  let .letE _ r2 r3 r4 := H2
  have ⟨_, hb⟩ := l1.isType henv hΓ
  refine ih4 (hΔ.cons nofun ?_) r4
  exact .vlet (ih3 hΔ r3 |>.of_l henv hΓ l1) (ih2 hΔ r2 |>.of_l henv hΓ hb)
| lit _ ih1 => let .lit r1 := H2; exact ih1 hΔ r1
| mdata _ ih1 => let .mdata r1 := H2; exact ih1 hΔ r1
| proj _ l2 ih1 => let .proj r1 r2 := H2; exact l2.uniq r2 (ih1 hΔ r1)
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.uniq
Proof state before:
case bvar
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ e✝ A✝ : VExpr
Δ✝ : VLCtx
i✝ : Nat
l1 : VLCtx.find? Δ✝ (Sum.inl i✝) = some (e✝, A✝)
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.bvar i✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Tactic:
let .bvar r1 := H2
Proof state after:
case bvar
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ e✝ A✝¹ : VExpr
Δ✝ : VLCtx
i✝ : Nat
l1 : VLCtx.find? Δ✝ (Sum.inl i✝) = some (e✝, A✝¹)
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.bvar i✝) e₂
A✝ : VExpr
r1 : VLCtx.find? Δ₂ (Sum.inl i✝) = some (e₂, A✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Theorem: Lean4Lean.TrExpr.uniq
Proof state before:
case bvar
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ e✝ A✝¹ : VExpr
Δ✝ : VLCtx
i✝ : Nat
l1 : VLCtx.find? Δ✝ (Sum.inl i✝) = some (e✝, A✝¹)
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.bvar i✝) e₂
A✝ : VExpr
r1 : VLCtx.find? Δ₂ (Sum.inl i✝) = some (e₂, A✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Tactic:
exact ⟨_, (hΔ.find?_uniq henv l1 r1).2⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.uniq
Proof state before:
case fvar
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ e✝ A✝ : VExpr
Δ✝ : VLCtx
fv✝ : FVarId
l1 : VLCtx.find? Δ✝ (Sum.inr fv✝) = some (e✝, A✝)
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.fvar fv✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Tactic:
let .fvar r1 := H2
Proof state after:
case fvar
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ e✝ A✝¹ : VExpr
Δ✝ : VLCtx
fv✝ : FVarId
l1 : VLCtx.find? Δ✝ (Sum.inr fv✝) = some (e✝, A✝¹)
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.fvar fv✝) e₂
A✝ : VExpr
r1 : VLCtx.find? Δ₂ (Sum.inr fv✝) = some (e₂, A✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Theorem: Lean4Lean.TrExpr.uniq
Proof state before:
case fvar
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ e✝ A✝¹ : VExpr
Δ✝ : VLCtx
fv✝ : FVarId
l1 : VLCtx.find? Δ✝ (Sum.inr fv✝) = some (e✝, A✝¹)
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.fvar fv✝) e₂
A✝ : VExpr
r1 : VLCtx.find? Δ₂ (Sum.inr fv✝) = some (e₂, A✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Tactic:
exact ⟨_, (hΔ.find?_uniq henv l1 r1).2⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.uniq
Proof state before:
case sort
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
u✝ : Level
u'✝ : VLevel
Δ✝ : VLCtx
l1 : VLevel.ofLevel Us u✝ = some u'✝
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.sort u✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.sort u'✝) e₂
Tactic:
let .sort r1 := H2
Proof state after:
case sort
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
u✝ : Level
u'✝¹ : VLevel
Δ✝ : VLCtx
l1 : VLevel.ofLevel Us u✝ = some u'✝¹
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.sort u✝) e₂
u'✝ : VLevel
r1 : VLevel.ofLevel Us u✝ = some u'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.sort u'✝¹) (VExpr.sort u'✝)
Theorem: Lean4Lean.TrExpr.uniq
Proof state before:
case sort
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
u✝ : Level
u'✝¹ : VLevel
Δ✝ : VLCtx
l1 : VLevel.ofLevel Us u✝ = some u'✝¹
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.sort u✝) e₂
u'✝ : VLevel
r1 : VLevel.ofLevel Us u✝ = some u'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.sort u'✝¹) (VExpr.sort u'✝)
Tactic:
cases l1.symm.trans r1
Proof state after:
case sort.refl
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
u✝ : Level
u'✝ : VLevel
Δ✝ : VLCtx
l1 : VLevel.ofLevel Us u✝ = some u'✝
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.sort u✝) e₂
r1 : VLevel.ofLevel Us u✝ = some u'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.sort u'✝) (VExpr.sort u'✝)
Theorem: Lean4Lean.TrExpr.uniq
Proof state before:
case sort.refl
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
u✝ : Level
u'✝ : VLevel
Δ✝ : VLCtx
l1 : VLevel.ofLevel Us u✝ = some u'✝
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.sort u✝) e₂
r1 : VLevel.ofLevel Us u✝ = some u'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.sort u'✝) (VExpr.sort u'✝)
Tactic:
exact ⟨_, .sort (.of_ofLevel l1)⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.uniq
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
l1 : env.constants c✝ = some (some ci✝)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
l3 : List.length us✝ = ci✝.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝) e₂
Tactic:
let .const r1 r2 r3 := 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
l1 : env.constants c✝ = some (some ci✝¹)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝¹
l3 : List.length us✝ = ci✝¹.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
ci✝ : VConstant
us'✝ : List VLevel
r1 : env.constants c✝ = some (some ci✝)
r2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
r3 : List.length us✝ = ci✝.uvars
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝¹) (VExpr.const c✝ us'✝)
Theorem: Lean4Lean.TrExpr.uniq
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
l1 : env.constants c✝ = some (some ci✝¹)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝¹
l3 : List.length us✝ = ci✝¹.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
ci✝ : VConstant
us'✝ : List VLevel
r1 : env.constants c✝ = some (some ci✝)
r2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
r3 : List.length us✝ = ci✝.uvars
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝¹) (VExpr.const c✝ us'✝)
Tactic:
cases l1.symm.trans r1
Proof state after:
case const.refl
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
c✝ : Name
ci✝ : VConstant
us'✝¹ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
l1 : env.constants c✝ = some (some ci✝)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝¹
l3 : List.length us✝ = ci✝.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
us'✝ : List VLevel
r2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
r1 : env.constants c✝ = some (some ci✝)
r3 : List.length us✝ = ci✝.uvars
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝¹) (VExpr.const c✝ us'✝)
Theorem: Lean4Lean.TrExpr.uniq
Proof state before:
case const.refl
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
c✝ : Name
ci✝ : VConstant
us'✝¹ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
l1 : env.constants c✝ = some (some ci✝)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝¹
l3 : List.length us✝ = ci✝.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
us'✝ : List VLevel
r2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
r1 : env.constants c✝ = some (some ci✝)
r3 : List.length us✝ = ci✝.uvars
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝¹) (VExpr.const c✝ us'✝)
Tactic:
cases l2.symm.trans r2
Proof state after:
case const.refl.refl
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
l1 : env.constants c✝ = some (some ci✝)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
l3 : List.length us✝ = ci✝.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
r1 : env.constants c✝ = some (some ci✝)
r3 : List.length us✝ = ci✝.uvars
r2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝) (VExpr.const c✝ us'✝)
Theorem: Lean4Lean.TrExpr.uniq
Proof state before:
case const.refl.refl
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
l1 : env.constants c✝ = some (some ci✝)
l2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
l3 : List.length us✝ = ci✝.uvars
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.const c✝ us✝) e₂
r1 : env.constants c✝ = some (some ci✝)
r3 : List.length us✝ = ci✝.uvars
r2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.const c✝ us'✝) (VExpr.const c✝ us'✝)
Tactic:
exact (TrExpr.const l1 l2 l3).wf henv hΔ.wf
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.uniq
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
l1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ (VExpr.forallE A✝ B✝)
l2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ A✝
a✝¹ : TrExpr env Us Δ✝ f✝ f'✝
a✝ : TrExpr env Us Δ✝ a✝² a'✝
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ f✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ a✝² e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.app f✝ a✝²) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.app f'✝ a'✝) e₂
Tactic:
let .app _ _ r3 r4 := H2
Proof state after:
case app
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ f'✝¹ A✝¹ B✝¹ a'✝¹ : VExpr
Δ✝ : VLCtx
f✝ a✝⁴ : Expr
l1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝¹ (VExpr.forallE A✝¹ B✝¹)
l2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝¹ A✝¹
a✝³ : TrExpr env Us Δ✝ f✝ f'✝¹
a✝² : TrExpr env Us Δ✝ a✝⁴ a'✝¹
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ f✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) f'✝¹ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ a✝⁴ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) a'✝¹ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.app f✝ a✝⁴) e₂
f'✝ A✝ B✝ a'✝ : VExpr
a✝¹ : HasType env (List.length Us) (VLCtx.toCtx Δ₂) f'✝ (VExpr.forallE A✝ B✝)
a✝ : HasType env (List.length Us) (VLCtx.toCtx Δ₂) a'✝ A✝
r3 : TrExpr env Us Δ₂ f✝ f'✝
r4 : TrExpr env Us Δ₂ a✝⁴ a'✝
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.app f'✝¹ a'✝¹) (VExpr.app f'✝ a'✝)