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

Require Export pr3_defs.

      Definition nf2: C -> T -> Prop :=
         [c,t1:?] (t2:?) (pr2 c t1 t2) -> t1 = t2.

      Tactic Definition NF2Unfold := (
         Match Context With
            | [ H1: (nf2 ?1 ?2); H2: (pr2 ?1 ?2 ?3) |- ? ] ->
               LApply (H1 ?3); [ Clear H1; Intros H1; Subst | XAuto ]
         ).

      Fixpoint nfs2 [c:C; ts:TList] : Prop := Cases ts of
         | TNil         => True
         | (TCons t ts) => (nf2 c t) /\ (nfs2 c ts)
      end.

   Section nf2_gen_base. (***************************************************)

      Lemma nf2_gen_lref: (c,d:?; u:?; i:?) (getl i c (CHead d (Bind Abbr) u)) ->
                          (nf2 c (TLRef i)) -> (P:Prop) P.
      Proof.
      Unfold nf2; Intros.
      LApply (H0 (lift (S i) (0) u)); [ Clear H0; Intros | XDEAuto 3 ].
      LiftGenBase.
      Qed.

      Lemma nf2_gen_abst: (c:?; u,t:?) (nf2 c (THead (Bind Abst) u t)) ->
                          (nf2 c u) /\ (nf2 (CHead c (Bind Abst) u) t).
      Proof.
      Unfold nf2; Intros; Split; Intros.
(* case 1: left operand *)
      LApply (H (THead (Bind Abst) t2 t)); [ Clear H; Intros | XAuto ].
      XInv; Subst; XAuto.
(* case 2: right operand *)
      LApply (H (THead (Bind Abst) u t2)); [ Clear H; Intros | Pr2XGenBase; XAuto ].
      XInv; Subst; XAuto.
      Qed.

      Lemma nf2_gen_cast: (c:?; u,t:?) (nf2 c (THead (Flat Cast) u t)) ->
                          (P:Prop) P.
      Proof.
      Intros; LApply (H t); [ Clear H; Intros | XAuto ].
      EApply thead_x_y_y; XDEAuto 1.
      Qed.

      Lemma nf2_gen_beta: (c:?; u,v,t:?)
                          (nf2 c (THead (Flat Appl) u (THead (Bind Abst) v t))) ->
                          (P:Prop) P.
      Proof.
      Unfold nf2; Intros.
      LApply (H (THead (Bind Abbr) u t)); [ Clear H; Intros | XAuto ].
      XInv.
      Qed.

      Lemma nf2_gen_flat: (f:?; c:?; u,t:?) (nf2 c (THead (Flat f) u t)) ->
                          (nf2 c u) /\ (nf2 c t).
      Proof.
      Unfold nf2; Split; Intros.
(* case 1: left operand *)
      LApply (H (THead (Flat f) t2 t)); [ Clear H; Intros | XAuto ].
      XInv; XAuto.
(* case 2: right:operand *)
      LApply (H (THead (Flat f) u t2)); [ Clear H; Intros | XAuto ].
      XInv; XAuto.
      Qed.

   End nf2_gen_base.

      Tactic Definition NF2GenBase := (
         Match Context With
            | [ H0: (getl ?1 ?2 (CHead ?3 (Bind Abbr) ?4));
                H1: (nf2 ?2 (TLRef ?1)) |- ? ] ->
               Apply (nf2_gen_lref ?2 ?3 ?4 ?1 H0 H1)
            | [ H: (nf2 ?1 (THead (Bind Abst) ?2 ?3)) |- ? ] ->
               LApply (nf2_gen_abst ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
               XDecompose H
            | [ H: (nf2 ?1 (THead (Flat Cast) ?2 ?3)) |- ? ] ->
               Apply (nf2_gen_cast ?1 ?2 ?3 H)
            | [ H: (nf2 ?1 (THead (Flat Appl) ?2 (THead (Bind Abst) ?3 ?4))) |- ? ] ->
               Apply (nf2_gen_beta ?1 ?2 ?3 ?4 H)
            | [ _: (nf2 ?1 (THead (Flat ?2) ?3 ?4)) |- ? ] ->
               LApply (nf2_gen_flat ?2 ?1 ?3 ?4); [ Intros H_x | XAuto ];
               XDecompose H_x
         ).

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

      Lemma nf2_sort: (c:?; n:?) (nf2 c (TSort n)).
      Proof.
      Unfold nf2; Intros.
      Pr2GenBase; Subst; XAuto.
      Qed.

      Lemma nf2_csort_lref: (n,i:?) (nf2 (CSort n) (TLRef i)).
      Proof.
      Unfold nf2; Intros.
      Pr2GenBase; Subst; Try GetLGenBase; XAuto.
      Qed.

      Theorem nf2_abst: (c:?; u:?) (nf2 c u) ->
                        (b:?; v,t:?) (nf2 (CHead c (Bind b) v) t) ->
                        (nf2 c (THead (Bind Abst) u t)).
      Proof.
      Unfold nf2; Intros.
      Pr2GenBase; Subst; XDEAuto 4.
      Qed.

      Theorem nf2_abst_shift: (c:?; u:?) (nf2 c u) ->
                              (t:?) (nf2 (CHead c (Bind Abst) u) t) ->
                              (nf2 c (THead (Bind Abst) u t)).
      Proof.
      Unfold nf2; Intros.
      Pr2GenBase; Subst; XDEAuto 4.
      Qed.

   End nf2_props.

      Hints Resolve nf2_sort nf2_csort_lref nf2_abst_shift : ld.

   Section nf2_pr3_props. (**************************************************)

      Lemma nf2_pr3_unfold: (c:?; t1,t2:?)
                            (pr3 c t1 t2) -> (nf2 c t1) -> t1 = t2.
      Proof.
      Intros until 1; XElim H; Intros.
(* case pr3_refl *)
      XAuto.
(* case pr3_sing *)
      NonLinear; NF2Unfold; Subst; XAuto.
      Qed.

   End nf2_pr3_props.

      Tactic Definition NF2Unfold3 := (
         Match Context With
            | [ H1: (nf2 ?1 ?2); H2: (pr3 ?1 ?2 ?3) |- ? ] ->
               XPoseClear H1 '(nf2_pr3_unfold ? ? ? H2 H1); Subst
            | [ |- ? ] -> NF2Unfold
         ).

   Section nfs2_props. (*****************************************************)

      Lemma nfs2_tapp: (c:?; t:?; ts:?) (nfs2 c (TApp ts t)) ->
                       (nfs2 c ts) /\ (nf2 c t).
      Proof.
      XElim ts; Simpl; Intros.
(* case 1: TNil *)
      XDecompose H; Clear H1; XAuto.
(* case 2: TCons *)
      XDecompose H0; XDecomPoseClear H '(H H2); Clear H2; XAuto.
      Qed.

   End nfs2_props.