Set Implicit Arguments.
Require Import LibLN LibNat.



(* ====================================================================== *)
(** ** Definitions *)

Implicit Types x y z : var.


(* ********************************************************************** *)
(** Grammar of terms *)

Inductive trm : Set :=
  | trm_bvar : nat -> trm
  | trm_fvar : var -> trm
  | trm_app  : trm -> trm -> trm
  | trm_abs  : trm -> trm.


(* ********************************************************************** *)
(** Opening *)

Fixpoint open_rec (k : nat) (u : trm) (t : trm) {struct t} : trm :=
  match t with
  | trm_bvar i    => If k = i then u else t
  | trm_fvar x    => t
  | trm_app t1 t2 => trm_app (open_rec k u t1) (open_rec k u t2)
  | trm_abs t1    => trm_abs (open_rec (S k) u t1) 
  end.

Definition open t u := open_rec 0 u t.


(* ********************************************************************** *)
(** Variable opening, defined in terms of opening *)

Definition open_var t x := open t (trm_fvar x).

Definition open_var_rec k x t := open_rec k (trm_fvar x) t.

(* ********************************************************************** *)
(** Variable closing *)

Fixpoint close_var_rec (k : nat) (z : var) (t : trm) {struct t} : trm :=
  match t with
  | trm_bvar i    => trm_bvar i 
  | trm_fvar x    => If x = z then (trm_bvar k) else t
  | trm_app t1 t2 => trm_app (close_var_rec k z t1) (close_var_rec k z t2)
  | trm_abs t1    => trm_abs (close_var_rec (S k) z t1) 
  end.

Definition close_var x t := close_var_rec 0 x t.


(* ********************************************************************** *)
(** Local closure, inductively defined *)

Inductive lc : trm -> Prop :=
  | lc_var : forall x, 
      lc (trm_fvar x)
  | lc_app : forall t1 t2,
      lc t1 -> lc t2 -> lc (trm_app t1 t2)
  | lc_abs : forall L t1,
      (forall x, x \notin L -> lc (open_var t1 x)) -> 
      lc (trm_abs t1). 

Definition body t :=
  exists L, forall x, x \notin L -> lc (open_var t x).


(* ********************************************************************** *)
(** Computation of the set of free variables *)

Fixpoint fv (t : trm) {struct t} : vars :=
  match t with
  | trm_bvar i    => \{}
  | trm_fvar x    => \{x}
  | trm_app t1 t2 => (fv t1) \u (fv t2)
  | trm_abs t1    => (fv t1)
  end.


(* ********************************************************************** *)
(** Closed terms *)

Definition closed t := 
  fv t = \{}.


(* ********************************************************************** *)
(** Substitution *)

Fixpoint subst (z : var) (u : trm) (t : trm) {struct t} : trm :=
  match t with
  | trm_bvar i    => t
  | trm_fvar x    => If x = z then u else t
  | trm_app t1 t2 => trm_app (subst z u t1) (subst z u t2)
  | trm_abs t1    => trm_abs (subst z u t1) 
  end.


(* ********************************************************************** *)
(** Size of a term *)

Fixpoint size (t : trm) {struct t} : nat :=
  match t with
  | trm_bvar i    => 1
  | trm_fvar x    => 1
  | trm_abs t1    => 1 + (size t1)
  | trm_app t1 t2 => 1 + (size t1) + (size t2)
  end.


(* ====================================================================== *)
(** ** Tactics *)

Hint Constructors lc.

(** Tactics for freshness *)

Ltac gather_vars :=
  let A := gather_vars_with (fun x : vars => x) in
  let B := gather_vars_with (fun x : var => \{ x }) in
  let C := gather_vars_with (fun x : trm => fv x) in
  constr:(A \u B \u C).

Tactic Notation "pick_fresh" ident(x) :=
  let L := gather_vars in pick_fresh_gen L x.
Tactic Notation "pick_fresh" ident(x) "from" constr(E) :=
  let L := gather_vars in pick_fresh_gen (L \u E) x.

