(************************************************************
* Correctness of the encoding of exceptions into sums       *
* verified using combined great-step semantics              *
*************************************************************)

Set Implicit Arguments.
Require Import LibVar Common.


(************************************************************)
(* * Definition of the language *)

(** Grammar of values and terms *)

Inductive val : Type :=
  | val_int : int -> val
  | val_abs : var -> trm -> val
  | val_inj : bool -> val -> val

with trm : Type :=
  | trm_val : val -> trm
  | trm_var : var -> trm
  | trm_abs : var -> trm -> trm
  | trm_app : trm -> trm -> trm
  | trm_inj : bool -> trm -> trm
  | trm_case : trm -> trm -> trm -> trm
  | trm_try : trm -> trm -> trm
  | trm_raise : trm -> trm.

Coercion trm_val : val >-> trm.
Implicit Types v : val.
Implicit Types t : trm.

(** Substitution *)

Fixpoint subst (x:var) (v:val) (t:trm) : trm :=
  let s := subst x v in
  match t with
  | trm_val v1 => trm_val v1
  | trm_var y => If x = y then v else t
  | trm_abs y t3 => trm_abs y (If x = y then t3 else s t3)
  | trm_app t1 t2 => trm_app (s t1) (s t2)  
  | trm_inj b t1 => trm_inj b (s t1)
  | trm_case t1 t2 t3 => trm_case (s t1) (s t2) (s t3)
  | trm_try t1 t2 => trm_try (s t1) (s t2)
  | trm_raise t1 => trm_raise (s t1)
  end.

(** Output of an evaluation *)

Inductive res :=
  | res_ret : val -> res
  | res_exn : val -> res.

Inductive out :=
  | out_ter : nat -> res -> out
  | out_div : out.

Coercion res_ret : val >-> res.
Implicit Types o : out.

(** Grammar of extended terms *)

Inductive ext : Type :=
  | ext_trm : trm -> ext
  | ext_app_1 : out -> trm -> ext
  | ext_app_2 : val -> out -> ext
  | ext_inj_1 : bool -> out -> ext
  | ext_case_1 : out -> trm -> trm -> ext
  | ext_try_1 : out -> trm -> ext
  | ext_raise_1 : out -> ext.

Coercion ext_trm : trm >-> ext.
Implicit Types e : ext.

(** Non-regular behaviors *)

Inductive abort : out -> Prop :=
  | abort_exn : forall n v, 
     abort (out_ter n (res_exn v))
  | abort_div : 
     abort out_div.

(** Partial order on the outcomes *)

Implicit Types n : nat.

Inductive faster : binary out :=
  | faster_ter : forall n n' r r',
      n < n' ->
      faster (out_ter n r) (out_ter n' r')
  | faster_div : forall o,
      faster o out_div.

