internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
C : DefinitionSafety
Q : ConstMap
env : Bool
venv : VEnv
H : TrEnv' C Q env venv
⊢ ∃ ds, VEnv.WF ds venv
Tactic:
induction H with
| empty => exact ⟨_, .empty⟩
| block _ h _ ih =>
  have ⟨_, H⟩ := ih
  exact ⟨_, H.decl <| .block h⟩
| «axiom» _ h1 h2 _ ih =>
  have ⟨_, H⟩ := ih
  exact ⟨_, H.decl <| .axiom (ci := ⟨_, _⟩) h1 h2⟩
| defn h1 h2 h3 _ ih =>
  have ⟨_, H⟩ := ih
  have := h1.1.2; dsimp [ConstantInfo.name, ConstantInfo.toConstantVal] at this
  exact ⟨_, H.decl <| .def h2 (this ▸ h3)⟩
| «opaque» h1 h2 h3 _ ih =>
  have ⟨_, H⟩ := ih
  have := h1.1.2; dsimp [ConstantInfo.name, ConstantInfo.toConstantVal] at this
  exact ⟨_, H.decl <| .opaque h2 (this ▸ h3)⟩
| quot h1 h2 _ _ ih =>
  have ⟨_, H⟩ := ih
  exact ⟨_, H.decl <| .quot h1 h2⟩
| induct h1 h2 _ _ ih =>
  have ⟨_, H⟩ := ih
  exact ⟨_, H.decl <| .induct h1 h2⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case empty