Tactic Notation "apply_fresh" constr(T) "as" ident(x) :=
  apply_fresh_base T gather_vars x.
Tactic Notation "apply_fresh" "*" constr(T) "as" ident(x) :=
  apply_fresh T as x; auto_star.
Tactic Notation "apply_fresh" constr(T) :=
  apply_fresh_base T gather_vars ltac_no_arg.
Tactic Notation "apply_fresh" "*" constr(T) :=
  apply_fresh T; auto_star.

Tactic Notation "exists_fresh" :=
  let y := fresh "y" in let Fry := fresh "Fr" y in
  exists_fresh_gen gather_vars y Fry.

(** Tactics for comparison of indices *)

Hint Extern 1 (_ < _) => nat_math.
Hint Extern 1 (_ <= _) => nat_math.

(** Tactics for equalities between sets *)

Lemma subset_union_2p : forall E1 E2 F1 F2 G : vars,
  E1 \c (F1 \u G) -> E2 \c (F2 \u G) -> (E1 \u E2) \c ((F1 \u F2) \u G).
Proof.
  introv H1 H2. intros x. specializes H1 x. specializes H2 x.
  repeat rewrite in_union in *. auto*.
Qed.

Lemma subset_remove_11 : forall x y : var, 
  x <> y -> \{x} \c (\{x} \- \{y}).
Proof.
  introv H. intros z M. rewrite in_singleton in M. subst.
  rewrite in_remove. split. rewrite~ in_singleton. auto.
Qed.

Lemma subset_remove_2p : forall E1 E2 F1 F2 G : vars,
  E1 \c (F1 \- G) -> E2 \c (F2 \- G) -> (E1 \u E2) \c ((F1 \u F2) \- G).
Proof. introv H1 H2. forwards: subset_union_2 H1 H2. rewrite~ union_remove. Qed.

Hint Resolve subset_union_weak_l subset_union_weak_r subset_refl
  subset_union_2 subset_union_2p subset_empty_l 
  subset_remove_2p subset_remove_11 : fset.

Ltac fset := first [ auto with fset ].


(* ====================================================================== *)
(** ** Proofs *)

(* ********************************************************************** *)
(** Variable closing and variable opening are reciprocal of one another *)

(** Showing that [close_var] after [open_var] is the identity is easy *)

Lemma close_open_var : forall x t, 
  x \notin fv t -> 
  close_var x (open_var t x) = t.
Proof.
  introv. unfold open_var, open, close_var. generalize 0.
  induction t; simpl; introv Fr; fequals~.
  case_nat~. simpl. case_var~.
  case_var~.
Qed.

(** The other direction is much harder; First, we first need
    to establish the injectivity of [open_var] *)

Lemma open_var_inj : forall x t1 t2, 
  x \notin (fv t1) -> x \notin (fv t2) -> 
  (open_var t1 x = open_var t2 x) -> (t1 = t2).
Proof.
  introv Fr1 Fr2 Eq.
  rewrite~ <- (@close_open_var x t1).
  rewrite~ <- (@close_open_var x t2).
  fequals~.
Qed.

(** Another proof of the same injectivity result *)

Lemma open_var_inj_alternative : forall x t1 t2, 
  x \notin (fv t1) -> x \notin (fv t2) -> 
  (open_var t1 x = open_var t2 x) -> (t1 = t2).
Proof.
  intros x t1. unfold open_var, open. generalize 0.
  induction t1; intro k; destruct t2; simpl; intros; inversion H1;
  try solve [ fequals*
            | do 2 try case_nat; inversions~ H1; try notin_false ].
Qed.

(** We also need one (tricky) auxiliary lemma to handle the binder case *)

Lemma open_close_var_on_open_var : forall x y z t i j,
  i <> j -> y <> x -> y \notin (fv t) ->
    open_var_rec i y (open_var_rec j z (close_var_rec j x t))
  = open_var_rec j z (close_var_rec j x (open_var_rec i y t)).
