Require Import Metalib.Metatheory.

Inductive term : Type :=
| BVar (_: nat)
| Var (x: atom)
| Let (t1: term) (t2: term)
| Lam (t: term)
| App (t1: term) (t2: term)
| Unit: term
| Pair (t1: term) (t2: term)
| Fst (t: term)
| Snd (t: term)
| InjL (t: term)
| InjR (t: term)
| Match (t: term) (t1: term) (t2: term)
.

Fixpoint subst (u:term) (y:atom) (t:term) : term :=
  match t with
  | BVar n ⇒ BVar n
  | Var x ⇒ if x == y then u else Var x
  | Let t1 t2 ⇒ Let (subst u y t1) (subst u y t2)
  | Lam t ⇒ Lam (subst u y t)
  | App t1 t2 ⇒ App (subst u y t1) (subst u y t2)
  | Unit ⇒ Unit
  | Pair t1 t2 ⇒ Pair (subst u y t1) (subst u y t2)
  | Fst t ⇒ Fst (subst u y t)
  | Snd t ⇒ Snd (subst u y t)
  | InjL t ⇒ InjL (subst u y t)
  | InjR t ⇒ InjR (subst u y t)
  | Match t t1 t2 ⇒ Match (subst u y t) (subst u y t1) (subst u y t2)
end.

Fixpoint fv (t:term) : atoms :=
  match t with
  | BVar _ ⇒ {}
  | Var x ⇒ {{x}}
  | Let t1 t2 ⇒ fv t1 `union` fv t2
  | Lam t ⇒ fv t
  | App t1 t2 ⇒ fv t1 `union` fv t2
  | Unit ⇒ {}
  | Pair t1 t2 ⇒ fv t1 `union` fv t2
  | Fst t ⇒ fv t
  | Snd t ⇒ fv t
  | InjL t ⇒ fv t
  | InjR t ⇒ fv t
  | Match t t1 t2 ⇒ fv t `union` fv t1 `union` fv t2
end.

Fixpoint open_rec (k:nat) (u:term) (e:term) {struct e}: term :=
  match e with
  | BVar n ⇒
    match lt_eq_lt_dec n k with
    | inleft (left _) ⇒ BVar n
    | inleft (right _) ⇒ u
    | inright _ ⇒ BVar (n - 1)
    end
  | Var x ⇒ Var x
  | Let t1 t2 ⇒ Let (open_rec k u t1) (open_rec (S k) u t2)
  | Lam t ⇒ Lam (open_rec (S k) u t)
  | App t1 t2 ⇒ App (open_rec k u t1) (open_rec k u t2)
  | Unit ⇒ Unit
  | Pair t1 t2 ⇒ Pair (open_rec k u t1) (open_rec k u t2)
  | Fst t ⇒ Fst (open_rec k u t)
  | Snd t ⇒ Snd (open_rec k u t)
  | InjL t ⇒ InjL (open_rec k u t)
  | InjR t ⇒ InjR (open_rec k u t)
  | Match t t1 t2 ⇒ Match (open_rec k u t) (open_rec (S k) u t1) (open_rec (S k) u t2)
end.

Definition open e u := open_rec 0 u e.

Module Notations.
Declare Scope term_scope.
Notation "[ z ~> u ] e" := (subst u z e) (at level 0) : term_scope.
Notation "e ^ x" := (open e (Var x)) : term_scope.
End Notations.
Import Notations.
Open Scope term_scope.

Inductive lc : term → Prop :=
| lc_Var : ∀ (x:atom),
    lc (Var x)
| lc_Let : ∀ (t1 t2:term),
    lc t1 →
    (∀ x , lc (t2 ^ x)) →
    lc (Let t1 t2)
| lc_Lam : ∀ (t:term),
    (∀ x , lc (t ^ x)) →
    lc (Lam t)
| lc_App : ∀ (t1 t2:term),
    lc t1 →
    lc t2 →
    lc (App t1 t2)
| lc_Unit :
    lc Unit
| lc_Pair : ∀ (t1 t2:term),
    lc t1 →
    lc t2 →
    lc (Pair t1 t2)
| lc_Fst : ∀ (t:term),
    lc t →
    lc (Fst t)
| lc_Snd : ∀ (t:term),
    lc t →
    lc (Snd t)
