Theorem: Lean4Lean.TrLCtx.map_toList (Lean4Lean/Verify/LocalContext.lean)

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
⊢ PersistentHashMap.toList' { fvarIdToDecl := PersistentHashMap.empty, decls := PersistentArray.empty }.fvarIdToDecl ~
    List.map (fun d => (LocalDecl.fvarId d, d))
      (LocalContext.toList { fvarIdToDecl := PersistentHashMap.empty, decls := PersistentArray.empty })
Tactic:
simp [LocalContext.toList]
State after:
no goals

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv✝ : FVarId
map✝ : PersistentHashMap FVarId LocalDecl
arr✝ : PersistentArray (Option LocalDecl)
Δ✝ : VLCtx
d✝ : LocalDecl
d'✝ : VLocalDecl
h1 : LocalDecl.fvarId d✝ = fv✝
h2 : PersistentHashMap.find? map✝ fv✝ = none
a✝ : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
h5 : TrLocalDecl env Us Δ✝ d✝ d'✝
⊢ PersistentHashMap.toList'
      { fvarIdToDecl := PersistentHashMap.insert map✝ fv✝ d✝,
          decls := PersistentArray.push arr✝ (some d✝) }.fvarIdToDecl ~
    List.map (fun d => (LocalDecl.fvarId d, d))
      (LocalContext.toList
        { fvarIdToDecl := PersistentHashMap.insert map✝ fv✝ d✝, decls := PersistentArray.push arr✝ (some d✝) })
Tactic:
subst h1
State after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
map✝ : PersistentHashMap FVarId LocalDecl
arr✝ : PersistentArray (Option LocalDecl)
Δ✝ : VLCtx
d✝ : LocalDecl
d'✝ : VLocalDecl
a✝ : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
h5 : TrLocalDecl env Us Δ✝ d✝ d'✝
h2 : PersistentHashMap.find? map✝ (LocalDecl.fvarId d✝) = none
⊢ PersistentHashMap.toList'
      { fvarIdToDecl := PersistentHashMap.insert map✝ (LocalDecl.fvarId d✝) d✝,
          decls := PersistentArray.push arr✝ (some d✝) }.fvarIdToDecl ~
    List.map (fun d => (LocalDecl.fvarId d, d))
      (LocalContext.toList
        { fvarIdToDecl := PersistentHashMap.insert map✝ (LocalDecl.fvarId d✝) d✝,
          decls := PersistentArray.push arr✝ (some d✝) })

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
map✝ : PersistentHashMap FVarId LocalDecl
arr✝ : PersistentArray (Option LocalDecl)
Δ✝ : VLCtx
d✝ : LocalDecl
d'✝ : VLocalDecl
a✝ : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
h5 : TrLocalDecl env Us Δ✝ d✝ d'✝
h2 : PersistentHashMap.find? map✝ (LocalDecl.fvarId d✝) = none
⊢ PersistentHashMap.toList'
      { fvarIdToDecl := PersistentHashMap.insert map✝ (LocalDecl.fvarId d✝) d✝,
          decls := PersistentArray.push arr✝ (some d✝) }.fvarIdToDecl ~
    List.map (fun d => (LocalDecl.fvarId d, d))
      (LocalContext.toList
        { fvarIdToDecl := PersistentHashMap.insert map✝ (LocalDecl.fvarId d✝) d✝,
          decls := PersistentArray.push arr✝ (some d✝) })
Tactic:
simp [LocalContext.toList]
State after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
map✝ : PersistentHashMap FVarId LocalDecl
arr✝ : PersistentArray (Option LocalDecl)
Δ✝ : VLCtx
d✝ : LocalDecl
d'✝ : VLocalDecl
a✝ : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
h5 : TrLocalDecl env Us Δ✝ d✝ d'✝
h2 : PersistentHashMap.find? map✝ (LocalDecl.fvarId d✝) = none
⊢ PersistentHashMap.toList' (PersistentHashMap.insert map✝ (LocalDecl.fvarId d✝) d✝) ~
    (LocalDecl.fvarId d✝, d✝) ::
      List.map (fun d => (LocalDecl.fvarId d, d)) (List.filterMap id (List.reverse (PersistentArray.toList' arr✝)))

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
map✝ : PersistentHashMap FVarId LocalDecl
arr✝ : PersistentArray (Option LocalDecl)
Δ✝ : VLCtx
d✝ : LocalDecl
d'✝ : VLocalDecl
a✝ : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
h5 : TrLocalDecl env Us Δ✝ d✝ d'✝
h2 : PersistentHashMap.find? map✝ (LocalDecl.fvarId d✝) = none
⊢ PersistentHashMap.toList' (PersistentHashMap.insert map✝ (LocalDecl.fvarId d✝) d✝) ~
    (LocalDecl.fvarId d✝, d✝) ::
      List.map (fun d => (LocalDecl.fvarId d, d)) (List.filterMap id (List.reverse (PersistentArray.toList' arr✝)))
Tactic:
exact h4.map_wf.toList'_insert _ _ (by rwa [h4.map_wf.find?_eq] at h2)
  |>.trans (.cons _ h4.map_toList)
State after:
no goals

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
map✝ : PersistentHashMap FVarId LocalDecl
arr✝ : PersistentArray (Option LocalDecl)
Δ✝ : VLCtx
d✝ : LocalDecl
d'✝ : VLocalDecl
a✝ : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
h5 : TrLocalDecl env Us Δ✝ d✝ d'✝
h2 : PersistentHashMap.find? map✝ (LocalDecl.fvarId d✝) = none
⊢ List.lookup (LocalDecl.fvarId d✝) (PersistentHashMap.toList' { fvarIdToDecl := map✝, decls := arr✝ }.fvarIdToDecl) =
    none
Tactic:
rwa [h4.map_wf.find?_eq] at h2
State after:
no goals