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

Require getl_props.
Require pr3_confluence.
Require nf2_props.
Require sn3_defs.
Require sn3_props.
Require pc3_props.
Require ty3_defs.
Require ty3_gen.
Require ty3_props.
Require ty3_sred.
Require ty3_sred_props.
Require ty3_arity_props.

   Section ty3_inference. (**************************************************)

      Hints Resolve pr3_t : ld.

      Theorem pc3_dec: (g:?; c:?; u1,t1:?) (ty3 g c u1 t1) ->
                       (u2,t2:?) (ty3 g c u2 t2) ->
                       (pc3 c u1 u2) \/ ((pc3 c u1 u2) -> False).
      Proof.
      Intros.
      XPoseClear H '(ty3_sn3 ? ? ? ? H); Clear t1.
      XPoseClear H0 '(ty3_sn3 ? ? ? ? H0); Clear g t2.
      XDecomPoseClear H '(nf2_sn3 ? ? H).
      XDecomPoseClear H0 '(nf2_sn3 ? ? H0).
      XDecomPose '(term_dec x x0); Subst.
(* case 1: x = x0 *)
      XDEAuto 3.
(* case 2: x <> x0 *)
      Right; Intros; Pc3Unfold.
      XDecomPose '(pr3_confluence ? ? ? H ? H6); Clear H H6 u2.
      XPoseClear H4 '(nf2_pr3_unfold ? ? ? H4 H3); Subst.
      XPose H '(nf2_pr3_confluence ? ? H2 ? H3 ? H1).
      EApply H0; XDEAuto 3.
      Qed.

      Hints Resolve sym_equal : ld.

      Theorem pc3_abst_dec: (g:?; c:?; u1,t1:?) (ty3 g c u1 t1) ->
                            (u2,t2:?) (ty3 g c u2 t2) ->
                            (EX u v2 | (pc3 c u1 (THead (Bind Abst) u2 u)) &
                                       (ty3 g c (THead (Bind Abst) v2 u) t1) &
                                       (pr3 c u2 v2) & (nf2 c v2)
                            ) \/
                            ((u:?) (pc3 c u1 (THead (Bind Abst) u2 u)) -> False).
      Proof.
      Intros.
      XPose H1 '(ty3_sn3 ? ? ? ? H).
      XPose H2 '(ty3_sn3 ? ? ? ? H0).
      XDecomPoseClear H1 '(nf2_sn3 ? ? H1).
      XDecomPoseClear H2 '(nf2_sn3 ? ? H2).
      XDecomPose '(abst_dec x x0); Subst.
(* case 1: x is Abst x0 *)
      Ty3SRed; XDEAuto 5.
