Cases on operational semantics relation

Stream: Program verification

[Siddharth Priya]

Apologies for the long listing.
I have two __equivalent__ definitions Eval and Eval2 of a small step operational semantics for a control flow graph based programming language. Eval uses a structure andEval2 uses two Words for bb,stmt directly rather than a structure.

structure ProgCount where
  bb: Word
  stmt: Word
deriving Inhabited, Repr

inductive Eval : ProgCount × Prog × Env × Mem × AccessPerms →
  ProgCount × Prog × Env × Mem × AccessPerms →
    Prop
  | AssgnRel : ∀ (pc: ProgCount) (newpc: ProgCount) (lplace : List Word) (rexpr : RExpr) (env : Env) (mem : Mem)
    (ap : AccessPerms) (values : List MemValue) (ty : TyVal) (newAp : AccessPerms)
    (newMem : Mem) (newEnv : Env) (prog: Prog) (stmt_list: List Stmt),
    prog.find? pc.bb = some stmt_list →
    (h : pc.stmt < stmt_list.length) →
    stmt_list.get ⟨pc.stmt, h⟩ = Stmt.Assgn lplace rexpr →
    RExprToValFn rexpr env mem ap = RhsResult.Ok values ty newAp newMem →
    (match lplace with
    | [newplace] =>
      let (newAddr, allocatedMem) := allocate newMem (typeSize ty)
      let updatedMem := WriteWordSeq allocatedMem newAddr values
      let (tag, newAp) := freshTag newAp
      let updatedEnv := env.insert newplace (newAddr, ty, tag)
      LhsResult.Ok updatedEnv newAp updatedMem
    | _ =>
      match getPlaceAddr lplace env with
      | none => LhsResult.Err s!"lhs Place {lplace} not found in environment."
      | some addr =>
        let updatedMem := WriteWordSeq newMem addr values
        LhsResult.Ok env newAp updatedMem) = LhsResult.Ok newEnv newAp newMem →
        newpc = {pc with stmt := pc.stmt + 1} →
    Eval (pc, prog, env, mem, ap) (newpc, prog, newEnv, newMem, newAp)
  | HaltRel : ∀ (pc: ProgCount) (prog: Prog) (env : Env) (mem : Mem) (ap : AccessPerms) (stmt_list: List Stmt),
    prog.find? pc.bb = some stmt_list →
    (h: pc.stmt < stmt_list.length) →
    stmt_list.get ⟨pc.stmt, h⟩ = Stmt.Halt →
    Eval (pc, prog, env, mem, ap) (pc, prog, env, mem, ap)

When I want to prove the following theorem, then on the reverse implication, LEAN is not happy using case only with HaltRel

theorem step_pc_stays_same_iff_halt
    {pc : ProgCount} {prog : Prog} {env : Env} {mem : Mem} {ap : AccessPerms}
    {stmt_list : List Stmt}
    (h_bb : prog.find? pc.bb = some stmt_list)
    (h_stmt: pc.stmt < stmt_list.length):
      (stmt_list.get ⟨pc.stmt, h_stmt⟩ = Stmt.Halt) ↔
    Eval (pc, prog, env, mem, ap) (pc, prog, env, mem, ap) := by
  apply Iff.intro
  { intros h_stmt_eq
    apply Eval.HaltRel
    exact h_bb
    exact h_stmt_eq
  }
  {
    intros h_eval
    cases h_eval
    case HaltRel s1 s2 s3 s4 =>
     -- Unify stmt_list and s1
      have : stmt_list = s1 := by
        rw [s4] at h_bb
        injection h_bb with h_eq
        symm
        exact h_eq
      subst this
      exact s3
  }

It says

