Require Import Metatheory.
Require Import LambdaES_Defs.
Require Import LambdaES_Infrastructure.
Require Import LambdaES_Tactics.
Require Import LambdaES_occ.
Require Import LambdaES_fv.
Require Import Arith.

Inductive ndr_n : pterm -> var -> var -> pterm -> nat -> Prop :=
  | ndr_bvar : forall x y z, ndr_n (pterm_bvar z) x y (pterm_bvar z) 0
  | ndr_varnone : forall x y z, ndr_n (pterm_fvar z) x y (pterm_fvar z) 0
  | ndr_varsome : forall x y, ndr_n (pterm_fvar x) x y (pterm_fvar y) 1
  | ndr_abs : forall t t' x y n, ndr_n t x y t' n ->
                        ndr_n(pterm_abs t) x y (pterm_abs t') n
  | ndr_app : forall t t' u u' x y n n' n'', n'' = n + n' ->
                        ndr_n t x y u n -> ndr_n t' x y u' n' ->
                        ndr_n (pterm_app t t') x y (pterm_app u u') n''
  | ndr_sub : forall t t' x y u u' n n' n'', n'' = n + n' ->
                        ndr_n (t) x y (t') n -> ndr_n u x y u' n' ->
                        ndr_n (pterm_sub t u) x y (pterm_sub t' u') n''.
Hint Constructors ndr_n.

 Definition ndr t x y t' := exists n, (1 <= n) /\ (n < fv_occ x t) /\ ndr_n t x y t' n.

Ltac ndr_elim H :=
  match type of H with
  | ndr ?t ?x ?y ?t' =>
      let n := fresh "n" in
      let H1 := fresh H in
      let H2 := fresh H in
      let H3 := fresh H in
      inversion H as [n H1] ; destruct H1 as [H1 H2] ; destruct H2 as [H2 H3]
end.

Ltac deep_elim_ndr H :=
  match type of H with
  | ndr ?t ?x ?y ?t' =>
      let n := fresh "n" in
      let H1 := fresh H in
      let H2 := fresh H in
      let H3 := fresh H in
      inversion H as [n H1] ; destruct H1 as [H1 H2] ; destruct H2 as [H2 H3] ; inversion H3 ; intros ; subst
end.

Lemma ndr_n_refl : forall t x y, ndr_n t x y t 0.
Proof.
  intro t. assert (0 = 0 + 0) as H by omega.
  basic_pterm_induction t using (rewrite H ; auto).
  rewrite H. apply ndr_app with (n:=0) (n':=0) ; auto.
  rewrite H. apply ndr_sub with (n:=0) (n':=0) ; auto.
Qed.
Hint Resolve ndr_n_refl.

Lemma ndr_n_opens : forall t x y t' n u, ndr_n t x y t' n -> ndr_n (t^^u) x y (t'^^u) n.
Proof. intros. unfold open. generalize 0. induction H ; simpl ; eauto. Qed.

Lemma ndr_n_opens_gen : forall t x y t' n u k, ndr_n t x y t' n -> ndr_n ({k~>u}t) x y ({k~>u}t') n.
Proof. intros. unfold open. gen k. induction H ; intros ; simpl ; eauto. Qed.

Lemma ndr_n_preservation_term : forall t, term t -> (forall t' x y n, ndr_n t x y t' n -> term t').
Proof.
  intros t H0. induction H0 using term_size_induction ; intros t' x' y' n Hn ; inversion Hn ; subst ; auto.
    destruct H. apply term_abs with (L := x \u (fv t1)). intros.
    apply H0 with (t2 :=t1) (x0:=x') (x:=x0) (y:=y') (n:=n) ; auto.
    unfold open. apply* ndr_n_opens.
    apply term_app ; eauto.
    destruct H.
    apply_fresh* term_sub.
    apply H1 with (t2 :=t1) (x0:=x') (x:=y) (y:=y') (n:=n0) ; auto.
    unfold open. apply* ndr_n_opens.
Qed.

Lemma ndr_preservation_term : forall t x y t', term t -> ndr t x y t' -> term t'.
Proof.
  intros t x y t' term_t ndr_. unfolds ndr.
  destruct ndr_ as [n [n_1 [n_fv ndr_]]].
  apply ndr_n_preservation_term with (t:=t) (x:=x) (y:=y) (n:=n) ; auto.
Qed.

Lemma arith_split : forall x y z, x <= y + z -> exists n1, exists n2, n1 <= y /\ n2 <= z /\ x = n1 + n2.
Proof.
  intros x y z H.
  assert (x > y \/ x <= y) as H1 by omega.
  destruct H1.
    exists y. exists (x-y). omega.
    exists x. exists 0. omega.
Qed.

Lemma ndr_n_exists : forall t x y n, n <= fv_occ x t -> exists t', ndr_n t x y t' n.
Proof.
  intros t x y. induction t ; intros ; simpls.
    assert (n0 = 0) by omega. subst. eauto.
    case_var.
      assert(n=0 \/ n=1) as H0 by omega.
      destruct H0 ; subst ; eauto.
      assert(n=0) by omega ; subst. eauto.
    destruct (IHt n) as [t0] ; eauto.
    apply arith_split in H.
    destruct H as [n1] ; destruct H as [n2]. destruct H as [H0]. destruct H as [H1].
    rewrite H. destruct (IHt1 n1) as [t1'] ; auto. destruct (IHt2 n2) as [t2'] ; auto.
    eauto.
    apply arith_split in H.
    destruct H as [n1] ; destruct H as [n2]. destruct H as [H0]. destruct H as [H1].
    rewrite H. destruct (IHt1 n1) as [t1'] ; auto. destruct (IHt2 n2) as [t2'] ; auto.
    eauto.
Qed.

Lemma ndr_exists : forall t x y, 1 < fv_occ x t -> exists t', ndr t x y t'.
Proof.
  intros. unfold ndr.
  destruct (ndr_n_exists t x y 1) as [t'] ; [omega|].
  eauto.
Qed.

Lemma ndr_n_preservation_body : forall t x y t' n, ndr_n t x y t' n -> body t -> body t'.
Proof.
  intros t x y t' n ndr_. gen t' n.
  induction t ; intros.
  inversion ndr_ ; subst*.
  inversion ndr_ ; subst*.
  inversion ndr_ ; subst.
  unfolds body.
  destruct H as [L].
  exists L.
  intros.
  apply ndr_n_preservation_term with (t:=pterm_abs t ^ x0) (x:=x) (y:=y) (n:=n).
    apply H ; auto.
    unfold open. apply ndr_n_opens_gen ; auto.
  inversion ndr_ ; subst*.
  apply body_distribute_over_application.
  apply body_distribute_over_application in H.
  destruct* H.
  inversion ndr_ ; subst.
  unfolds body.
  destruct H as [L].
  exists L.
  intros.
  apply ndr_n_preservation_term with (t:=t1[t2] ^ x0) (x:=x) (y:=y) (n:=n0+n').
    apply* H.
    unfold open. apply* ndr_n_opens_gen.
Qed.

Lemma ndr_n_occ_preservation : forall t x y t' n, ndr_n t x y t' n ->
           forall k, ((bv_occ_k k t) = (bv_occ_k k t')).
Proof. intro t. induction t ; intros x y t' m H ; inv H ; try reflexivity ; simpl ; eauto. Qed.

Lemma ndr_n_fv_occ : forall t t' x y n, ~(x = y) -> ndr_n t x y t' n -> fv_occ y t' = fv_occ y t + n.
  intros. induction H0 ; auto ; simpl.
    repeat case_var ; simpl ; auto.
    rewrite IHndr_n1 ; auto. rewrite IHndr_n2 ; auto. omega.
    rewrite IHndr_n1 ; auto. pick_fresh z. rewrite fv_occ_open_var with (y:=z) ; auto.
    rewrite IHndr_n2 ; auto.
    rewrite <-fv_occ_open_var ; auto. omega.
Qed.
Hint Rewrite ndr_n_fv_occ using (solve [auto]) : bv_occ_rewrite.

Lemma ndr_n_gt_fv : forall t t' x y n, ~(x = y) -> ndr_n t x y t' n -> n <= fv_occ x t.
Proof.
  intros t t' x y n x_neq_y ndr_.
  induction ndr_ ; simpl ; eauto.
    case_var*.
    case_var*.
    rewrite H. apply plus_le_compat ; auto.
    rewrite H. apply plus_le_compat ; auto.
Qed.

Lemma ndr_n_fv_occ_x : forall t t' x y n, ~(x = y) -> ndr_n t x y t' n -> fv_occ x t' = fv_occ x t - n.
Proof.
  intros.
  induction H0 ; auto ; simpl.
    repeat case_var ; simpl ; auto.
    case_var*. case_var. auto.
    rewrite IHndr_n1 ; auto. rewrite IHndr_n2 ; auto.
    assert (n <= fv_occ x t). apply ndr_n_gt_fv with (t':=u) (y:=y) ; auto.
    assert (n' <= fv_occ x t'). apply ndr_n_gt_fv with (t':=u') (y:=y) ; auto.
    omega.
    rewrite IHndr_n1 ; auto. pick_fresh z.
    rewrite fv_occ_open_var with (y:=z) ; auto.
    rewrite IHndr_n2 ; auto.
    rewrite <-fv_occ_open_var ; auto.
    assert (n <= fv_occ x t). apply ndr_n_gt_fv with (t':=t') (y:=y) ; auto.
    assert (n' <= fv_occ x u). apply ndr_n_gt_fv with (t':=u') (y:=y) ; auto.
    omega.
Qed.

Lemma ndr_subst : forall t t' u x y n,
        x <>y ->
        y \notin fv t ->
        y \notin fv u ->
        ndr_n t x y t' n ->
        [x~>u]t = [y~>u]([x~>u]t').
Proof.
  intros t t' u x y n x_neq_y y_notin_t y_notin_u ndr_.
  induction ndr_ ; simpl.
  reflexivity.
  case_var. rewrite subst_fresh ; auto.
    simpl. case_var. elim y_notin_t. simpl. VSD.fsetdec.
    reflexivity.
  case_var. case_var. simpl. case_var. reflexivity.
  fequals. apply IHndr_ ; auto.
  simpl in y_notin_t. fequals. apply IHndr_1 ; auto. apply IHndr_2 ; auto.
  simpl in y_notin_t. fequals. apply IHndr_1 ; auto. apply IHndr_2 ; auto.
Qed.

Lemma fv_subst_commute : forall t x y u v, x <>y ->
        x \notin fv v ->
        y \notin fv u ->
        ([y~>v][x~>u]t) = ([x~>u][y~>v]t).
Proof.
intros. induction t ; simpl.
  reflexivity.
  case_var. case_var. simpl. case_var. auto. rewrite subst_fresh ; auto.
  case_var ; simpl. case_var. rewrite subst_fresh ; auto.
  case_var. case_var. auto.
  fequals.
  fequals.
  fequals.
Qed.

Lemma ndr_n_close_open : forall t a b t' u n,
        a \notin fv t -> a <> b ->
        b \notin fv t -> b \notin fv u ->
        a \notin fv u -> ndr_n (t^a) a b t' n ->
        [a~>u]([b~>u]t') = t ^^ u.
Proof.
  intros.
  rewrite fv_subst_commute ; auto.
  rewrite subst_intro with (x:=a) ; auto.
  rewrite <-ndr_subst with (t:=t^a) (n:=n) ; auto.
  apply fv_notin_open ; auto.
Qed.

Ltac get_ndr_root H :=
match (type of H) with
| ndr_n ?t _ _ ?t' _ =>
  match goal with
  | Hroot : ndr_n ?root _ _ t _ |- _ => get_ndr_root Hroot
  | Hroot : ndr ?root _ _ t |- _ => get_ndr_root Hroot
  | _ => H
  end
| ndr ?t _ _ ?t' =>
  match goal with
  | Hroot : ndr_n ?root _ _ t _ |- _ => get_ndr_root Hroot
  | Hroot : ndr ?root _ _ t |- _ => get_ndr_root Hroot
  | _ => H
  end
end.

Ltac ndr_extractor H :=
  match (type of H) with
  | ndr_n ?t _ _ _ _ =>
      let tmp1 := fresh H in
      duplicate H tmp1 ;
      try(apply ndr_n_preservation_term in tmp1 ; [|now auto with term_building_db] ; term_extractor tmp1) ;
      let tmp2 := fresh H in
      duplicate H tmp2 ;
      try (apply ndr_n_preservation_body in tmp2 ; [|now auto with term_building_db] ; term_extractor tmp2) ;
      let tmp3 := fresh H in
      duplicate H tmp3 ;
      try (apply ndr_n_fv_occ in tmp3 ; [|now auto]) ;
      let tmp4 := fresh H in
      duplicate H tmp4 ;
      try (apply ndr_n_fv_occ_x in tmp4 ; first[auto|VSD.fsetdec]) ;
      let tmp5 := fresh H in
      
      remove_if_same H tmp1 ;
      remove_if_same H tmp2 ;
      remove_if_same H tmp3 ;
      remove_if_same H tmp4 ;
      remove_dupterms
  | ndr ?t _ _ _ =>
      let tmp1 := fresh H in
      duplicate H tmp1 ;
      try(apply ndr_preservation_term in tmp1 ; [|now auto with term_building_db] ; term_extractor tmp1) ;

      
      remove_if_same H tmp1 ;

      remove_dupterms
  end.

Ltac saturate_ndr :=
try(
  match goal with
  | H : ndr_n _ _ _ _ _ |- _ =>
    let root := get_ndr_root H in
    ndr_extractor root ; generalize root ; clear root ; saturate_ndr
  | H : ndr _ _ _ _ |- _ =>
    let root := get_ndr_root H in
    ndr_extractor root ; generalize root ; clear root ; saturate_ndr

  | _ => idtac
end).

Ltac term_solver := now (saturate_term ; intros ; saturate_ndr ; intros ; auto with term_building_db ).

Hint Rewrite subst_fv_occ using solve[auto|VSD.fsetdec|term_solver] : bv_occ_rewrite.
Hint Rewrite bv_occ_term using (term_solver) : bv_occ_rewrite.

Ltac saturate_rewrite :=
try(
  match goal with
  | H : ?t = ?t' |- _ => rewrite H ; generalize H ; clear H ; saturate_rewrite
  end
).

Ltac bv_occ_solver := now(
  saturate_term ; intros ; saturate_ndr ; intros ;
  autorewrite with bv_occ_rewrite using (saturate_rewrite ; intros) ;
  simpl ; auto with arith ; try omega).