internlm/Lean-Github huggingface dataset:
Theorem: List.NodupKeys.lookup_eq_some
Proof state before:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
b' : β
x✝ : Bool
nd : (∀ (a' : α × β), a' ∈ l → ¬a = a'.fst) ∧ NodupKeys l
⊢ b = b' ↔ b = b' ∨ (a, b) ∈ l
Tactic:
refine (or_iff_left_of_imp fun h => ?_).symm
Proof state after:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
b' : β
x✝ : Bool
nd : (∀ (a' : α × β), a' ∈ l → ¬a = a'.fst) ∧ NodupKeys l
h : (a, b) ∈ l
⊢ b = b'
Theorem: List.NodupKeys.lookup_eq_some
Proof state before:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
b' : β
x✝ : Bool
nd : (∀ (a' : α × β), a' ∈ l → ¬a = a'.fst) ∧ NodupKeys l
h : (a, b) ∈ l
⊢ b = b'
Tactic:
cases nd.1 _ h rfl
Proof state after:
no goals
Theorem: List.NodupKeys.lookup_eq_some
Proof state before:
case cons.h_2
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : (a == a') = false
⊢ lookup a l = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l
Tactic:
simp at h
Proof state after:
case cons.h_2
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : ¬a = a'
⊢ lookup a l = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l
Theorem: List.NodupKeys.lookup_eq_some
Proof state before:
case cons.h_2
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : ¬a = a'
⊢ lookup a l = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l
Tactic:
simp [h, ih nd.2]
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.lookup_isSome
Proof state before:
fv : FVarId
ofv : Option FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
⊢ Option.isSome (List.lookup (some fv) ((ofv, d) :: Δ)) = Option.isSome (find? ((ofv, d) :: Δ) (Sum.inr fv))
Tactic:
simp [List.lookup, find?, next]
Proof state after:
fv : FVarId
ofv : Option FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
⊢ Option.isSome
      (match some fv == ofv with
      | true => some d
      | false => List.lookup (some fv) Δ) =
    Option.isSome
      (match
        match ofv, Sum.inr fv with
        | none, Sum.inl 0 => none
        | none, Sum.inl (Nat.succ n) => some (Sum.inl n)
        | some val, Sum.inl n => some (Sum.inl n)
        | none, Sum.inr fv' => some (Sum.inr fv')
        | some fv, Sum.inr fv' => if (fv == fv') = true then none else some (Sum.inr fv') with
      | none => some (VLocalDecl.value d, VLocalDecl.type d)
      | some v =>
        Option.bind (find? Δ v) fun __discr =>
          some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd))
Theorem: Lean4Lean.VLCtx.lookup_isSome
Proof state before:
fv : FVarId
ofv : Option FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
⊢ Option.isSome
      (match some fv == ofv with
      | true => some d
      | false => List.lookup (some fv) Δ) =
    Option.isSome
      (match
        match ofv, Sum.inr fv with
        | none, Sum.inl 0 => none
        | none, Sum.inl (Nat.succ n) => some (Sum.inl n)
        | some val, Sum.inl n => some (Sum.inl n)
        | none, Sum.inr fv' => some (Sum.inr fv')
        | some fv, Sum.inr fv' => if (fv == fv') = true then none else some (Sum.inr fv') with
      | none => some (VLocalDecl.value d, VLocalDecl.type d)
      | some v =>
        Option.bind (find? Δ v) fun __discr =>
          some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd))
Tactic:
cases ofv with
| none =>
  simp [show (some fv == none) = false from rfl, lookup_isSome]
  cases find? Δ (.inr fv) <;> simp [bind]
| some fv' =>
  simp [show (some fv == some fv') = (fv == fv') from rfl, beq_comm fv]
  cases fv' == fv <;> simp [lookup_isSome]
  cases find? Δ (.inr fv) <;> simp [bind]
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.lookup_isSome
Proof state before:
case none
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
⊢ Option.isSome
      (match some fv == none with
      | true => some d
      | false => List.lookup (some fv) Δ) =
    Option.isSome
      (match
        match none, Sum.inr fv with
        | none, Sum.inl 0 => none
        | none, Sum.inl (Nat.succ n) => some (Sum.inl n)
        | some val, Sum.inl n => some (Sum.inl n)
        | none, Sum.inr fv' => some (Sum.inr fv')
        | some fv, Sum.inr fv' => if (fv == fv') = true then none else some (Sum.inr fv') with
      | none => some (VLocalDecl.value d, VLocalDecl.type d)
      | some v =>
        Option.bind (find? Δ v) fun __discr =>
          some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd))
Tactic:
simp [show (some fv == none) = false from rfl, lookup_isSome]
Proof state after:
case none
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
⊢ Option.isSome (find? Δ (Sum.inr fv)) =
    Option.isSome
      (Option.bind (find? Δ (Sum.inr fv)) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd))
