Library sect_3_2_small_step_lambda_refocus

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 Expr2 :=
| V2 : Val2 -> Expr2
| T2 : Trm2 -> Expr2
with Val2 :=
| NAT2 : nat -> Val2
| CLO2 : Identifier ->
          Expr2 ->
          list (Identifier * Val2) ->
          Val2
| UNIT2 : Val2
| TRUE : Val2
| FALSE : Val2
| VEXC : Exception2 ->
          Val2
with Trm2 :=
| VAR2 : Identifier ->
           Trm2
| APP2 : Expr2 ->
           Expr2 ->
           Trm2
| ABS2 : Identifier ->
           Expr2 ->
           Trm2
| THROW2 : Val2 ->
           Trm2
| IF2 : Expr2 ->
           Expr2 ->
           Expr2 ->
           Trm2
| EQ2 : Expr2 ->
           Expr2 ->
           Trm2
| CATCH2 : Expr2 ->
           Expr2 ->
           Trm2
with Exception2 :=
| TAU2 : Exception2
| ERR2 : Val2 -> Exception2.

Definition is_val2 (v : Expr2) :=
  match v with
    | (V2 _) => true
    | _ => false
  end.

Auxiliary entities

Environments
Definition Env2 := list (Identifier * Val2).

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.

Exc2 read-write label component
Definition Exc2 := (Exception2 * Exception2)%type.

Full label
Definition Label2 := (Env2 * Div * Exc2 * unit)%type.

Definition get_env2 (l : Label2) : Env2 :=
  match l with
    | (rho, _, _, _) => rho
  end.

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

Definition get_exc2 (l : Label2) : Exc2 :=
  match l with
    | (_, _, exc, _) => exc
  end.