(* case 2: x is not Abst x0 *)
      Right; Intros; Pc3Unfold; Pr3Confluence; Clear H H0 u1 t1 t2.
      XPoseClear H6 '(nf2_pr3_unfold ? ? ? H6 H4); Subst.
      Repeat (Pr3GenBase; Subst); NF2GenBase; Clear H3 H6 H8 u u0 x3.
      XPose H3 '(nf2_pr3_confluence ? ? H5 ? H ? H1).
      EApply H2; XDEAuto 5.
      Qed.

      Hints Resolve ex2_sym getl_flt pc3_t ty3_conv ty3_tred : ld.

      Lemma ty3_inference: (g:?; c:?; t1:?)
                           ( (*#* #xp *) EX t2 | (ty3 g c t1 t2)) \/
                           ((t2:?) (ty3 g c t1 t2) -> False).
      Proof.
      Intros; Pattern c t1; Apply flt_wf_ind; Clear c t1.
      Intros c2 t2; XElim t2; Intros.
(* case 1: TSort *)
      XDEAuto 3.
(* case 2: TBRef n *)
      XDecomPose '(getl_dec c2 n).
(* case 2.1: index is valid *)
      LApply (H x0 x2); [ Clear H; Intros H; XDecompose H | XDEAuto 2 ].
(* case 2.1.1: x2 is typable *)
      NewInduction x1; [ XDEAuto 4 | XDEAuto 4 | Right; Intros; Clear IHx1 ].
      Ty3GenBase; GetLDis; XInv.
(* case 2.1.2: x2 is not typable *)
      Right; Intros.
      Ty3GenBase; GetLDis; XInv; Subst; EApply H0; XDEAuto 2.
(* case 2.2: index is invalid *)
      Right; Intros; Ty3GenBase; EApply H0; XDEAuto 2.
(* case 3: THead k *)
      NewInduction k.
(* case 3.1: Bind b *)
      LApply (H1 c2 t); [ Intros H2; XDecompose H2 | XAuto ].
(* case 3.1.1: t is typable *)
      LApply (H1 (CHead c2 (Bind b) t) t0); [ Clear H1; Intros H1; XDecompose H1 | XAuto ].
(* case 3.1.1.1: t0 is typable *)
      XDEAuto 4.
(* case 3.1.1.2: t0 is not typable *)
      Right; Intros; Ty3GenBase; EApply H2; XDEAuto 2.
(* case 3.1.2: t is not typable *)
      Right; Intros; Ty3GenBase; EApply H3; XDEAuto 2.
(* case 3.2: Flat f *)
      NewInduction f.
(* case 3.2.1: Appl *)
      LApply (H1 c2 t); [ Intros H2; XDecompose H2 | XAuto ].
(* case 3.2.1.1: t is typable *)
      LApply (H1 c2 t0); [ Clear H1; Intros H1; XDecompose H1 | XAuto ].
(* case 3.2.1.1.1: t0 is typable *)
      Ty3Correct; Move H4 after H1; Ty3Correct.
      Rename t into u; Rename x into u0; Rename x2 into u1.
      Rename t0 into t; Rename x0 into t0; Rename x1 into t1.
      XPose H5 '(ty3_sn3 ? ? ? ? H2).
      XDecomPoseClear H5 '(nf2_sn3 ? ? H5).
      Rename x into nu0.
      XPose H5 '(ty3_sred_pr3 ? ? ? H6 ? ? H2).
      XDecomPose '(pc3_abst_dec ? ? ? ? H1 ? ? H5).
(* case 3.2.1.1.1.1: t0 converts to Abst nu0 *)
      XPoseClear H12 '(nf2_pr3_unfold ? ? ? H11 H7); Subst; Clear H11.
      Left; EApply ex_intro.
      EApply ty3_appl; [ Idtac | XDEAuto 2 ]; XDEAuto 2.
(* case 3.2.1.1.1.2: t0 does not convert to Abst nu0 *)
      Right; Intros; Ty3GenBase; Ty3Dis; Ty3Dis; EApply H8.
      EApply pc3_t; [ Apply pc3_s; Apply H10 | XDEAuto 4 ].
(* case 3.2.1.1.2: t0 is not typable *)
      Right; Intros; Ty3GenBase; EApply H2; XDEAuto 2.
(* case 3.2.1.2: t is not typable *)
      Right; Intros; Ty3GenBase; EApply H3; XDEAuto 2.
(* case 3.2.2: Cast *)
      Clear H H0.
      LApply (H1 c2 t); [ Intros H2; XDecompose H2 | XAuto ].
(* case 3.2.2.1: t is typable *)
      LApply (H1 c2 t0); [ Clear H1; Intros H1; XDecompose H1 | XAuto ].
(* case 3.2.2.1.1: t0 is typable *)
      Ty3Correct.
      Rename t into u; Rename x into u0.
      Rename t0 into t; Rename x0 into t0; Rename x1 into t1.
      XDecomPose '(pc3_dec ? ? ? ? H ? ? H0).
(* case 3.2.2.1.1.1: t0 and u are convertible *)
      XDEAuto 5.
(* case 3.2.2.1.1.2: t0 and u are not convertible *)
      Right; Intros; Ty3GenBase; Repeat Ty3Dis; EApply H1; XAuto.
(* case 3.2.2.1.2: t0 is not typable *)
      Right; Intros; Ty3GenBase; EApply H; XDEAuto 2.
(* case 3.2.2.2: t is not typable *)
      Right; Intros; Ty3GenBase; Ty3Correct; EApply H; XDEAuto 2.
      Qed.

   End ty3_inference.