Library sect_4_side_effects

Refocused small-step syntax-directed MSOS for lambda-calculus

with exception handling

Require Export Coq.Lists.List
               Coq.Arith.EqNat
               Coq.Structures.Equalities
               Coq.Program.Equality.

Language syntax

Definition Identifier := nat.

Inductive Expr3 :=
| V3 : Val3 -> Expr3
| T3 : Trm3 -> Expr3
with Val3 :=
| NAT3 : nat -> Val3
| CLO3 : Identifier ->
           Expr3 ->
           list (Identifier * Val3) ->
           Val3
| UNIT3 : Val3
| TRUE3 : Val3
| FALSE3 : Val3
| VEXC3 : Exception3 ->
           Val3
with Trm3 :=
| VAR3 : Identifier ->
           Trm3
| APP3 : Expr3 ->
           Expr3 ->
           Trm3
| ABS3 : Identifier ->
           Expr3 ->
           Trm3
| THROW3 : Val3 ->
           Trm3
| IF3 : Expr3 ->
           Expr3 ->
           Expr3 ->
           Trm3
| EQ3 : Expr3 ->
           Expr3 ->
           Trm3
| CATCH3 : Exception3 ->
           Expr3 ->
           Expr3 ->
           Trm3
with Exception3 :=
| TAU3 : Exception3
| ERR3 : Val3 -> Exception3.

Definition is_val3 (v : Expr3) :=
  match v with
    | (V3 _) => true
    | _ => false
  end.

Auxiliary entities

Environments
Definition Env3 := list (Identifier * Val3).

