Theorem: Lean4Lean.TrEnv'.WF (Lean4Lean/Verify/Environment.lean)

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⟩
State after:
no goals

State before:
case empty
C : DefinitionSafety
Q : ConstMap
env : Bool
venv : VEnv
⊢ ∃ ds, VEnv.WF ds VEnv.empty
Tactic:
exact ⟨_, .empty⟩
State after:
no goals

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
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'✝

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⟩
State after:
no goals

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
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'✝

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⟩
State after:
no goals

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
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'✝))

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
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'✝))

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
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'✝))

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)⟩
State after:
no goals

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
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'✝

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
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'✝

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
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'✝

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)⟩
State after:
no goals

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
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'✝

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⟩
State after:
no goals

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
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'✝

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⟩
State after:
no goals