Set Implicit Arguments.
Require Import Metatheory LambdaES_Defs LambdaES_Tactics LambdaES_fv.
Require Import Arith.

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

Ltac pick_fresh Y :=
  let L := gather_vars in (pick_fresh_gen L Y).

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.

Hint Constructors term.

Fixpoint pterm_size (t : pterm) {struct t} : nat :=
 match t with
 | pterm_bvar i => 1
 | pterm_fvar x => 1
 | pterm_abs t1 => 1 + (pterm_size t1)
 | pterm_app t1 t2 => 1 + (pterm_size t1) + (pterm_size t2)
 | pterm_sub t1 t2 => 1 + (pterm_size t1) + (pterm_size t2)
 end.

Fixpoint subst (z : var) (u : pterm) (t : pterm) {struct t} : pterm :=
  match t with
  | pterm_bvar i => pterm_bvar i
  | pterm_fvar x => if x == z then u else (pterm_fvar x)
  | pterm_abs t1 => pterm_abs (subst z u t1)
  | pterm_app t1 t2 => pterm_app (subst z u t1) (subst z u t2)
  | pterm_sub t1 t2 => pterm_sub (subst z u t1) (subst z u t2)
  end.
Notation "[ z ~> u ] t" := (subst z u t) (at level 62).

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

Lemma open_var_inj : forall (x:var) t1 t2, x \notin (fv t1) ->
        x \notin (fv t2) -> (t1 ^ x = t2 ^ x) -> (t1 = t2).
Proof.
  intros x t1. unfold open. generalize 0.
  induction t1; intro k; destruct t2; simpl; intros; inversion H1;
  try solve [ f_equal*
  | do 2 try case_nat; inversions* H1; try notin_contradiction ].
  rewrite IHt1_1 with (n:=k) (t2:=t2_1) ; auto.
  rewrite IHt1_2 with (n:=k) (t2:=t2_2) ; auto.
  rewrite IHt1_1 with (n:=S k) (t2:=t2_1) ; auto.
  rewrite IHt1_2 with (n:=k) (t2:=t2_2) ; auto.
Qed.

Lemma open_rec_term_core :forall t j v i u, i <> j ->
        {j ~> v}t = {i ~> u}({j ~> v}t) ->
        t = {i ~> u}t.
Proof.
  induction t; introv Neq Equ; simpls; inversion* Equ; fequals*.
  case_nat*. case_nat*.
Qed.

Lemma open_rec_term : forall t u, term t -> forall k, t = {k ~> u}t.
Proof.
  induction 1; intros; simpl; fequals*; unfolds open ;
  pick_fresh x; apply* (@open_rec_term_core t1 0 (pterm_fvar x)).
Qed.

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

Lemma subst_open_gen : forall x u t1 t2 k, term u ->
  [x ~> u] ({k ~> t2}t1) = {k ~> ([x ~> u]t2)} ([x ~> u]t1).
Proof.
  intros x u t1 t2 k term_u. gen k.
  induction t1; intros; simpl; fequals*.
  case_nat*. case_var*. apply* open_rec_term.
Qed.

Lemma subst_open : forall x u t1 t2, term u ->
  [x ~> u] (t1 ^^ t2) = ([x ~> u]t1) ^^ ([x ~> u]t2).
Proof. intros. apply subst_open_gen. exact H. Qed.

Lemma subst_open_var : forall x y u t, y <> x -> term u ->
  ([x ~> u]t) ^ y = [x ~> u] (t ^ y).
Proof.
  introv Neq Wu. rewrite* subst_open. simpl. case_var*.
Qed.

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

Lemma subst_term : forall t z u,
  term u -> term t -> term ([z ~> u]t).
Proof.
  induction 2; simpls*.
  case_var*.
  apply_fresh term_abs. rewrite* subst_open_var.
  apply_fresh term_sub. rewrite* subst_open_var. assumption.
Qed.
Hint Resolve subst_term.

Lemma term_is_a_body : forall t, term t -> body t.
Proof.
  intros. unfold body. exists {}. intros. unfold open. rewrite <- open_rec_term. auto. auto.
Qed.

Lemma body_open_term : forall t u, body t -> term u -> term (t ^^ u).
Proof.
  intros. destruct H. pick_fresh y. rewrite* (@subst_intro y).
Qed.
Hint Resolve body_open_term.

