(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require iso_defs.
Require drop1_defs.
Require getl_props.
Require pr2_gen.
Require pr3_gen.
Require pr3_confluence.
Require nf2_defs.

   Section nf2_props. (******************************************************)

      Theorem nf2_pr3_confluence: (c:?; t1:?) (nf2 c t1) -> (t2:?) (nf2 c t2) ->
                                  (t:?) (pr3 c t t1) -> (pr3 c t t2) -> t1 = t2.
      Proof.
      Intros; Pr3Confluence; Clear t.
      XPoseClear H '(nf2_pr3_unfold ? ? ? H2 H); Subst; Clear H2.
      XPoseClear H0 '(nf2_pr3_unfold ? ? ? H1 H0); Subst; Clear H1; XAuto.
      Qed.

      Lemma nf2_appls_lref: (c:?; i:?) (nf2 c (TLRef i)) ->
                            (vs:?) (nfs2 c vs) ->
                            (nf2 c (THeads (Flat Appl) vs (TLRef i))).
      Proof.
      XElim vs; Simpl; Intros.
(* case 1: TNil *)
      Clear H0; XAuto.
(* case 2: TCons *)
      XDecompose H1; XPoseClear H0 '(H0 H3); Clear H H3.
      Unfold nf2; Intros.
      Pr2Gen; Subst.
(* case 2.1: pr0_comp *)
      Repeat NF2Unfold; Clear H4 H5; XAuto.
(* case 2.2: pr0_delta *)
      NewInduction t0; Simpl in H3; XInv.
(* case 2.3: pr0_upsilon *)
      NewInduction t0; Simpl in H4; XInv.
      Qed.

      Theorem nf2_appl_lref: (c:?; u:?) (nf2 c u) -> (i:?) (nf2 c (TLRef i)) ->
                             (nf2 c (THead (Flat Appl) u (TLRef i))).
      Proof.
      Intros.
      XPoseClear H0 '(nf2_appls_lref ? ? H0 (TCons u TNil)).
      Simpl in H0; XAuto.
      Qed.

      Lemma nf2_lref_abst: (c,e:?; u:?; i:?) (getl i c (CHead e (Bind Abst) u)) ->
                           (nf2 c (TLRef i)).
      Proof.
      Unfold nf2; Intros.
      Pr2Gen; Subst; Try (GetLDis; XInv); XAuto.
      Qed.

      Lemma nf2_lift: (d:?; t:?) (nf2 d t) ->
                      (c:?; h,i:?) (drop h i c d) -> (nf2 c (lift h i t)).
      Proof.
      Unfold nf2; Intros; Pr2Gen; Subst.
      XPoseClear H '(H ? H3); Subst; XAuto.
      Qed.

      Hints Resolve nf2_lift : ld.

      Lemma nf2_lift1: (e:?; hds:?; c:?; t:?) (drop1 hds c e) ->
                       (nf2 e t) -> (nf2 c (lift1 hds t)).
      Proof.
      XElim hds; Simpl; Intros;
      Drop1GenBase; XDEAuto 3.
      Qed.

   End nf2_props.

      Hints Resolve nf2_appls_lref nf2_appl_lref nf2_lref_abst
                    nf2_lift nf2_lift1 : ld.

   Section nf2_iso_props. (**************************************************)

      Lemma nf2_iso_appls_lref: (c:?; i:?) (nf2 c (TLRef i)) ->
                                (vs:?; u:?) (pr3 c (THeads (Flat Appl) vs (TLRef i)) u) ->
                                (iso (THeads (Flat Appl) vs (TLRef i)) u).
      Proof.
      XElim vs; Simpl; Intros.
(* case 1: nil *)
      NF2Unfold3; XAuto.
(* case 2: cons *)
      Pr3Gen; Subst.
(* case 2.1: pr0_cong *)
      XAuto.
(* case 2.2: pr0_beta *)
      XPoseClear H0 '(H0 ? H5); IsoGenBase.
(* case 2.3: pr0_upsilon *)
      XPoseClear H0 '(H0 ? H4); IsoGenBase.
      Qed.

   End nf2_iso_props.