Inductive before : binary out :=
  | before_ter : forall n n' r,
      n < n' ->
      before (out_ter n r) (out_ter n' r)
  | before_div : 
      before out_div out_div.

Definition faster_before o1 o2 o :=
  before o2 o /\ faster o1 o.

(** Semantics *)

CoInductive red : ext -> out -> Prop :=
  | red_val : forall n v,
      red v (out_ter n v)
  | red_abs : forall n x t,
      red (trm_abs x t) (out_ter n (val_abs x t))
  | red_app : forall o1 o2 o t1 t2,
      red t1 o1 -> 
      red (ext_app_1 o1 t2) o2 -> 
      faster_before o1 o2 o ->
      red (trm_app t1 t2) o
  | red_app_1_abort : forall o1 o t2,
      abort o1 ->
      before o1 o ->
      red (ext_app_1 o1 t2) o
  | red_app_1 : forall o2 o3 o n v1 t2,
      red t2 o2 -> 
      red (ext_app_2 v1 o2) o3 -> 
      faster_before o2 o3 o ->
      red (ext_app_1 (out_ter n v1) t2) o
  | red_app_2_abort : forall o2 v1 o,
      abort o2 ->
      before o2 o ->
      red (ext_app_2 v1 o2) o
  | red_app_2 : forall o3 o n x t3 v2,
      red (subst x v2 t3) o3 -> 
      before o3 o ->
      red (ext_app_2 (val_abs x t3) (out_ter n v2)) o
  | red_inj : forall o1 o2 b t1 o,
      red t1 o1 ->
      red (ext_inj_1 b o1) o2 ->
      faster_before o1 o2 o ->
      red (trm_inj b t1) o
  | red_inj_1_abort : forall o1 b o,
      abort o1 ->
      before o1 o ->
      red (ext_inj_1 b o1) o
  | red_inj_1 : forall n b v1,
      red (ext_inj_1 b (out_ter n v1)) (out_ter n (val_inj b v1))
  | red_case : forall o1 o2 t1 t2 t3 o,
      red t1 o1 -> 
      red (ext_case_1 o1 t2 t3) o2 -> 
      faster_before o1 o2 o ->
      red (trm_case t1 t2 t3) o
  | red_case_1_abort : forall o1 t2 t3 o,
      abort o1 ->
      before o1 o ->
      red (ext_case_1 o1 t2 t3) o
  | red_case_1_true : forall o1 n v1 t2 t3 o,
      red (trm_app t2 v1) o1 -> 
      before o1 o ->
      red (ext_case_1 (out_ter n (val_inj true v1)) t2 t3) o
  | red_case_1_false : forall o1 n v1 t2 t3 o,
      red (trm_app t3 v1) o1 -> 
      before o1 o ->
      red (ext_case_1 (out_ter n (val_inj false v1)) t2 t3) o
  | red_try : forall o1 o2 t1 t2 o,
      red t1 o1 -> 
      red (ext_try_1 o1 t2) o2 -> 
      faster_before o1 o2 o ->
      red (trm_try t1 t2) o
  | red_try_1_val : forall n v1 t2,
      red (ext_try_1 (out_ter n v1) t2) (out_ter n v1)
  | red_try_1_exn : forall o1 n v1 t2 o,
      red (trm_app t2 v1) o1 -> 
      before o1 o ->
      red (ext_try_1 (out_ter n (res_exn v1)) t2) o
  | red_try_1_div : forall t2,
      red (ext_try_1 out_div t2) out_div
  | red_raise : forall o1 o2 t1 o,
      red t1 o1 ->
      red (ext_raise_1 o1) o2 ->
      faster_before o1 o2 o ->
      red (trm_raise t1) o
  | red_raise_1_abort : forall o1 o,
      abort o1 ->
      before o1 o ->
      red (ext_raise_1 o1) o
  | red_raise_1 : forall n v1,
      red (ext_raise_1 (out_ter n v1)) (out_ter n (res_exn v1)).

Definition reds e r := exists n, red e (out_ter n r).

Definition divs e := red e out_div.


(************************************************************)
(* * Specific lemmas for reasoning on sets of variables *)

Lemma notin_remove : forall A x (E F:fset A),
  x \notin (E \- F) = (x \notin E \/ x \in F).
Proof.
  intros. unfolds notin. rewrite in_remove.
  unfolds notin. rew_logic*.
Qed.

Lemma notin_remove_l : forall A x (E F:fset A),
  x \notin (E \- F) -> x \notin E \/ x \in F.
Proof. introv H. rewrite~ notin_remove in H. Qed.

Lemma notin_remove_r : forall A x (E F:fset A),
  (x \notin E \/ x \in F) -> x \notin (E \- F).
Proof. introv H. rewrite~ notin_remove. Qed.

Lemma notin_remove_inv : forall A x (E F:fset A),
  x \notin (E \- F) -> x \notin F -> x \notin E.
Proof. introv H1 H2. destruct~ (notin_remove_l H1). false. Qed.

Lemma notin_remove_weaken : forall E F (x:var),
  x \notin E ->
  x \notin (E \- F).
Proof. intros. applys~ notin_remove_r. Qed.

Lemma notin_to_fresh : forall xs n E F,
  fresh E n xs -> 
  (forall x, x \notin E -> x \notin F) ->
  fresh F n xs.
Proof.
  induction xs; introv Fr H.
  auto.
  destruct n. false. simpls. destruct Fr.
   split~. applys* IHxs.
Qed. 

Lemma fresh_remove_weaken : forall E F n xs,
  fresh E n xs ->
  fresh (E \- F) n xs.
Proof.
  intros. applys* notin_to_fresh. applys* notin_remove_weaken.
Qed.

Lemma remove_self : forall A (E:fset A),
  E \- E = \{}.
Proof.
  intros. applys fset_extens; intros x H.
  rewrite in_remove in H. false*.
  rewrite in_empty in H. false.
Qed.

Lemma union_remove : forall A (E F:fset A),
  (forall x, x \in E -> x \notin F) ->
  (E \u F) \- F = E.
Proof.
  introv M. applys fset_extens; intros x H.
  rewrite in_remove, in_union in H. destruct H as [[?|?] ?].
    auto.
    false*.
  rewrite in_remove, in_union. auto.
Qed.

Lemma union_remove' : forall A (E F:fset A),
  (forall x, x \in E -> x \notin F) ->
  (F \u E) \- F = E.
Proof.
  introv M. applys fset_extens; intros x H.
  rewrite in_remove, in_union in H. destruct H as [[?|?] ?].
    false*.
    auto.
  rewrite in_remove, in_union. auto.
Qed.

Hint Rewrite union_empty_l union_empty_r remove_self : fset_simpl.
Ltac fset_simpl := autorewrite with fset_simpl.

Lemma notin_elim_single : forall A (y:A) (E:fset A),
  y \notin E ->
 (forall x, x \in E -> x \notin \{y}).
Proof.
  introv H M. rewrite notin_singleton. intro_subst. false.
Qed.

Lemma notin_remove_single_inv : forall A x y (E:fset A),
  x \notin (E \- \{y}) -> x <> y -> x \notin E.
Proof.
  introv H1 H2. applys* notin_remove_inv. 
  rewrite~ notin_singleton. 
Qed.


(************************************************************)
(* * Facts *)

Hint Constructors abort red faster before.
Hint Extern 1 (_ < _) => abstracts math.
Hint Extern 1 (_ <= _) => abstracts math.

(** Update of indices *)

Definition map f o :=
  match o with
  | out_ter n v => out_ter (f n) v
  | out_div => out_div 
  end.

Definition add d o := map (fun n => (n+d)%nat) o.

(** Properties of partial order *)

Lemma faster_le_l : forall o n n' b,
  faster o (out_ter n b) -> n <= n' -> faster o (out_ter n' b).