| lc_InjL : ∀ (t:term),
    lc t →
    lc (InjL t)
| lc_InjR : ∀ (t:term),
    lc t →
    lc (InjR t)
| lc_Match : ∀ (t t1 t2:term),
    lc t →
    (∀ x , lc (t1 ^ x)) →
    (∀ x , lc (t2 ^ x)) →
    lc (Match t t1 t2)
.

Fixpoint is_value (t : term) : Prop :=
  match t with
  | Lam _ ⇒ True
  | Unit ⇒ True
  | Pair t1 t2 ⇒ is_value t1 ∧ is_value t2
  | InjL t ⇒ is_value t
  | InjR t ⇒ is_value t
  | _ ⇒ False
  end.

Fixpoint is_extended_value (t: term) : Prop :=
  match t with
  | BVar _ ⇒ False
  | Var _ | Lam _ | Unit ⇒ True
  | Pair t1 t2 ⇒ is_extended_value t1 ∧ is_extended_value t2
  | InjL t | InjR t ⇒ is_extended_value t
  | Let _ _ | App _ _ | Fst _ | Snd _ | Match _ _ _ ⇒ False
  end.

Inductive step : term → term → Prop :=
 | step_App_beta : ∀ t1 t2,
     is_value t2 →
     step (App (Lam t1) t2) (open t1 t2)
 | step_App_left : ∀ t1 t2 t1',
     step t1 t1' →
     step (App t1 t2) (App t1' t2)
 | step_App_right : ∀ t1 t2 t2',
     is_value t1 →
     step t2 t2' →
     step (App t1 t2) (App t1 t2')
 | step_Let_beta_v : ∀ t1 t2,
     is_value t1 →
     step (Let t1 t2) (open t2 t1)
 | step_Let_left : ∀ t1 t2 t1',
     step t1 t1' →
     step (Let t1 t2) (Let t1' t2)
| step_Pair_Fst : ∀ t1 t2,
    is_value t1 →
    is_value t2 →
    step (Fst (Pair t1 t2)) t1
| step_Pair_Snd : ∀ t1 t2,
    is_value t1 →
    is_value t2 →
    step (Snd (Pair t1 t2)) t2
| step_Pair_left : ∀ t1 t2 t1',
    step t1 t1' →
    step (Pair t1 t2) (Pair t1' t2)
| step_Pair_right : ∀ t1 t2 t2',
    is_value t1 →
    step t2 t2' →
    step (Pair t1 t2) (Pair t1 t2')
| step_Fst : ∀ t t',
    step t t' →
    step (Fst t) (Fst t')
| step_Snd : ∀ t t',
    step t t' →
    step (Snd t) (Snd t')
| step_InjL : ∀ t t',
    step t t' →
    step (InjL t) (InjL t')
| step_InjR : ∀ t t',
    step t t' →
    step (InjR t) (InjR t')
| step_Match_InjL: ∀ t t1 t2,
    is_value t →
    step (Match (InjL t) t1 t2) (open t1 t)
| step_Match_InjR: ∀ t t1 t2,
    is_value t →
    step (Match (InjR t) t1 t2) (open t2 t)
| step_Match: ∀ t t' t1 t2,
    step t t' →
    step (Match t t1 t2) (Match t' t1 t2)
.

Hint Constructors step lc : core.

Lemma subst_refl x t: subst (Var x) x t = t.
Proof.
  induction t; simpl; f_equal; auto.
  destruct (x0 == x); congruence.
Qed.

Require Relations.Relation_Operators.

Definition steps: relation term :=
  Relations.Relation_Operators.clos_refl_trans_1n _ step.

Definition eval t v :=
  steps t v ∧ is_value v.

Definition good_value (v: term) : Prop :=
  lc v
  ∧ is_value v
  ∧ fv v [<=] empty.

Lemma good_value_lc v: good_value v → lc v.
Proof.
  unfold good_value. tauto.
Qed.
Hint Resolve good_value_lc : core.

Lemma good_value_value v: good_value v → is_value v.
Proof.
  unfold good_value. tauto.
Qed.
Hint Resolve good_value_value : core.

Lemma good_value_closed v: good_value v → fv v [<=] empty.
Proof.
  unfold good_value. tauto.
Qed.
Hint Resolve good_value_closed : core.