Theorem: Lean4Lean.VLCtx.lookup_isSome (Lean4Lean/Verify/VLCtx.lean)

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]
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))

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

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]
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))

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

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]
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))

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]
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))

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