Fixpoint map_lookup {Value : Type}
                    (m : list (Identifier * Value))
                    (i : Identifier) :=
  match m with
    | nil => None
    | cons (i', v) m' =>
      match beq_nat i i' with
        | true => Some v
        | false => map_lookup m' i
      end
  end.

Fixpoint map_update {Value : Type}
                    (m : list (Identifier * Value))
                    (i : Identifier)
                    (v : Value) :=
  match m with
    | nil => cons (i, v) nil
    | cons (i', v) m' =>
      match beq_nat i i' with
        | true => cons (i, v) m'
        | false => map_update m' i v
      end
  end.

Divergence flag
Inductive Div :=
| UPARROW : Div
| DNARROW : Div.

Exc3 read-write label component
Definition Exc3 := (Exception3 * Exception3)%type.

Full label
Definition Label3 := (Env3 * Div * Exc3 * unit)%type.

Definition get_env3 (l : Label3) : Env3 :=
  match l with
    | (rho, _, _, _) => rho
  end.

Definition get_div3 (l : Label3) : Div :=
  match l with
    | (_, div, _, _) => div
  end.

Definition get_exc3 (l : Label3) : Exc3 :=
  match l with
    | (_, _, exc, _) => exc
  end.

Definition replace_env3 (l : Label3) (rho : Env3) : Label3 :=
  match l with
    | (rho', div, exc, tail) => (rho, div, exc, tail)
  end.

Definition replace_div3 (l : Label3) (div : Div) : Label3 :=
  match l with
    | (rho, div', exc, tail) => (rho, div, exc, tail)
  end.

Definition replace_exc3 (l : Label3) (exc : Exc3) : Label3 :=
  match l with
    | (rho, div, exc', tail) => (rho, div, exc, tail)
  end.

Definition unobs_label3 (l : Label3) : Prop :=
  match l with
    | (_, DNARROW, (TAU3, TAU3), _) =>
      True
    | (_, DNARROW, (ERR3 v, ERR3 v'), _) =>
      v = v'
    | (_, _, _, _) => False
  end.

Definition is_abr_ter3 (l : Label3) :=
  match l with
    | (_, _, (_, ERR3 _), _) => true
    | (_, _, (ERR3 _, _), _) => true
    | _ => false
  end.

Refocused semantics

Inductive PBStep3 : Expr3 -> Label3 -> Expr3 -> Prop :=
| PBSTEP3_VAR x env v :
    map_lookup env x = Some v ->
    PBStep3 (T3 (VAR3 x)) (env, DNARROW, (TAU3, TAU3), tt) (V3 v)
| PBSTEP3_ABS x t env :
    PBStep3 (T3 (ABS3 x t))
            (env, DNARROW, (TAU3, TAU3), tt)
            (V3 (CLO3 x t env))
| PBSTEP3_APP1 t1 env a a' e1' e2 e3 :
    PBStep3 (T3 t1) (env, DNARROW, (TAU3, a), tt) e1' ->
    PBStep3 (T3 (APP3 e1' e2)) (env, DNARROW, (a, a'), tt) e3 ->
    PBStep3 (T3 (APP3 (T3 t1) e2)) (env, DNARROW, (TAU3, a'), tt) e3
| PBSTEP3_APP2 t2 a e2' v1 a' env e3 :
    PBStep3 (T3 t2) (env, DNARROW, (TAU3, a), tt) e2' ->
    PBStep3 (T3 (APP3 (V3 v1) e2'))
            (env, DNARROW, (a, a'), tt)
            e3 ->
    PBStep3 (T3 (APP3 (V3 v1) (T3 t2)))
            (env, DNARROW, (TAU3, a'), tt)
            e3
| PBSTEP3_APP3 t rho x v2 a e' a' e3 env :
    PBStep3 (T3 t) (map_update rho x v2, DNARROW, (TAU3, a), tt) e' ->
    PBStep3 (T3 (APP3 (V3 (CLO3 x e' rho)) (V3 v2)))
            (env, DNARROW, (a, a'), tt) e3 ->
    PBStep3 (T3 (APP3 (V3 (CLO3 x (T3 t) rho)) (V3 v2)))
            (env, DNARROW, (TAU3, a'), tt) e3
| PBSTEP3_APP4 x v rho env v2 :
    PBStep3 (T3 (APP3 (V3 (CLO3 x (V3 v) rho)) (V3 v2)))
            (env, DNARROW, (TAU3, TAU3), tt)
            (V3 v)
| PBSTEP3_THROW v env :
    PBStep3 (T3 (THROW3 v))
            (env, DNARROW, (TAU3, ERR3 v), tt)
            (V3 UNIT3)
| PBSTEP3_IF t e' e1 e2 env a a' e3 :
    PBStep3 (T3 t) (env, DNARROW, (TAU3, a), tt) e' ->
    PBStep3 (T3 (IF3 e' e1 e2))
            (env, DNARROW, (a, a'), tt) e3 ->
    PBStep3 (T3 (IF3 (T3 t) e1 e2)) (env, DNARROW, (TAU3, a'), tt) e3
| PBSTEP3_IFTRUE e1 e2 e3 env a :
    PBStep3 e1
            (env, DNARROW, (TAU3, a), tt)
            e3 ->
    PBStep3 (T3 (IF3 (V3 TRUE3) e1 e2))
            (env, DNARROW, (TAU3, a), tt)
            e3
| PBSTEP3_IFFALSE e1 e2 e3 env a :
    PBStep3 e2
            (env, DNARROW, (TAU3, a), tt)
            e3 ->
    PBStep3 (T3 (IF3 (V3 FALSE3) e1 e2))
            (env, DNARROW, (TAU3, a), tt)
            e3
| PBSTEP3_EQ1 t1 env e1' e2 a a' e3 :
    PBStep3 (T3 t1) (env, DNARROW, (TAU3, a), tt) e1' ->
    PBStep3 (T3 (EQ3 e1' e2))
            (env, DNARROW, (a, a'), tt)
            e3 ->
    PBStep3 (T3 (EQ3 (T3 t1) e2))
            (env, DNARROW, (TAU3, a'), tt) e3
| PBSTEP3_EQ2 t2 env e2' v1 a a' e3 :
    PBStep3 (T3 t2) (env, DNARROW, (TAU3, a), tt) e2' ->
    PBStep3 (T3 (EQ3 (V3 v1) e2'))
            (env, DNARROW, (a, a'), tt)
            e3 ->
    PBStep3 (T3 (EQ3 (V3 v1) (T3 t2)))
            (env, DNARROW, (TAU3, a'), tt)
            e3
| PBSTEP3_EQ v1 v2 env :
    v1 = v2 ->
    PBStep3 (T3 (EQ3 (V3 v1) (V3 v2)))
            (env, DNARROW, (TAU3, TAU3), tt)
            (V3 TRUE3)
| PBSTEP3_EQN v1 v2 env :
    v1 <> v2 ->
    PBStep3 (T3 (EQ3 (V3 v1) (V3 v2)))
            (env, DNARROW, (TAU3, TAU3), tt)
            (V3 FALSE3)
| PBSTEP3_CATCH_V v1 e2 env :
    PBStep3 (T3 (CATCH3 TAU3 (V3 v1) e2))
            (env, DNARROW, (TAU3, TAU3), tt)
            (V3 v1)
| PBSTEP3_CATCH_ERR v e1 e2 e3 env a :
    PBStep3 (T3 (APP3 e2 (V3 v))) (env, DNARROW, (TAU3, a), tt)
            e3 ->
    PBStep3 (T3 (CATCH3 (ERR3 v) e1 e2))
            (env, DNARROW, (TAU3, a), tt)
            e3
| PBSTEP3_CATCH t1 e1' env a e2 e3 a' :
    PBStep3 (T3 t1)
            (env, DNARROW, (TAU3, a), tt)
            e1' ->
    PBStep3 (T3 (CATCH3 a e1' e2))
            (env, DNARROW, (TAU3, a'), tt)
            e3 ->
    PBStep3 (T3 (CATCH3 TAU3 (T3 t1) e2))
            (env, DNARROW, (TAU3, a'), tt)
            e3
| PBREFL3_V v l :
    unobs_label3 l ->
    PBStep3 (V3 v) l (V3 v)
| PBREFL3_ERR e v l :
    get_exc3 l = (ERR3 v, ERR3 v) ->
    unobs_label3 (replace_exc3 l (TAU3, TAU3)) ->
    PBStep3 e l e.

Small-step semantics

Inductive Step3 : Expr3 -> Label3 -> Expr3 -> Prop :=
| STEP3_VAR x l v :
    unobs_label3 l ->
    map_lookup (get_env3 l) x = Some v ->
    Step3 (T3 (VAR3 x)) l (V3 v)
| STEP3_ABS x t l :
    unobs_label3 l ->
    Step3 (T3 (ABS3 x t)) l (V3 (CLO3 x t (get_env3 l)))
| STEP3_APP1 t1 e2 e1' l :
    Step3 (T3 t1) l e1' ->
    Step3 (T3 (APP3 (T3 t1) e2)) l (T3 (APP3 e1' e2))
| STEP3_APP2 v1 t2 l e2' :
    Step3 (T3 t2) l e2' ->
    Step3 (T3 (APP3 (V3 v1) (T3 t2))) l (T3 (APP3 (V3 v1) e2'))
| STEP3_APP3 x t e' rho v2 l :
    Step3 (T3 t) (replace_env3 l (map_update rho x v2)) e' ->
    Step3 (T3 (APP3 (V3 (CLO3 x (T3 t) rho)) (V3 v2)))
          l
          (T3 (APP3 (V3 (CLO3 x e' rho)) (V3 v2)))
| STEP3_APP4 x v rho v2 l :
    unobs_label3 l ->
    Step3 (T3 (APP3 (V3 (CLO3 x (V3 v) rho)) (V3 v2))) l (V3 v)
| STEP3_THROW v l :
    get_exc3 l = (TAU3, ERR3 v) ->
    unobs_label3 (replace_exc3 l (TAU3, TAU3)) ->
    Step3 (T3 (THROW3 v)) l (V3 UNIT3)
| STEP3_IF t e' e1 e2 l :
    Step3 (T3 t) l e' ->
    Step3 (T3 (IF3 (T3 t) e1 e2)) l
          (T3 (IF3 e' e1 e2))
| STEP3_IFTRUE e1 e2 l :
    unobs_label3 l ->
    Step3 (T3 (IF3 (V3 TRUE3) e1 e2)) l e1
| STEP3_IFFALSE e1 e2 l :
    unobs_label3 l ->
    Step3 (T3 (IF3 (V3 FALSE3) e1 e2)) l e2
| STEP3_EQ1 t1 e1' e2 l :
    Step3 (T3 t1) l e1' ->
    Step3 (T3 (EQ3 (T3 t1) e2)) l (T3 (EQ3 e1' e2))
| STEP3_EQ2 v1 t2 e2' l :
    Step3 (T3 t2) l e2' ->
    Step3 (T3 (EQ3 (V3 v1) (T3 t2))) l (T3 (EQ3 (V3 v1) e2'))
| STEP3_EQ v1 v2 l :
    v1 = v2 ->
    unobs_label3 l ->
    Step3 (T3 (EQ3 (V3 v1) (V3 v2))) l (V3 TRUE3)
| STEP3_EQN v1 v2 l :
    v1 <> v2 ->
    unobs_label3 l ->
    Step3 (T3 (EQ3 (V3 v1) (V3 v2))) l (V3 FALSE3)
| STEP3_CATCH_V v1 e2 l :
    unobs_label3 l ->
    Step3 (T3 (CATCH3 TAU3 (V3 v1) e2)) l (V3 v1)
| STEP3_CATCH_ERR v e1 e2 l :
    unobs_label3 l ->
    Step3 (T3 (CATCH3 (ERR3 v) e1 e2)) l (T3 (APP3 e2 (V3 v)))
| STEP3_CATCH t1 e1' e2 l l' a :
    Step3 (T3 t1) l e1' ->
    get_exc3 l = (TAU3, a) ->
    l' = (replace_exc3 l (TAU3, TAU3)) ->
    Step3 (T3 (CATCH3 TAU3 (T3 t1) e2))
          l'
          (T3 (CATCH3 a e1' e2)).

Inductive Eval3 : Expr3 -> Label3 -> Expr3 -> Prop :=
| EVAL3 t1 e2 e3 env a a' :
    Step3 (T3 t1) (env, DNARROW, (TAU3, a), tt) e2 ->
    Eval3 e2 (env, DNARROW, (a, a'), tt) e3 ->
    Eval3 (T3 t1) (env, DNARROW, (TAU3, a'), tt) e3
| REFL3_V v l :
    unobs_label3 l ->
    Eval3 (V3 v) l (V3 v)
| REFL3_ERR e v l :
    get_exc3 l = (ERR3 v, ERR3 v) ->
    unobs_label3 (replace_exc3 l (TAU3, TAU3)) ->
    Eval3 e l e.

Inductive Trans3 : Expr3 -> Label3 -> Expr3 -> Prop :=
| TRANS3 t1 e2 e3 env a a' :
    Step3 (T3 t1) (env, DNARROW, (TAU3, a), tt) e2 ->
    Trans3 e2 (env, DNARROW, (a, a'), tt) e3 ->
    Trans3 (T3 t1) (env, DNARROW, (TAU3, a'), tt) e3
| REFL3 env e a :
    Trans3 e (env, DNARROW, (a, a), tt) e.

Extending with side-effects

Language syntax

Definition Location := nat.

Inductive Expr4 :=
| V4 : Val4 -> Expr4
| T4 : Trm4 -> Expr4
with Val4 :=
| NAT4 : nat -> Val4
| CLO4 : Identifier ->
           Expr4 ->
           list (Identifier * Val4) ->
           Val4
| UNIT4 : Val4
| TRUE4 : Val4
| FALSE4 : Val4
| VEXC4 : Exception4 ->
           Val4
| LOC : Location ->
           Val4
with Trm4 :=
| VAR4 : Identifier ->
            Trm4
| APP4 : Expr4 ->
            Expr4 ->
            Trm4
| ABS4 : Identifier ->
            Expr4 ->
            Trm4
| THROW4 : Val4 ->
            Trm4
| IF4 : Expr4 ->
            Expr4 ->
            Expr4 ->
            Trm4
| EQ4 : Expr4 ->
            Expr4 ->
            Trm4
| CATCH4 : Exception4 ->
            Expr4 ->
            Expr4 ->
            Trm4
| PRINT4 : Expr4 ->
            Trm4
| REF4 : Expr4 ->
            Trm4
| DEREF4 : Expr4 ->
            Trm4
| ASSIGN4 : Expr4 ->
            Expr4 ->
            Trm4
with Exception4 :=
| TAU4 : Exception4
| ERR4 : Val4 -> Exception4.

Definition is_val4 (v : Expr4) :=
  match v with
    | (V4 _) => true
    | _ => false
  end.

Auxiliary entities

Environments
Definition Env4 := list (Identifier * Val4).

Exc4 read-write label component
Definition Exc4 := (Exception4 * Exception4)%type.

Out4 write-only label component
Definition Out4 := list Val4.

Store4 read-write label component
Definition Store4 := ((list (Location * Val4)) * (list (Location * Val4)))%type.

Definition fresh_loc (s : list (Location * Val4)) : Location :=
  (fold_left max (map (fun p => match p with
                                  | (loc, _) => loc
                                end) s) 0) + 1.

Full label
Definition Label4 := (Env4 * Div * Exc4 * Out4 * Store4 * unit)%type.

Definition get_env4 (l : Label4) : Env4 :=
  match l with
    | (rho, _, _, _, _, _) => rho
  end.

Definition get_div4 (l : Label4) : Div :=
  match l with
    | (_, div, _, _, _, _) => div
  end.

Definition get_exc4 (l : Label4) : Exc4 :=
  match l with
    | (_, _, exc, _, _, _) => exc
  end.

Definition get_out4 (l : Label4) : Out4 :=
  match l with
    | (_, _, _, out, _, _) => out
  end.

Definition get_store4 (l : Label4) : Store4 :=
  match l with
    | (_, _, _, _, store, _) => store
  end.

Definition replace_env4 (l : Label4) (rho : Env4) : Label4 :=
  match l with
    | (rho', div, exc, out, store, tail) => (rho, div, exc, out, store, tail)
  end.

Definition replace_div4 (l : Label4) (div : Div) : Label4 :=
  match l with
    | (rho, div', exc, out, store, tail) => (rho, div, exc, out, store, tail)
  end.

Definition replace_exc4 (l : Label4) (exc : Exc4) : Label4 :=
  match l with
    | (rho, div, exc', out, store, tail) => (rho, div, exc, out, store, tail)
  end.

Definition replace_out4 (l : Label4) (out : Out4) : Label4 :=
  match l with
    | (rho, div, exc, out', store, tail) => (rho, div, exc, out, store, tail)
  end.

Definition replace_store4 (l : Label4) (store : Store4) : Label4 :=
  match l with
    | (rho, div, exc, out, store', tail) => (rho, div, exc, out, store, tail)
  end.

Definition unobs_label4 (l : Label4) : Prop :=
  match l with
    | (_, DNARROW, (TAU4, TAU4), nil, (store, store'), _) =>
      store = store'
    | (_, DNARROW, (ERR4 v, ERR4 v'), nil, (store, store'), _) =>
      v = v' /\ store = store'
    | _ => False
  end.

Definition is_abr_ter4 (l : Label4) :=
  match l with
    | (_, _, (_, ERR4 _), _, _, _) => true
    | (_, _, (ERR4 _, _), _, _, _) => true
    | _ => false
  end.

Small-step semantics

Inductive Step4 : Expr4 -> Label4 -> Expr4 -> Prop :=
| STEP4_VAR x l v :
    unobs_label4 l ->
    map_lookup (get_env4 l) x = Some v ->
    Step4 (T4 (VAR4 x)) l (V4 v)
| STEP4_ABS x t l :
    unobs_label4 l ->
    Step4 (T4 (ABS4 x t)) l (V4 (CLO4 x t (get_env4 l)))
| STEP4_APP1 t1 e2 e1' l :
    Step4 (T4 t1) l e1' ->
    Step4 (T4 (APP4 (T4 t1) e2)) l (T4 (APP4 e1' e2))
| STEP4_APP2 v1 t2 l e2' :
    Step4 (T4 t2) l e2' ->
    Step4 (T4 (APP4 (V4 v1) (T4 t2))) l (T4 (APP4 (V4 v1) e2'))
| STEP4_APP3 x t e' rho v2 l :
    Step4 (T4 t) (replace_env4 l (map_update rho x v2)) e' ->
    Step4 (T4 (APP4 (V4 (CLO4 x (T4 t) rho)) (V4 v2)))
          l
          (T4 (APP4 (V4 (CLO4 x e' rho)) (V4 v2)))
| STEP4_APP4 x v rho v2 l :
    unobs_label4 l ->
    Step4 (T4 (APP4 (V4 (CLO4 x (V4 v) rho)) (V4 v2))) l (V4 v)
| STEP4_THROW v l :
    get_exc4 l = (TAU4, ERR4 v) ->
    unobs_label4 (replace_exc4 l (TAU4, TAU4)) ->
    Step4 (T4 (THROW4 v)) l (V4 UNIT4)
| STEP4_IF t e' e1 e2 l :
    Step4 (T4 t) l e' ->
    Step4 (T4 (IF4 (T4 t) e1 e2)) l
          (T4 (IF4 e' e1 e2))
| STEP4_IFTRUE e1 e2 l :
    unobs_label4 l ->
    Step4 (T4 (IF4 (V4 TRUE4) e1 e2)) l e1
| STEP4_IFFALSE e1 e2 l :
    unobs_label4 l ->
    Step4 (T4 (IF4 (V4 FALSE4) e1 e2)) l e2
| STEP4_EQ1 t1 e1' e2 l :
    Step4 (T4 t1) l e1' ->
    Step4 (T4 (EQ4 (T4 t1) e2)) l (T4 (EQ4 e1' e2))
| STEP4_EQ2 v1 t2 e2' l :
    Step4 (T4 t2) l e2' ->
    Step4 (T4 (EQ4 (V4 v1) (T4 t2))) l (T4 (EQ4 (V4 v1) e2'))
| STEP4_EQ v1 v2 l :
    v1 = v2 ->
    unobs_label4 l ->
    Step4 (T4 (EQ4 (V4 v1) (V4 v2))) l (V4 TRUE4)
| STEP4_EQN v1 v2 l :
    v1 <> v2 ->
    unobs_label4 l ->
    Step4 (T4 (EQ4 (V4 v1) (V4 v2))) l (V4 FALSE4)
| STEP4_CATCH_V v1 e2 l :
    unobs_label4 l ->
    Step4 (T4 (CATCH4 TAU4 (V4 v1) e2)) l (V4 v1)
| STEP4_CATCH_ERR v e1 e2 l :
    unobs_label4 l ->
    Step4 (T4 (CATCH4 (ERR4 v) e1 e2)) l (T4 (APP4 e2 (V4 v)))
| STEP4_CATCH t1 e1' e2 l l' a :
    Step4 (T4 t1) l e1' ->
    get_exc4 l = (TAU4, a) ->
    l' = (replace_exc4 l (TAU4, TAU4)) ->
    Step4 (T4 (CATCH4 TAU4 (T4 t1) e2))
          l'
          (T4 (CATCH4 a e1' e2))
| STEP4_PRINT t l e :
    Step4 (T4 t) l e ->
    Step4 (T4 (PRINT4 (T4 t))) l (T4 (PRINT4 e))
| STEP4_PRINT_V v l :
    unobs_label4 (replace_out4 l nil) ->
    get_out4 l = v :: nil ->
    Step4 (T4 (PRINT4 (V4 v))) l (V4 UNIT4)
| STEP4_REF t l e :
    Step4 (T4 t) l e ->
    Step4 (T4 (REF4 (T4 t))) l (T4 (REF4 e))
| STEP4_REF_V v l loc store :
    unobs_label4 (replace_store4 l (store, store)) ->
    get_store4 l = (store, map_update store loc v) ->
    fresh_loc store = loc ->
    Step4 (T4 (REF4 (V4 v))) l (V4 (LOC loc))
| STEP4_DEREF t l e :
    Step4 (T4 t) l e ->
    Step4 (T4 (DEREF4 (T4 t))) l (T4 (DEREF4 e))
| STEP4_DEREF_LOC l store loc v :
    unobs_label4 l ->
    get_store4 l = (store, store) ->
    map_lookup store loc = Some v ->
    Step4 (T4 (DEREF4 (V4 (LOC loc)))) l (V4 v)
| STEP4_ASSIGN1 t1 l e1 e2 :
    Step4 (T4 t1) l e1 ->
    Step4 (T4 (ASSIGN4 (T4 t1) e2)) l (T4 (ASSIGN4 e1 e2))
| STEP4_ASSIGN2 t2 l e2 v1 :
    Step4 (T4 t2) l e2 ->
    Step4 (T4 (ASSIGN4 (V4 v1) (T4 t2))) l (T4 (ASSIGN4 (V4 v1) e2))
| STEP4_ASSIGN_V loc v l store :
    unobs_label4 (replace_store4 l (store, store)) ->
    get_store4 l = (store, map_update store loc v) ->
    Step4 (T4 (ASSIGN4 (V4 (LOC loc)) (V4 v))) l (V4 UNIT4).

Inductive Eval4 : Expr4 -> Label4 -> Expr4 -> Prop :=
| EVAL4 t1 e2 e4 env a a' out out' store store' store'' :
    Step4 (T4 t1) (env, DNARROW, (TAU4, a), out, (store, store'), tt) e2 ->
    Eval4 e2 (env, DNARROW, (a, a'), out', (store', store''), tt) e4 ->
    Eval4 (T4 t1) (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt) e4
| REFL4_V v l :
    unobs_label4 l ->
    Eval4 (V4 v) l (V4 v)
| REFL4_ERR e v l :
    get_exc4 l = (ERR4 v, ERR4 v) ->
    unobs_label4 (replace_exc4 l (TAU4, TAU4)) ->
    Eval4 e l e.

Inductive Trans4 : Expr4 -> Label4 -> Expr4 -> Prop :=
| TRANS4 t1 e2 e4 env a a' out out' store store' store'' :
    Step4 (T4 t1) (env, DNARROW, (TAU4, a), out, (store, store'), tt) e2 ->
    Trans4 e2 (env, DNARROW, (a, a'), out', (store', store''), tt) e4 ->
    Trans4 (T4 t1) (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt) e4
| REFL4 env e a store :
    Trans4 e (env, DNARROW, (a, a), nil, (store, store), tt) e.

Refocused semantics

Inductive PBStep4 : Expr4 -> Label4 -> Expr4 -> Prop :=
| PBSTEP4_VAR x env v store :
    map_lookup env x = Some v ->
    PBStep4 (T4 (VAR4 x))
            (env, DNARROW, (TAU4, TAU4), nil, (store, store), tt)
            (V4 v)
| PBSTEP4_ABS x t env store :
    PBStep4 (T4 (ABS4 x t))
            (env, DNARROW, (TAU4, TAU4), nil, (store, store), tt)
            (V4 (CLO4 x t env))
| PBSTEP4_APP1 t1 env a a' e1' e2 e4 out out' store store' store'' :
    PBStep4 (T4 t1)
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e1' ->
    PBStep4 (T4 (APP4 e1' e2))
            (env, DNARROW, (a, a'), out', (store', store''), tt)
            e4 ->
    PBStep4 (T4 (APP4 (T4 t1) e2))
            (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt)
            e4
| PBSTEP4_APP2 t2 a e2' v1 a' env e4 out out' store store' store'' :
    PBStep4 (T4 t2) (env, DNARROW, (TAU4, a), out, (store, store'), tt) e2' ->
    PBStep4 (T4 (APP4 (V4 v1) e2'))
            (env, DNARROW, (a, a'), out', (store', store''), tt)
            e4 ->
    PBStep4 (T4 (APP4 (V4 v1) (T4 t2)))
            (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt)
            e4
| PBSTEP4_APP3 t rho x v2 a e' a' e4 env out out' store store' store'' :
    PBStep4 (T4 t)
            (map_update rho x v2, DNARROW, (TAU4, a), out, (store, store'), tt)
            e' ->
    PBStep4 (T4 (APP4 (V4 (CLO4 x e' rho)) (V4 v2)))
            (env, DNARROW, (a, a'), out', (store', store''), tt) e4 ->
    PBStep4 (T4 (APP4 (V4 (CLO4 x (T4 t) rho)) (V4 v2)))
            (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt)
            e4
| PBSTEP4_APP4 x v rho env v2 store :
    PBStep4 (T4 (APP4 (V4 (CLO4 x (V4 v) rho)) (V4 v2)))
            (env, DNARROW, (TAU4, TAU4), nil, (store, store), tt)
            (V4 v)
| PBSTEP4_THROW v env store :
    PBStep4 (T4 (THROW4 v))
            (env, DNARROW, (TAU4, ERR4 v), nil, (store, store), tt)
            (V4 UNIT4)
| PBSTEP4_IF t e' e1 e2 env a a' e3 out out' store store' store'' :
    PBStep4 (T4 t)
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e' ->
    PBStep4 (T4 (IF4 e' e1 e2))
            (env, DNARROW, (a, a'), out', (store', store''), tt)
            e3 ->
    PBStep4 (T4 (IF4 (T4 t) e1 e2))
            (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt)
            e3
| PBSTEP4_IFTRUE e1 e2 e3 env a out store store' :
    PBStep4 e1
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e3 ->
    PBStep4 (T4 (IF4 (V4 TRUE4) e1 e2))
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e3
| PBSTEP4_IFFALSE e1 e2 e3 env a out store store' :
    PBStep4 e2
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e3 ->
    PBStep4 (T4 (IF4 (V4 FALSE4) e1 e2))
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e3
| PBSTEP4_EQ1 t1 env e1' e2 a a' e3 out out' store store' store'' :
    PBStep4 (T4 t1)
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e1' ->
    PBStep4 (T4 (EQ4 e1' e2))
            (env, DNARROW, (a, a'), out', (store', store''), tt)
            e3 ->
    PBStep4 (T4 (EQ4 (T4 t1) e2))
            (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt)
            e3
| PBSTEP4_EQ2 t2 env e2' v1 a a' e3 out out' store store' store'' :
    PBStep4 (T4 t2)
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e2' ->
    PBStep4 (T4 (EQ4 (V4 v1) e2'))
            (env, DNARROW, (a, a'), out', (store', store''), tt)
            e3 ->
    PBStep4 (T4 (EQ4 (V4 v1) (T4 t2)))
            (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt)
            e3
| PBSTEP4_EQ v1 v2 env store :
    v1 = v2 ->
    PBStep4 (T4 (EQ4 (V4 v1) (V4 v2)))
            (env, DNARROW, (TAU4, TAU4), nil, (store, store), tt)
            (V4 TRUE4)
| PBSTEP4_EQN v1 v2 env store :
    v1 <> v2 ->
    PBStep4 (T4 (EQ4 (V4 v1) (V4 v2)))
            (env, DNARROW, (TAU4, TAU4), nil, (store, store), tt)
            (V4 FALSE4)
| PBSTEP4_CATCH_V v1 e2 env store :
    PBStep4 (T4 (CATCH4 TAU4 (V4 v1) e2))
            (env, DNARROW, (TAU4, TAU4), nil, (store, store), tt)
            (V4 v1)
| PBSTEP4_CATCH_ERR v e1 e2 e3 env a out store store' :
    PBStep4 (T4 (APP4 e2 (V4 v)))
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e3 ->
    PBStep4 (T4 (CATCH4 (ERR4 v) e1 e2))
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e3
| PBSTEP4_CATCH t1 e1' env a e2 e3 a' out out' store store' store'' :
    PBStep4 (T4 t1)
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e1' ->
    PBStep4 (T4 (CATCH4 a e1' e2))
            (env, DNARROW, (TAU4, a'), out', (store', store''), tt)
            e3 ->
    PBStep4 (T4 (CATCH4 TAU4 (T4 t1) e2))
            (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt)
            e3
| PBSTEP4_PRINT t e e' env a a' out out' store store' store'' :
    PBStep4 (T4 t)
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e ->
    PBStep4 (T4 (PRINT4 e))
            (env, DNARROW, (a, a'), out', (store', store''), tt)
            e' ->
    PBStep4 (T4 (PRINT4 (T4 t)))
            (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt)
            e'
| PBSTEP4_PRINT_V v env store :
    PBStep4 (T4 (PRINT4 (V4 v)))
            (env, DNARROW, (TAU4, TAU4), v :: nil, (store, store), tt)
            (V4 UNIT4)
| PBSTEP4_REF t e e' env a a' out out' store store' store'' :
    PBStep4 (T4 t)
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e ->
    PBStep4 (T4 (REF4 e))
            (env, DNARROW, (a, a'), out', (store', store''), tt)
            e' ->
    PBStep4 (T4 (REF4 (T4 t)))
            (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt)
            e'
| PBSTEP4_REF_V v env loc store :
    fresh_loc store = loc ->
    PBStep4 (T4 (REF4 (V4 v)))
            (env, DNARROW, (TAU4, TAU4), nil, (store, map_update store loc v), tt)
            (V4 (LOC loc))
| PBSTEP4_DEREF t e e' env a a' out out' store store' store'' :
    PBStep4 (T4 t)
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e ->
    PBStep4 (T4 (DEREF4 e))
            (env, DNARROW, (a, a'), out', (store', store''), tt)
            e' ->
    PBStep4 (T4 (DEREF4 (T4 t)))
            (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt)
            e'
| PBSTEP4_DEREF_LOC loc v env store :
    map_lookup store loc = Some v ->
    PBStep4 (T4 (DEREF4 (V4 (LOC loc))))
            (env, DNARROW, (TAU4, TAU4), nil, (store, store), tt)
            (V4 v)
| PBSTEP4_ASSIGN1 t1 e1 e2 e' env a a' out out' store store' store'' :
    PBStep4 (T4 t1)
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e1 ->
    PBStep4 (T4 (ASSIGN4 e1 e2))
            (env, DNARROW, (a, a'), out', (store', store''), tt)
            e' ->
    PBStep4 (T4 (ASSIGN4 (T4 t1) e2))
            (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt)
            e'
| PBSTEP4_ASSIGN2 t2 v1 e2 e' env a a' out out' store store' store'' :
    PBStep4 (T4 t2)
            (env, DNARROW, (TAU4, a), out, (store, store'), tt)
            e2 ->
    PBStep4 (T4 (ASSIGN4 (V4 v1) e2))
            (env, DNARROW, (a, a'), out', (store', store''), tt)
            e' ->
    PBStep4 (T4 (ASSIGN4 (V4 v1) (T4 t2)))
            (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt)
            e'
| PBSTEP4_ASSIGN_V loc v env store :
    PBStep4 (T4 (ASSIGN4 (V4 (LOC loc)) (V4 v)))
            (env, DNARROW, (TAU4, TAU4), nil, (store, map_update store loc v), tt)
            (V4 UNIT4)
| PBREFL4_V v l :
    unobs_label4 l ->
    PBStep4 (V4 v) l (V4 v)
| PBREFL4_ERR e v l :
    get_exc4 l = (ERR4 v, ERR4 v) ->
    unobs_label4 (replace_exc4 l (TAU4, TAU4)) ->
    PBStep4 e l e.

Proof that transitive closure corresponds to iteration relation.
Theorem trans4_v_sound :
  forall e l e',
    Trans4 e l e' ->
    is_val4 e' = true ->
    Eval4 e l e'.
Proof.
  induction 1; intro.
  - eapply EVAL4.
    + apply H.
    + inversion H0; subst; apply IHTrans4; apply H1.
  - destruct e; inversion H; apply REFL4_V.
    destruct a; destruct store; simpl; try split; reflexivity.
Qed.

Theorem trans4_e_sound :
  forall e l e',
    Trans4 e l e' ->
    is_abr_ter4 l = true ->
    Eval4 e l e'.
Proof.
  induction 1; intro.
  - eapply EVAL4.
    + apply H.
    + inversion H0; subst; apply IHTrans4;
      destruct a'; inversion H1; reflexivity.
  - destruct a; inversion H.
    eapply REFL4_ERR; reflexivity; apply I.
Qed.

Theorem trans4_v_complete :
  forall e l e',
    Eval4 e l e' ->
    is_val4 e' = true ->
    Trans4 e l e'.
Proof.
  induction 1; intro.
  - eapply TRANS4;
    [ apply H
    | apply IHEval4; apply H1 ].
  - destruct l; destruct p; destruct p; destruct p; destruct p; destruct u;
    destruct d; simpl in H; try inversion H;
    destruct e; destruct e; destruct e1; try inversion H;
    destruct o; try inversion H;
    destruct s; try inversion H; subst;
    apply REFL4.
  - destruct l; destruct p; destruct p; destruct p; destruct p; destruct u;
    destruct d; simpl in H0; try inversion H0;
    destruct e0; destruct e0; destruct e2; try inversion H0;
    destruct o; try inversion H0;
    destruct s; try inversion H0; subst; inversion H; subst;
    apply REFL4.
Qed.

Theorem trans4_e_complete :
  forall e l e',
    Eval4 e l e' ->
    is_abr_ter4 l = true ->
    Trans4 e l e'.
Proof.
  induction 1; intro.
  - eapply TRANS4.
    apply H.
    apply IHEval4.
    destruct a'; inversion H1.
    destruct a; reflexivity.
  - destruct l; destruct p; destruct p; destruct p; destruct p; destruct u;
    destruct d; simpl in H; try inversion H;
    destruct e; destruct e; destruct e1; try inversion H;
    destruct o; try inversion H;
    destruct s; try inversion H; subst;
    apply REFL4.
  - destruct l; destruct p; destruct p; destruct p; destruct p; destruct u;
    destruct d; simpl in H0; try inversion H0;
    destruct e0; destruct e0; destruct e2; try inversion H0;
    destruct o; try inversion H0;
    destruct s; try inversion H0; subst; inversion H; subst;
    apply REFL4.
Qed.

Transitivity of Trans4
Lemma trans4 :
  forall e1 e2 e3 env a a' out out' store store' store'',
    Trans4 e1 (env, DNARROW, (TAU4, a), out, (store, store'), tt) e2 ->
    Trans4 e2 (env, DNARROW, (a, a'), out', (store', store''), tt) e3 ->
    Trans4 e1 (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt) e3.
Proof.
  intros.
  dependent induction H.
  - rewrite <- app_assoc.
    eapply TRANS4.
    apply H.
    destruct a0.
    + eapply IHTrans4.
      reflexivity.
      apply H1.
    + inversion H0; subst.
      inversion H1; subst.
      apply REFL4.
  - apply H0.
Qed.

A single step constitutes an instance of a transitive step
Lemma single_trans4 :
  forall t1 e1' env a out store store',
    Step4 (T4 t1) (env, DNARROW, (TAU4, a), out, (store, store'), tt) e1' ->
    Trans4 (T4 t1) (env, DNARROW, (TAU4, a), out, (store, store'), tt) e1'.
Proof.
  intros.
  assert (H_app_nil : out = out ++ nil).
  symmetry; apply app_nil_r.
  rewrite H_app_nil.
  eapply TRANS4.
  apply H.
  apply REFL4.
Qed.

Congruence proofs
Lemma congruence4_app1 :
  forall t1 e2 e1' l,
    Trans4 (T4 t1) l e1' ->
    Trans4 (T4 (APP4 (T4 t1) e2)) l (T4 (APP4 e1' e2)).
Proof.
  induction 1.
  - eapply TRANS4;
    [ apply STEP4_APP1; apply H
    | apply IHTrans4 ].
  - apply REFL4.
Qed.

Lemma congruence4_app2 :
  forall t2 e2' v1 l,
    Trans4 (T4 t2) l e2' ->
    Trans4 (T4 (APP4 (V4 v1) (T4 t2))) l (T4 (APP4 (V4 v1) e2')).
Proof.
  induction 1.
  - eapply TRANS4;
    [ apply STEP4_APP2; apply H
    | apply IHTrans4 ].
  - apply REFL4.
Qed.

Lemma congruence4_app3 :
  forall x t e' rho v2 out store store' a',
    Trans4 (T4 t)
           (map_update rho x v2, DNARROW, (TAU4, a'),
            out, (store, store'), tt)
           e' ->
    forall env a'0 out0 store0 store'0,
      a'0 = a' ->
      out0 = out ->
      store0 = store ->
      store'0 = store' ->
      Trans4 (T4 (APP4 (V4 (CLO4 x (T4 t) rho)) (V4 v2)))
             (env, DNARROW, (TAU4, a'0),
              out0, (store0, store'0), tt)
             (T4 (APP4 (V4 (CLO4 x e' rho)) (V4 v2))).
Proof.
  intros x t e' rho v2 out store store' a' H.
  dependent induction H; intros; subst.
  - eapply TRANS4.
    + apply STEP4_APP3.
      apply H.
    + destruct e2.
      inversion H0; subst.
      apply REFL4.
      destruct a.
      eapply IHTrans4; try reflexivity.
      inversion H0; subst.
      apply REFL4.
  - apply REFL4.
Qed.

Lemma congruence4_if :
  forall t e' e1 e2 l,
    Trans4 (T4 t) l e' ->
    Trans4 (T4 (IF4 (T4 t) e1 e2)) l
           (T4 (IF4 e' e1 e2)).
Proof.
  induction 1.
  - eapply TRANS4;
    [ apply STEP4_IF; apply H
    | apply IHTrans4 ].
  - apply REFL4.
Qed.

Lemma congruence4_eq1 :
  forall t1 e1' e2 l,
    Trans4 (T4 t1) l e1' ->
    Trans4 (T4 (EQ4 (T4 t1) e2)) l (T4 (EQ4 e1' e2)).
Proof.
  induction 1.
  - eapply TRANS4;
    [ apply STEP4_EQ1; apply H
    | apply IHTrans4 ].
  - apply REFL4.
Qed.

Lemma congruence4_eq2 :
  forall v1 t2 e2' l,
    Trans4 (T4 t2) l e2' ->
    Trans4 (T4 (EQ4 (V4 v1) (T4 t2))) l (T4 (EQ4 (V4 v1) e2')).
Proof.
  induction 1.
  - eapply TRANS4;
    [ apply STEP4_EQ2; apply H
    | apply IHTrans4 ].
  - apply REFL4.
Qed.

Lemma congruence4_catch :
  forall t1 e1' e2 l a,
    Trans4 (T4 t1) l e1' ->
    get_exc4 l = (TAU4, a) ->
    forall l',
      l' = (replace_exc4 l (TAU4, TAU4)) ->
      Trans4 (T4 (CATCH4 TAU4 (T4 t1) e2))
             l'
             (T4 (CATCH4 a e1' e2)).
Proof.
  induction 1; intros; subst.
  - eapply TRANS4.
    eapply STEP4_CATCH.
    apply H.
    reflexivity.
    reflexivity.
    inversion H1; subst.
    destruct a0.
    + assert (H_app_nil : out' = out' ++ nil).
      symmetry; apply app_nil_r.
      rewrite H_app_nil.
      eapply IHTrans4.
      reflexivity.
      simpl.
      rewrite <- H_app_nil.
      reflexivity.
    + inversion H0; subst.
      apply REFL4.
  - inversion H; subst.
    apply REFL4.
Qed.

Lemma congruence4_print :
  forall t l e,
    Trans4 (T4 t) l e ->
    Trans4 (T4 (PRINT4 (T4 t))) l (T4 (PRINT4 e)).
Proof.
  induction 1.
  - eapply TRANS4;
    [ apply STEP4_PRINT ; apply H
    | apply IHTrans4 ].
  - apply REFL4.
Qed.

Lemma congruence4_ref :
  forall t l e,
    Trans4 (T4 t) l e ->
    Trans4 (T4 (REF4 (T4 t))) l (T4 (REF4 e)).
Proof.
  induction 1.
  - eapply TRANS4;
    [ apply STEP4_REF ; apply H
    | apply IHTrans4 ].
  - apply REFL4.
Qed.

Lemma congruence4_deref :
  forall t l e,
    Trans4 (T4 t) l e ->
    Trans4 (T4 (DEREF4 (T4 t))) l (T4 (DEREF4 e)).
Proof.
  induction 1.
  - eapply TRANS4;
    [ apply STEP4_DEREF ; apply H
    | apply IHTrans4 ].
  - apply REFL4.
Qed.

Lemma congruence4_assign1 :
  forall t1 l e1 e2,
    Trans4 (T4 t1) l e1 ->
    Trans4 (T4 (ASSIGN4 (T4 t1) e2)) l (T4 (ASSIGN4 e1 e2)).
Proof.
  induction 1.
  - eapply TRANS4;
    [ apply STEP4_ASSIGN1 ; apply H
    | apply IHTrans4 ].
  - apply REFL4.
Qed.

Lemma congruence4_assign2 :
  forall t2 l e2 v1,
    Trans4 (T4 t2) l e2 ->
    Trans4 (T4 (ASSIGN4 (V4 v1) (T4 t2))) l (T4 (ASSIGN4 (V4 v1) e2)).
Proof.
  induction 1.
  - eapply TRANS4;
    [ apply STEP4_ASSIGN2 ; apply H
    | apply IHTrans4 ].
  - apply REFL4.
Qed.

Ltac generalize_out_nil_r :=
  match goal with
    | [ |- Trans4 _ (_, _, _, ?out, _, _) _ ] =>
      assert (H_app_nil : out = out ++ nil);
        [symmetry; apply app_nil_r|];
        rewrite H_app_nil
    | [ |- PBStep4 _ (_, _, _, ?out, _, _) _ ] =>
      assert (H_app_nil : out = out ++ nil);
        [symmetry; apply app_nil_r|];
        rewrite H_app_nil
  end.

Ltac generalize_out_nil_l :=
  match goal with
    | [ |- Trans4 _ (_, _, _, ?out, _, _) _ ] =>
      assert (H_nil_app : out = nil ++ out);
        [reflexivity|];
        rewrite H_nil_app
    | [ |- PBStep4 _ (_, _, _, ?out, _, _) _ ] =>
      assert (H_nil_app : out = nil ++ out);
        [reflexivity|];
        rewrite H_nil_app
  end.

Ltac solve4_nil_r := try generalize_out_nil_r; try eapply TRANS4; try constructor; try apply I;
                     try reflexivity; try assumption.

Ltac solve4_nil_l := try generalize_out_nil_l; try eapply TRANS4; try constructor; try apply I;
                     try reflexivity; try assumption.

Theorem refocus_sound :
  forall e l e',
    PBStep4 e l e' ->
    Trans4 e l e'.
Proof.
  induction 1.
  - solve4_nil_r.
  - solve4_nil_r.
  - eapply trans4.
    apply congruence4_app1.
    apply IHPBStep4_1.
    apply IHPBStep4_2.
  - eapply trans4.
    apply congruence4_app2.
    apply IHPBStep4_1.
    apply IHPBStep4_2.
  - eapply trans4.
    eapply congruence4_app3; try reflexivity.
    apply IHPBStep4_1.
    apply IHPBStep4_2.
  - solve4_nil_r.
  - solve4_nil_r.
  - eapply trans4.
    apply congruence4_if.
    apply IHPBStep4_1.
    apply IHPBStep4_2.
  - solve4_nil_l.
    Focus 2.
    apply IHPBStep4.
    reflexivity.
  - solve4_nil_l.
    Focus 2.
    apply IHPBStep4.
    reflexivity.
  - eapply trans4.
    apply congruence4_eq1.
    apply IHPBStep4_1.
    apply IHPBStep4_2.
  - eapply trans4.
    apply congruence4_eq2.
    apply IHPBStep4_1.
    apply IHPBStep4_2.
  - solve4_nil_r.
  - generalize_out_nil_r.
    eapply TRANS4.
    apply STEP4_EQN.
    apply H.
    instantiate (1:=store).
    instantiate (1:=TAU4).
    reflexivity.
    apply REFL4.
  - solve4_nil_r.
  - solve4_nil_l.
    instantiate (1:=store).
    instantiate (1:=TAU4).
    reflexivity.
    apply IHPBStep4.
  - eapply trans4.
    eapply congruence4_catch.
    apply IHPBStep4_1.
    reflexivity.
    reflexivity.
    apply IHPBStep4_2.
  - eapply trans4.
    eapply congruence4_print.
    apply IHPBStep4_1.
    apply IHPBStep4_2.
  - solve4_nil_r.
  - eapply trans4.
    eapply congruence4_ref.
    apply IHPBStep4_1.
    apply IHPBStep4_2.
  - solve4_nil_r.
    eapply STEP4_REF_V.
    Focus 2.
    reflexivity.
    reflexivity.
    apply H.
  - eapply trans4.
    eapply congruence4_deref.
    apply IHPBStep4_1.
    apply IHPBStep4_2.
  - solve4_nil_r.
    eapply STEP4_DEREF_LOC.
    Focus 2.
    reflexivity.
    reflexivity.
    apply H.
  - eapply trans4.
    eapply congruence4_assign1.
    apply IHPBStep4_1.
    apply IHPBStep4_2.
  - eapply trans4.
    eapply congruence4_assign2.
    apply IHPBStep4_1.
    apply IHPBStep4_2.
  - solve4_nil_r.
    eapply STEP4_ASSIGN_V.
    Focus 2.
    reflexivity.
    reflexivity.
  - destruct l. destruct p. destruct p. destruct p. destruct p.
    destruct e. destruct u. destruct s.
    destruct d; destruct e; destruct e1; destruct o; destruct l; destruct l0; simpl in H;
    try inversion H; try inversion H0; try inversion H1;
    try apply REFL4.
  - destruct l. destruct p. destruct p. destruct p. destruct p.
    destruct e0. destruct u. destruct s.
    destruct d; destruct e; destruct e1; destruct o; destruct l; destruct l0; simpl in H;
    try inversion H; try inversion H0; try inversion H1;
    try apply REFL4.
Qed.

Completeness of refocusing

Helper lemma 1: a single step that terminates corresponds to a refocused step
Lemma single_abr_ter_refocus :
  forall t1 e' env v out store store',
    Step4 (T4 t1) (env, DNARROW, (TAU4, ERR4 v), out, (store, store'), tt) e' ->
    PBStep4 (T4 t1) (env, DNARROW, (TAU4, ERR4 v), out, (store, store'), tt) e'.
Proof.
  intros.
  dependent induction H;
    try (match goal with
           | [ H' : unobs_label4 _ |- _ ] =>
             simpl in H'; inversion H'
         end).
  - generalize_out_nil_r.
    eapply PBSTEP4_APP1.
    apply IHStep4.
    reflexivity.
    eapply PBREFL4_ERR.
    reflexivity.
    reflexivity.
  - generalize_out_nil_r.
    eapply PBSTEP4_APP2.
    apply IHStep4.
    reflexivity.
    eapply PBREFL4_ERR.
    reflexivity.
    reflexivity.
  - generalize_out_nil_r.
    eapply PBSTEP4_APP3.
    apply IHStep4.
    simpl.
    reflexivity.
    eapply PBREFL4_ERR.
    reflexivity.
    reflexivity.
  - destruct out; inversion H0.
    eapply PBSTEP4_THROW.
  - generalize_out_nil_r.
    eapply PBSTEP4_IF.
    apply IHStep4.
    reflexivity.
    eapply PBREFL4_ERR.
    reflexivity.
    reflexivity.
  - generalize_out_nil_r.
    eapply PBSTEP4_EQ1.
    apply IHStep4.
    reflexivity.
    eapply PBREFL4_ERR.
    reflexivity.
    reflexivity.
  - generalize_out_nil_r.
    eapply PBSTEP4_EQ2.
    apply IHStep4.
    reflexivity.
    eapply PBREFL4_ERR.
    reflexivity.
    reflexivity.
  - destruct l; destruct p; destruct p; destruct p; destruct p;
    destruct d; destruct u; inversion H1.
  - generalize_out_nil_r.
    eapply PBSTEP4_PRINT.
    apply IHStep4.
    reflexivity.
    eapply PBREFL4_ERR.
    reflexivity.
    reflexivity.
  - generalize_out_nil_r.
    eapply PBSTEP4_REF.
    apply IHStep4.
    reflexivity.
    eapply PBREFL4_ERR.
    reflexivity.
    reflexivity.
  - generalize_out_nil_r.
    eapply PBSTEP4_DEREF.
    apply IHStep4.
    reflexivity.
    eapply PBREFL4_ERR.
    reflexivity.
    reflexivity.
  - generalize_out_nil_r.
    eapply PBSTEP4_ASSIGN1.
    apply IHStep4.
    reflexivity.
    eapply PBREFL4_ERR.
    reflexivity.
    reflexivity.
  - generalize_out_nil_r.
    eapply PBSTEP4_ASSIGN2.
    apply IHStep4.
    reflexivity.
    eapply PBREFL4_ERR.
    reflexivity.
    reflexivity.
Qed.

Helper lemma 2: a refocused step can be broken into a small-step and a pretty-big-step
Lemma pb_step_prepend :
  forall t1 e2 env a out store store',
    Step4 (T4 t1)
          (env, DNARROW, (TAU4, a), out, (store, store'), tt)
          e2 ->
    forall e3 a' out' store'',
      PBStep4 e2
              (env, DNARROW, (a, a'), out', (store', store''), tt)
              e3 ->
      PBStep4 (T4 t1)
              (env, DNARROW, (TAU4, a'), out ++ out', (store, store''), tt)
              e3.
Proof.
  intros t1 e2 env a out store store' H e3 a' out' store''.
  generalize_eqs H.
  intro; subst.
  generalize dependent store''.
  generalize dependent out'.
  generalize dependent a'.
  generalize dependent e3.
  generalize dependent store'.
  generalize dependent store.
  generalize dependent env.
  induction H; intros.
  - dependent destruction H1; destruct a; destruct out; simpl in H; inversion H.
    inversion H2; subst; destruct a'; destruct out'; simpl in H4; inversion H4; try inversion H3;
    apply PBSTEP4_VAR;
    apply H0.
  - dependent destruction H0; destruct a; destruct out; simpl in H; inversion H.
    inversion H1; subst; destruct a'; destruct out'; simpl in H3; inversion H3; try inversion H2.
    apply PBSTEP4_ABS.
  - dependent destruction H0;
    inversion H1; subst.
    + rewrite app_assoc.
      eapply PBSTEP4_APP1.
      eapply IHStep4.
      reflexivity.
      apply H10.
      apply H11.
    + eapply PBSTEP4_APP1.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      apply PBREFL4_V.
      instantiate (1:=store').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + eapply PBSTEP4_APP1.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      apply PBREFL4_V.
      instantiate (1:=store').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + eapply PBSTEP4_APP1.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      apply PBREFL4_V.
      instantiate (1:=store'').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + inversion H0; subst.
      eapply PBSTEP4_APP1.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      inversion H1.
      simpl in H4.
      destruct out'; inversion H4.
      reflexivity.
  - dependent destruction H0;
    inversion H1; subst.
    + rewrite app_assoc.
      eapply PBSTEP4_APP2.
      eapply IHStep4.
      reflexivity.
      apply H10.
      apply H11.
    + eapply PBSTEP4_APP2.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      instantiate (2:=store').
      instantiate (2:=TAU4).
      apply PBREFL4_V.
      reflexivity.
      apply H1.
    + eapply PBSTEP4_APP2.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      instantiate (2:=store'').
      instantiate (2:=TAU4).
      apply PBREFL4_V.
      reflexivity.
      apply H1.
    + inversion H0; subst.
      eapply PBSTEP4_APP2.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      inversion H1.
      destruct out'; inversion H4.
      reflexivity.
  - dependent destruction H0;
    inversion H1; subst.
    + rewrite app_assoc.
      eapply PBSTEP4_APP3.
      eapply IHStep4.
      reflexivity.
      apply H12.
      apply H13.
    + eapply PBSTEP4_APP3.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      apply PBREFL4_V.
      instantiate (1:=store'').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + inversion H0; subst.
      eapply PBSTEP4_APP3.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      reflexivity.
      apply H1.
  - dependent destruction H0; destruct a; destruct out; simpl in H; inversion H.
    inversion H1; subst; destruct a'; destruct out'; simpl in H3; inversion H3; try inversion H2.
    apply PBSTEP4_APP4.
  - dependent destruction H1;
    inversion H2; subst; destruct a'; destruct out'; simpl in H1; inversion H1; subst;
    destruct out; inversion H0; subst;
    try inversion H;
    apply PBSTEP4_THROW.
  - dependent destruction H0;
    inversion H1; subst.
    + rewrite app_assoc.
      eapply PBSTEP4_IF.
      eapply IHStep4.
      reflexivity.
      apply H11.
      apply H12.
    + eapply PBSTEP4_IF.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_V.
      instantiate (1:=store').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + eapply PBSTEP4_IF.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_V.
      instantiate (1:=store').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + inversion H0; subst.
      generalize_out_nil_r.
      eapply PBSTEP4_IF.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      inversion H1.
      destruct out'; inversion H4.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      inversion H1.
      destruct out'; inversion H4.
      reflexivity.
  - dependent destruction H0; destruct a; destruct out; simpl in H; inversion H.
    destruct a'; eapply PBSTEP4_IFTRUE; apply H1.
  - dependent destruction H0; destruct a; destruct out; simpl in H; inversion H.
    destruct a'; eapply PBSTEP4_IFFALSE; apply H1.
  - dependent destruction H0;
    inversion H1; subst.
    + rewrite app_assoc.
      eapply PBSTEP4_EQ1.
      eapply IHStep4.
      reflexivity.
      apply H10.
      apply H11.
    + eapply PBSTEP4_EQ1.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_V.
      instantiate (1:=store').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + eapply PBSTEP4_EQ1.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_V.
      instantiate (1:=store'').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + eapply PBSTEP4_EQ1.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_V.
      instantiate (1:=store'').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + inversion H0; subst.
      generalize_out_nil_r.
      eapply PBSTEP4_EQ1.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      inversion H1.
      destruct out'; inversion H4.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      inversion H1.
      destruct out'; inversion H4.
      reflexivity.
  - dependent destruction H0;
    inversion H1; subst.
    + rewrite app_assoc.
      eapply PBSTEP4_EQ2.
      eapply IHStep4.
      reflexivity.
      apply H10.
      apply H11.
    + eapply PBSTEP4_EQ2.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_V.
      instantiate (1:=store'').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + eapply PBSTEP4_EQ2.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_V.
      instantiate (1:=store'').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + inversion H0; subst.
      eapply PBSTEP4_EQ2.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      inversion H1.
      destruct out'; inversion H4; reflexivity.
  - dependent destruction H1; destruct a; destruct out; simpl in H0; inversion H0.
    inversion H2; subst; destruct a'; destruct out'; simpl in H3; inversion H3; try inversion H1.
    apply PBSTEP4_EQ; reflexivity.
  - dependent destruction H1; destruct a; destruct out; simpl in H0; inversion H0.
    inversion H2; subst; destruct a'; destruct out'; simpl in H4; inversion H4; try inversion H3.
    apply PBSTEP4_EQN. apply H.
  - dependent destruction H0; destruct a; destruct out; simpl in H; inversion H.
    inversion H1; subst; destruct a'; destruct out'; simpl in H3; inversion H3; try inversion H2.
    apply PBSTEP4_CATCH_V.
  - dependent destruction H0; destruct a; destruct out; simpl in H; inversion H.
    apply PBSTEP4_CATCH_ERR.
    apply H1.
  - inversion H3; subst;
    destruct l; destruct p; destruct p; destruct p; destruct p;
    destruct u; destruct s; destruct e; destruct d; dependent destruction H2.
    + eapply PBSTEP4_CATCH.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      apply PBREFL4_V.
      instantiate (1:=store'').
      instantiate (1:=TAU4).
      reflexivity.
      apply PBSTEP4_CATCH_V.
    + eapply single_abr_ter_refocus in H.
      eapply PBSTEP4_CATCH.
      apply H.
      eapply PBSTEP4_CATCH_ERR.
      apply H14.
    + rewrite app_assoc.
      eapply PBSTEP4_CATCH.
      eapply IHStep4.
      reflexivity.
      apply H14.
      apply H15.
  - dependent destruction H0;
    inversion H1; subst.
    + rewrite app_assoc.
      eapply PBSTEP4_PRINT.
      eapply IHStep4.
      reflexivity.
      apply H9.
      apply H10.
    + eapply PBSTEP4_PRINT.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      apply PBREFL4_V.
      instantiate (1:=store'').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + eapply PBSTEP4_PRINT.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      destruct H_app_nil.
      inversion H0; subst.
      eapply PBREFL4_ERR.
      reflexivity.
      instantiate (1:=store').
      reflexivity.
      inversion H0; subst.
      eapply PBREFL4_ERR.
      reflexivity.
      inversion H1.
      destruct out'; inversion H4.
      reflexivity.
  - dependent destruction H1;
    destruct a; destruct out; inversion H; inversion H0; subst.
    inversion H2; subst;
    destruct a'; destruct out'; inversion H3; try inversion H1.
    eapply PBSTEP4_PRINT_V.
  - dependent destruction H0;
    inversion H1; subst.
    + rewrite app_assoc.
      eapply PBSTEP4_REF.
      eapply IHStep4.
      reflexivity.
      apply H9.
      apply H10.
    + eapply PBSTEP4_REF.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      apply PBREFL4_V.
      instantiate (1:=store').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + eapply PBSTEP4_REF.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      destruct H_app_nil.
      inversion H0; subst.
      eapply PBREFL4_ERR.
      reflexivity.
      instantiate (1:=store').
      reflexivity.
      inversion H0; subst.
      eapply PBREFL4_ERR.
      reflexivity.
      inversion H1.
      destruct out'; inversion H4.
      reflexivity.
  - dependent destruction H2;
    destruct a; destruct out; inversion H; inversion H0; subst.
    destruct a'; destruct out'; inversion H3; subst; try inversion H2;
    try inversion H4.
    simpl in H4; subst.
    eapply PBSTEP4_REF_V.
    reflexivity.
  - dependent destruction H0;
    inversion H1; subst.
    + rewrite app_assoc.
      eapply PBSTEP4_DEREF.
      eapply IHStep4.
      reflexivity.
      apply H9.
      apply H10.
    + eapply PBSTEP4_DEREF.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      apply PBREFL4_V.
      instantiate (1:=store'').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + eapply PBSTEP4_DEREF.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      destruct H_app_nil.
      inversion H0; subst.
      eapply PBREFL4_ERR.
      reflexivity.
      instantiate (1:=store').
      reflexivity.
      inversion H0; subst.
      eapply PBREFL4_ERR.
      reflexivity.
      inversion H1.
      destruct out'; inversion H4.
      reflexivity.
  - dependent destruction H2;
    destruct a; destruct out; inversion H; inversion H0; subst.
    inversion H3; subst;
    destruct a'; destruct out'; inversion H5; try inversion H4.
    eapply PBSTEP4_DEREF_LOC.
    subst.
    apply H1.
  - dependent destruction H0;
    inversion H1; subst.
    + rewrite app_assoc.
      eapply PBSTEP4_ASSIGN1.
      eapply IHStep4.
      reflexivity.
      apply H10.
      apply H11.
    + eapply PBSTEP4_ASSIGN1.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      apply PBREFL4_V.
      instantiate (1:=store').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + eapply PBSTEP4_ASSIGN1.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      apply PBREFL4_V.
      instantiate (1:=store').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + inversion H0; subst.
      eapply PBSTEP4_ASSIGN1.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      destruct out'; inversion H2.
      reflexivity.
  - dependent destruction H0;
    inversion H1; subst.
    + rewrite app_assoc.
      eapply PBSTEP4_ASSIGN2.
      eapply IHStep4.
      reflexivity.
      apply H10.
      apply H11.
    + eapply PBSTEP4_ASSIGN2.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      apply PBREFL4_V.
      instantiate (1:=store').
      instantiate (1:=TAU4).
      reflexivity.
      apply H1.
    + inversion H0; subst.
      eapply PBSTEP4_ASSIGN2.
      generalize_out_nil_r.
      eapply IHStep4.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      reflexivity.
      eapply PBREFL4_ERR.
      reflexivity.
      destruct out'; inversion H2.
      reflexivity.
  - dependent destruction H1;
    destruct a; destruct out; inversion H; inversion H0; subst.
    inversion H2; subst;
    destruct a'; destruct out'; inversion H4; try inversion H3.
    eapply PBSTEP4_ASSIGN_V.
Qed.

Theorem refocus_complete :
  forall e l e',
    Trans4 e l e' ->
    (is_val4 e' = true \/ is_abr_ter4 l = true) ->
    PBStep4 e l e'.
Proof.
  induction 1; intros.
  - eapply pb_step_prepend.
    apply H.
    apply IHTrans4.
    inversion H1.
    left.
    apply H2.
    destruct a'; inversion H2.
    right; destruct a; reflexivity.
  - inversion H.
    + destruct e; inversion H0.
      apply PBREFL4_V.
      destruct a.
      reflexivity.
      simpl; split; reflexivity.
    + destruct a; inversion H0.
      eapply PBREFL4_ERR.
      reflexivity.
      simpl; split; reflexivity.
Qed.