unsolved goals
case mpr.AssgnRel
pc : ProgCount
prog : Prog
env : Env
mem : Mem
ap : AccessPerms
stmt_list : List Stmt
h_bb : Lean.AssocList.find? pc.bb prog = some stmt_list
h_stmt : pc.stmt < stmt_list.length
lplace✝ : List Word
rexpr✝ : RExpr
values✝ : List MemValue
ty✝ : TyVal
stmt_list✝ : List Stmt
h✝ : pc.stmt < stmt_list✝.length
a✝⁴ : stmt_list✝.get ⟨pc.stmt, h✝⟩ = Assgn lplace✝ rexpr✝
a✝³ : Lean.AssocList.find? pc.bb prog = some stmt_list✝
a✝² : pc = { bb := pc.bb, stmt := pc.stmt + 1 }
a✝¹ : RExprToValFn rexpr✝ env mem ap = RhsResult.Ok values✝ ty✝ ap mem
a✝ :
  (match lplace✝ with
    | [newplace] =>
      match allocate mem (typeSize ty✝) with
      | (newAddr, allocatedMem) =>
        let updatedMem := WriteWordSeq allocatedMem newAddr values✝;
        match freshTag ap with
        | (tag, newAp) =>
          let updatedEnv := Lean.AssocList.insert env newplace (newAddr, ty✝, tag);
          LhsResult.Ok updatedEnv newAp updatedMem
    | x =>
      match getPlaceAddr lplace✝ env with
      | none =>
        LhsResult.Err
          (ToString.toString "lhs Place " ++ ToString.toString lplace✝ ++ ToString.toString " not found in environment.")
      | some addr =>
        let updatedMem := WriteWordSeq mem addr values✝;
        LhsResult.Ok env ap updatedMem) =
    LhsResult.Ok env ap mem
⊢ stmt_list.get ⟨pc.stmt, h_stmt⟩ = Halt

However if I tweak the relation such that the Program Counter is not a structure but individual Words (Nat), then LEAN is convinced that only one case (HaltRel) is enough on the reverse implication. Why?

abbrev PC := Word
abbrev BB := Word

inductive Eval2 : BB × PC  × Prog × Env × Mem × AccessPerms →
  BB × PC × Prog × Env × Mem × AccessPerms →
    Prop
  | AssgnRel : ∀ (bb: BB)  (pc: PC) (newpc: ProgCount) (lplace : List Word) (rexpr : RExpr) (env : Env) (mem : Mem)
    (ap : AccessPerms) (values : List MemValue) (ty : TyVal) (newAp : AccessPerms)
    (newMem : Mem) (newEnv : Env) (prog: Prog) (stmt_list: List Stmt),
    prog.find? bb = some stmt_list →
    (h : pc < stmt_list.length) →
    stmt_list.get ⟨pc, h⟩ = Stmt.Assgn lplace rexpr →
    RExprToValFn rexpr env mem ap = RhsResult.Ok values ty newAp newMem →
    (match lplace with
    | [newplace] =>
      let (newAddr, allocatedMem) := allocate newMem (typeSize ty)
      let updatedMem := WriteWordSeq allocatedMem newAddr values
      let (tag, newAp) := freshTag newAp
      let updatedEnv := env.insert newplace (newAddr, ty, tag)
      LhsResult.Ok updatedEnv newAp updatedMem
    | _ =>
      match getPlaceAddr lplace env with
      | none => LhsResult.Err s!"lhs Place {lplace} not found in environment."
      | some addr =>
        let updatedMem := WriteWordSeq newMem addr values
        LhsResult.Ok env newAp updatedMem) = LhsResult.Ok newEnv newAp newMem →
    Eval2 (bb, pc, prog, env, mem, ap) (bb, pc + 1, prog, newEnv, newMem, newAp)
  | HaltRel : ∀ (bb: BB) (pc: PC) (prog: Prog) (env : Env) (mem : Mem) (ap : AccessPerms) (stmt_list: List Stmt),
    prog.find? bb = some stmt_list →
    (h: pc < stmt_list.length) →
    stmt_list.get ⟨pc, h⟩ = Stmt.Halt →
    Eval2 (bb, pc, prog, env, mem, ap) (bb, pc, prog, env, mem, ap)


theorem step_pc_stays_same_iff_halt2
    {bb: BB} {pc : PC} {prog : Prog} {env : Env} {mem : Mem} {ap : AccessPerms}
    {stmt_list : List Stmt}
    (h_bb : prog.find? bb = some stmt_list)
    (h_stmt: pc < stmt_list.length):
      (stmt_list.get ⟨pc, h_stmt⟩ = Stmt.Halt) ↔
    Eval2 (bb, pc, prog, env, mem, ap) (bb, pc, prog, env, mem, ap) := by
  apply Iff.intro
  { intros h_stmt_eq
    apply Eval2.HaltRel
    exact h_bb
    exact h_stmt_eq
  }
  {
    intros h
    cases h
    case HaltRel s1 s2 s3 s4 =>
     -- Unify stmt_list and s1
      have : stmt_list = s1 := by
        rw [s4] at h_bb
        injection h_bb with h_eq
        symm
        exact h_eq
      subst this
      exact s3
}