Proof. introv O L. inverts* O. Qed.

Lemma before_le_l : forall o n n' b,
  before o (out_ter n b) -> n <= n' -> before o (out_ter n' b).
Proof. introv O L. inverts* O. Qed.

Lemma faster_before_le_l : forall o1 o2 n n' b,
  faster_before o1 o2 (out_ter n b) -> n <= n' -> 
  faster_before o1 o2 (out_ter n' b).
Proof.  
  hint faster_le_l, before_le_l.
  unfold faster_before. introv [O1 O2] L. split*. 
Qed.

Hint Resolve faster_before_le_l.

(** Automation for the partial order *)

Lemma faster_succ : forall n b,
  faster (out_ter n b) (out_ter (S n) b).
Proof. intros. auto. Qed.

Lemma before_succ : forall n b,
  before (out_ter n b) (out_ter (S n) b).
Proof. intros. auto. Qed.

Lemma before_succ' : forall o,
  before o (map S o).
Proof. intros. destruct o; simple~. Qed.

Lemma before_add : forall n m o,
  n < m -> 
  before (add n o) (add m o).
Proof. intros. destruct o; simple~. Qed.

Lemma before_pred : forall n v,
  O < n ->
  before (out_ter (n-1) v) (out_ter n v).
Proof. auto. Qed.

Lemma faster_pred : forall n v,
  O < n ->
  faster (out_ter (n-1) v) (out_ter n v).
Proof. auto. Qed.

Lemma before_map_le : forall (f g:nat->nat) o1 o2,
  before (map g o1) o2 -> (forall n, f n <= g n) ->
  before (map f o1) o2.
Proof.
  introv B L. destruct o1; inverts B; simple.
  specializes L n. constructor. math.
  auto.
Qed.

Definition monotone (f:nat->nat) :=
  forall n1 n2, n1 < n2 -> f n1 < f n2.

Lemma faster_map : forall f o1 o2,
  monotone f -> faster o1 o2 -> faster (map f o1) (map f o2).
Proof.
  introv M F. inverts F as.
  introv H. constructor. forwards~: M n n'.
  constructor.
Qed.

Hint Resolve before_pred.
Hint Extern 1 (before _ _) => apply before_succ.
Hint Extern 1 (before _ _) => apply before_succ'.
Hint Extern 1 (faster _ _) => apply faster_succ.
Hint Extern 3 (faster_before _ _ _) => split.

Lemma faster_before_zero : forall o1 o2 v,
  before o1 o2 ->
  faster_before (out_ter O v) o1 o2.
Proof. intros. inverts H; simple*. Qed.

Lemma faster_before_zero_succ : forall o1 v,
  faster_before (out_ter O v) o1 (map S o1).
Proof. intros. apply~ faster_before_zero. Qed.

(** Additional automation *)

Lemma faster_before_max : forall n1 n2 b1 b2,
  faster_before (out_ter n1 b1) (out_ter n2 b2) 
                (out_ter (S (max n1 n2)) b2).
Proof. 
  intros. forwards [[? ?]|[? ?]]: max_cases n1 n2; split~. 
Qed.

Ltac max_resolve :=
  simpl; match goal with |- context [max ?n1 ?n2] =>
    let e := fresh "m" in
    destruct (max_cases n1 n2) as [[? ?]|[? ?]];
    set (e := max n1 n2) in *; clearbody e end.

Hint Resolve faster_before_max.
Hint Extern 1 (before _ _) => (abstracts max_resolve); constructor.
Hint Extern 1 (faster_before _ _ _) => apply faster_before_max.


(************************************************************)
(* * Derived reduction rules *)

Lemma red_inj_val : forall b v1,
   red (trm_inj b v1) (out_ter 1 (val_inj b v1)).
Proof.
  intros. applys* red_inj.
Defined.

Lemma red_abs_beta : forall o1 o x t3 v2,
   red (subst x v2 t3) o1 ->
   before (add 2 o1) o ->
   red (trm_app (trm_abs x t3) v2) o.
Proof.
  introv R B. applys red_app. auto.
  applys red_app_1. auto. 
  applys red_app_2 R. apply before_succ'.
  apply faster_before_zero_succ.
  apply faster_before_zero.
  clear R. (* required for guard condition *)
  destruct o1; inverts B; simple~.
Defined.

Lemma red_abs_beta' : forall o1 o x t3 v2,
   red (subst x v2 t3) o1 ->
   before (add 2 o1) o ->
   red (trm_app (val_abs x t3) v2) o.
Proof.
  introv R B. applys red_app. auto.
  applys red_app_1. auto. 
  applys red_app_2 R. apply before_succ'.
  apply faster_before_zero_succ.
  apply faster_before_zero.
  clear R. (* required for guard condition *) 
  destruct o1; inverts B; simple~.
Defined.


(************************************************************)
(* * Freshness *)

(** Two modes for freshness: "not used" and "not free" *)

Inductive vars_opt := not_used | not_free.

Definition add_bound f E (x:var) :=
  match f with 
  | not_used => E \u \{x}
  | not_free => E \- \{x}
  end.

Lemma notin_add_bound : forall x f y E,
  x \notin add_bound f E y ->
  x \notin E \- \{y}.
Proof.
  intros. destruct f; simpls.
  applys~ notin_remove_weaken.
  auto.
Qed.

(** Set of free variables and used variables *)

Fixpoint trm_vars (f:vars_opt) (t:trm) : vars :=
  let r := trm_vars f in
  match t with
  | trm_val v1 => val_vars f v1
  | trm_var x => \{x}
  | trm_abs x t1 => add_bound f (r t1) x
  | trm_app t1 t2 => (r t1) \u (r t2)
  | trm_inj b t1 => (r t1)
  | trm_case t1 t2 t3 => (r t1) \u (r t2) \u (r t3)
  | trm_try t1 t2 => (r t1) \u (r t2)
  | trm_raise t1 => (r t1)
  end 

with val_vars (f:vars_opt) (v:val) : vars :=
  match v with
  | val_int n => \{}
  | val_abs x t1 => add_bound f (trm_vars f t1) x
  | val_inj b v1 => val_vars f v1
  end.

Definition res_vars (f:vars_opt) (r:res) := 
  match r with
  | res_ret v => trm_vars f v
  | res_exn v => trm_vars f v
  end.

Definition out_vars (f:vars_opt) (o:out) :=
  match o with
  | out_ter n r => res_vars f r
  | out_div => \{}
  end.

Definition ext_vars (f:vars_opt) (e:ext) :=
  let trm_vars := trm_vars f in
  let out_vars := out_vars f in
  match e with
  | ext_trm t1 => trm_vars t1 
  | ext_app_1 o1 t1 => out_vars o1 \u trm_vars t1
  | ext_app_2 v1 o2 => trm_vars v1 \u out_vars o2
  | ext_inj_1 b o1 => out_vars o1
  | ext_case_1 o1 t2 t3 => out_vars o1 \u trm_vars t2 \u trm_vars t3
  | ext_try_1 o1 t2 => out_vars o1 \u trm_vars t2
  | ext_raise_1 o1 => out_vars o1
  end.

(** Substitution is the identity function on fresh vars *)

Lemma subst_id : forall f x v t, 
  x \notin trm_vars f t -> 
  subst x v t = t. 
Proof.
  induction t; introv F; simpls; fequals~.
  case_if*. notin_false.
  case_if*. applys IHt. destruct f; simpls~.
   applys~ notin_remove_inv F.
Qed.
  
Lemma subst_notin : forall t x y v,
  x \notin (trm_vars not_used t) ->
  x \notin (val_vars not_used v) ->
  x \notin (trm_vars not_used (subst y v t)).
Proof. induction t; introv Frt Frv; simpls~; try case_if*. Qed.

Lemma fresh_subst : forall xs n t y v,
  fresh (trm_vars not_used t) n xs ->
  fresh (val_vars not_used v) n xs ->
  fresh (trm_vars not_used (subst y v t)) n xs.
Proof. 
  induction xs; introv Frt Frv.
  auto.
  destruct n. false. simpls. 
   destruct Frt. destruct Frv.
   hint subst_notin. auto.
Qed.

(** Reduction of terms does not introduce new variables *)

Hint Extern 1 (_ \notin ext_vars _ _) => unfold ext_vars.

Lemma notin_red : forall n x e r,
  red e (out_ter n r) ->
  x \notin ext_vars not_used e ->
  x \notin res_vars not_used r.
Proof.
  induction n using peano_induction. introv R F. 
  asserts IH: (forall e m r, red e (out_ter m r) -> 
    m < n -> x \notin ext_vars not_used e ->
    x \notin res_vars not_used r).
    intros. applys* H. clear H.    
  inverts R as; simpls.
  auto.
  auto.
  introv R1 R2 [L2 L1]. inverts L1. inverts L2.
   forwards~: IH R1. forwards~: IH R2.
  introv A B. inverts B. simpls~.
  introv R1 R2 [L2 L1]. inverts L1. inverts L2.
   forwards~: IH R1. forwards~: IH R2. simpls~.
  introv A B. inverts B. simpls~.
  introv R1 B. inverts B. forwards~: IH R1. simpls.
   applys~ subst_notin. 
  introv R1 R2 [L2 L1]. inverts L1. inverts L2.
   forwards~: IH R1. forwards~: IH R2.
  introv A B. inverts B. simpls~.
  auto.
  introv R1 R2 [L2 L1]. inverts L1. inverts L2.
   forwards~: IH R1. forwards~: IH R2.
  introv A B. inverts B. simpls~.
  introv R1 B. inverts B. forwards~: IH R1. simpls~.
  introv R1 B. inverts B. forwards~: IH R1. simpls~.
  introv R1 R2 [L2 L1]. inverts L1. inverts L2.
   forwards~: IH R1. forwards~: IH R2.
  auto.
  introv R1 B. inverts B. forwards~: IH R1. simpls~.
  introv R1 R2 [L2 L1]. inverts L1. inverts L2.
   forwards~: IH R1. forwards~: IH R2.
  introv A B. inverts B. simpls~.
  auto.
Qed. 

Lemma fresh_red : forall n m xs e r,
  red e (out_ter n r) ->
  fresh (ext_vars not_used e) m xs ->
  fresh (res_vars not_used r) m xs.
Proof.
  introv R Fr. applys* notin_to_fresh.
  intros. applys* notin_red.
Qed.



(************************************************************)
(* * Translation of exceptions *)

(** Variables introduced by the translation *)

Parameter x1 x2 x3 : var.
Parameter x1_neq_x2 : x1 <> x2.
Parameter x1_neq_x3 : x1 <> x3.
Parameter x2_neq_x3 : x2 <> x3.

Definition L := x1::x2::x3::nil.
Lemma L_eq : L = x1::x2::x3::nil.
Proof. auto. Defined.
Opaque L.

Hint Resolve x1_neq_x2 x2_neq_x3 x1_neq_x3.

Hint Extern 1 (_ \notin _) => rewrite L_eq in *. 

Coercion trm_var : var >-> trm.

(** Definition of the translation *)

Definition tr_ret t := trm_inj true t.
Definition tr_exn t := trm_inj false t.

Definition tr_bind t' x k :=
  trm_case t' (trm_abs x k) (trm_abs x (tr_exn (trm_var x))).

Definition tr_cont t' :=
  trm_abs x2 (tr_bind t' x3 (trm_app x3 x2)).

Fixpoint tr_trm (t:trm) : trm := 
  let s := tr_trm in
  match t with
  | trm_val v => tr_ret (tr_val v)
  | trm_var y => tr_ret t
  | trm_abs y t3 => tr_ret (trm_abs y (s t3))
  | trm_app t1 t2 => 
      tr_bind (s t1) x1 
       (tr_bind (s t2) x2 
         (trm_app x1 x2))
  | trm_inj b t1 => 
      tr_bind (s t1) x1 (tr_ret (trm_inj b x1))
  | trm_case t1 t2 t3 => 
      tr_bind (s t1) x1 
       (trm_case x1 (tr_cont (s t2)) (tr_cont (s t3)))
  | trm_try t1 t2 => 
     trm_case (s t1) (trm_abs x1 (tr_ret x1)) 
                     (tr_cont (s t2))
  | trm_raise t1 => 
      tr_bind (s t1) x1 (tr_exn x1)
  end

with tr_val (v:val) : val := 
  match v with
  | val_abs y t3 => val_abs y (tr_trm t3)
  | val_inj b v1 => val_inj b (tr_val v1)
  | _ => v
  end.

Definition tr_res (r:res) :=
  match r with
    | res_ret v => res_ret (val_inj true (tr_val v))
    | res_exn v => res_ret (val_inj false (tr_val v))
  end.

Definition tr_out (o:out) :=
  match o with
  | out_ter n r => out_ter n (tr_res r)
  | out_div => out_div
  end.

(** Distribution of substitution over the translation *)

Ltac imp x :=
  try rewrite L_eq in *;
  asserts: (x \notin \{x}); [ auto | notin_false ]. 

Ltac imp_any :=
  solve [ imp x1 | imp x2 | imp x3 ].

Ltac neq_any :=
  solve [ false x1_neq_x2; assumption
        | false x1_neq_x3; assumption
        | false x2_neq_x3; assumption ].

Ltac simpl_subst :=
  repeat (case_if; try neq_any; try imp_any).

Lemma tr_val_subst : forall x v t, 
  fresh (trm_vars not_used t \u \{x}) 3 L ->
  tr_trm (subst x v t) = subst x (tr_val v) (tr_trm t).
Proof.
  induction t; introv F; simpls.
  fequals.
  simpl_subst; fequals.
  simpl_subst; fequals. rewrite~ IHt.
  simpl_subst. rewrite~ IHt1. rewrite~ IHt2.
  simpl_subst. rewrite~ IHt.
  simpl_subst. rewrite~ IHt1.
   rewrite~ IHt2. rewrite~ IHt3.
  simpl_subst. rewrite~ IHt1. rewrite~ IHt2.
  simpl_subst. rewrite~ IHt.
Qed.

Lemma subst_tr_bind : forall t x k y v,
  x <> y ->
    subst y v (tr_bind t x k) 
  = tr_bind (subst y v t) x (subst y v k).
Proof. introv N. simpl. case_if. fequals. Qed.

Lemma subst_tr_cont : forall t y v,
  fresh (\{y}) 2 (x2::x3::nil) ->
    subst y v (tr_cont t) 
  = tr_cont (subst y v t).
Proof. introv H. simpl. simpl_subst. fequals. Qed.

Lemma tr_trm_vars : forall t,
  fresh (trm_vars not_used t) 3 L ->
  fresh (trm_vars not_free (tr_trm t)) 3 L
with tr_val_vars : forall v,
  fresh (trm_vars not_used v) 3 L ->
  fresh (trm_vars not_free (tr_val v)) 3 L.
Proof.
  (* trm *)
  induction t; introv F; simpls.
  apply~ tr_val_vars.
  auto.
  applys~ fresh_remove_weaken.
  specializes~ IHt1. specializes~ IHt2. fset_simpl.
   do 2 (rewrite union_remove; [ | apply~ notin_elim_single ]).
   auto.
  specializes~ IHt. fset_simpl. auto.
  specializes~ IHt1. specializes~ IHt2. specializes~ IHt3.
   fset_simpl.
   rewrite (@union_remove' _ \{x2}); [ | apply~ notin_elim_single ]. 
   do 2 (rewrite union_remove; [ | apply~ notin_elim_single ]).
   rewrite union_remove'; [ | apply~ notin_elim_single ].
   auto.
  specializes~ IHt1. specializes~ IHt2. fset_simpl.
   rewrite union_remove'; [ | apply~ notin_elim_single ]. 
   rewrite union_remove; [ | apply~ notin_elim_single ]. 
   auto.
  specializes~ IHt. fset_simpl. auto.
  (* val *)
  induction v; introv F; simpls.
  auto.
  applys fresh_remove_weaken. applys~ tr_trm_vars.
  auto.
Qed.

(** Auxiliary definitions, lemmas and tactics *)

Notation "'nine' n" := ((n+n+n+n+n+n+n+n+n)%nat) (at level 20).
Definition cin n := (nine n + 8)%nat.

Lemma faster_tr_out : forall o1 o2,
  faster o1 o2 -> faster (tr_out o1) (tr_out o2).
Proof. introv F. inverts F; simple~. Qed.

Ltac simpl_substs := simpl; case_if; tryfalse.

Lemma monotone_cin : monotone cin.
Proof. introv L. unfold cin. math. Qed.

Hint Resolve monotone_cin.

Lemma faster_cin_tr_out : forall o1 o2,
  faster o1 o2 ->
  faster (map cin (tr_out o1)) (map cin (tr_out o2)).
Proof. intros. applys~ faster_map; applys~ faster_tr_out. Qed.
Hint Immediate faster_cin_tr_out.

Definition correctness :=
  forall t o, red t o -> 
  fresh (trm_vars not_used t) 3 L ->
  red (tr_trm t) (map cin (tr_out o)).

Ltac done := simpl; unfolds cin; auto.

(** Verification of [tr_bind] *)

Lemma red_tr_bind_abort : forall o3 o2 o o1 t1 x k,
  correctness -> 
  red t1 o1 ->
  abort o1 -> 
  before o1 o2 ->
  before o2 o ->
  faster o1 o ->
  before (map cin (tr_out o1)) o3 ->
  fresh (trm_vars not_used t1) 3 L ->
  red (tr_bind (tr_trm t1) x k) o3.
Proof.
  introv C R A B1 B2 F1 B3 Fr. inverts A.
  inverts B1. inverts B2. inverts B3. inverts F1.
   applys red_case. applys* C.
   simpl. applys red_case_1_false.
   applys red_abs_beta. unfold tr_exn. simpl_substs.
   applys red_inj_val. auto. auto. done. 
  inverts F1. inverts B3. inverts B1. applys red_case.
   applys* C. applys* red_case_1_abort. auto.
Defined.

Lemma red_tr_bind_ret : forall o3 t1 n v1 k x1 o4,
  correctness ->
  red t1 (out_ter n v1) ->
  faster (map cin (tr_out (out_ter n v1))) o4 ->
  red (subst x1 (tr_val v1) k) o3 ->
  before (add 4 o3) o4 -> 
  fresh (trm_vars not_used t1) 3 L ->
  red (tr_bind (tr_trm t1) x1 k) o4.
Proof.
  introv C R F1 R3 B3 Fr. 
  applys red_case; [ applys* C | | eauto ].
  simpl. applys red_case_1_true (add 3 o3).
  applys red_abs_beta. eauto. 
  applys~ before_add. applys~ before_add.
Defined.

(** Verification of [tr_cont] *)

Lemma red_tr_cont : forall o2 o t v,
  correctness ->
  red (trm_app t v) o2 ->
  before (add 4 (map cin (tr_out o2))) o ->
  fresh (trm_vars not_used t) 3 L ->
  fresh (val_vars not_used v) 3 L ->
  red (trm_app (tr_cont (tr_trm t)) (tr_val v)) o.
Proof.
  introv C R B3 Frt Frv. inverts R as R1 R2 [L2 L1].
  applys red_abs_beta (add 2 (map cin (tr_out o2))).
  rewrite~ subst_tr_bind. simpl.
  simpl_subst. forwards M: tr_trm_vars Frt. auto.
  rewrite~ (@subst_id not_free). clear M.
  inverts R2 as.
    introv A B. applys red_tr_bind_abort o0; eauto.
     inverts B; inverts L2; done.
    introv R3 R4 [L4 L3]. applys* red_tr_bind_ret (map cin (tr_out o4)).
      inverts L1; done.
      inverts R3. inverts R4 as.
        introv A B. inverts A.
        introv R5 L5. simpl. case_if; tryfalse.
         applys red_abs_beta'. 
         forwards M: fresh_red R1 Frt. simpl in M. 
         rewrite~ <- tr_val_subst. 
         applys* C. applys~ fresh_subst.
         inverts L5; done.
       inverts L4; inverts L2; done.
  destruct o2; inverts B3; done.
Defined.

(** Verification of the transformation [tr_trm].
    Recall that [correctness] is define as:
    [forall t o, red t o -> red (tr_trm t) (map cin (tr_out o))] *)

Lemma tr_trm_correct : correctness.
Proof.
  cofixs IH. introv R Fr. inverts R as; simpls.
  (* case val *)
  unfolds cin. applys* red_inj.
  (* case abs *)
  unfolds cin. applys* red_inj.
  (* case app *)
  introv R1 R2 [L2 L1]. inverts R2 as. 
    introv A B. applys red_tr_bind_abort o2; eauto.
     inverts B; inverts L2; done.
    introv R3 R4 [L4 L3].
     applys* red_tr_bind_ret (add 4 (map cin (tr_out o2)));
       [ |inverts L4; inverts L2; done ].
     rewrite~ subst_tr_bind.
     rewrite (@subst_id not_free); [ | applys~ tr_trm_vars ].
     simpl. simpl_subst. inverts R4 as. 
      introv A B. applys* red_tr_bind_abort o3 o2.
         inverts B; inverts L4; done.
       introv R5 L5.
         applys* red_tr_bind_ret (add 4 (map cin (tr_out o3))).
           inverts L3; done.
           simpl. case_if; tryfalse.
           asserts~ Fr1: (fresh (trm_vars not_used t1) 3 L).
            forwards M1: fresh_red R1 Fr1. simpl in M1.
           asserts~ Fr2: (fresh (trm_vars not_used t2) 3 L).
            forwards M2: fresh_red R3 Fr2. simpl in M2.
            applys red_abs_beta'.
              rewrite <- tr_val_subst.
                applys* IH.
                applys~ fresh_subst.
                auto.
             inverts L5; inverts L4; done.  
           inverts L5; inverts L4; done.
  (* case inj *)
  introv R1 R2 [L2 L1]. inverts R2 as.
    introv A B. applys* red_tr_bind_abort.
      clear_coind. destruct o1; done. inverts B; inverts L2; done.
    applys* red_tr_bind_ret.
      simpl_substs. applys red_inj. applys red_inj_val.
      applys red_inj_1. applys faster_before_max.
      inverts L2. done.
  (* case case *)
  introv R1 R2 [L2 L1].
   asserts~ Fr1: (fresh (trm_vars not_used t1) 3 L).
   asserts~ Fr2: (fresh (trm_vars not_used t2) 3 L). inverts R2 as.
    introv A B. applys red_tr_bind_abort o2; eauto.
     inverts B; inverts L2; done.
    introv R3 L3. applys red_tr_bind_ret
      (map (fun n => (n-5)%nat) (map cin (tr_out o))); eauto;
      [| clear_coind; destruct o; done ].
     sets_eq T: tr_cont. simpl. subst. case_if;tryfalse.
     do 2 rewrite~ subst_tr_cont. 
     do 2 (rewrite (@subst_id not_free); [ | applys~ tr_trm_vars ]).
     applys red_case. applys red_val O. 
     applys red_case_1_true.
     forwards M: fresh_red R1 Fr1. simpl in M.
     applys* red_tr_cont. auto.
     inverts L2. inverts L3. inverts L1. done. inverts L3. done.
    introv R3 L3. applys red_tr_bind_ret 
      (map (fun n => (n-5)%nat) (map cin (tr_out o))); eauto;
      [| clear_coind; destruct o; done ].
     sets_eq T: tr_cont. simpl. subst. simpl_subst.
     do 2 rewrite~ subst_tr_cont.
     do 2 (rewrite (@subst_id not_free); [ | applys~ tr_trm_vars ]).
     applys red_case. applys red_val O. 
     applys red_case_1_false.
     forwards M: fresh_red R1 Fr1. simpl in M.
     applys* red_tr_cont. auto.
     inverts L2. inverts L3. inverts L1. done. inverts L3. done. 
  (* case try *)
  introv R1 R2 [L2 L1]. inverts R2 as.
  inverts L2. inverts L1. applys* red_case. simpl.
   applys red_case_1_true. applys red_abs_beta.
   simpl. case_if; tryfalse. applys red_inj_val.
   auto. auto. done.
  introv R3 L3. applys* red_case. simpl. 
   applys red_case_1_false.
   asserts~ Fr1: (fresh (trm_vars not_used t1) 3 L).
   forwards M: fresh_red R1 Fr1. simpl in M.
   applys* red_tr_cont.
   auto. inverts L3; inverts L2; inverts L1; done.
  inverts L2. applys* red_case.
  (* case raise *)
  introv R1 R2 [L2 L1]. inverts R2 as.
    introv A B. applys* red_tr_bind_abort.
      clear_coind; destruct o1; done. inverts B; inverts L2; done.
    applys* red_tr_bind_ret.
      simpl_substs. applys red_inj_val.
      inverts L2. done.
Qed. 
(* Warning: the check of the guard condition takes about 1 minute *)