Definition replace_env2 (l : Label2) (rho : Env2) : Label2 :=
  match l with
    | (rho', div, exc, tail) => (rho, div, exc, tail)
  end.

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

Definition replace_exc2 (l : Label2) (exc : Exc2) : Label2 :=
  match l with
    | (rho, div, exc', tail) => (rho, div, exc, tail)
  end.

Definition unobs_label2 (l : Label2) : Prop :=
  match l with
    | (_, DNARROW, (TAU2, TAU2), _) =>
      True
    | (_, DNARROW, (ERR2 v, ERR2 v'), _) =>
      v = v'
    | (_, _, _, _) => False
  end.

Definition is_abr_ter2 (l : Label2) :=
  match l with
    | (_, _, (_, ERR2 _), _) => true
    | (_, _, (ERR2 _, _), _) => true
    | _ => false
  end.

Small-step rules

Auxiliary helper predicate for extracting the value from an error entity.
Definition unwrap_err2 (err : Exception2) : Val2 :=
  match err with
    | ERR2 v => v
    | _ => UNIT2
  end.

Added STEP2_ M7 rule
Inductive Step2 : Expr2 -> Label2 -> Expr2 -> Prop :=
| STEP2_VAR x l v :
    unobs_label2 l ->
    map_lookup (get_env2 l) x = Some v ->
    Step2 (T2 (VAR2 x)) l (V2 v)
| STEP2_ABS x t l :
    unobs_label2 l ->
    Step2 (T2 (ABS2 x t)) l (V2 (CLO2 x t (get_env2 l)))
| STEP2_APP1 t1 e2 e1' l :
    Step2 (T2 t1) l e1' ->
    Step2 (T2 (APP2 (T2 t1) e2)) l (T2 (APP2 e1' e2))
| STEP2_APP2 v1 t2 l e2' :
    Step2 (T2 t2) l e2' ->
    Step2 (T2 (APP2 (V2 v1) (T2 t2))) l (T2 (APP2 (V2 v1) e2'))
| STEP2_APP3 x t e' rho v2 l :
    Step2 (T2 t) (replace_env2 l (map_update rho x v2)) e' ->
    Step2 (T2 (APP2 (V2 (CLO2 x (T2 t) rho)) (V2 v2)))
          l
          (T2 (APP2 (V2 (CLO2 x e' rho)) (V2 v2)))
| STEP2_APP4 x v rho v2 l :
    unobs_label2 l ->
    Step2 (T2 (APP2 (V2 (CLO2 x (V2 v) rho)) (V2 v2))) l (V2 v)
| STEP2_THROW v l :
    get_exc2 l = (TAU2, ERR2 v) ->
    unobs_label2 (replace_exc2 l (TAU2, TAU2)) ->
    Step2 (T2 (THROW2 v)) l (V2 UNIT2)
| STEP2_IF t e' e1 e2 l :
    Step2 (T2 t) l e' ->
    Step2 (T2 (IF2 (T2 t) e1 e2)) l
          (T2 (IF2 e' e1 e2))
| STEP2_IFTRUE e1 e2 l :
    unobs_label2 l ->
    Step2 (T2 (IF2 (V2 TRUE) e1 e2)) l e1
| STEP2_IFFALSE e1 e2 l :
    unobs_label2 l ->
    Step2 (T2 (IF2 (V2 FALSE) e1 e2)) l e2
| STEP2_EQ1 t1 e1' e2 l :
    Step2 (T2 t1) l e1' ->
    Step2 (T2 (EQ2 (T2 t1) e2)) l (T2 (EQ2 e1' e2))
| STEP2_EQ2 v1 t2 e2' l :
    Step2 (T2 t2) l e2' ->
    Step2 (T2 (EQ2 (V2 v1) (T2 t2))) l (T2 (EQ2 (V2 v1) e2'))
| STEP2_EQ v1 v2 l :
    v1 = v2 ->
    unobs_label2 l ->
    Step2 (T2 (EQ2 (V2 v1) (V2 v2))) l (V2 TRUE)
| STEP2_EQN v1 v2 l :
    v1 <> v2 ->
    unobs_label2 l ->
    Step2 (T2 (EQ2 (V2 v1) (V2 v2))) l (V2 FALSE)
| STEP2_CATCH_V v1 e2 l :
    unobs_label2 l ->
    Step2 (T2 (CATCH2 (V2 v1) e2)) l (V2 v1)
| STEP2_CATCH t1 e1' e2 l l' a :
    Step2 (T2 t1) l e1' ->
    get_exc2 l = (TAU2, a) ->
    l' = (replace_exc2 l (TAU2, TAU2)) ->
    Step2 (T2 (CATCH2 (T2 t1) e2))
          l'
          (T2 (IF2 (T2 (EQ2 (V2 (VEXC a)) (V2 (VEXC TAU2))))
                   (T2 (CATCH2 e1' e2))
                   (T2 (APP2 e2 (V2 (unwrap_err2 a)))))).

Inductive Eval2 : Expr2 -> Label2 -> Expr2 -> Prop :=
| EVAL2 t1 e2 e3 env a a' :
    Step2 (T2 t1) (env, DNARROW, (TAU2, a), tt) e2 ->
    Eval2 e2 (env, DNARROW, (a, a'), tt) e3 ->
    Eval2 (T2 t1) (env, DNARROW, (TAU2, a'), tt) e3
| REFL2_V v l :
    unobs_label2 l ->
    Eval2 (V2 v) l (V2 v)
| REFL2_ERR e v l :
    get_exc2 l = (ERR2 v, ERR2 v) ->
    unobs_label2 (replace_exc2 l (TAU2, TAU2)) ->
    Eval2 e l e.

Refocusing

We refocus by:
1. introducing a refocusing rule; 2. specializing congruence rules; and 3. specializing evaluation rules.

1. Introduce refocusing rule

Introducing the REFOCUS rule
Inductive R1Step2 : Expr2 -> Label2 -> Expr2 -> Prop :=
| R1REFOCUS t1 e1' l :
    R1Eval2 (T2 t1) l e1' ->
    R1Step2 (T2 t1) l e1'
| R1STEP2_VAR x l v :
    unobs_label2 l ->
    map_lookup (get_env2 l) x = Some v ->
    R1Step2 (T2 (VAR2 x)) l (V2 v)
| R1STEP2_ABS x t l :
    unobs_label2 l ->
    R1Step2 (T2 (ABS2 x t)) l (V2 (CLO2 x t (get_env2 l)))
| R1STEP2_APP1 t1 e2 e1' l :
    R1Step2 (T2 t1) l e1' ->
    R1Step2 (T2 (APP2 (T2 t1) e2)) l (T2 (APP2 e1' e2))
| R1STEP2_APP2 v1 t2 l e2' :
    R1Step2 (T2 t2) l e2' ->
    R1Step2 (T2 (APP2 (V2 v1) (T2 t2))) l (T2 (APP2 (V2 v1) e2'))
| R1STEP2_APP3 x t e' rho v2 l :
    R1Step2 (T2 t) (replace_env2 l (map_update rho x v2)) e' ->
    R1Step2 (T2 (APP2 (V2 (CLO2 x (T2 t) rho)) (V2 v2)))
            l
            (T2 (APP2 (V2 (CLO2 x e' rho)) (V2 v2)))
| R1STEP2_APP4 x v rho v2 l :
    unobs_label2 l ->
    R1Step2 (T2 (APP2 (V2 (CLO2 x (V2 v) rho)) (V2 v2))) l (V2 v)
| R1STEP2_THROW v l :
    get_exc2 l = (TAU2, ERR2 v) ->
    unobs_label2 (replace_exc2 l (TAU2, TAU2)) ->
    R1Step2 (T2 (THROW2 v)) l (V2 UNIT2)
| R1STEP2_IF t e' e1 e2 l :
    R1Step2 (T2 t) l e' ->
    R1Step2 (T2 (IF2 (T2 t) e1 e2)) l
            (T2 (IF2 e' e1 e2))
| R1STEP2_IFTRUE e1 e2 l :
    unobs_label2 l ->
    R1Step2 (T2 (IF2 (V2 TRUE) e1 e2)) l e1
| R1STEP2_IFFALSE e1 e2 l :
    unobs_label2 l ->
    R1Step2 (T2 (IF2 (V2 FALSE) e1 e2)) l e2
| R1STEP2_EQ1 t1 e1' e2 l :
    R1Step2 (T2 t1) l e1' ->
    R1Step2 (T2 (EQ2 (T2 t1) e2)) l (T2 (EQ2 e1' e2))
| R1STEP2_EQ2 v1 t2 e2' l :
    R1Step2 (T2 t2) l e2' ->
    R1Step2 (T2 (EQ2 (V2 v1) (T2 t2))) l (T2 (EQ2 (V2 v1) e2'))
| R1STEP2_EQ v1 v2 l :
    v1 = v2 ->
    unobs_label2 l ->
    R1Step2 (T2 (EQ2 (V2 v1) (V2 v2))) l (V2 TRUE)
| R1STEP2_EQN v1 v2 l :
    v1 <> v2 ->
    unobs_label2 l ->
    R1Step2 (T2 (EQ2 (V2 v1) (V2 v2))) l (V2 FALSE)
| R1STEP2_CATCH_V v1 e2 l :
    unobs_label2 l ->
    R1Step2 (T2 (CATCH2 (V2 v1) e2)) l (V2 v1)
| R1STEP2_CATCH t1 e1' e2 l a l' :
    R1Step2 (T2 t1) l e1' ->
    get_exc2 l = (TAU2, a) ->
    l' = (replace_exc2 l (TAU2, TAU2)) ->
    R1Step2 (T2 (CATCH2 (T2 t1) e2))
            l'
            (T2 (IF2 (T2 (EQ2 (V2 (VEXC a)) (V2 (VEXC TAU2))))
                     (T2 (CATCH2 e1' e2))
                     (T2 (APP2 e2 (V2 (unwrap_err2 a))))))
with R1Eval2 : Expr2 -> Label2 -> Expr2 -> Prop :=
| R1EVAL2 t1 e2 e3 env a a' :
    R1Step2 (T2 t1) (env, DNARROW, (TAU2, a), tt) e2 ->
    R1Eval2 e2 (env, DNARROW, (a, a'), tt) e3 ->
    R1Eval2 (T2 t1) (env, DNARROW, (TAU2, a'), tt) e3
| R1REFL2_V v l :
    unobs_label2 l ->
    R1Eval2 (V2 v) l (V2 v)
| R1REFL2_ERR e v l :
    get_exc2 l = (ERR2 v, ERR2 v) ->
    unobs_label2 (replace_exc2 l (TAU2, TAU2)) ->
    R1Eval2 e l e.

The resulting relation allows big-steps that fully reduces terms to occur anywhere a small-step could occur. However, the definition is mutually inductive, and we are interested in obtaining a semantics which always reduces terms as far as possible. Motivated by this end, we specialize all congruence rules.

2. Specialize congruence rules

All rules [R] of the form 
           t1 --> e1'
-------------------------------- [R]
F(...,t1,...) --> F(...,e1',...)
are ufolded 
           t1 -->* e1'
          ------------ [REFOCUS]
           t1 --> e1'
-------------------------------- [R]
F(...,t1,...) --> F(...,e1',...)
into 
           t1 -->* e1'
-------------------------------- [R-REFOCUS]
F(...,t1,...) --> F(...,e1',...)

Inductive R2Step2 : Expr2 -> Label2 -> Expr2 -> Prop :=
| R2STEP2_VAR x l v :
    unobs_label2 l ->
    map_lookup (get_env2 l) x = Some v ->
    R2Step2 (T2 (VAR2 x)) l (V2 v)
| R2STEP2_ABS x t l :
    unobs_label2 l ->
    R2Step2 (T2 (ABS2 x t)) l (V2 (CLO2 x t (get_env2 l)))
| R2STEP2_APP1 t1 e2 e1' l :
    R2Eval2 (T2 t1) l e1' ->
    R2Step2 (T2 (APP2 (T2 t1) e2)) l (T2 (APP2 e1' e2))
| R2STEP2_APP2 v1 t2 l e2' :
    R2Eval2 (T2 t2) l e2' ->
    R2Step2 (T2 (APP2 (V2 v1) (T2 t2))) l (T2 (APP2 (V2 v1) e2'))
| R2STEP2_APP3 x t e' rho v2 l :
    R2Eval2 (T2 t) (replace_env2 l (map_update rho x v2)) e' ->
    R2Step2 (T2 (APP2 (V2 (CLO2 x (T2 t) rho)) (V2 v2)))
            l
            (T2 (APP2 (V2 (CLO2 x e' rho)) (V2 v2)))
| R2STEP2_APP4 x v rho v2 l :
    unobs_label2 l ->
    R2Step2 (T2 (APP2 (V2 (CLO2 x (V2 v) rho)) (V2 v2))) l (V2 v)
| R2STEP2_THROW v l :
    get_exc2 l = (TAU2, ERR2 v) ->
    unobs_label2 (replace_exc2 l (TAU2, TAU2)) ->
    R2Step2 (T2 (THROW2 v)) l (V2 UNIT2)
| R2STEP2_IF t e' e1 e2 l :
    R2Eval2 (T2 t) l e' ->
    R2Step2 (T2 (IF2 (T2 t) e1 e2)) l
            (T2 (IF2 e' e1 e2))
| R2STEP2_IFTRUE e1 e2 l :
    unobs_label2 l ->
    R2Step2 (T2 (IF2 (V2 TRUE) e1 e2)) l e1
| R2STEP2_IFFALSE e1 e2 l :
    unobs_label2 l ->
    R2Step2 (T2 (IF2 (V2 FALSE) e1 e2)) l e2
| R2STEP2_EQ1 t1 e1' e2 l :
    R2Eval2 (T2 t1) l e1' ->
    R2Step2 (T2 (EQ2 (T2 t1) e2)) l (T2 (EQ2 e1' e2))
| R2STEP2_EQ2 v1 t2 e2' l :
    R2Eval2 (T2 t2) l e2' ->
    R2Step2 (T2 (EQ2 (V2 v1) (T2 t2))) l (T2 (EQ2 (V2 v1) e2'))
| R2STEP2_EQ v1 v2 l :
    v1 = v2 ->
    unobs_label2 l ->
    R2Step2 (T2 (EQ2 (V2 v1) (V2 v2))) l (V2 TRUE)
| R2STEP2_EQN v1 v2 l :
    v1 <> v2 ->
    unobs_label2 l ->
    R2Step2 (T2 (EQ2 (V2 v1) (V2 v2))) l (V2 FALSE)
| R2STEP2_CATCH_V v1 e2 l :
    unobs_label2 l ->
    R2Step2 (T2 (CATCH2 (V2 v1) e2)) l (V2 v1)
| R2STEP2_CATCH t1 e1' e2 l a l' :
    R2Eval2 (T2 t1) l e1' ->
    get_exc2 l = (TAU2, a) ->
    l' = (replace_exc2 l (TAU2, TAU2)) ->
    R2Step2 (T2 (CATCH2 (T2 t1) e2))
            l'
            (T2 (IF2 (T2 (EQ2 (V2 (VEXC a)) (V2 (VEXC TAU2))))
                     (T2 (CATCH2 e1' e2))
                     (T2 (APP2 e2 (V2 (unwrap_err2 a))))))
with R2Eval2 : Expr2 -> Label2 -> Expr2 -> Prop :=
| R2EVAL2 t1 e2 e3 env a a' :
    R2Step2 (T2 t1) (env, DNARROW, (TAU2, a), tt) e2 ->
    R2Eval2 e2 (env, DNARROW, (a, a'), tt) e3 ->
    R2Eval2 (T2 t1) (env, DNARROW, (TAU2, a'), tt) e3
| R2REFL2_V v l :
    unobs_label2 l ->
    R2Eval2 (V2 v) l (V2 v)
| R2REFL2_ERR e v l :
    get_exc2 l = (ERR2 v, ERR2 v) ->
    unobs_label2 (replace_exc2 l (TAU2, TAU2)) ->
    R2Eval2 e l e.

The resulting semantics fully reduces sub-terms whenever a congruence rule is applied. However, R2Step2 and R2Eval2 remain mutually inductive. We unfold the R2EVAL2 rule to eliminate the mutual dependency.

Step 3. Specialize evaluation rules

For each rule [R-REFOCUS] we unfold the evaluation rule: 
 e --> e'    e' -->* e''
 ----------------------- [EVAL]
       e -->* e''

           t1 -->* e1'
 -------------------------------- [R-REFOCUS]
 F(...,t1,...) --> F(...,e1',...)              F(...,e1',...) -->* e''
 --------------------------------------------------------------------- [EVAL]
           F(...,t1,...) --> e''
which gives the pretty-big-step rule: 


 t1 -->* e1'    F(...,e1',...) -->* e''
 -------------------------------------- [R-PBS]
        F(...,t1,...) --> e''

Inductive R3Step2 : Expr2 -> Label2 -> Expr2 -> Prop :=
| R3STEP2_VAR x l v :
    unobs_label2 l ->
    map_lookup (get_env2 l) x = Some v ->
    R3Step2 (T2 (VAR2 x)) l (V2 v)
| R3STEP2_ABS x t l :
    unobs_label2 l ->
    R3Step2 (T2 (ABS2 x t)) l (V2 (CLO2 x t (get_env2 l)))
| R3STEP2_APP1 t1 e2 e1' l :
    R3Eval2 (T2 t1) l e1' ->
    R3Step2 (T2 (APP2 (T2 t1) e2)) l (T2 (APP2 e1' e2))
| R3STEP2_APP2 v1 t2 l e2' :
    R3Eval2 (T2 t2) l e2' ->
    R3Step2 (T2 (APP2 (V2 v1) (T2 t2))) l (T2 (APP2 (V2 v1) e2'))
| R3STEP2_APP3 x t e' rho v2 l :
    R3Eval2 (T2 t) (replace_env2 l (map_update rho x v2)) e' ->
    R3Step2 (T2 (APP2 (V2 (CLO2 x (T2 t) rho)) (V2 v2)))
            l
            (T2 (APP2 (V2 (CLO2 x e' rho)) (V2 v2)))
| R3STEP2_APP4 x v rho v2 l :
    unobs_label2 l ->
    R3Step2 (T2 (APP2 (V2 (CLO2 x (V2 v) rho)) (V2 v2))) l (V2 v)
| R3STEP2_THROW v l :
    get_exc2 l = (TAU2, ERR2 v) ->
    unobs_label2 (replace_exc2 l (TAU2, TAU2)) ->
    R3Step2 (T2 (THROW2 v)) l (V2 UNIT2)
| R3STEP2_IF t e' e1 e2 l :
    R3Eval2 (T2 t) l e' ->
    R3Step2 (T2 (IF2 (T2 t) e1 e2)) l
            (T2 (IF2 e' e1 e2))
| R3STEP2_IFTRUE e1 e2 l :
    unobs_label2 l ->
    R3Step2 (T2 (IF2 (V2 TRUE) e1 e2)) l e1
| R3STEP2_IFFALSE e1 e2 l :
    unobs_label2 l ->
    R3Step2 (T2 (IF2 (V2 FALSE) e1 e2)) l e2
| R3STEP2_EQ1 t1 e1' e2 l :
    R3Eval2 (T2 t1) l e1' ->
    R3Step2 (T2 (EQ2 (T2 t1) e2)) l (T2 (EQ2 e1' e2))
| R3STEP2_EQ2 v1 t2 e2' l :
    R3Eval2 (T2 t2) l e2' ->
    R3Step2 (T2 (EQ2 (V2 v1) (T2 t2))) l (T2 (EQ2 (V2 v1) e2'))
| R3STEP2_EQ v1 v2 l :
    v1 = v2 ->
    unobs_label2 l ->
    R3Step2 (T2 (EQ2 (V2 v1) (V2 v2))) l (V2 TRUE)
| R3STEP2_EQN v1 v2 l :
    v1 <> v2 ->
    unobs_label2 l ->
    R3Step2 (T2 (EQ2 (V2 v1) (V2 v2))) l (V2 FALSE)
| R3STEP2_CATCH_V v1 e2 l :
    unobs_label2 l ->
    R3Step2 (T2 (CATCH2 (V2 v1) e2)) l (V2 v1)
| R3STEP2_CATCH t1 e1' e2 l a l' :
    R3Eval2 (T2 t1) l e1' ->
    get_exc2 l = (TAU2, a) ->
    l' = (replace_exc2 l (TAU2, TAU2)) ->
    R3Step2 (T2 (CATCH2 (T2 t1) e2))
            l'
            (T2 (IF2 (T2 (EQ2 (V2 (VEXC a)) (V2 (VEXC TAU2))))
                     (T2 (CATCH2 e1' e2))
                     (T2 (APP2 e2 (V2 (unwrap_err2 a))))))
with R3Eval2 : Expr2 -> Label2 -> Expr2 -> Prop :=
| R3EVAL2_VAR x env v :
    map_lookup env x = Some v ->
    R3Eval2 (T2 (VAR2 x)) (env, DNARROW, (TAU2, TAU2), tt) (V2 v)
| R3EVAL2_ABS x t env :
    R3Eval2 (T2 (ABS2 x t))
            (env, DNARROW, (TAU2, TAU2), tt)
            (V2 (CLO2 x t env))
| R3EVAL2_APP1 t1 env a a' e1' e2 e3 :
    R3Eval2 (T2 t1) (env, DNARROW, (TAU2, a), tt) e1' ->
    R3Eval2 (T2 (APP2 e1' e2)) (env, DNARROW, (a, a'), tt) e3 ->
    R3Eval2 (T2 (APP2 (T2 t1) e2)) (env, DNARROW, (TAU2, a'), tt) e3
| R3EVAL2_APP2 t2 a e2' v1 a' env e3 :
    R3Eval2 (T2 t2) (env, DNARROW, (TAU2, a), tt) e2' ->
    R3Eval2 (T2 (APP2 (V2 v1) e2'))
             (env, DNARROW, (a, a'), tt)
             e3 ->
    R3Eval2 (T2 (APP2 (V2 v1) (T2 t2)))
             (env, DNARROW, (TAU2, a'), tt)
             e3
| R3EVAL2_APP3 t rho x v2 a e' a' e3 env :
    R3Eval2 (T2 t) (map_update rho x v2, DNARROW, (TAU2, a), tt) e' ->
    R3Eval2 (T2 (APP2 (V2 (CLO2 x e' rho)) (V2 v2)))
             (env, DNARROW, (a, a'), tt) e3 ->
    R3Eval2 (T2 (APP2 (V2 (CLO2 x (T2 t) rho)) (V2 v2)))
             (env, DNARROW, (TAU2, a'), tt) e3
| R3EVAL2_APP4 x v rho env v2 :
    R3Eval2 (T2 (APP2 (V2 (CLO2 x (V2 v) rho)) (V2 v2)))
             (env, DNARROW, (TAU2, TAU2), tt)
             (V2 v)
| R3EVAL2_THROW v env :
    R3Eval2 (T2 (THROW2 v))
             (env, DNARROW, (TAU2, ERR2 v), tt)
             (V2 UNIT2)
| R3EVAL2_IF t e' e1 e2 env a a' e3 :
    R3Eval2 (T2 t) (env, DNARROW, (TAU2, a), tt) e' ->
    R3Eval2 (T2 (IF2 e' e1 e2))
             (env, DNARROW, (a, a'), tt) e3 ->
    R3Eval2 (T2 (IF2 (T2 t) e1 e2)) (env, DNARROW, (TAU2, a'), tt) e3
| R3EVAL2_IFTRUE e1 e2 e3 env a :
    R3Eval2 e1
             (env, DNARROW, (TAU2, a), tt)
             e3 ->
    R3Eval2 (T2 (IF2 (V2 TRUE) e1 e2))
             (env, DNARROW, (TAU2, a), tt)
             e3
| R3EVAL2_IFFALSE e1 e2 e3 env a :
    R3Eval2 e2
             (env, DNARROW, (TAU2, a), tt)
             e3 ->
    R3Eval2 (T2 (IF2 (V2 FALSE) e1 e2))
             (env, DNARROW, (TAU2, a), tt)
             e3
| R3EVAL2_EQ1 t1 env e1' e2 a a' e3 :
    R3Eval2 (T2 t1) (env, DNARROW, (TAU2, a), tt) e1' ->
    R3Eval2 (T2 (EQ2 e1' e2))
             (env, DNARROW, (a, a'), tt)
             e3 ->
    R3Eval2 (T2 (EQ2 (T2 t1) e2))
             (env, DNARROW, (TAU2, a'), tt) e3
| R3EVAL2_EQ2 t2 env e2' v1 a a' e3 :
    R3Eval2 (T2 t2) (env, DNARROW, (TAU2, a), tt) e2' ->
    R3Eval2 (T2 (EQ2 (V2 v1) e2'))
             (env, DNARROW, (a, a'), tt)
             e3 ->
    R3Eval2 (T2 (EQ2 (V2 v1) (T2 t2)))
             (env, DNARROW, (TAU2, a'), tt)
             e3
| R3EVAL2_EQ v1 v2 env :
    v1 = v2 ->
    R3Eval2 (T2 (EQ2 (V2 v1) (V2 v2)))
             (env, DNARROW, (TAU2, TAU2), tt)
             (V2 TRUE)
| R3EVAL2_EQN v1 v2 env :
    v1 <> v2 ->
    R3Eval2 (T2 (EQ2 (V2 v1) (V2 v2)))
             (env, DNARROW, (TAU2, TAU2), tt)
             (V2 FALSE)
| R3EVAL2_CATCH_V v1 e2 env :
    R3Eval2 (T2 (CATCH2 (V2 v1) e2))
             (env, DNARROW, (TAU2, TAU2), tt)
             (V2 v1)
| R3EVAL2_CATCH t1 e1' env a e2 e3 a' :
    R3Eval2 (T2 t1)
             (env, DNARROW, (TAU2, a), tt)
             e1' ->
    R3Eval2 (T2 (IF2 (T2 (EQ2 (V2 (VEXC a)) (V2 (VEXC TAU2))))
                     (T2 (CATCH2 e1' e2))
                     (T2 (APP2 e2 (V2 (unwrap_err2 a))))))
             (env, DNARROW, (a, a'), tt)
             e3 ->
    R3Eval2 (T2 (CATCH2 (T2 t1) e2))
             (env, DNARROW, (TAU2, a'), tt)
             e3
| R3REFL2_V v l :
    unobs_label2 l ->
    R3Eval2 (V2 v) l (V2 v)
| R3REFL2_ERR e v l :
    get_exc2 l = (ERR2 v, ERR2 v) ->
    unobs_label2 (replace_exc2 l (TAU2, TAU2)) ->
    R3Eval2 e l e.

The resulting definition of R3Eval2 is fully reducing and does not depend on the definition of R3Step2. Furthermore, we notice that R3Eval2 1. evaluates a single sub-term at a time; and 2. is syntax-directed. The defined relation is therefore a pretty-big-step relation. We rename our definition and remove redundant rules.
Inductive PBStep1 : Expr2 -> Label2 -> Expr2 -> Prop :=
| PBSTEP1_VAR x env v :
    map_lookup env x = Some v ->
    PBStep1 (T2 (VAR2 x)) (env, DNARROW, (TAU2, TAU2), tt) (V2 v)
| PBSTEP1_ABS x t env :
    PBStep1 (T2 (ABS2 x t))
            (env, DNARROW, (TAU2, TAU2), tt)
            (V2 (CLO2 x t env))
| PBSTEP1_APP1 t1 env a a' e1' e2 e3 :
    PBStep1 (T2 t1) (env, DNARROW, (TAU2, a), tt) e1' ->
    PBStep1 (T2 (APP2 e1' e2)) (env, DNARROW, (a, a'), tt) e3 ->
    PBStep1 (T2 (APP2 (T2 t1) e2)) (env, DNARROW, (TAU2, a'), tt) e3
| PBSTEP1_APP2 t2 a e2' v1 a' env e3 :
    PBStep1 (T2 t2) (env, DNARROW, (TAU2, a), tt) e2' ->
    PBStep1 (T2 (APP2 (V2 v1) e2'))
            (env, DNARROW, (a, a'), tt)
            e3 ->
    PBStep1 (T2 (APP2 (V2 v1) (T2 t2)))
            (env, DNARROW, (TAU2, a'), tt)
            e3
| PBSTEP1_APP3 t rho x v2 a e' a' e3 env :
    PBStep1 (T2 t) (map_update rho x v2, DNARROW, (TAU2, a), tt) e' ->
    PBStep1 (T2 (APP2 (V2 (CLO2 x e' rho)) (V2 v2)))
            (env, DNARROW, (a, a'), tt) e3 ->
    PBStep1 (T2 (APP2 (V2 (CLO2 x (T2 t) rho)) (V2 v2)))
            (env, DNARROW, (TAU2, a'), tt) e3
| PBSTEP1_APP4 x v rho env v2 :
    PBStep1 (T2 (APP2 (V2 (CLO2 x (V2 v) rho)) (V2 v2)))
            (env, DNARROW, (TAU2, TAU2), tt)
            (V2 v)
| PBSTEP1_THROW v env :
    PBStep1 (T2 (THROW2 v))
            (env, DNARROW, (TAU2, ERR2 v), tt)
            (V2 UNIT2)
| PBSTEP1_IF t e' e1 e2 env a a' e3 :
    PBStep1 (T2 t) (env, DNARROW, (TAU2, a), tt) e' ->
    PBStep1 (T2 (IF2 e' e1 e2))
            (env, DNARROW, (a, a'), tt) e3 ->
    PBStep1 (T2 (IF2 (T2 t) e1 e2)) (env, DNARROW, (TAU2, a'), tt) e3
| PBSTEP1_IFTRUE e1 e2 e3 env a :
    PBStep1 e1
            (env, DNARROW, (TAU2, a), tt)
            e3 ->
    PBStep1 (T2 (IF2 (V2 TRUE) e1 e2))
            (env, DNARROW, (TAU2, a), tt)
            e3
| PBSTEP1_IFFALSE e1 e2 e3 env a :
    PBStep1 e2
            (env, DNARROW, (TAU2, a), tt)
            e3 ->
    PBStep1 (T2 (IF2 (V2 FALSE) e1 e2))
            (env, DNARROW, (TAU2, a), tt)
            e3
| PBSTEP1_EQ1 t1 env e1' e2 a a' e3 :
    PBStep1 (T2 t1) (env, DNARROW, (TAU2, a), tt) e1' ->
    PBStep1 (T2 (EQ2 e1' e2))
            (env, DNARROW, (a, a'), tt)
            e3 ->
    PBStep1 (T2 (EQ2 (T2 t1) e2))
            (env, DNARROW, (TAU2, a'), tt) e3
| PBSTEP1_EQ2 t2 env e2' v1 a a' e3 :
    PBStep1 (T2 t2) (env, DNARROW, (TAU2, a), tt) e2' ->
    PBStep1 (T2 (EQ2 (V2 v1) e2'))
            (env, DNARROW, (a, a'), tt)
            e3 ->
    PBStep1 (T2 (EQ2 (V2 v1) (T2 t2)))
            (env, DNARROW, (TAU2, a'), tt)
            e3
| PBSTEP1_EQ v1 v2 env :
    v1 = v2 ->
    PBStep1 (T2 (EQ2 (V2 v1) (V2 v2)))
            (env, DNARROW, (TAU2, TAU2), tt)
            (V2 TRUE)
| PBSTEP1_EQN v1 v2 env :
    v1 <> v2 ->
    PBStep1 (T2 (EQ2 (V2 v1) (V2 v2)))
            (env, DNARROW, (TAU2, TAU2), tt)
            (V2 FALSE)
| PBSTEP1_CATCH_V v1 e2 env :
    PBStep1 (T2 (CATCH2 (V2 v1) e2))
            (env, DNARROW, (TAU2, TAU2), tt)
            (V2 v1)
| PBSTEP1_CATCH t1 e1' env a e2 e3 a' :
    PBStep1 (T2 t1)
            (env, DNARROW, (TAU2, a), tt)
            e1' ->
    PBStep1 (T2 (IF2 (T2 (EQ2 (V2 (VEXC a)) (V2 (VEXC TAU2))))
                     (T2 (CATCH2 e1' e2))
                     (T2 (APP2 e2 (V2 (unwrap_err2 a))))))
            (env, DNARROW, (TAU2, a'), tt)
            e3 ->
    PBStep1 (T2 (CATCH2 (T2 t1) e2))
            (env, DNARROW, (TAU2, a'), tt)
            e3
| PBREFL_V v l :
    unobs_label2 l ->
    PBStep1 (V2 v) l (V2 v)
| PBREFL_ERR e v l :
    get_exc2 l = (ERR2 v, ERR2 v) ->
    unobs_label2 (replace_exc2 l (TAU2, TAU2)) ->
    PBStep1 e l e.

We now prove the correctness of this transformation.

Correctness of refocusing

Transitive closure of small-step evaluation

Inductive Trans2 : Expr2 -> Label2 -> Expr2 -> Prop :=
| TRANS2 t1 e2 e3 env a a' :
    Step2 (T2 t1) (env, DNARROW, (TAU2, a), tt) e2 ->
    Trans2 e2 (env, DNARROW, (a, a'), tt) e3 ->
    Trans2 (T2 t1) (env, DNARROW, (TAU2, a'), tt) e3
| REFL2 env e a :
    Trans2 e (env, DNARROW, (a, a), tt) e.

Proof that transitive closure corresponds to iteration relation.
Theorem trans_v_sound :
  forall e l e',
    Trans2 e l e' ->
    is_val2 e' = true ->
    Eval2 e l e'.
Proof.
  induction 1; intro.
  - eapply EVAL2.
    + apply H.
    + inversion H0; subst; apply IHTrans2; apply H1.
  - destruct e; inversion H; apply REFL2_V.
    destruct a; reflexivity.
Qed.

Theorem trans_e_sound :
  forall e l e',
    Trans2 e l e' ->
    is_abr_ter2 l = true ->
    Eval2 e l e'.
Proof.
  induction 1; intro.
  - eapply EVAL2.
    + apply H.
    + inversion H0; subst; apply IHTrans2;
      destruct a'; inversion H1; reflexivity.
  - destruct a; inversion H.
    eapply REFL2_ERR; reflexivity; apply I.
Qed.

Theorem trans_v_complete :
  forall e l e',
    Eval2 e l e' ->
    is_val2 e' = true ->
    Trans2 e l e'.
Proof.
  induction 1; intro.
  - eapply TRANS2;
    [ apply H
    | apply IHEval2; apply H1 ].
  - destruct l; destruct p; destruct p; destruct u;
    destruct d; simpl in H; try inversion H;
    destruct e; destruct e; destruct e1; try inversion H;
    apply REFL2.
  - destruct l; destruct p; destruct p; destruct u;
    destruct d; simpl in H0; try inversion H0;
    destruct e0; destruct e0; destruct e2; inversion H;
    subst.
    apply REFL2.
Qed.

Theorem trans_e_complete :
  forall e l e',
    Eval2 e l e' ->
    is_abr_ter2 l = true ->
    Trans2 e l e'.
Proof.
  induction 1; intro.
  - eapply TRANS2.
    apply H.
    apply IHEval2.
    destruct a'; inversion H1.
    destruct a; reflexivity.
  - destruct l; destruct p; destruct p; destruct u.
    destruct d; simpl in H; try inversion H.
    destruct e; destruct e; destruct e1; try inversion H.
    apply REFL2.
    apply REFL2.
  - destruct l; destruct p; destruct p; destruct u.
    destruct d; simpl in H0; try inversion H0.
    destruct e0; destruct e0; destruct e2; inversion H.
    subst.
    apply REFL2.
Qed.

Soundness of refocusing

Proof that the refocused relation corresponds to the transitive closure of the small-step relation following Leroy, Grall, and Ciobaca.
Transitivity of Trans2
Lemma trans :
  forall e1 e2 e3 env a a',
    Trans2 e1 (env, DNARROW, (TAU2, a), tt) e2 ->
    Trans2 e2 (env, DNARROW, (a, a'), tt) e3 ->
    Trans2 e1 (env, DNARROW, (TAU2, a'), tt) e3.
Proof.
  intros.
  dependent induction H.
  - eapply TRANS2.
    apply H.
    destruct a0.
    + eapply IHTrans2.
      reflexivity.
      apply H1.
    + inversion H0; subst.
      inversion H1; subst.
      apply REFL2.
  - apply H0.
Qed.

A single step is an instance of a transitive step
Lemma single_trans :
  forall t1 e1' env a,
    Step2 (T2 t1) (env, DNARROW, (TAU2, a), tt) e1' ->
    Trans2 (T2 t1) (env, DNARROW, (TAU2, a), tt) e1'.
Proof.
  intros.
  eapply TRANS2.
  apply H.
  apply REFL2.
Qed.

Congruence proofs
Lemma congruence_app1 :
  forall t1 e2 e1' l,
    Trans2 (T2 t1) l e1' ->
    Trans2 (T2 (APP2 (T2 t1) e2)) l (T2 (APP2 e1' e2)).
Proof.
  induction 1.
  - eapply TRANS2;
    [ apply STEP2_APP1; apply H
    | apply IHTrans2 ].
  - apply REFL2.
Qed.

Lemma congruence_app2 :
  forall t2 e2' v1 l,
    Trans2 (T2 t2) l e2' ->
    Trans2 (T2 (APP2 (V2 v1) (T2 t2))) l (T2 (APP2 (V2 v1) e2')).
Proof.
  induction 1.
  - eapply TRANS2;
    [ apply STEP2_APP2; apply H
    | apply IHTrans2 ].
  - apply REFL2.
Qed.

Lemma congruence_app3 :
  forall x t e' rho v2 l,
    Trans2 (T2 t) (replace_env2 l (map_update rho x v2)) e' ->
    Trans2 (T2 (APP2 (V2 (CLO2 x (T2 t) rho)) (V2 v2)))
           l
           (T2 (APP2 (V2 (CLO2 x e' rho)) (V2 v2))).
Proof.
  induction 1.
  -
If we try to eapply TRANS2 Coq reports: 
Error: Impossible to unify
 "Trans2 (T2 ?1996) (?1999, DNARROW, (TAU2, ?2001), tt) ?1998" with
 "Trans2 (T2 (APP2 (V2 (CLO2 x (T2 t1) rho)) (V2 v2))) l
    (T2 (APP2 (V2 (CLO2 x e3 rho)) (V2 v2)))".
To resolve this we unfold the label and use dependent equality.
Abort.

Lemma congruence_app3 :
  forall x t e' rho v2 a' env,
    Trans2 (T2 t) (map_update rho x v2, DNARROW, (TAU2, a'), tt) e' ->
    Trans2 (T2 (APP2 (V2 (CLO2 x (T2 t) rho)) (V2 v2)))
           (env, DNARROW, (TAU2, a'), tt)
           (T2 (APP2 (V2 (CLO2 x e' rho)) (V2 v2))).
Proof.   intros.
  generalize_eqs H.
  intros. destruct H0.
  induction H.
  - eapply TRANS2;
    [ dependent destruction H1;
      apply STEP2_APP3; apply H
    | ].
    destruct a. apply IHTrans2. apply H1.
    inversion H0; subst.
    dependent destruction H1.
    apply REFL2.
  - dependent destruction H1.
    apply REFL2.
Qed.

Lemma congruence_if :
  forall t e' e1 e2 l,
    Trans2 (T2 t) l e' ->
    Trans2 (T2 (IF2 (T2 t) e1 e2)) l
           (T2 (IF2 e' e1 e2)).
Proof.
  induction 1.
  - eapply TRANS2;
    [ apply STEP2_IF; apply H
    | apply IHTrans2 ].
  - apply REFL2.
Qed.

Lemma congruence_eq1 :
  forall t1 e1' e2 l,
    Trans2 (T2 t1) l e1' ->
    Trans2 (T2 (EQ2 (T2 t1) e2)) l (T2 (EQ2 e1' e2)).
Proof.
  induction 1.
  - eapply TRANS2;
    [ apply STEP2_EQ1; apply H
    | apply IHTrans2 ].
  - apply REFL2.
Qed.

Lemma congruence_eq2 :
  forall v1 t2 e2' l,
    Trans2 (T2 t2) l e2' ->
    Trans2 (T2 (EQ2 (V2 v1) (T2 t2))) l (T2 (EQ2 (V2 v1) e2')).
Proof.
  induction 1.
  - eapply TRANS2;
    [ apply STEP2_EQ2; apply H
    | apply IHTrans2 ].
  - apply REFL2.
Qed.

Trans2 gives an intermediate term, a value, or an abruptly terminated term.
Lemma trans_ter :
  forall e l e',
    Trans2 e l e' ->
    (is_val2 e' = false /\ is_abr_ter2 l = false) \/
    (is_val2 e' = true /\ is_abr_ter2 l = false) \/
    is_abr_ter2 l = true.
Proof.
  induction 1.
  - inversion IHTrans2.
    + destruct a.
      * left. apply H1.
      * inversion H0; subst.
        inversion H1.
        inversion H3.
    + destruct a.
      * right. apply H1.
      * inversion H0; subst.
        inversion H1.
        right.
        left.
        apply H2.
        right.
        right.
        reflexivity.
  - destruct e; destruct a.
    + right. left. split; reflexivity.
    + right.
      right.
      reflexivity.
    + left.
      split; reflexivity.
    + right. right. reflexivity.
Qed.

The lemma that we want about catch is the following:
Lemma congruence_catch_value :
  forall t1 e1' e2 l a,
    Trans2 (T2 t1) l e1' ->
    is_val2 e1' = true /\ is_abr_ter2 l = false ->
    get_exc2 l = (TAU2, a) ->
    Trans2 (T2 (CATCH2 (T2 t1) e2))
           l
           (T2 (IF2 (T2 (EQ2 (V2 (VEXC TAU2)) (V2 (VEXC TAU2))))
                    (T2 (CATCH2 e1' e2))
                    (T2 (APP2 e2 (V2 (unwrap_err2 TAU2)))))).
Proof.
  induction 1; intros.
  - eapply TRANS2.
    eapply STEP2_CATCH.
    apply H.
    reflexivity.
    reflexivity.
    destruct e3; inversion H1; inversion H3.
    destruct a0.
    + eapply TRANS2.
      apply STEP2_IF.
      apply STEP2_EQ.
      reflexivity.
      instantiate (1:=TAU2).
      apply I.
      eapply TRANS2.
      apply STEP2_IFTRUE.
      instantiate (1:=TAU2).
      apply I.
      apply IHTrans2.
      apply H1.
      apply H2.
    + inversion H0; subst; inversion H4.
  - inversion H0; subst.
    inversion H. destruct e; inversion H1.
    eapply TRANS2.
    apply STEP2_CATCH_V.
    instantiate (1:=TAU2).
    apply I.
At this point we are stuck. Proving this case requires us to either modify our relation to be modulo a suitable notion of similarity.
An alternative approach is to give a simpler lemma, which we opt for here.
Abort.

A simpler lemma:
Lemma congruence_catch_value :
  forall t1 e1' e2 l a,
    Trans2 (T2 t1) l e1' ->
    is_val2 e1' = true /\ is_abr_ter2 l = false ->
    get_exc2 l = (TAU2, a) ->
    Trans2 (T2 (CATCH2 (T2 t1) e2)) l
           e1'.
Proof.
  induction 1; intros.
  - eapply TRANS2.
    eapply STEP2_CATCH.
    apply H.
    reflexivity.
    reflexivity.
    destruct e3; inversion H1; inversion H3.
    destruct a0.
    + eapply TRANS2.
      apply STEP2_IF.
      apply STEP2_EQ.
      reflexivity.
      instantiate (1:=TAU2).
      apply I.
      eapply TRANS2.
      apply STEP2_IFTRUE.
      instantiate (1:=TAU2).
      apply I.
      apply IHTrans2.
      apply H1.
      apply H2.
    + inversion H0; subst; inversion H4.
  - inversion H0; subst.
    inversion H. destruct e; inversion H1.
    eapply TRANS2.
    apply STEP2_CATCH_V.
    instantiate (1:=TAU2).
    apply I.
    apply REFL2.
Qed.

Similarly for the case where abrupt termination occurs:
Lemma congruence_catch_abr_ter :
  forall t1 e1' e2 l a l',
    Trans2 (T2 t1) l e1' ->
    is_abr_ter2 l = true ->
    get_exc2 l = (TAU2, a) ->
    l' = replace_exc2 l (TAU2, TAU2) ->
    Trans2 (T2 (CATCH2 (T2 t1) e2))
           l'
           (T2 (APP2 e2 (V2 (unwrap_err2 a)))).
Proof.
  induction 1; intros; subst.
  - eapply TRANS2.
    eapply STEP2_CATCH.
    apply H.
    reflexivity.
    reflexivity.
    inversion H2; subst.
    destruct a0.
    + eapply TRANS2.
      apply STEP2_IF.
      apply STEP2_EQ.
      reflexivity.
      instantiate (1:=TAU2).
      apply I.
      eapply TRANS2.
      apply STEP2_IFTRUE.
      instantiate (1:=TAU2).
      apply I.
      apply IHTrans2.
      apply H1.
      apply H2.
      reflexivity.
    + destruct a; inversion H1.
      eapply TRANS2.
      apply STEP2_IF.
      apply STEP2_EQN.
      unfold not; intro.
      inversion H3.
      instantiate (1:=TAU2).
      apply I.
      eapply TRANS2.
      apply STEP2_IFFALSE.
      instantiate (1:=TAU2).
      apply I.
      inversion H0; subst.
      apply REFL2.
  - destruct a0; inversion H.
    inversion H0.
Qed.

Ltac solve := try eapply TRANS2; try constructor; try apply I;
              try reflexivity; try assumption.

We try to prove our soundness theorem:
Theorem refocus_sound :
  forall e l e',
    PBStep1 e l e' ->
    Trans2 e l e'.
Proof.
  induction 1.
  - solve.
  - solve.
  - eapply trans.
    apply congruence_app1.
    apply IHPBStep1_1.
    apply IHPBStep1_2.
  - eapply trans.
    apply congruence_app2.
    apply IHPBStep1_1.
    apply IHPBStep1_2.
  - eapply trans.
    apply congruence_app3.
    apply IHPBStep1_1.
    apply IHPBStep1_2.
  - solve.
  - solve.
  - eapply trans.
    apply congruence_if.
    apply IHPBStep1_1.
    apply IHPBStep1_2.
  - solve. Focus 2.
    apply IHPBStep1.
    apply I.
  - solve. Focus 2.
    apply IHPBStep1.
    apply I.
  - eapply trans.
    apply congruence_eq1.
    apply IHPBStep1_1.
    apply IHPBStep1_2.
  - eapply trans.
    apply congruence_eq2.
    apply IHPBStep1_1.
    apply IHPBStep1_2.
  - solve.
  - eapply TRANS2.
    apply STEP2_EQN.
    apply H.
    instantiate (1:=TAU2).
    apply I.
    apply REFL2.
  - solve.
  -
Proving this case would be straightforward given a lemma of the form that we originally envisaged for congruence_catch_value. Instead, we need to prove a few properties about the derivation of IF terms of the particular structure that we get in this particular case of the soundness proof. We give these before returning to this theorem.
Abort.

Helper lemma for congruence_catch_value case.
Lemma pb_if_eq_catch_v :
  forall v e2 env a' e3,
    PBStep1
      (T2
         (IF2 (T2 (EQ2 (V2 (VEXC TAU2)) (V2 (VEXC TAU2))))
              (T2 (CATCH2 (V2 v) e2)) (T2 (APP2 e2 (V2 (unwrap_err2 TAU2))))))
      (env, DNARROW, (TAU2, a'), tt) e3 ->
    e3 = (V2 v) /\
    a' = TAU2.
Proof.
  intros.
  inversion H; subst. inversion H6; subst. inversion H7; subst.
  inversion H8; subst.
  split; reflexivity.
  inversion H0.
  inversion H0.
  destruct H5; reflexivity.
  inversion H0.
  inversion H0.
Qed.

Helper lemma for congruence_catch_abr_ter case.
Definition pb_if_neq_catch_abr_ter :
  forall v e1' e2 env a' e3,
    PBStep1
      (T2
         (IF2 (T2 (EQ2 (V2 (VEXC (ERR2 v))) (V2 (VEXC TAU2))))
              (T2 (CATCH2 e1' e2))
              (T2 (APP2 e2 (V2 (unwrap_err2 (ERR2 v)))))))
      (env, DNARROW, (TAU2, a'), tt) e3 ->
    PBStep1
      (T2 (APP2 e2 (V2 (unwrap_err2 (ERR2 v)))))
      (env, DNARROW, (TAU2, a'), tt) e3.
Proof.
  intros.
  inversion H; subst.
  inversion H6; subst.
  inversion H5.
  inversion H7; subst.
  apply H8.
  inversion H0.
  inversion H0.
  inversion H0.
Qed.

Helper lemma for congruence_catch_abr_ter case.
Definition eval_if_neq_catch_abr_ter :
  forall v e1' e2 env a e',
    Eval2
      (T2
         (IF2 (T2 (EQ2 (V2 (VEXC (ERR2 v))) (V2 (VEXC TAU2))))
              e1'
              (T2 (APP2 e2 (V2 (unwrap_err2 (ERR2 v)))))))
      (env, DNARROW, (TAU2, a), tt)
      e' ->
    Eval2
      (T2 (APP2 e2 (V2 (unwrap_err2 (ERR2 v)))))
      (env, DNARROW, (TAU2, a), tt)
      e'.
Proof.
  intros v e1' e2 env a e' T.
  inversion T.
  inversion H2; subst. inversion H10; subst. inversion H1.
  inversion H4; subst.
  inversion H8; subst.
  simpl.
  destruct a1.
  apply H9.
  inversion H7.
  inversion H; subst.
  inversion H6.
  subst.
  inversion H.
Qed.

Helper lemma: we prove that pretty-big-step evaluation always produces a value or an abruptly terminated label. Convenient for contradicting a nonsensical case in connection with the catch case.
Lemma pbstep_ter :
  forall e l e',
    PBStep1 e l e' ->
    is_val2 e' = true \/ is_abr_ter2 l = true.
Proof.
  induction 1.
  - left; reflexivity.
  - left; reflexivity.
  - destruct a.
    + apply IHPBStep1_2.
    + inversion H0; subst.
      inversion H1.
      right; reflexivity.
  - destruct a.
    + apply IHPBStep1_2.
    + inversion H0; subst.
      inversion H1; subst.
      right; reflexivity.
  - destruct a.
    + apply IHPBStep1_2.
    + inversion H0; subst.
      inversion H1; subst.
      right; reflexivity.
  - left; reflexivity.
  - left; reflexivity.
  - destruct a.
    + apply IHPBStep1_2.
    + inversion H0; subst.
      inversion H1; subst.
      right; reflexivity.
  - destruct IHPBStep1.
    + left; assumption.
    + right; assumption.
  - destruct IHPBStep1.
    + left; assumption.
    + right; assumption.
  - destruct a.
    + apply IHPBStep1_2.
    + inversion H0; subst.
      inversion H1; subst.
      right; reflexivity.
  - destruct a.
    + apply IHPBStep1_2.
    + inversion H0; subst.
      inversion H1; subst.
      right; reflexivity.
  - left; reflexivity.
  - left; reflexivity.
  - left; reflexivity.
  - destruct a; apply IHPBStep1_2.
  - left; reflexivity.
  - destruct l. destruct p. destruct p. destruct e0. inversion H; subst.
    right; reflexivity.
Qed.

Theorem refocus_sound :
  forall e l e',
    PBStep1 e l e' ->
    Trans2 e l e'.
Proof.
  induction 1.
  - solve.
  - solve.
  - eapply trans.
    apply congruence_app1.
    apply IHPBStep1_1.
    apply IHPBStep1_2.
  - eapply trans.
    apply congruence_app2.
    apply IHPBStep1_1.
    apply IHPBStep1_2.
  - eapply trans.
    apply congruence_app3.
    apply IHPBStep1_1.
    apply IHPBStep1_2.
  - solve.
  - solve.
  - eapply trans.
    apply congruence_if.
    apply IHPBStep1_1.
    apply IHPBStep1_2.
  - solve. Focus 2.
    apply IHPBStep1.
    apply I.
  - solve. Focus 2.
    apply IHPBStep1.
    apply I.
  - eapply trans.
    apply congruence_eq1.
    apply IHPBStep1_1.
    apply IHPBStep1_2.
  - eapply trans.
    apply congruence_eq2.
    apply IHPBStep1_1.
    apply IHPBStep1_2.
  - solve.
  - eapply TRANS2.
    apply STEP2_EQN.
    apply H.
    instantiate (1:=TAU2).
    apply I.
    apply REFL2.
  - solve.
  - destruct a. destruct e1'.
    + eapply trans.
      eapply congruence_catch_value.
      apply IHPBStep1_1.
      split; reflexivity.
      reflexivity.
      apply pb_if_eq_catch_v in H0. destruct H0; subst.
      apply REFL2.
    + apply pbstep_ter in H. destruct H; inversion H.
    + eapply trans.
      eapply congruence_catch_abr_ter.
      apply IHPBStep1_1.
      reflexivity.
      reflexivity.
      reflexivity.
      apply pb_if_neq_catch_abr_ter in H0.
      simpl in H0.
      apply pbstep_ter in H0. destruct H0.
      * destruct e3; inversion H0.
        apply trans_v_complete.
        apply trans_v_sound in IHPBStep1_2.
        eapply eval_if_neq_catch_abr_ter.
        apply IHPBStep1_2. reflexivity. reflexivity.
      * destruct a'; inversion H0.
        apply trans_e_complete.
        apply trans_e_sound in IHPBStep1_2.
        eapply eval_if_neq_catch_abr_ter.
        apply IHPBStep1_2. reflexivity. reflexivity.
  - destruct l. destruct p. destruct p. destruct e. destruct d. inversion H.
    destruct u. destruct e; destruct e1; inversion H.
    apply REFL2.
    subst.
    apply REFL2.
  - destruct l. destruct p. destruct p. destruct e. destruct d. inversion H0.
    destruct u. destruct e0. destruct e; destruct e0; inversion H; subst.
    apply REFL2.
    destruct d. inversion H0.
    destruct u. destruct e0. destruct e; destruct e0; inversion H; subst.
    apply REFL2.
Qed.

This concludes our proof of soundness of the semantics resulting for refocusing.
The soundness proof given here was somewhat tedious, due to the non-compositional nature of our catch-rule. It is possible to incrementally factor the rules for catch into a compositional semantics.
Since we will be extending our language, we perform this factorization, and use the modified semantics from here on out.

Soundness of refocusing -- factored

The updated language syntax is:

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

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.

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.

By an equally straightforward transformation, we can go back to a 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.

Transitive closure
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.

Proof that transitive closure corresponds to iteration relation.
Theorem trans3_v_sound :
  forall e l e',
    Trans3 e l e' ->
    is_val3 e' = true ->
    Eval3 e l e'.
Proof.
  induction 1; intro.
  - eapply EVAL3.
    + apply H.
    + inversion H0; subst; apply IHTrans3; apply H1.
  - destruct e; inversion H; apply REFL3_V.
    destruct a; reflexivity.
Qed.

Theorem trans3_e_sound :
  forall e l e',
    Trans3 e l e' ->
    is_abr_ter3 l = true ->
    Eval3 e l e'.
Proof.
  induction 1; intro.
  - eapply EVAL3.
    + apply H.
    + inversion H0; subst; apply IHTrans3;
      destruct a'; inversion H1; reflexivity.
  - destruct a; inversion H.
    eapply REFL3_ERR; reflexivity; apply I.
Qed.

Theorem trans3_v_complete :
  forall e l e',
    Eval3 e l e' ->
    is_val3 e' = true ->
    Trans3 e l e'.
Proof.
  induction 1; intro.
  - eapply TRANS3;
    [ apply H
    | apply IHEval3; apply H1 ].
  - destruct l; destruct p; destruct p; destruct u;
    destruct d; simpl in H; try inversion H;
    destruct e; destruct e; destruct e1; try inversion H;
    apply REFL3.
  - destruct l; destruct p; destruct p; destruct u;
    destruct d; simpl in H0; try inversion H0;
    destruct e0; destruct e0; destruct e2; inversion H;
    subst.
    apply REFL3.
Qed.

Theorem trans3_e_complete :
  forall e l e',
    Eval3 e l e' ->
    is_abr_ter3 l = true ->
    Trans3 e l e'.
Proof.
  induction 1; intro.
  - eapply TRANS3.
    apply H.
    apply IHEval3.
    destruct a'; inversion H1.
    destruct a; reflexivity.
  - destruct l; destruct p; destruct p; destruct u.
    destruct d; simpl in H; try inversion H.
    destruct e; destruct e; destruct e1; try inversion H.
    apply REFL3.
    apply REFL3.
  - destruct l; destruct p; destruct p; destruct u.
    destruct d; simpl in H0; try inversion H0.
    destruct e0; destruct e0; destruct e2; inversion H.
    subst.
    apply REFL3.
Qed.

Proof that the refocused relation corresponds to the transitive closure of the small-step relation following Leroy, Grall, and Ciobaca.
Transitivity of Trans3
Lemma trans3 :
  forall e1 e2 e3 env a a',
    Trans3 e1 (env, DNARROW, (TAU3, a), tt) e2 ->
    Trans3 e2 (env, DNARROW, (a, a'), tt) e3 ->
    Trans3 e1 (env, DNARROW, (TAU3, a'), tt) e3.
Proof.
  intros.
  dependent induction H.
  - eapply TRANS3.
    apply H.
    destruct a0.
    + eapply IHTrans3.
      reflexivity.
      apply H1.
    + inversion H0; subst.
      inversion H1; subst.
      apply REFL3.
  - apply H0.
Qed.

A single step constitutes an instance of a transitive step
Lemma single_trans3 :
  forall t1 e1' env a,
    Step3 (T3 t1) (env, DNARROW, (TAU3, a), tt) e1' ->
    Trans3 (T3 t1) (env, DNARROW, (TAU3, a), tt) e1'.
Proof.
  intros.
  eapply TRANS3.
  apply H.
  apply REFL3.
Qed.

Congruence proofs
Lemma congruence3_app1 :
  forall t1 e2 e1' l,
    Trans3 (T3 t1) l e1' ->
    Trans3 (T3 (APP3 (T3 t1) e2)) l (T3 (APP3 e1' e2)).
Proof.
  induction 1.
  - eapply TRANS3;
    [ apply STEP3_APP1; apply H
    | apply IHTrans3 ].
  - apply REFL3.
Qed.

Lemma congruence3_app2 :
  forall t2 e2' v1 l,
    Trans3 (T3 t2) l e2' ->
    Trans3 (T3 (APP3 (V3 v1) (T3 t2))) l (T3 (APP3 (V3 v1) e2')).
Proof.
  induction 1.
  - eapply TRANS3;
    [ apply STEP3_APP2; apply H
    | apply IHTrans3 ].
  - apply REFL3.
Qed.

Lemma congruence3_app3 :
  forall x t e' rho v2 l,
    Trans3 (T3 t) (replace_env3 l (map_update rho x v2)) e' ->
    Trans3 (T3 (APP3 (V3 (CLO3 x (T3 t) rho)) (V3 v2)))
           l
           (T3 (APP3 (V3 (CLO3 x e' rho)) (V3 v2))).
Proof.
  induction 1.
  -
If we try to eapply TRANS2 Coq reports: 
Error: Impossible to unify
 "Trans2 (T2 ?1996) (?1999, DNARROW, (TAU2, ?2001), tt) ?1998" with
 "Trans2 (T2 (APP2 (V2 (CLO2 x (T2 t1) rho)) (V2 v2))) l
    (T2 (APP2 (V2 (CLO2 x e3 rho)) (V2 v2)))".
To resolve this we unfold the label and use dependent equality.
Abort.

Lemma congruence3_app3 :
  forall x t e' rho v2 a' env,
    Trans3 (T3 t) (map_update rho x v2, DNARROW, (TAU3, a'), tt) e' ->
    Trans3 (T3 (APP3 (V3 (CLO3 x (T3 t) rho)) (V3 v2)))
           (env, DNARROW, (TAU3, a'), tt)
           (T3 (APP3 (V3 (CLO3 x e' rho)) (V3 v2))).
Proof.   intros.
  generalize_eqs H.
  intros. destruct H0.
  induction H.
  - eapply TRANS3;
    [ dependent destruction H1;
      apply STEP3_APP3; apply H
    | ].
    destruct a. apply IHTrans3. apply H1.
    inversion H0; subst.
    dependent destruction H1.
    apply REFL3.
  - dependent destruction H1.
    apply REFL3.
Qed.

Lemma congruence3_if :
  forall t e' e1 e2 l,
    Trans3 (T3 t) l e' ->
    Trans3 (T3 (IF3 (T3 t) e1 e2)) l
           (T3 (IF3 e' e1 e2)).
Proof.
  induction 1.
  - eapply TRANS3;
    [ apply STEP3_IF; apply H
    | apply IHTrans3 ].
  - apply REFL3.
Qed.

Lemma congruence3_eq1 :
  forall t1 e1' e2 l,
    Trans3 (T3 t1) l e1' ->
    Trans3 (T3 (EQ3 (T3 t1) e2)) l (T3 (EQ3 e1' e2)).
Proof.
  induction 1.
  - eapply TRANS3;
    [ apply STEP3_EQ1; apply H
    | apply IHTrans3 ].
  - apply REFL3.
Qed.

Lemma congruence3_eq2 :
  forall v1 t2 e2' l,
    Trans3 (T3 t2) l e2' ->
    Trans3 (T3 (EQ3 (V3 v1) (T3 t2))) l (T3 (EQ3 (V3 v1) e2')).
Proof.
  induction 1.
  - eapply TRANS3;
    [ apply STEP3_EQ2; apply H
    | apply IHTrans3 ].
  - apply REFL3.
Qed.

Lemma congruence3_catch :
  forall t1 e1' e2 l l' a,
    Trans3 (T3 t1) l e1' ->
    get_exc3 l = (TAU3, a) ->
    l' = (replace_exc3 l (TAU3, TAU3)) ->
    Trans3 (T3 (CATCH3 TAU3 (T3 t1) e2))
           l'
           (T3 (CATCH3 a e1' e2)).
Proof.
  induction 1; intros; subst.
  - eapply TRANS3.
    eapply STEP3_CATCH.
    apply H.
    reflexivity.
    reflexivity.
    inversion H1; subst.
    destruct a0.
    + eapply IHTrans3.
      reflexivity.
      reflexivity.
    + inversion H0; subst.
      apply REFL3.
  - inversion H; subst.
    apply REFL3.
Qed.

Ltac solve3 := try eapply TRANS3; try constructor; try apply I;
              try reflexivity; try assumption.

Theorem refocus_sound3 :
  forall e l e',
    PBStep3 e l e' ->
    Trans3 e l e'.
Proof.
  induction 1.
  - solve3.
  - solve3.
  - eapply trans3.
    apply congruence3_app1.
    apply IHPBStep3_1.
    apply IHPBStep3_2.
  - eapply trans3.
    apply congruence3_app2.
    apply IHPBStep3_1.
    apply IHPBStep3_2.
  - eapply trans3.
    apply congruence3_app3.
    apply IHPBStep3_1.
    apply IHPBStep3_2.
  - solve3.
  - solve3.
  - eapply trans3.
    apply congruence3_if.
    apply IHPBStep3_1.
    apply IHPBStep3_2.
  - solve3. Focus 2.
    apply IHPBStep3.
    apply I.
  - solve3. Focus 2.
    apply IHPBStep3.
    apply I.
  - eapply trans3.
    apply congruence3_eq1.
    apply IHPBStep3_1.
    apply IHPBStep3_2.
  - eapply trans3.
    apply congruence3_eq2.
    apply IHPBStep3_1.
    apply IHPBStep3_2.
  - solve3.
  - eapply TRANS3.
    apply STEP3_EQN.
    apply H.
    instantiate (1:=TAU3).
    apply I.
    apply REFL3.
  - solve3.
  - solve3.
    instantiate (1:=TAU3).
    apply I.
    apply IHPBStep3.
  - eapply trans3.
    eapply congruence3_catch.
    apply IHPBStep3_1.
    reflexivity.
    reflexivity.
    apply IHPBStep3_2.
  - destruct l. destruct p. destruct p. destruct e. destruct u.
    destruct d; destruct e; destruct e1; simpl in H; try inversion H;
    apply REFL3.
  - destruct l. destruct p. destruct p. destruct e0. destruct u.
    destruct d; destruct e0; destruct e2; simpl in H;
    try inversion H0; try inversion H;
    apply REFL3.
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,
    Step3 (T3 t1) (env, DNARROW, (TAU3, ERR3 v), tt) e' ->
    PBStep3 (T3 t1) (env, DNARROW, (TAU3, ERR3 v), tt) e'.
Proof.
  intros.
  dependent induction H;
    try (match goal with
           | [ H' : unobs_label3 _ |- _ ] =>
             simpl in H'; inversion H'
         end).
  - eapply PBSTEP3_APP1.
    apply IHStep3.
    reflexivity.
    eapply PBREFL3_ERR.
    reflexivity.
    apply I.
  - eapply PBSTEP3_APP2.
    apply IHStep3.
    reflexivity.
    eapply PBREFL3_ERR.
    reflexivity.
    apply I.
  - eapply PBSTEP3_APP3.
    apply IHStep3.
    simpl.
    reflexivity.
    eapply PBREFL3_ERR.
    reflexivity.
    apply I.
  - eapply PBSTEP3_THROW.
  - eapply PBSTEP3_IF.
    apply IHStep3.
    reflexivity.
    eapply PBREFL3_ERR.
    reflexivity.
    apply I.
  - eapply PBSTEP3_EQ1.
    apply IHStep3.
    reflexivity.
    eapply PBREFL3_ERR.
    reflexivity.
    apply I.
  - eapply PBSTEP3_EQ2.
    apply IHStep3.
    reflexivity.
    eapply PBREFL3_ERR.
    reflexivity.
    apply I.
  - destruct l; destruct p; destruct p; destruct d; destruct u; inversion H1; subst.
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,
    Step3 (T3 t1) (env, DNARROW, (TAU3, a), tt) e2 ->
    forall e3 a',
      PBStep3 e2 (env, DNARROW, (a, a'), tt) e3 ->
      PBStep3 (T3 t1) (env, DNARROW, (TAU3, a'), tt) e3.
Proof.
  intros t1 e2 env a H e3 a'.
  generalize_eqs H.
  intro; subst.
  generalize dependent e3.
  generalize dependent a'.
  generalize dependent env.
  induction H; intros.
  - dependent destruction H1; destruct a; simpl in H; inversion H.
    inversion H2; subst; destruct a'; simpl in H3; inversion H3; try inversion H1.
    apply PBSTEP3_VAR.
    apply H0.
  - dependent destruction H0; destruct a; simpl in H; inversion H.
    inversion H1; subst; destruct a'; simpl in H2; inversion H2; try inversion H0.
    apply PBSTEP3_ABS.
  - dependent destruction H0;
    inversion H1; subst.
    + eapply PBSTEP3_APP1.
      apply IHStep3.
      reflexivity.
      apply H7.
      apply H8.
    + eapply PBSTEP3_APP1.
      apply IHStep3.
      reflexivity.
      apply PBREFL3_V.
      instantiate (1:=TAU3).
      apply I.
      apply H1.
    + eapply PBSTEP3_APP1.
      apply IHStep3.
      reflexivity.
      apply PBREFL3_V.
      instantiate (1:=TAU3).
      apply I.
      apply H1.
    + eapply PBSTEP3_APP1.
      apply IHStep3.
      reflexivity.
      apply PBREFL3_V.
      instantiate (1:=TAU3).
      apply I.
      apply H1.
    + inversion H0; subst.
      eapply PBSTEP3_APP1.
      apply IHStep3.
      reflexivity.
      eapply PBREFL3_ERR.
      reflexivity.
      apply I.
      eapply PBREFL3_ERR.
      reflexivity.
      apply I.
  - dependent destruction H0;
    inversion H1; subst.
    + eapply PBSTEP3_APP2.
      apply IHStep3.
      reflexivity.
      apply H7.
      apply H8.
    + eapply PBSTEP3_APP2.
      apply IHStep3.
      reflexivity.
      instantiate (2:=TAU3).
      apply PBREFL3_V.
      apply I.
      apply H1.
    + eapply PBSTEP3_APP2.
      apply IHStep3.
      reflexivity.
      instantiate (2:=TAU3).
      apply PBREFL3_V.
      apply I.
      apply H1.
    + inversion H0; subst.
      eapply PBSTEP3_APP2.
      apply IHStep3.
      reflexivity.
      eapply PBREFL3_ERR.
      reflexivity.
      apply I.
      eapply PBREFL3_ERR.
      reflexivity.
      apply I.
  - dependent destruction H0;
    inversion H1; subst.
    + eapply PBSTEP3_APP3.
      eapply IHStep3.
      reflexivity.
      apply H9.
      apply H10.
    + eapply PBSTEP3_APP3.
      eapply IHStep3.
      reflexivity.
      apply PBREFL3_V.
      instantiate (1:=TAU3).
      apply I.
      apply H1.
    + inversion H0; subst.
      eapply PBSTEP3_APP3.
      eapply IHStep3.
      reflexivity.
      eapply PBREFL3_ERR.
      reflexivity.
      apply I.
      apply H1.
  - dependent destruction H0; destruct a; simpl in H; inversion H.
    inversion H1; subst; destruct a'; simpl in H2; inversion H2; try inversion H0.
    apply PBSTEP3_APP4.
  - dependent destruction H1;
    inversion H2; subst; destruct a'; simpl in H1; inversion H1; subst;
    try inversion H;
    apply PBSTEP3_THROW.
  - dependent destruction H0;
    inversion H1; subst.
    + eapply PBSTEP3_IF.
      eapply IHStep3.
      reflexivity.
      apply H8.
      apply H9.
    + eapply PBSTEP3_IF.
      eapply IHStep3.
      reflexivity.
      eapply PBREFL3_V.
      instantiate (1:=TAU3).
      apply I.
      apply H1.
    + eapply PBSTEP3_IF.
      eapply IHStep3.
      reflexivity.
      eapply PBREFL3_V.
      instantiate (1:=TAU3).
      apply I.
      apply H1.
    + inversion H0; subst.
      eapply PBSTEP3_IF.
      eapply IHStep3.
      reflexivity.
      eapply PBREFL3_ERR.
      reflexivity.
      apply I.
      eapply PBREFL3_ERR.
      reflexivity.
      apply I.
  - dependent destruction H0; destruct a; simpl in H; inversion H.
    destruct a'; eapply PBSTEP3_IFTRUE; apply H1.
  - dependent destruction H0; destruct a; simpl in H; inversion H.
    destruct a'; eapply PBSTEP3_IFFALSE; apply H1.
  - dependent destruction H0;
    inversion H1; subst.
    + eapply PBSTEP3_EQ1.
      eapply IHStep3.
      reflexivity.
      apply H7.
      apply H8.
    + eapply PBSTEP3_EQ1.
      eapply IHStep3.
      reflexivity.
      eapply PBREFL3_V.
      instantiate (1:=TAU3).
      apply I.
      apply H1.
    + eapply PBSTEP3_EQ1.
      eapply IHStep3.
      reflexivity.
      eapply PBREFL3_V.
      instantiate (1:=TAU3).
      apply I.
      apply H1.
    + eapply PBSTEP3_EQ1.
      eapply IHStep3.
      reflexivity.
      eapply PBREFL3_V.
      instantiate (1:=TAU3).
      apply I.
      apply H1.
    + inversion H0; subst.
      eapply PBSTEP3_EQ1.
      eapply IHStep3.
      reflexivity.
      eapply PBREFL3_ERR.
      reflexivity.
      apply I.
      eapply PBREFL3_ERR.
      reflexivity.
      apply I.
  - dependent destruction H0;
    inversion H1; subst.
    + eapply PBSTEP3_EQ2.
      eapply IHStep3.
      reflexivity.
      apply H7.
      apply H8.
    + eapply PBSTEP3_EQ2.
      eapply IHStep3.
      reflexivity.
      eapply PBREFL3_V.
      instantiate (1:=TAU3).
      apply I.
      apply H1.
    + eapply PBSTEP3_EQ2.
      eapply IHStep3.
      reflexivity.
      eapply PBREFL3_V.
      instantiate (1:=TAU3).
      apply I.
      apply H1.
    + inversion H0; subst.
      eapply PBSTEP3_EQ2.
      eapply IHStep3.
      reflexivity.
      eapply PBREFL3_ERR.
      reflexivity.
      apply I.
      eapply PBREFL3_ERR.
      reflexivity.
      apply I.
  - dependent destruction H1; destruct a; simpl in H0; inversion H0.
    inversion H2; subst; destruct a'; simpl in H1; inversion H1; try inversion H.
    apply PBSTEP3_EQ; reflexivity.
  - dependent destruction H1; destruct a; simpl in H0; inversion H0.
    inversion H2; subst; destruct a'; simpl in H3; inversion H3; try inversion H1.
    apply PBSTEP3_EQN. apply H.
  - dependent destruction H0; destruct a; simpl in H; inversion H.
    inversion H1; subst; destruct a'; simpl in H2; inversion H2; try inversion H0.
    apply PBSTEP3_CATCH_V.
  - dependent destruction H0; destruct a; simpl in H; inversion H.
    apply PBSTEP3_CATCH_ERR.
    apply H1.
  - inversion H3; subst;
    destruct l; destruct p; destruct p; destruct u;
    destruct e; destruct d; dependent destruction H2.
    + eapply PBSTEP3_CATCH.
      eapply IHStep3.
      reflexivity.
      apply PBREFL3_V.
      instantiate (1:=TAU3).
      apply I.
      apply PBSTEP3_CATCH_V.
    + eapply single_abr_ter_refocus in H.
      eapply PBSTEP3_CATCH.
      apply H.
      eapply PBSTEP3_CATCH_ERR.
      apply H11.
    + eapply PBSTEP3_CATCH.
      eapply IHStep3.
      reflexivity.
      apply H11.
      apply H12.
Qed.

Theorem refocus_complete :
  forall e l e',
    Trans3 e l e' ->
    (is_val3 e' = true \/ is_abr_ter3 l = true) ->
    PBStep3 e l e'.
Proof.
  induction 1; intros.
  - eapply pb_step_prepend.
    apply H.
    apply IHTrans3.
    inversion H1.
    left.
    apply H2.
    destruct a'; inversion H2.
    right; destruct a; reflexivity.
  - inversion H.
    + destruct e; inversion H0.
      apply PBREFL3_V.
      destruct a.
      apply I.
      simpl; reflexivity.
    + destruct a; inversion H0.
      eapply PBREFL3_ERR.
      reflexivity.
      apply I.
Qed.