C : DefinitionSafety
Q : ConstMap
env : Bool
venv : VEnv
⊢ ∃ ds, VEnv.WF ds VEnv.empty
Tactic:
exact ⟨_, .empty⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case block
C : DefinitionSafety
Q : ConstMap
env : Bool
venv : VEnv
ci✝ : ConstantInfo
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
env✝ : VEnv
a✝¹ : ¬isAsSafeAs C ci✝ = true
h : VEnv.addConst env✝ (ConstantInfo.name ci✝) none = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Tactic:
have ⟨_, H⟩ := ih
Proof state after:
case block
C : DefinitionSafety
Q : ConstMap
env : Bool
venv : VEnv
ci✝ : ConstantInfo
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
env✝ : VEnv
a✝¹ : ¬isAsSafeAs C ci✝ = true
h : VEnv.addConst env✝ (ConstantInfo.name ci✝) none = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case block
C : DefinitionSafety
Q : ConstMap
env : Bool
venv : VEnv
ci✝ : ConstantInfo
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
env✝ : VEnv
a✝¹ : ¬isAsSafeAs C ci✝ = true
h : VEnv.addConst env✝ (ConstantInfo.name ci✝) none = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Tactic:
exact ⟨_, H.decl <| .block h⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case axiom
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : AxiomVal
ci'✝ : VConstant
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
a✝¹ : TrConstant C env✝ (ConstantInfo.axiomInfo ci✝) ci'✝
h1 : VConstant.WF env✝ ci'✝
h2 : VEnv.addConst env✝ ci✝.name (some ci'✝) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Tactic:
have ⟨_, H⟩ := ih
Proof state after:
case axiom
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : AxiomVal
ci'✝ : VConstant
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
a✝¹ : TrConstant C env✝ (ConstantInfo.axiomInfo ci✝) ci'✝
h1 : VConstant.WF env✝ ci'✝
h2 : VEnv.addConst env✝ ci✝.name (some ci'✝) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case axiom
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : AxiomVal
ci'✝ : VConstant
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
a✝¹ : TrConstant C env✝ (ConstantInfo.axiomInfo ci✝) ci'✝
h1 : VConstant.WF env✝ ci'✝
h2 : VEnv.addConst env✝ ci✝.name (some ci'✝) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Tactic:
exact ⟨_, H.decl <| .axiom (ci := ⟨_, _⟩) h1 h2⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case defn
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : DefinitionVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.defnInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
⊢ ∃ ds, VEnv.WF ds (VEnv.addDefEq env'✝ (VDefVal.toDefEq ci'✝))
Tactic:
have ⟨_, H⟩ := ih
Proof state after:
case defn
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : DefinitionVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.defnInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
⊢ ∃ ds, VEnv.WF ds (VEnv.addDefEq env'✝ (VDefVal.toDefEq ci'✝))
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case defn
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : DefinitionVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.defnInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
⊢ ∃ ds, VEnv.WF ds (VEnv.addDefEq env'✝ (VDefVal.toDefEq ci'✝))
Tactic:
have := h1.1.2
Proof state after:
case defn
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : DefinitionVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.defnInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
this : ConstantInfo.name (ConstantInfo.defnInfo ci✝) = ci'✝.name
⊢ ∃ ds, VEnv.WF ds (VEnv.addDefEq env'✝ (VDefVal.toDefEq ci'✝))
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case defn
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : DefinitionVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.defnInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
this : ConstantInfo.name (ConstantInfo.defnInfo ci✝) = ci'✝.name
⊢ ∃ ds, VEnv.WF ds (VEnv.addDefEq env'✝ (VDefVal.toDefEq ci'✝))
Tactic:
dsimp [ConstantInfo.name, ConstantInfo.toConstantVal] at this
Proof state after:
case defn
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : DefinitionVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.defnInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
this : ci✝.name = ci'✝.name
⊢ ∃ ds, VEnv.WF ds (VEnv.addDefEq env'✝ (VDefVal.toDefEq ci'✝))
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case defn
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : DefinitionVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.defnInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
this : ci✝.name = ci'✝.name
⊢ ∃ ds, VEnv.WF ds (VEnv.addDefEq env'✝ (VDefVal.toDefEq ci'✝))
Tactic:
exact ⟨_, H.decl <| .def h2 (this ▸ h3)⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case opaque
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : OpaqueVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.opaqueInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Tactic:
have ⟨_, H⟩ := ih
Proof state after:
case opaque
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : OpaqueVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.opaqueInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case opaque
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : OpaqueVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.opaqueInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Tactic:
have := h1.1.2
Proof state after:
case opaque
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : OpaqueVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.opaqueInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
this : ConstantInfo.name (ConstantInfo.opaqueInfo ci✝) = ci'✝.name
⊢ ∃ ds, VEnv.WF ds env'✝
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case opaque
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : OpaqueVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.opaqueInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
this : ConstantInfo.name (ConstantInfo.opaqueInfo ci✝) = ci'✝.name
⊢ ∃ ds, VEnv.WF ds env'✝
Tactic:
dsimp [ConstantInfo.name, ConstantInfo.toConstantVal] at this
Proof state after:
case opaque
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : OpaqueVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.opaqueInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
this : ci✝.name = ci'✝.name
⊢ ∃ ds, VEnv.WF ds env'✝
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case opaque
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env✝ : VEnv
ci✝ : OpaqueVal
env'✝ : VEnv
C✝ : ConstMap
Q✝ : Bool
ci'✝ : VDefVal
h1 : TrDefVal C env✝ (ConstantInfo.opaqueInfo ci✝) ci'✝
h2 : VDefVal.WF env✝ ci'✝
h3 : VEnv.addConst env✝ ci✝.name (some ci'✝.toVConstant) = some env'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
this : ci✝.name = ci'✝.name
⊢ ∃ ds, VEnv.WF ds env'✝
Tactic:
exact ⟨_, H.decl <| .opaque h2 (this ▸ h3)⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case quot
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env'✝ env✝ : VEnv
C✝ C'✝ : ConstMap
h1 : VEnv.QuotReady env✝
h2 : VEnv.addQuot env✝ = some env'✝
a✝¹ : AddQuot env✝ C✝ C'✝
a✝ : TrEnv' C C✝ false env✝
ih : ∃ ds, VEnv.WF ds env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Tactic:
have ⟨_, H⟩ := ih
Proof state after:
case quot
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env'✝ env✝ : VEnv
C✝ C'✝ : ConstMap
h1 : VEnv.QuotReady env✝
h2 : VEnv.addQuot env✝ = some env'✝
a✝¹ : AddQuot env✝ C✝ C'✝
a✝ : TrEnv' C C✝ false env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case quot
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env'✝ env✝ : VEnv
C✝ C'✝ : ConstMap
h1 : VEnv.QuotReady env✝
h2 : VEnv.addQuot env✝ = some env'✝
a✝¹ : AddQuot env✝ C✝ C'✝
a✝ : TrEnv' C C✝ false env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Tactic:
exact ⟨_, H.decl <| .quot h1 h2⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case induct
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env'✝ : VEnv
C✝ : ConstMap
decl✝ : VInductDecl
C'✝ : ConstMap
Q✝ : Bool
env✝ : VEnv
h1 : VInductDecl.WF env✝ decl✝
h2 : VEnv.addInduct env✝ decl✝ = some env'✝
a✝¹ : AddInduct C✝ decl✝ C'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Tactic:
have ⟨_, H⟩ := ih
Proof state after:
case induct
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env'✝ : VEnv
C✝ : ConstMap
decl✝ : VInductDecl
C'✝ : ConstMap
Q✝ : Bool
env✝ : VEnv
h1 : VInductDecl.WF env✝ decl✝
h2 : VEnv.addInduct env✝ decl✝ = some env'✝
a✝¹ : AddInduct C✝ decl✝ C'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Theorem: Lean4Lean.TrEnv'.WF
Proof state before:
case induct
C : DefinitionSafety
Q : ConstMap
env : Bool
venv env'✝ : VEnv
C✝ : ConstMap
decl✝ : VInductDecl
C'✝ : ConstMap
Q✝ : Bool
env✝ : VEnv
h1 : VInductDecl.WF env✝ decl✝
h2 : VEnv.addInduct env✝ decl✝ = some env'✝
a✝¹ : AddInduct C✝ decl✝ C'✝
a✝ : TrEnv' C C✝ Q✝ env✝
ih : ∃ ds, VEnv.WF ds env✝
w✝ : List VDecl
H : VEnv.WF w✝ env✝
⊢ ∃ ds, VEnv.WF ds env'✝
Tactic:
exact ⟨_, H.decl <| .induct h1 h2⟩
Proof state after:
no goals
Theorem: Lean4Lean.InScope.natLitToConstructor
Proof state before:
P : FVarId → Prop
n k : Nat
⊢ InScope P (Expr.natLitToConstructor n) k
Tactic:
cases n <;> simp [InScope]
Proof state after:
no goals
Theorem: Lean4Lean.InScope.strLitToConstructor
Proof state before:
P : FVarId → Prop
s : String
k : Nat
⊢ InScope P (Expr.strLitToConstructor s) k
Tactic:
simp [InScope, String.foldr_eq]
Proof state after:
P : FVarId → Prop
s : String
k : Nat
⊢ InScope P
    (List.foldr
      (fun c e =>
        Expr.app
          (Expr.app (Expr.app (Expr.const `List.cons [Level.zero]) (Expr.const `Char []))
            (Expr.app (Expr.const `Char.ofNat []) (Expr.lit (Literal.natVal (Char.toNat c)))))
          e)
      (Expr.app (Expr.const `List.nil [Level.zero]) (Expr.const `Char [])) s.data)
    k
Theorem: Lean4Lean.InScope.strLitToConstructor
Proof state before:
P : FVarId → Prop
s : String
k : Nat
⊢ InScope P
    (List.foldr
      (fun c e =>
        Expr.app
          (Expr.app (Expr.app (Expr.const `List.cons [Level.zero]) (Expr.const `Char []))
            (Expr.app (Expr.const `Char.ofNat []) (Expr.lit (Literal.natVal (Char.toNat c)))))
          e)
      (Expr.app (Expr.const `List.nil [Level.zero]) (Expr.const `Char [])) s.data)
    k
Tactic:
induction s.data <;> simp [*, InScope]
Proof state after:
no goals
Theorem: Lean4Lean.InScope.fvars_cons
Proof state before:
Δ : VLCtx
e : Expr
k : Nat
ofv : Option FVarId
d : VLocalDecl
a : FVarId
h : a ∈ VLCtx.fvars Δ
⊢ a ∈ VLCtx.fvars ((ofv, d) :: Δ)
Tactic:
cases ofv <;> simp [h]
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.WF.find?_wf
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ : VLCtx
hΔ : WF env U Δ
H : find? Δ v = some (e, A)
⊢ HasType env U (toCtx Δ) e A
Tactic:
let (ofv, d') :: Δ := Δ
Proof state after:
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
H : find? ((ofv, d') :: Δ) v = some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Theorem: Lean4Lean.VLCtx.WF.find?_wf
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
H : find? ((ofv, d') :: Δ) v = some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Tactic:
unfold VLCtx.find? at H
Proof state after:
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
H :
  (match next ofv v with
    | none => some (VLocalDecl.value d', VLocalDecl.type d')
    | some v => do
      let __discr ← find? Δ v
      match __discr with
        | (e, A) => some (VExpr.liftN (VLocalDecl.depth d') e, VExpr.liftN (VLocalDecl.depth d') A)) =
    some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Theorem: Lean4Lean.VLCtx.WF.find?_wf
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
H :
  (match next ofv v with
    | none => some (VLocalDecl.value d', VLocalDecl.type d')
    | some v => do
      let __discr ← find? Δ v
      match __discr with
        | (e, A) => some (VExpr.liftN (VLocalDecl.depth d') e, VExpr.liftN (VLocalDecl.depth d') A)) =
    some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Tactic:
split at H
Proof state after:
case h_1
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv v = none
H : some (VLocalDecl.value d', VLocalDecl.type d') = some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A

case h_2
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
H :
  (do
      let __discr ← find? Δ v✝
      match __discr with
        | (e, A) => some (VExpr.liftN (VLocalDecl.depth d') e, VExpr.liftN (VLocalDecl.depth d') A)) =
    some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Theorem: Lean4Lean.VLCtx.WF.find?_wf
Proof state before:
case h_1
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv v = none
H : some (VLocalDecl.value d', VLocalDecl.type d') = some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Tactic:
cases H
Proof state after:
case h_1.refl
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv v = none
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) (VLocalDecl.value d') (VLocalDecl.type d')
Theorem: Lean4Lean.VLCtx.WF.find?_wf
Proof state before:
case h_1.refl
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv v = none
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) (VLocalDecl.value d') (VLocalDecl.type d')
Tactic:
exact hΔ.2.2.hasType
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.WF.find?_wf
Proof state before:
case h_2
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
H :
  (do
      let __discr ← find? Δ v✝
      match __discr with
        | (e, A) => some (VExpr.liftN (VLocalDecl.depth d') e, VExpr.liftN (VLocalDecl.depth d') A)) =
    some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Tactic:
simp [bind, Option.bind_eq_some] at H
Proof state after:
case h_2
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
H : ∃ a, find? Δ v✝ = some a ∧ VExpr.liftN (VLocalDecl.depth d') a.fst = e ∧ VExpr.liftN (VLocalDecl.depth d') a.snd = A
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Theorem: Lean4Lean.VLCtx.WF.find?_wf
Proof state before:
case h_2
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
H : ∃ a, find? Δ v✝ = some a ∧ VExpr.liftN (VLocalDecl.depth d') a.fst = e ∧ VExpr.liftN (VLocalDecl.depth d') a.snd = A
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Tactic:
obtain ⟨⟨d'', n'⟩, H, rfl, rfl⟩ := H
Proof state after:
case h_2.intro.mk.intro.intro
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
d'' n' : VExpr
H : find? Δ v✝ = some (d'', n')
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) (VExpr.liftN (VLocalDecl.depth d') (d'', n').fst)
    (VExpr.liftN (VLocalDecl.depth d') (d'', n').snd)
Theorem: Lean4Lean.VLCtx.WF.find?_wf
Proof state before:
case h_2.intro.mk.intro.intro
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
d'' n' : VExpr
H : find? Δ v✝ = some (d'', n')
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) (VExpr.liftN (VLocalDecl.depth d') (d'', n').fst)
    (VExpr.liftN (VLocalDecl.depth d') (d'', n').snd)
Tactic:
obtain h3 := hΔ.1.find?_wf H
Proof state after:
case h_2.intro.mk.intro.intro
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
d'' n' : VExpr
H : find? Δ v✝ = some (d'', n')
h3 : HasType env U (toCtx Δ) d'' n'
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) (VExpr.liftN (VLocalDecl.depth d') (d'', n').fst)
    (VExpr.liftN (VLocalDecl.depth d') (d'', n').snd)
Theorem: Lean4Lean.VLCtx.WF.find?_wf
Proof state before:
case h_2.intro.mk.intro.intro
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
d'' n' : VExpr
H : find? Δ v✝ = some (d'', n')
h3 : HasType env U (toCtx Δ) d'' n'
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) (VExpr.liftN (VLocalDecl.depth d') (d'', n').fst)
    (VExpr.liftN (VLocalDecl.depth d') (d'', n').snd)
Tactic:
exact h3.weakN henv VLocalDecl.is_liftN
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.WF.fvars_nodup
Proof state before:
env : VEnv
U : Nat
fv : FVarId
snd✝ : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U Δ
h : ∀ (fv_1 : FVarId), some fv = some fv_1 → ¬fv_1 ∈ fvars Δ
right✝ : VLocalDecl.WF env U (VLCtx.toCtx Δ) snd✝
⊢ List.Nodup (fvars ((some fv, snd✝) :: Δ))
Tactic:
suffices fv ∉ fvars Δ from (fvars_nodup hΔ).cons (fun _ h e => this (e ▸ h))
Proof state after:
env : VEnv
U : Nat
fv : FVarId
snd✝ : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U Δ
h : ∀ (fv_1 : FVarId), some fv = some fv_1 → ¬fv_1 ∈ fvars Δ
right✝ : VLocalDecl.WF env U (VLCtx.toCtx Δ) snd✝
⊢ ¬fv ∈ fvars Δ
Theorem: Lean4Lean.VLCtx.WF.fvars_nodup
Proof state before:
env : VEnv
U : Nat
fv : FVarId
snd✝ : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U Δ
h : ∀ (fv_1 : FVarId), some fv = some fv_1 → ¬fv_1 ∈ fvars Δ
right✝ : VLocalDecl.WF env U (VLCtx.toCtx Δ) snd✝
⊢ ¬fv ∈ fvars Δ
Tactic:
simpa using h
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.toCtx
Proof state before:
Δ Δ' : VLCtx
dk n k : Nat
W : LiftN Δ Δ' dk n k
⊢ Ctx.LiftN n k (VLCtx.toCtx Δ) (VLCtx.toCtx Δ')
Tactic:
induction W with
| refl => exact .zero []
| @skip_fvar _ Δ' _ _ d _ ih =>
  match d with
  | .vlet .. => exact ih
  | .vlam A =>
    generalize hΓ' : VLCtx.toCtx Δ' = Γ' at ih
    let .zero As eq := ih
    simp [VLCtx.toCtx, hΓ']
    exact .zero (A :: As) (eq ▸ rfl)
| cons_bvar d _ ih =>
  match d with
  | .vlet .. => exact ih
  | .vlam A => exact .succ ih
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.toCtx
Proof state before:
case refl
Δ Δ' : VLCtx
dk n k : Nat
Δ✝ : VLCtx
⊢ Ctx.LiftN 0 0 (VLCtx.toCtx Δ✝) (VLCtx.toCtx Δ✝)
Tactic:
exact .zero []
Proof state after:
no goals