Theorem: Lean4Lean.VLCtx.lookup_isSome
Proof state before:
case none
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
⊢ Option.isSome (find? Δ (Sum.inr fv)) =
    Option.isSome
      (Option.bind (find? Δ (Sum.inr fv)) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd))
Tactic:
cases find? Δ (.inr fv) <;> simp [bind]
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.lookup_isSome
Proof state before:
case some
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
fv' : FVarId
⊢ Option.isSome
      (match some fv == some fv' with
      | true => some d
      | false => List.lookup (some fv) Δ) =
    Option.isSome
      (match
        match some fv', Sum.inr fv with
        | none, Sum.inl 0 => none
        | none, Sum.inl (Nat.succ n) => some (Sum.inl n)
        | some val, Sum.inl n => some (Sum.inl n)
        | none, Sum.inr fv' => some (Sum.inr fv')
        | some fv, Sum.inr fv' => if (fv == fv') = true then none else some (Sum.inr fv') with
      | none => some (VLocalDecl.value d, VLocalDecl.type d)
      | some v =>
        Option.bind (find? Δ v) fun __discr =>
          some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd))
Tactic:
simp [show (some fv == some fv') = (fv == fv') from rfl, beq_comm fv]
Proof state after:
case some
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
fv' : FVarId
⊢ Option.isSome
      (match fv' == fv with
      | true => some d
      | false => List.lookup (some fv) Δ) =
    Option.isSome
      (match if (fv' == fv) = true then none else some (Sum.inr fv) with
      | none => some (VLocalDecl.value d, VLocalDecl.type d)
      | some v =>
        Option.bind (find? Δ v) fun __discr =>
          some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd))
Theorem: Lean4Lean.VLCtx.lookup_isSome
Proof state before:
case some
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
fv' : FVarId
⊢ Option.isSome
      (match fv' == fv with
      | true => some d
      | false => List.lookup (some fv) Δ) =
    Option.isSome
      (match if (fv' == fv) = true then none else some (Sum.inr fv) with
      | none => some (VLocalDecl.value d, VLocalDecl.type d)
      | some v =>
        Option.bind (find? Δ v) fun __discr =>
          some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd))
Tactic:
cases fv' == fv <;> simp [lookup_isSome]
Proof state after:
case some.false
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
fv' : FVarId
⊢ Option.isSome (find? Δ (Sum.inr fv)) =
    Option.isSome
      (Option.bind (find? Δ (Sum.inr fv)) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd))
Theorem: Lean4Lean.VLCtx.lookup_isSome
Proof state before:
case some.false
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
fv' : FVarId
⊢ Option.isSome (find? Δ (Sum.inr fv)) =
    Option.isSome
      (Option.bind (find? Δ (Sum.inr fv)) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd))