Proof.
  unfold open_var_rec.
  induction t; simpl; intros; try solve [ fequals~ ].
  do 2 (case_nat; simpl); try solve [ case_var~ | case_nat~ ]. 
  case_var~. simpl. case_nat~. 
Qed.

(** Now we can prove that [open_var] after [close_var] is the identity *)

Lemma open_close_var : forall x t, 
  lc t -> 
  open_var (close_var x t) x = t.
Proof.
  introv T. unfold open_var, open, close_var. generalize 0.
  induction T; simpl; introv; fequals~.
  case_var~. simpl. case_nat~.
  match goal with |- ?t = _ => pick_fresh y from (fv t) end.
   apply~ (@open_var_inj y).
   lets M: open_close_var_on_open_var. unfold open_var_rec in M.
   unfold open_var, open. rewrite~ M. apply~ H0.
Qed.

(** As a bonus, we get the injectivity of [close_var] *)

Lemma close_var_inj : forall x t1 t2, 
  lc t1 -> lc t2 ->
  (close_var x t1 = close_var x t2) -> (t1 = t2).
Proof.
  introv T1 T2 Eq.
  rewrite~ <- (@open_close_var x t1).
  rewrite~ <- (@open_close_var x t2).
  fequals~.
Qed.


(* ********************************************************************** *)
(** Properties of [body] *)

(** An abstraction is locally closed iff it satifies the predicate [body] *) 

Lemma lc_abs_iff_body : forall t1, 
  lc (trm_abs t1) <-> body t1.
Proof. intros. unfold body. iff H; inversions* H. Qed.


(* ********************************************************************** *)
(** Interaction of [fv] with [open_var] and [close_var] *)

(** Opening with [u] adds [fv u] to the set of free variables *)

Lemma fv_open : forall t u,
  fv (open t u) \c fv t \u fv u.
Proof.
  introv. unfold open. generalize 0.
  induction t; intros k; simpl; try fset.
  case_nat; simpl; fset. 
Qed.

(** In particular, opening with variable [x] adds [x] to the set 
    of free variables *)

Lemma open_var_fv : forall x t,
  fv (open_var t x) \c (fv t \u \{x}).
Proof. intros. apply fv_open. Qed.

(** Closing w.r.t variable [x] removes [x] from the set of free variables *)

Lemma close_var_fv : forall x t,
  fv (close_var x t) \c (fv t \- \{x}).
Proof.
  introv. unfold close_var. generalize 0.
  induction t; intros k; simpl; try fset.
  case_var; simpl; fset. 
Qed.


(* ********************************************************************** *)
(** Properties of substitution *)

(** Distributivity of [subst] on [open].
    Two (tricky) intermediate lemmas are required *)

Lemma open_rec_lc_ind : forall t j v i u, i <> j ->
  open_rec i u (open_rec j v t) = open_rec j v t ->
  open_rec i u t = t.
Proof.
  induction t; introv Nq Eq;
   simpls; inversions~ Eq; fequals*.
  case_nat~. case_nat~.
Qed.

Lemma open_rec_lc : forall u t k,
  lc t -> open_rec k u t = t.
Proof.
  unfold open_var_rec. introv T. gen k.
  induction T; intros; simpl; fequals~. 
  pick_fresh y. apply~ (@open_rec_lc_ind t1 0 (trm_fvar y)).
  apply~ H0.
Qed.

Lemma subst_open : forall x u t v, lc u -> 
  subst x u (open t v) = open (subst x u t) (subst x u v).
Proof.
  intros. unfold open. generalize 0.
  induction t; intros; simpl; fequals~.
  case_nat~.
  case_var~. rewrite~ open_rec_lc.
Qed.

(** In particular, we can distribute [subst] on [open_var] *)

Lemma subst_open_var : forall x y u t, 
  y <> x -> lc u -> 
  subst x u (open_var t y) = open_var (subst x u t) y.
