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

Require subst0_gen.
Require dnf_dec.
Require pr3_defs.
Require pr0_gen.

   Section nf0_dec. (********************************************************)

      Lemma nf0_dec: (t1:?) ((t2:?) (pr0 t1 t2) -> t1 = t2) \/
                     (EX t2 | (t1 = t2 -> (P:Prop) P) & (pr0 t1 t2)).
      Proof.
      XElim t1; Intros.
(* case 1: TSort *)
      Left; Intros; Pr0Gen; Subst; XAuto.
(* case 2: TLRef *)
      Left; Intros; Pr0Gen; Subst; XAuto.
(* case 3: THead *)
      NewInduction k.
(* case 3.1: Bind *)
      NewInduction b.
(* case 3.1.1: Abbr *)
      Right; Clear H H0; XDecomPose '(dnf_dec t t0 (0)); Subst.
(* case 3.1.1.1: pr0_delta *)
      EApply ex2_intro; [ Intros | EApply pr0_delta; XDEAuto 2 ].
      XInv; Subst; Subst0XGenBase.
(* case 3.1.1.2: pr0_zeta *)
      EApply ex2_intro; [ Intros | Apply pr0_zeta; XDEAuto 2 ].
      TInv.
(* case 3.1.2: Abst *)
      XDecompose H; [ XDecompose H0 | Idtac ].
(* case 3.1.2.1: t,t0 normal *)
      Left; Intros; Pr0Gen.
      XPoseClear H '(H ? H3); XPoseClear H1 '(H1 ? H2); Subst; XAuto.
(* case 3.1.2.2: t normal, t0 not normal *)
      Right; EApply ex2_intro; [ Intros | EApply pr0_comp; XDEAuto 2 ].
      XInv; Subst; Apply H2; XAuto.
(* case 3.1.2.3: t not normal *)
      Right; EApply ex2_intro; [ Intros | EApply pr0_comp; XDEAuto 2 ].
      XInv; Subst; Apply H2; XAuto.
(* case 3.1.3: Void *)
      XDecomPose '(dnf_dec t t0 (0)); Subst.
(* case 3.1.3.1: not pr0_zeta *)
      XDecompose H; [ XDecompose H0 | Idtac ].
(* case 3.1.3.1.1: t,t0 normal *)
      Left; Intros; Pr0Gen.
(* case 3.1.3.1.1.1: pr0_comp *)
      XPoseClear H '(H ? H4); XPoseClear H1 '(H1 ? H3); Subst; XAuto.
(* case 3.1.3.1.1.2: pr0_zeta *)
      XPoseClear H '(H ? H0); Clear H0 H1; Subst; Subst0Gen.
(* case 3.1.3.1.2: t normal, t0 not normal *)
      Right; EApply ex2_intro; [ Intros | EApply pr0_comp; XDEAuto 2 ].
      XInv; Subst; Apply H3; XAuto.
(* case 3.1.3.1.3: t not normal *)
      Right; EApply ex2_intro; [ Intros | EApply pr0_comp; XDEAuto 2 ].
      XInv; Subst; Apply H3; XAuto.
(* case 3.1.3.2: pr0_zeta *)
      Right; EApply ex2_intro; [ Intros | Apply pr0_zeta; XDEAuto 2 ].
      TInv.
(* case 3.2: Flat *)
      NewInduction f.
(* case 3.2.1: Appl *)
      XDecomPose '(binder_dec t0); Subst.
(* case 3.2.1.1: t0 is a binder *)
      NewInduction x0.
(* case 3.2.1.1.1: pr0_upsilon *)
      Right; EApply ex2_intro; [ Intros | Apply pr0_upsilon; XDEAuto 2 ].
      XInv.
(* case 3.2.1.1.2: pr0_beta *)
      Right; EApply ex2_intro; [ Intros | Apply pr0_beta; XDEAuto 2 ].
      XInv.
(* case 3.2.1.1.3: pr0_upsilon *)
      Right; EApply ex2_intro; [ Intros | Apply pr0_upsilon; XDEAuto 2 ].
      XInv.
(* case 3.2.1.2: t0 is not a binder *)
      XDecompose H; [ XDecompose H0 | Idtac ].
(* case 3.2.1.2.1: t,t0 normal *)
      Left; Intros; Pr0Gen.
(* case 3.2.1.2.1.1: pr0_comp *)
      XPoseClear H '(H ? H4); XPoseClear H2 '(H2 ? H3); Subst; XAuto.
(* case 3.2.1.2.1.2: pr0_beta *)
      Subst; EApply H1; XAuto.
(* case 3.2.1.2.1.3: pr0_upsilon *)
      Subst; EApply H1; XAuto.
(* case 3.2.1.2.2: t normal, t0 not normal *)
      Right; EApply ex2_intro; [ Intros | EApply pr0_comp; XDEAuto 2 ].
      XInv; Subst; Apply H3; XAuto.
(* case 3.2.1.2.3: t not normal *)
      Right; EApply ex2_intro; [ Intros | EApply pr0_comp; XDEAuto 2 ].
      XInv; Subst; Apply H3; XAuto.
(* case 3.2.2: Cast *)
      Right; Clear H H0.
      EApply ex2_intro; [ Intros | EApply pr0_tau; XDEAuto 2 ].
      TInv.
      Qed.

   End nf0_dec.