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

Require dnf_dec.
Require arity_defs.
Require arity_gen.
Require nf2_defs.

   Section nf2_gen. (********************************************************)

      Remark nf2_gen_aux: (b:?; x,u:?; d:?)
                          (THead (Bind b) u (lift (1) d x)) = x ->
                          (P:Prop) P.
      Proof.
      XElim x; Intros.
(* case 1: TSort *)
      XInv.
(* case 2: TLRef *)
      XInv.
(* case 2: THead *)
      XInv; Rewrite <- H3 in H1; Clear H2 H3 k u.
      Rewrite lift_bind in H1; EApply H0; XDEAuto 1.
      Qed.

      Lemma nf2_gen_abbr: (c:?; u,t:?) (nf2 c (THead (Bind Abbr) u t)) ->
                          (P:Prop) P.
      Proof.
      Unfold nf2; Intros.
      XDecomPose '(dnf_dec u t O); Subst.
(* case 1: subst0 *)
      LApply (H (THead (Bind Abbr) u (lift (1) (0) x))); [ Clear H; Intros | XDEAuto 4 ].
      XInv; Subst; EApply subst0_refl; XDEAuto 1.
(* case 2: subst0 *)
      LApply (H x); [ Clear H; Intros | XDEAuto 4 ].
      EApply nf2_gen_aux; XDEAuto 1.
      Qed.

      Lemma nf2_gen_void: (c:?; u,t:?) (nf2 c (THead (Bind Void) u (lift (1) (0) t))) ->
                          (P:Prop) P.
      Proof.
      Unfold nf2; Intros.
      LApply (H t); [ Clear H; Intros | XDEAuto 4 ].
      EApply nf2_gen_aux; XDEAuto 1.
      Qed.

   End nf2_gen.

      Tactic Definition NF2Gen := (
         Match Context With
            | [ H: (nf2 ?1 (THead (Bind Abbr) ?2 ?3)) |- ? ] ->
               Apply (nf2_gen_abbr ?1 ?2 ?3 H)
            | [ H: (nf2 ?1 (THead (Bind Void) ?2 (lift (1) (0) ?3))) |- ? ] ->
               Apply (nf2_gen_void ?1 ?2 ?3 H)
            | [ |- ? ] -> NF2GenBase
         ).

   Section nf2_inv_all. (****************************************************)

      Lemma arity_nf2_inv_all: (g:?; c:?; t:?; a:?) (arity g c t a) ->
                               (nf2 c t) -> (OR
                               (EX w u | t = (THead (Bind Abst) w u) &
                                         (nf2 c w) &
                                         (nf2 (CHead c (Bind Abst) w) u)
                               ) |
                               (EX n | t = (TSort n)) |
                               (EX ws i | t = (THeads (Flat Appl) ws (TLRef i)) &
                                          (nfs2 c ws) & (nf2 c (TLRef i))
                               )).
      Proof.
      Intros until 1; XElim H; Clear c t a; Intros.
(* case 1: arity_sort *)
      XDEAuto 3.
(* case 2: arity_abbr *)
      NF2Gen.
(* case 3: arity_abst *)
      Apply or3_intro2.
      EApply ex3_2_intro with x0:=TNil; Simpl; XDEAuto 2.
(* case 4: arity_bind *)
      Clear H0 H1 H3; NewInduction b.
(* case 4.1: Abbr *)
      NF2Gen.
(* case 4.2: Abst *)
      EqFalse.
(* case 4.3: Void *)
      ArityGen; Subst; NF2Gen.
(* case 5: arity_head *)
      Clear H H0 H1 H2; NF2Gen; XDEAuto 3.
(* case 6: arity_appl *)
      NF2Gen; XDecomPoseClear H2 '(H2 H5); Clear H H0 H5; Subst.
(* case 6.1: Abst *)
      NF2Gen.
(* case 6.2: Sort *)
      ArityGen; LEqGenBase.
(* case 6.3: LRef *)
      Apply or3_intro2.
      EApply ex3_2_intro with x0:=(TCons u x0); Simpl; XDEAuto 2.
(* case 7: arity_cast *)
      Clear H H0 H1 H2; NF2Gen.
(* case 8: arity_repl *)
      XDecomPoseClear H0 '(H0 H2); Clear H H1 H2; Subst; XDEAuto 3.
      Qed.

   End nf2_inv_all.