internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.TrExpr.uniq
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
l1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹
l2✝ : 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'✝¹
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ ty✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝) Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ body✝ e₂ →
          IsDefEqU env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty'✝¹) :: Δ✝)) body'✝¹ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.forallE name✝ ty✝ body✝ bi✝) e₂
w✝¹ : VLevel
l1' : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ (VExpr.sort w✝¹)
w✝ : VLevel
l2 : HasType env (List.length Us) (ty'✝¹ :: VLCtx.toCtx Δ✝) body'✝¹ (VExpr.sort w✝)
ty'✝ body'✝ : VExpr
a✝¹ : IsType env (List.length Us) (VLCtx.toCtx Δ₂) ty'✝
a✝ : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ₂) body'✝
r3 : TrExpr env Us Δ₂ ty✝ ty'✝
r4 : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ₂) body✝ body'✝
hA : IsDefEq env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ ty'✝ (VExpr.sort w✝¹)
hB : IsDefEq env (List.length Us) (ty'✝¹ :: VLCtx.toCtx Δ✝) body'✝¹ body'✝ (VExpr.sort w✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.forallE ty'✝¹ body'✝¹) (VExpr.forallE ty'✝ body'✝)
Tactic:
exact ⟨_, .forallEDF hA hB⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.uniq
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
l1 : 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'✝
ih2 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ ty✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ e₂
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ val✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ body✝ e₂ →
          IsDefEqU env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝)) body'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) body'✝ e₂
Tactic:
have hΓ := hΔ.wf.toCtx
Proof state after:
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
l1 : 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'✝
ih2 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ ty✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ e₂
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ val✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ body✝ e₂ →
          IsDefEqU env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝)) body'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e₂
hΓ : OnCtx (VLCtx.toCtx Δ✝) (IsType env (List.length Us))
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) body'✝ e₂
Theorem: Lean4Lean.TrExpr.uniq
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
l1 : 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'✝
ih2 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ ty✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ e₂
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ val✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ body✝ e₂ →
          IsDefEqU env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝)) body'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e₂
hΓ : OnCtx (VLCtx.toCtx Δ✝) (IsType env (List.length Us))
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) body'✝ e₂
Tactic:
let .letE _ r2 r3 r4 := H2
Proof state after:
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
l1 : 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'✝
ih2 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ ty✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ e₂
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ val✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) val'✝¹ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝¹ val'✝¹) :: Δ✝) Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ body✝ e₂ →
          IsDefEqU env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlet ty'✝¹ val'✝¹) :: Δ✝)) body'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e₂
hΓ : OnCtx (VLCtx.toCtx Δ✝) (IsType env (List.length Us))
val'✝ ty'✝ : VExpr
a✝ : HasType env (List.length Us) (VLCtx.toCtx Δ₂) val'✝ ty'✝
r2 : TrExpr env Us Δ₂ ty✝ ty'✝
r3 : TrExpr env Us Δ₂ val✝ val'✝
r4 : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ₂) body✝ e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) body'✝ e₂
Theorem: Lean4Lean.TrExpr.uniq
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
l1 : 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'✝
ih2 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ ty✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ e₂
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ val✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) val'✝¹ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝¹ val'✝¹) :: Δ✝) Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ body✝ e₂ →
          IsDefEqU env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlet ty'✝¹ val'✝¹) :: Δ✝)) body'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e₂
hΓ : OnCtx (VLCtx.toCtx Δ✝) (IsType env (List.length Us))
val'✝ ty'✝ : VExpr
a✝ : HasType env (List.length Us) (VLCtx.toCtx Δ₂) val'✝ ty'✝
r2 : TrExpr env Us Δ₂ ty✝ ty'✝
r3 : TrExpr env Us Δ₂ val✝ val'✝
r4 : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ₂) body✝ e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) body'✝ e₂
Tactic:
have ⟨_, hb⟩ := l1.isType henv hΓ
Proof state after:
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
l1 : 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'✝
ih2 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ ty✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ e₂
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ val✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) val'✝¹ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝¹ val'✝¹) :: Δ✝) Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ body✝ e₂ →
          IsDefEqU env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlet ty'✝¹ val'✝¹) :: Δ✝)) body'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e₂
hΓ : OnCtx (VLCtx.toCtx Δ✝) (IsType env (List.length Us))
val'✝ ty'✝ : VExpr
a✝ : HasType env (List.length Us) (VLCtx.toCtx Δ₂) val'✝ ty'✝
r2 : TrExpr env Us Δ₂ ty✝ ty'✝
r3 : TrExpr env Us Δ₂ val✝ val'✝
r4 : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ₂) body✝ e₂
w✝ : VLevel
hb : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ (VExpr.sort w✝)
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) body'✝ e₂
Theorem: Lean4Lean.TrExpr.uniq
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
l1 : 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'✝
ih2 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ ty✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ e₂
ih3 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ val✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) val'✝¹ e₂
ih4 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝¹ val'✝¹) :: Δ✝) Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ body✝ e₂ →
          IsDefEqU env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlet ty'✝¹ val'✝¹) :: Δ✝)) body'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e₂
