Require Export Coq.Lists.List
               Coq.Arith.EqNat.

Definition Identifier := nat.

Inductive Val :=
| NAT : nat -> Val
| CLO : Identifier ->
        Trm ->
        list (Identifier * Val) ->
        Val
with Trm :=
| VAR : Identifier ->
        Trm
| APP : Trm ->
        Trm ->
        Trm
| ABS : Identifier ->
        Trm ->
        Trm
| V : Val ->
        Trm.

Definition Env := list (Identifier * Val).

Fixpoint map_lookup (m : list (Identifier * Val))
                    (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 (m : list (Identifier * Val))
                    (i : Identifier)
                    (v : Val) :=
  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.

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

Definition Label := (Env * Div * unit)%type.

Definition get_env (l : Label) : Env :=
  match l with
    | (e, d, _) => e
  end.

Definition get_div (l : Label) : Div :=
  match l with
    | (_, d, _) => d
  end.

Definition replace_env (l : Label) (e : Env) : Label :=
  match l with
    | (e', d, tail) => (e, d, tail)
  end.

Definition replace_div (l : Label) (d : Div) : Label :=
  match l with
    | (e, d', tail) => (e, d, tail)
  end.

Definition unobs_label (l : Label) : bool :=
  match l with
    | (e, DNARROW, _) => true
    | (e, UPARROW, _) => false
  end.

Inductive Step : Trm -> Label -> Trm -> Prop :=
| STEP_VAR x l v :
    unobs_label l = true ->
    map_lookup (get_env l) x = Some v ->
    Step (VAR x) l (V v)
| STEP_ABS x t l :
    unobs_label l = true ->
    Step (ABS x t) l (V (CLO x t (get_env l)))
| STEP_APP1 t1 t2 t1' l :
    Step t1 l t1' ->
    Step (APP t1 t2) l (APP t1' t2)
| STEP_APP2 v1 t2 l t2' :
    Step t2 l t2' ->
    Step (APP (V v1) t2) l (APP (V v1) t2')
| STEP_APP3 x t t' rho v2 l :
    Step t (replace_env l (map_update rho x v2)) t' ->
    Step (APP (V (CLO x t rho)) (V v2)) l (APP (V (CLO x t' rho)) (V v2))
| STEP_APP4 x v rho v2 l :
    unobs_label l = true ->
    Step (APP (V (CLO x (V v) rho)) (V v2)) l (V v).

Hint Constructors Step.

Inductive Trans : Trm -> Label -> Trm -> Prop :=
| TRANS t1 e1 e2 env :
    Step t1 (env, DNARROW, tt) e1 ->
    Trans e1 (env, DNARROW, tt) e2 ->
    Trans t1 (env, DNARROW, tt) e2
| REFL t l :
    unobs_label l = true ->
    Trans t l t.

CoInductive co_Trans : Trm -> Label -> Trm -> Prop :=
| co_TRANS t1 e1 e2 env :
    Step t1 (env, DNARROW, tt) e1 ->
    co_Trans e1 (env, DNARROW, tt) e2 ->
    co_Trans t1 (env, DNARROW, tt) e2
| co_REFL t l :
    unobs_label l = true ->
    co_Trans t l t.

Hint Constructors Trans.
Hint Constructors co_Trans.

Example test_var :
  exists v,
    Step (VAR 0) ((0, NAT 42) :: nil, DNARROW, tt) (V v).
Proof.
  eexists; apply STEP_VAR; simpl; eauto.
Qed.

Example test_lambda_id :
  exists v,
    Trans (APP (ABS 0 (VAR 0)) (V (NAT 42)))
          (nil, DNARROW, tt)
          (V v).
Proof.
  eexists; eapply TRANS; auto.
  eapply TRANS.
  apply STEP_APP3.
  simpl.
  apply STEP_VAR; simpl; auto.
  eapply TRANS.
  apply STEP_APP4; auto.
  auto.
Qed.