Tactic:
cases find? Δ (.inr fv) <;> simp [bind]
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.lookup_eq_some
Proof state before:
fv : FVarId
⊢ (∃ x, List.lookup (some fv) [] = some x) ↔ fv ∈ fvars []
Tactic:
simp
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.lookup_eq_some
Proof state before:
fv : FVarId
ofv : Option FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
⊢ (∃ x, List.lookup (some fv) ((ofv, d) :: Δ) = some x) ↔ fv ∈ fvars ((ofv, d) :: Δ)
Tactic:
cases ofv with
| none => simp [List.lookup, show (some fv == none) = false from rfl, lookup_eq_some]
| some fv' =>
  simp [List.lookup, show (some fv == some fv') = (fv == fv') from rfl]
  cases e : fv == fv' <;> simp at e <;> simp [e, lookup_eq_some]
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.lookup_eq_some
Proof state before:
case none
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
⊢ (∃ x, List.lookup (some fv) ((none, d) :: Δ) = some x) ↔ fv ∈ fvars ((none, d) :: Δ)
Tactic:
simp [List.lookup, show (some fv == none) = false from rfl, lookup_eq_some]
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.lookup_eq_some
Proof state before:
case some
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
fv' : FVarId
⊢ (∃ x, List.lookup (some fv) ((some fv', d) :: Δ) = some x) ↔ fv ∈ fvars ((some fv', d) :: Δ)
Tactic:
simp [List.lookup, show (some fv == some fv') = (fv == fv') from rfl]
Proof state after:
case some
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
fv' : FVarId
⊢ (∃ x,
      (match fv == fv' with
        | true => some d
        | false => List.lookup (some fv) Δ) =
        some x) ↔
    fv = fv' ∨ fv ∈ fvars Δ
Theorem: Lean4Lean.VLCtx.lookup_eq_some
Proof state before:
case some
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
fv' : FVarId
⊢ (∃ x,
      (match fv == fv' with
        | true => some d
        | false => List.lookup (some fv) Δ) =
        some x) ↔
    fv = fv' ∨ fv ∈ fvars Δ
Tactic:
cases e : fv == fv' <;> simp at e <;> simp [e, lookup_eq_some]
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.find?_eq_some
Proof state before:
fv : FVarId
Δ : VLCtx
⊢ (∃ x, find? Δ (Sum.inr fv) = some x) ↔ fv ∈ fvars Δ
Tactic:
rw [← Option.isSome_iff_exists, ← lookup_isSome, Option.isSome_iff_exists, lookup_eq_some]
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.map_toList
Proof 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]
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.map_toList
Proof 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
Proof 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✝) })
Theorem: Lean4Lean.TrLCtx.map_toList
Proof 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]
Proof 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✝)))
Theorem: Lean4Lean.TrLCtx.map_toList
Proof 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)
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.map_toList
Proof 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
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.forall₂
Proof state before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
⊢ List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d))
    (LocalContext.toList { fvarIdToDecl := PersistentHashMap.empty, decls := PersistentArray.empty }) []