Lemma term_open_term : forall t u, term t -> term u -> term (t ^^ u).
Proof. intros. apply* body_open_term. apply* term_is_a_body. Qed.

Lemma term_abs_to_body : forall t1, term (pterm_abs t1) -> body t1.
Proof. intros. unfold body. inversion* H. Qed.

Lemma body_to_term_abs : forall t1, body t1 -> term (pterm_abs t1).
Proof. intros. inversion* H. Qed.

Lemma term_sub_to_body : forall t s, term (t[s]) -> body t.
Proof. intros. unfold body. inversion* H. Qed.

Lemma term_sub_to_term : forall t s, term (t[s]) -> term s.
Proof. intros. inversion* H. Qed.

Lemma body_to_subs : forall t u, body t -> term u -> term (pterm_sub t u).
Proof. intros. inversion* H. Qed.

Lemma term_to_subs : forall t u, term t -> term u -> term (pterm_sub t u).
Proof. intros. apply_fresh term_sub. apply term_open_term. assumption. auto. auto. Qed.

Lemma term_app_to_term_l : forall t1 t2, term (pterm_app t1 t2) -> term t1.
Proof. intros. inversion* H. Qed.

Lemma term_app_to_term_r : forall t1 t2, term (pterm_app t1 t2) -> term t2.
Proof. intros. inversion* H. Qed.

Lemma fvar_body : forall x, body (pterm_fvar x).
Proof. intro. unfold body. exists {}. intros. unfold open. simpl. apply term_var. Qed.

Hint Resolve term_abs_to_body body_to_term_abs term_sub_to_body body_to_subs fvar_body.


Lemma body_distribute_over_application : forall t u, body (pterm_app t u) <-> body t /\ body u.
Proof.
  split.
    unfold body; unfold open; simpl ; intros; elim H; intros.
    split ; exists x; intros; specialize (H0 x0); specialize (H0 H1) ;
    inversion H0 ; assumption.
    intros. unfold body in H. unfold body. destruct H.
    destruct H. destruct H0.
    exists (x \u x0). intros.
    unfold open. simpl. constructor.
      specialize (H x1) . auto.
      specialize (H0 x1) . auto.
Qed.


Lemma term_abs_term : forall t, term t -> term (pterm_abs t).
Proof.
  intros. apply term_abs with (L:={}). intros. apply term_open_term. assumption. auto.
Qed.

Lemma body_abs : forall t, body t -> body (pterm_abs t).
Proof.
  intros. unfold body. exists {}.
  intros. apply* term_open_term.
Qed.

Lemma close_var_rec_open : forall t x y z i j , i <> j -> x <> y -> y \notin fv t ->
  {i ~> pterm_fvar y}({j ~> pterm_fvar z} (close_rec j x t)) = {j ~> pterm_fvar z}(close_rec j x ({i ~> pterm_fvar y}t)).
Proof.
  induction t; simpl; intros; try solve [ f_equal* ].
  do 2 (case_nat; simpl); try solve [ case_var* | case_nat* ].
  case_var*. simpl. case_nat*.
Qed.


Lemma open_close_var : forall x t, term t -> t = (close t x) ^ x.
Proof.
  introv W. unfold close, open. generalize 0.
  induction W; intros k; simpls; f_equal*.
  case_var*. simpl. case_nat*.
  let L := gather_vars in match goal with |- _ = ?t =>
    destruct (var_fresh (L \u fv t)) as [y Fr] end.
  apply* (@open_var_inj y).
  unfolds open. rewrite* close_var_rec_open. VSD.fsetdec.
  let L := gather_vars in match goal with |- _ = ?t =>
    destruct (var_fresh (L \u fv t)) as [y Fr] end.
  apply* (@open_var_inj y).
  unfolds open. rewrite* close_var_rec_open. VSD.fsetdec.
Qed.

Lemma close_var_body : forall x t, term t -> body (close t x).
Proof.
  introv W. exists {{x}}. intros y Fr.
  unfold open, close. generalize 0. gen y.
  induction W; intros y Fr k; simpls.
  case_var; simpl. case_nat*.
  auto*.
  apply_fresh* term_abs.
   unfolds open. rewrite* close_var_rec_open. VSD.fsetdec.
  apply* term_app.
  apply_fresh* term_sub. unfolds open. rewrite* close_var_rec_open. VSD.fsetdec.