Proof.
  introv N U. unfold open_var. rewrite~ subst_open.
  fequals. simpl. case_if~.
Qed.

(** For the distributivity of [subst] on [close_var],
    one simple intermediate lemmas is required to 
    say that closing on a fresh name is the identity *)

Lemma close_var_rec_fresh : forall k x t,
  x \notin fv t -> close_var_rec k x t = t.
Proof.
  introv. gen k. induction t; simpl; intros; fequals*. 
  case_var~. 
Qed.

(** Distributivity of [subst] on [close_var] *)

Lemma subst_close_var : forall x y u t, 
  y <> x -> y \notin fv u -> 
  subst x u (close_var y t) = close_var y (subst x u t).
Proof.
  introv N F. unfold close_var. generalize 0.
  induction t; intros k; simpl; fequals~.
  case_var~; simpl.
    case_var~; simpl. case_var~.
    case_var~; simpl.
      rewrite~ close_var_rec_fresh.
      case_var~.
Qed.

(** Substitution for a fresh name is the identity *)

Lemma subst_fresh : forall x t u, 
  x \notin fv t -> subst x u t = t.
Proof. intros. induction t; simpls; fequals~. case_var~. Qed.

(** Substitution can be introduced to decompose an opening *)

Lemma subst_intro : forall x t u, 
  x \notin (fv t) -> lc u ->
  open t u = subst x u (open_var t x).
Proof.
  introv F U. unfold open_var. rewrite~ subst_open.
  fequals. rewrite~ subst_fresh. simpl. case_var~.
Qed.

(** An alternative, longer proof, but with fewer hypotheses *)

Lemma subst_intro_alternative : forall x t u, 
  x \notin (fv t) -> 
  open t u = subst x u (open_var t x).
Proof.
  introv H. unfold open_var, open. generalize 0. gen H.
  induction t; simpl; intros; fequals*.
  case_nat*.
  simpl. case_var*.
  case_var*.
Qed.

(** Substitution can be introduced to decompose a variable
    closing in terms of another one using a different name *)

Lemma close_var_rename : forall x y t,
  x \notin fv t ->
  close_var y t = close_var x (subst y (trm_fvar x) t).
Proof.
  introv. unfold close_var. generalize 0.
  induction t; simpl; intros k F; fequals~.
  case_var; simpl; case_var~.
Qed.


(* ********************************************************************** *)
(** Preservation of local closure through substitution and opening *)

(** Substitution of a locally closed terms into another one produces
    a locally closed term *)

Lemma subst_lc : forall z u t,
  lc u -> lc t -> lc (subst z u t).
Proof.
  introv U T. induction T; simple~.
  case_var~.
  apply_fresh lc_abs. rewrite~ <- subst_open_var.
Qed.

(** Substitution of a locally closed terms into a body one produces
    another body *)

Lemma subst_body : forall z t u,
  lc u -> body t -> body (subst z u t).
Proof.
  introv U [L H]. exists_fresh. 
  rewrite~ <- subst_open_var. apply~ subst_lc.
Qed.

(** Opening of a body with a locally closed terms produces a 
    locally closed term *)

Lemma open_lc : forall t u,
  body t -> lc u -> lc (open t u).
Proof.
  introv [L H] U. pick_fresh y. rewrite~ (@subst_intro y).
  apply~ subst_lc. 
Qed.


(* ********************************************************************** *)
(** Two additional lemmas (not used in practical developments) *)

(** A body becomes a locally closed term when [open_var] is applied *)

Lemma open_var_lc : forall t1 x, 
  body t1 -> lc (open_var t1 x).
Proof.
  introv [L M]. pick_fresh y. unfold open_var. 
  rewrite~ (@subst_intro y). applys~ subst_lc.
Qed. 

(** A locally closed term becomes a body when [closed_var] is applied *)

Lemma close_var_lc : forall t x, 
  lc t -> body (close_var x t).
Proof.
  introv T. exists_fresh.
  rewrite~ (@close_var_rename y).
  rewrite~ open_close_var; apply~ subst_lc.