hΓ : OnCtx (VLCtx.toCtx Δ✝) (IsType env (List.length Us))
val'✝ ty'✝ : VExpr
a✝ : HasType env (List.length Us) (VLCtx.toCtx Δ₂) val'✝ ty'✝
r2 : TrExpr env Us Δ₂ ty✝ ty'✝
r3 : TrExpr env Us Δ₂ val✝ val'✝
r4 : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ₂) body✝ e₂
w✝ : VLevel
hb : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝¹ (VExpr.sort w✝)
⊢ VLocalDecl.IsDefEq env (List.length Us) (VLCtx.toCtx Δ✝) (VLocalDecl.vlet ty'✝¹ val'✝¹) (VLocalDecl.vlet ty'✝ val'✝)
Tactic:
exact .vlet (ih3 hΔ r3 |>.of_l henv hΓ l1) (ih2 hΔ r2 |>.of_l henv hΓ hb)
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.uniq
Proof state before:
case lit
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
Δ✝ : VLCtx
e✝ : VExpr
l✝ : Literal
a✝ : TrExpr env Us Δ✝ (Literal.toConstructor l✝) e✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ (Literal.toConstructor l✝) e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.lit l✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Tactic:
let .lit r1 := H2
Proof state after:
case lit
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
Δ✝ : VLCtx
e✝ : VExpr
l✝ : Literal
a✝ : TrExpr env Us Δ✝ (Literal.toConstructor l✝) e✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ (Literal.toConstructor l✝) e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.lit l✝) e₂
r1 : TrExpr env Us Δ₂ (Literal.toConstructor l✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Theorem: Lean4Lean.TrExpr.uniq
Proof state before:
case lit
env : VEnv
Δ₁ : VLCtx
henv : Ordered env
Us : List Name
e : Expr
e₁ : VExpr
Δ✝ : VLCtx
e✝ : VExpr
l✝ : Literal
a✝ : TrExpr env Us Δ✝ (Literal.toConstructor l✝) e✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr},
        TrExpr env Us Δ₂ (Literal.toConstructor l✝) e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.lit l✝) e₂
r1 : TrExpr env Us Δ₂ (Literal.toConstructor l✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e✝ e₂
Tactic:
exact ih1 hΔ r1
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.uniq
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'✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ e✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.mdata d✝ e✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂
Tactic:
let .mdata r1 := H2
Proof state after:
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'✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ e✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.mdata d✝ e✝) e₂
r1 : TrExpr env Us Δ₂ e✝ e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂
Theorem: Lean4Lean.TrExpr.uniq
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'✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ e✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.mdata d✝ e✝) e₂
r1 : TrExpr env Us Δ₂ e✝ e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂
Tactic:
exact ih1 hΔ r1
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.uniq
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'✝
l2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ e✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.proj s✝ i✝ e✝) e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e''✝ e₂
Tactic:
let .proj r1 r2 := H2
Proof state after:
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'✝¹
l2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝¹ e''✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ e✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝¹ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.proj s✝ i✝ e✝) e₂
e'✝ : VExpr
r1 : TrExpr env Us Δ₂ e✝ e'✝
r2 : TrProj (VLCtx.toCtx Δ₂) s✝ i✝ e'✝ e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e''✝ e₂
Theorem: Lean4Lean.TrExpr.uniq
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'✝¹
l2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝¹ e''✝
ih1 :
  ∀ {Δ₂ : VLCtx},
    VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
      ∀ {e₂ : VExpr}, TrExpr env Us Δ₂ e✝ e₂ → IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝¹ e₂
Δ₂ : VLCtx
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
e₂ : VExpr
H2 : TrExpr env Us Δ₂ (Expr.proj s✝ i✝ e✝) e₂
e'✝ : VExpr
r1 : TrExpr env Us Δ₂ e✝ e'✝
r2 : TrProj (VLCtx.toCtx Δ₂) s✝ i✝ e'✝ e₂
⊢ IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e''✝ e₂
Tactic:
exact l2.uniq r2 (ih1 hΔ r1)
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case bvar
env : VEnv
n : Nat
Δ₁✝ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
e A : VExpr
Δ₁ : VLCtx
i : Nat
h1 : VLCtx.find? Δ₁ (Sum.inl i) = some (e, A)
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.bvar i) dk
⊢ ∃ e', TrExpr env Us Δ (Expr.bvar i) e'
Tactic:
suffices ∃ p, Δ.find? (.inl i) = some p from let ⟨_, h⟩ := this; ⟨_, .bvar h⟩
Proof state after:
case bvar
env : VEnv
n : Nat
Δ₁✝ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
e A : VExpr
Δ₁ : VLCtx
i : Nat
h1 : VLCtx.find? Δ₁ (Sum.inl i) = some (e, A)
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.bvar i) dk
⊢ ∃ p, VLCtx.find? Δ (Sum.inl i) = some p
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case bvar
env : VEnv
n : Nat
Δ₁✝ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
e A : VExpr
Δ₁ : VLCtx
i : Nat
h1 : VLCtx.find? Δ₁ (Sum.inl i) = some (e, A)
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.bvar i) dk
⊢ ∃ p, VLCtx.find? Δ (Sum.inl i) = some p
Tactic:
simp [InScope] at hs
Proof state after:
case bvar
env : VEnv
n : Nat
Δ₁✝ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
e A : VExpr
Δ₁ : VLCtx
i : Nat
h1 : VLCtx.find? Δ₁ (Sum.inl i) = some (e, A)
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂
hs : i < dk
⊢ ∃ p, VLCtx.find? Δ (Sum.inl i) = some p
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case bvar
env : VEnv
n : Nat
Δ₁✝ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
e A : VExpr
Δ₁ : VLCtx
i : Nat
h1 : VLCtx.find? Δ₁ (Sum.inl i) = some (e, A)
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂
hs : i < dk
⊢ ∃ p, VLCtx.find? Δ (Sum.inl i) = some p
Tactic:
induction W generalizing i e A Δ₁ with | @cons_bvar _ Δ₂ _ _ _ d W ih => ?_ | _ => cases hs
Proof state after:
case bvar.cons_bvar
env : VEnv
n : Nat
Δ₁✝ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂✝ : VLCtx
dk k : Nat
Δ✝ Δ₂ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
W : VLCtx.LiftN Δ✝ Δ₂ dk✝ n✝ k✝
ih :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂ → i < dk✝ → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
Δ₁ : VLCtx
i : Nat
h1 : VLCtx.find? Δ₁ (Sum.inl i) = some (e, A)
hΔ : VLCtx.IsDefEq env (List.length Us) Δ₁ ((none, VLocalDecl.liftN d n✝ k✝) :: Δ₂)
hs : i < dk✝ + 1
⊢ ∃ p, VLCtx.find? ((none, d) :: Δ✝) (Sum.inl i) = some p
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case bvar.cons_bvar
env : VEnv
n : Nat
Δ₁✝ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂✝ : VLCtx
dk k : Nat
Δ✝ Δ₂ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
W : VLCtx.LiftN Δ✝ Δ₂ dk✝ n✝ k✝
ih :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂ → i < dk✝ → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
Δ₁ : VLCtx
i : Nat
h1 : VLCtx.find? Δ₁ (Sum.inl i) = some (e, A)
hΔ : VLCtx.IsDefEq env (List.length Us) Δ₁ ((none, VLocalDecl.liftN d n✝ k✝) :: Δ₂)
hs : i < dk✝ + 1
⊢ ∃ p, VLCtx.find? ((none, d) :: Δ✝) (Sum.inl i) = some p
Tactic:
obtain ⟨d, Δ₂, rfl, hΔ₁⟩ : ∃ d Δ₁', Δ₁ = (none, d) :: Δ₁' ∧
    VLCtx.IsDefEq env Us.length Δ₁' Δ₂ := by cases d <;> cases hΔ <;> exact ⟨_, _, rfl, ‹_›⟩
Proof state after:
case bvar.cons_bvar.intro.intro.intro
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂✝¹ : VLCtx
dk k : Nat
Δ✝ Δ₂✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : VLCtx.LiftN Δ✝ Δ₂✝ dk✝ n✝ k✝
ih :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂✝ → i < dk✝ → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
i : Nat
hs : i < dk✝ + 1
d : VLocalDecl
Δ₂ : List (Option FVarId × VLocalDecl)
hΔ₁ : VLCtx.IsDefEq env (List.length Us) Δ₂ Δ₂✝
h1 : VLCtx.find? ((none, d) :: Δ₂) (Sum.inl i) = some (e, A)
hΔ : VLCtx.IsDefEq env (List.length Us) ((none, d) :: Δ₂) ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ₂✝)
⊢ ∃ p, VLCtx.find? ((none, d✝) :: Δ✝) (Sum.inl i) = some p