Qed.

Lemma close_fresh : forall t x k, x \notin fv t -> close_rec k x t = t.
Proof.
  intros t x k x_notin_t. unfold close. gen k.
  induction t ; intro k ; simpls* ; try (fequals ; eauto).
    case_var*.
Qed.

Lemma subst_close : forall t x y u,
    x \notin fv u ->
    y \notin fv u ->
    x <> y ->
[y ~> u] (close t x) = close ([y ~> u]t) x.
Proof.
  intros t x y u x_notin_u y_notin_u x_neq_y.
  unfold close. generalize 0 as k.
  induction t ; intro k ; simpls* ; try (fequals ; eauto).
    case_var ; simpl ; case_var ; simpls.
      case_var*.
      rewrite* close_fresh.
      case_var*.
Qed.

Lemma subst_as_close_open : forall t x u, term t -> [x ~> u] t = (close t x) ^^ u.
Proof.
  intros t x u term_t. rewrite subst_intro with (x:=x).
  rewrite <- open_close_var with (x:=x) ; auto.
  apply notin_fv_close.
Qed.

Lemma pterm_size_open_var : forall t x, pterm_size t = pterm_size (t^x).
Proof. intro t. unfold open. generalize 0. basic_pterm_induction t. case_nat*. Qed.

Lemma peano_induction :
 forall (P:nat->Prop),
   (forall n, (forall m, m < n -> P m) -> P n) ->
   (forall n, P n).
Proof.
  introv H. cuts* K: (forall n m, m < n -> P m).
  induction n; introv Le. inversion Le. apply H.
  intros. apply IHn. omega.
Qed.

Lemma term_size_induction :
 forall P : pterm -> Prop,
 (forall x, P (pterm_fvar x)) ->
 (forall t1,
    body t1 ->
    (forall t2 x, x \notin fv t2 -> pterm_size t2 = pterm_size t1 ->
      term (t2 ^ x) -> P (t2 ^ x)) ->
    P (pterm_abs t1)) ->
 (forall t1 t2,
    term t1 -> P t1 -> term t2 -> P t2 -> P (pterm_app t1 t2)) ->
(forall t1 t3,
    term t3 -> P t3 -> body t1 ->
    (forall t2 x, x \notin fv t2 -> pterm_size t2 = pterm_size t1 ->
      term (t2 ^ x) -> P (t2 ^ x)) ->
    P (t1[t3])) ->
 (forall t, term t -> P t).
Proof.
  intros P Ha Hb Hc Hd t.
  gen_eq n: (pterm_size t). gen t.
  induction n using peano_induction.
  introv Eq T. subst. inverts T.
     apply Ha.
     apply* Hb.
       introv Fr Eq T.
       apply~ H. rewrite <- pterm_size_open_var. simpl. omega.
     apply~ Hc. apply~ H. simpl; omega. apply~ H. simpl; omega.
     apply* Hd.
       apply~ H. simpl; omega.
       introv Fr Eq T. apply~ H. rewrite <- pterm_size_open_var. simpl. omega.
Qed.

Ltac remove_dupterms :=
try match goal with
| H1 : term ?t,
  H2 : term ?t |- _ => clear H2
| H1 : body ?t,
  H2 : body ?t |- _ => clear H2
end.

Hint Resolve
    term_var
    term_app
    body_open_term
    term_open_term
    body_to_term_abs
    body_to_subs
    term_to_subs
    term_abs_term
    close_var_body : term_building_db.

Ltac term_extractor H :=
try(
  match (type of H) with
  | term (pterm_app ?u ?u') =>
        let tmp := fresh H in
        duplicate H tmp;
        apply term_app_to_term_l in tmp ; term_extractor tmp;
        apply term_app_to_term_r in H ; term_extractor H
  | term (pterm_sub ?t ?u) =>
        let tmp := fresh H in
        duplicate H tmp;
        apply term_sub_to_term in tmp ; term_extractor tmp;
        apply term_sub_to_body in H ; term_extractor H
  | term (pterm_abs ?t) =>
        apply term_abs_to_body in H ; term_extractor H
  |_ => generalize H ; clear H
  end).

Ltac saturate_term :=
try(
  match goal with
  | H : term _ |- _ => term_extractor H ; saturate_term
end).