Qed.



(* ====================================================================== *)
(** ** An induction principle for locally closed terms *)

(** Interaction of [size] with [open_var] *)

Lemma size_open_var : forall x t,
  size (open_var t x) = size t.
Proof.
  intros. unfold open_var, open. generalize 0.
  induction t; intros; simple~. case_nat~.
Qed.

(** Interaction of [size] with [close_var] *)

Lemma size_close_var : forall x t,
  size (close_var x t) = size t.
Proof.
  intros. unfold close_var. generalize 0.
  induction t; intros; simple~. case_var~.
Qed.

(** The induction principle *)

Lemma lc_induct_size : forall P : trm -> Prop,
  (forall x, P (trm_fvar x)) ->
  (forall t1 t2,
     lc t1 -> P t1 -> lc t2 -> P t2 -> P (trm_app t1 t2)) ->
  (forall t1,
     body t1 ->
     (forall t2 x, x \notin fv t2 -> size t2 = size t1 ->
       lc (open_var t2 x) -> P (open_var t2 x)) -> 
     P (trm_abs t1)) ->
  (forall t, lc t -> P t).
Proof.
  intros P Hvar Happ Habs t. 
  induction t using (@measure_induction _ size).
  introv T. inverts T; simpl in H; auto.
  apply~ Habs. exists_fresh; auto. introv Fr Eq T.
   apply~ H. rewrite~ size_open_var.
Qed.



(* ====================================================================== *)
(** ** Alternative definition for local closure *)


(* ********************************************************************** *)
(** Local closure, recursively defined *)

Fixpoint lc_at (k:nat) (t:trm) {struct t} : Prop :=
  match t with 
  | trm_bvar i    => i < k
  | trm_fvar x    => True
  | trm_app t1 t2 => lc_at k t1 /\ lc_at k t2
  | trm_abs t1    => lc_at (S k) t1
  end.

Definition lc' t := lc_at 0 t.

Definition body' t := lc_at 1 t.