Tactic:
simp [LocalContext.toList]
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.forall₂
Proof 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✝
a✝² : PersistentHashMap.find? map✝ fv✝ = none
a✝¹ : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
a✝ : TrLocalDecl env Us Δ✝ d✝ d'✝
⊢ List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d))
    (LocalContext.toList
      { fvarIdToDecl := PersistentHashMap.insert map✝ fv✝ d✝, decls := PersistentArray.push arr✝ (some d✝) })
    ((some fv✝, d'✝) :: Δ✝)
Tactic:
subst h1
Proof 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✝ } Δ✝
a✝¹ : TrLocalDecl env Us Δ✝ d✝ d'✝
a✝ : PersistentHashMap.find? map✝ (LocalDecl.fvarId d✝) = none
⊢ List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d))
    (LocalContext.toList
      { fvarIdToDecl := PersistentHashMap.insert map✝ (LocalDecl.fvarId d✝) d✝,
        decls := PersistentArray.push arr✝ (some d✝) })
    ((some (LocalDecl.fvarId d✝), d'✝) :: Δ✝)
Theorem: Lean4Lean.TrLCtx.forall₂
Proof 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✝ } Δ✝
a✝¹ : TrLocalDecl env Us Δ✝ d✝ d'✝
a✝ : PersistentHashMap.find? map✝ (LocalDecl.fvarId d✝) = none
⊢ List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d))
    (LocalContext.toList
      { fvarIdToDecl := PersistentHashMap.insert map✝ (LocalDecl.fvarId d✝) d✝,
        decls := PersistentArray.push arr✝ (some d✝) })
    ((some (LocalDecl.fvarId d✝), d'✝) :: Δ✝)
Tactic:
simp [LocalContext.toList]
Proof 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✝ } Δ✝
a✝¹ : TrLocalDecl env Us Δ✝ d✝ d'✝
a✝ : PersistentHashMap.find? map✝ (LocalDecl.fvarId d✝) = none
⊢ List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d))
    (d✝ :: List.filterMap id (List.reverse (PersistentArray.toList' arr✝))) ((some (LocalDecl.fvarId d✝), d'✝) :: Δ✝)
Theorem: Lean4Lean.TrLCtx.forall₂
Proof 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✝ } Δ✝
a✝¹ : TrLocalDecl env Us Δ✝ d✝ d'✝
a✝ : PersistentHashMap.find? map✝ (LocalDecl.fvarId d✝) = none
⊢ List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d))
    (d✝ :: List.filterMap id (List.reverse (PersistentArray.toList' arr✝))) ((some (LocalDecl.fvarId d✝), d'✝) :: Δ✝)
Tactic:
exact .cons rfl h4.forall₂
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.fvars_eq
Proof state before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
H : TrLCtx env Us lctx Δ
⊢ LocalContext.fvars lctx = VLCtx.fvars Δ
Tactic:
simp [LocalContext.fvars, VLCtx.fvars, LocalContext.toList]
Proof state after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
H : TrLCtx env Us lctx Δ
⊢ List.map (fun x => LocalDecl.fvarId x) (List.filterMap id (List.reverse (PersistentArray.toList' lctx.decls))) =
    List.filterMap (fun x => x.fst) Δ
Theorem: Lean4Lean.TrLCtx.fvars_eq
Proof state before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
H : TrLCtx env Us lctx Δ
⊢ List.map (fun x => LocalDecl.fvarId x) (List.filterMap id (List.reverse (PersistentArray.toList' lctx.decls))) =
    List.filterMap (fun x => x.fst) Δ
Tactic:
induction H with
| nil => rfl
| cons h1 _ _ _ _ ih => simp [h1, ← ih]
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.fvars_eq
Proof state before:
case nil
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
⊢ List.map (fun x => LocalDecl.fvarId x)
      (List.filterMap id
        (List.reverse
          (PersistentArray.toList'
            { fvarIdToDecl := PersistentHashMap.empty, decls := PersistentArray.empty }.decls))) =
    List.filterMap (fun x => x.fst) []
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.fvars_eq
Proof state before:
case cons
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✝
a✝³ : PersistentHashMap.find? map✝ fv✝ = none
a✝² : LocalDecl.index d✝ = arr✝.size
a✝¹ : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
a✝ : TrLocalDecl env Us Δ✝ d✝ d'✝
ih :
  List.map (fun x => LocalDecl.fvarId x)
      (List.filterMap id (List.reverse (PersistentArray.toList' { fvarIdToDecl := map✝, decls := arr✝ }.decls))) =
    List.filterMap (fun x => x.fst) Δ✝
⊢ List.map (fun x => LocalDecl.fvarId x)
      (List.filterMap id
        (List.reverse
          (PersistentArray.toList'
            { fvarIdToDecl := PersistentHashMap.insert map✝ fv✝ d✝,
                decls := PersistentArray.push arr✝ (some d✝) }.decls))) =
    List.filterMap (fun x => x.fst) ((some fv✝, d'✝) :: Δ✝)
Tactic:
simp [h1, ← ih]
Proof state after:
no goals
Theorem: Lean4Lean.TrLCtx.find?_isSome
Proof state before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ Option.isSome (LocalContext.find? lctx fv) = Option.isSome (VLCtx.find? Δ (Sum.inr fv))
Tactic:
rw [LocalContext.find?, H.map_wf.find?_eq, ← VLCtx.lookup_isSome,
  H.map_toList.lookup_eq H.map_wf.nodupKeys, List.map_fst_lookup]
Proof state after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (LocalContext.toList lctx)) =
    Option.isSome (List.lookup (some fv) Δ)
Theorem: Lean4Lean.TrLCtx.find?_isSome
Proof state before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (LocalContext.toList lctx)) =
    Option.isSome (List.lookup (some fv) Δ)
Tactic:
have := H.forall₂
Proof state after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
this : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) (LocalContext.toList lctx) Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (LocalContext.toList lctx)) =
    Option.isSome (List.lookup (some fv) Δ)
Theorem: Lean4Lean.TrLCtx.find?_isSome
Proof state before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
this : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) (LocalContext.toList lctx) Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (LocalContext.toList lctx)) =
    Option.isSome (List.lookup (some fv) Δ)
Tactic:
generalize lctx.toList = l at this ⊢
Proof state after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
l : List LocalDecl
this : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l) = Option.isSome (List.lookup (some fv) Δ)