(* ********************************************************************** *)
(** Equivalence of [lc] and [lc'] *)

Lemma lc_rec_open_var_rec : forall x t k,
  lc_at k (open_var_rec k x t) -> lc_at (S k) t.
Proof.
  unfold open_var_rec.
  induction t; simpl; introv H; auto*.
  case_nat; simpls~.
Qed.

Lemma lc_to_lc' : forall t,
  lc t -> lc' t.
Proof.
  introv T. induction T; unfold lc'; simple~.
  pick_fresh x. apply~ (@lc_rec_open_var_rec x). apply~ H0.
Qed.

Lemma lc_at_open_var_rec : forall x t k,
  lc_at (S k) t -> lc_at k (open_var_rec k x t).
Proof.
  unfold open_var_rec.
  induction t; simpl; introv H; auto*. case_nat; simple~.
Qed.

Lemma lc'_to_lc : forall t,
  lc' t -> lc t.
Proof.
  introv. unfold lc'.
  induction t using (@measure_induction _ size).
  destruct t; simpl; introv T'; simpl in H; auto*.
  apply_fresh lc_abs. apply H. rewrite~ size_open_var.
   apply~ lc_at_open_var_rec.
Qed.

Lemma lc_eq_lc' : lc = lc'.
Proof. extens. split. applys lc_to_lc'. applys lc'_to_lc. Qed.


(* ********************************************************************** *)
(** Equivalence of [body] and [body'] *)

Lemma body_to_body' : forall t,
  body t -> body' t.
Proof.
  introv [L H]. pick_fresh x. 
  applys (@lc_rec_open_var_rec x).
  apply lc_to_lc'. apply~ H.
Qed.

Lemma body'_to_body : forall t,
  body' t -> body t.
Proof.
  introv B. exists (\{}:vars). introv F.
  apply lc'_to_lc. apply~ lc_at_open_var_rec.
Qed.

Lemma body_eq_body' : body = body'.
Proof. extens. split. applys body_to_body'. applys body'_to_body. Qed.


(* ********************************************************************** *)
(** Weakening property of [lc_at] *)

Lemma lc_at_weaken_ind : forall k1 k2 t,
  lc_at k1 t -> k1 <= k2 -> lc_at k2 t.
Proof. introv. gen k1 k2. induction t; simpl; introv T Lt; auto*. Qed.

Lemma lc_at_weaken : forall k t,
  lc' t -> lc_at k t.
Proof. introv H. apply~ (@lc_at_weaken_ind 0). Qed.


(* ********************************************************************** *)
(** Proofs revisited with [lc_at] *)

(** The inductions are now simpler because they are structural *)

Lemma lc'_abs_to_body' : forall t1, 
  lc' (trm_abs t1) -> body' t1.
Proof. auto. Qed.

Lemma body'_to_lc'_abs : forall t1, 
  body' t1 -> lc' (trm_abs t1).
Proof. auto. Qed.

Lemma open_var_lc' : forall x t,
  body' t -> lc' (open_var t x).
Proof.
  introv B. applys~ lc_at_open_var_rec.
Qed.

Lemma close_var_body' : forall x t,
  lc' t -> body' (close_var x t).
Proof.
  introv. unfold lc', body', close_var.
  generalize 0. induction t; simpl; intros k T; auto*.
  case_var~. simpl. nat_math.
Qed.

Lemma subst_lc' : forall z u t,
  lc' u -> lc' t -> lc' (subst z u t).
Proof.
  introv U. unfold lc'. generalize 0.
  induction t; simpl; introv T; auto*.
  case_var~. apply~ lc_at_weaken.
Qed.

Lemma subst_body' : forall z u t,
  lc' u -> body' t -> body' (subst z u t).
Proof.
  introv U. unfold body'. generalize 1.
  induction t; simpl; introv T; auto*.
  case_var~. apply~ lc_at_weaken.
Qed.

Lemma open_rec_lc'_ind : forall u t k,
  lc_at k t -> open_rec k u t = t.
Proof.
  introv. gen k. induction t; simpl; introv F; fequals*.
  case_nat~. false. nat_math.
Qed.

Lemma open_rec_lc' : forall u t k,
  lc' t -> open_rec k u t = t.
Proof.
  unfold lc'. introv T.
  apply open_rec_lc'_ind. apply* lc_at_weaken.
Qed.

Lemma subst_open' : forall x u t v, lc' u -> 
  subst x u (open t v) = open (subst x u t) (subst x u v).
Proof.
  intros. unfold open. generalize 0.
  induction t; intros; simpl; fequals~.
  case_nat~.
  case_var~. rewrite~ open_rec_lc'.
Qed.

Lemma subst_intro' : forall x t u, 
  x \notin (fv t) -> lc' u ->
  open t u = subst x u (open_var t x).
Proof.
  introv F U. unfold open_var. rewrite~ subst_open'.
  fequals. rewrite~ subst_fresh. simpl. case_var~.
Qed.

Lemma open_lc' : forall t u,
  body' t -> lc' u -> lc' (open t u).
Proof.
  introv B U. pick_fresh y. rewrite~ (@subst_intro' y).
  apply~ subst_lc'. apply~ open_var_lc'.
Qed.

Lemma open_close_var' : forall x t, 
  lc' t -> 
  open_var (close_var x t) x = t.
Proof.
  introv. unfold lc', open_var, open, close_var. generalize 0.
  induction t; simpl; introv Lt; fequals*.
  case_nat~. false. nat_math.
  case_var~. simpl. case_nat~.
Qed.

Lemma close_var_inj' : forall x t1 t2, 
  lc' t1 -> lc' t2 ->
  (close_var x t1 = close_var x t2) -> (t1 = t2).
Proof.
  introv T1 T2 Eq.
  rewrite~ <- (@open_close_var' x t1).
  rewrite~ <- (@open_close_var' x t2).
  fequals~.
Qed.