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

Require aprem_defs.
Require arity_defs.
Require arity_gen.
Require arity_props.
Require arity_sred.
Require sc3_defs.
Require sc3_props.
Require sc3_arity.
Require ty3_defs.
Require ty3_gen.
Require ty3_props.
Require ty3_sred_props.

   Section ty3_arity_props. (************************************************)

      Hints Resolve getl_drop leq_sym arity_repl : ld.

      Lemma ty3_arity: (g:?; c:?; t1,t2:?) (ty3 g c t1 t2) ->
                       (EX a1 | (arity g c t1 a1) &
                                (arity g c t2 (asucc g a1))
                       ).
      Proof.
      Intros until 1; XElim H; Clear c t1 t2; Intros.
(* case 1: ty3_conv *)
      XDecompose H0; XDecompose H2; Clear H H1 H5.
      Pc3Unfold; Repeat AritySRedKeep; ArityDis; Subst; XDEAuto 4.
(* case 2: ty3_sort *)
      EApply ex2_intro; [ XAuto | Simpl; XAuto ].
(* case 3: ty3_abbr *)
      XDecompose H1; Clear H0; XDEAuto 5.
(* case 4: ty3_abst *)
      XDecompose H1; Clear H0.
      XDecomPose '(leq_asucc g x); XDEAuto 7.
(* case 5: ty3_bind *)
      XDecompose H0; XDecompose H2; Clear H H1.
      XDecomPose '(leq_asucc g x); NewInduction b; XDEAuto 7.
(* case 6: ty3_appl *)
      XDecompose H0; XDecompose H2; Clear H H1.
      ArityGenBase; SymEqual; ASuccGenBase; Subst.
      ArityDis; Subst; ASuccDis; XDEAuto 7.
(* case 7: ty3_cast *)
      XDecompose H0; XDecompose H2; ArityDis; XDEAuto 6.
      Qed.

      Lemma ty3_predicative: (g:?; c:?; v,t,u:?)
                             (ty3 g c (THead (Bind Abst) v t) u) ->
                             (pc3 c u v) -> (P:Prop) P.
      Proof.
      Intros; Move H after P; NonLinear.
      Ty3GenBase; Clear H3 H4 H1 x0 x2.
      XPoseClear H '(ty3_conv ? ? ? ? H2 ? ? H H0); Clear H2 H0 x1 u.
      XDecomPose '(ty3_arity ? ? ? ? H); Clear H.
      ArityGenBase; ArityDis; Clear H2 H3 c v t.
      EApply leq_ahead_asucc_false; Simpl in H; XDEAuto 2.
      Qed.

      Theorem ty3_repellent: (g:?; c:?; w,t,u1:?)
                             (ty3 g c (THead (Bind Abst) w t) u1) -> (u2:?)
                             (ty3 g (CHead c (Bind Abst) w) t (lift (1) (0) u2)) ->
                             (pc3 c u1 u2) -> (P:Prop) P.
      Proof.
      Intros.
      Ty3Correct; Ty3Gen; Clear H3 x.
      XPoseClear H4 '(ty3_conv ? ? ? ? H4 ? ? H H1); Clear H H1 u1 x0.
      XDecomPoseClear H0 '(ty3_arity ? ? ? ? H0).
      XDecomPoseClear H4 '(ty3_arity ? ? ? ? H4).
      ArityGen; ArityDis; ASuccDis; Clear H2 u2.
      EApply arity_repellent; XDEAuto 2.
      Qed.

      Lemma ty3_acyclic: (g:?; c:?; t,u:?)
                         (ty3 g c t u) -> (pc3 c u t) -> (P:Prop) P.
      Proof.
      Intros.
      XPoseClear H '(ty3_conv ? ? ? ? H ? ? H H0); Clear H0 u.
      XDecomPose '(ty3_arity ? ? ? ? H); Clear H.
      ArityDis; Clear H0 c t.
      EApply leq_asucc_false; XDEAuto 2.
      Qed.

      Hints Resolve sc3_sn3 : ld.

      Lemma ty3_sn3: (g:?; c:?; t,u:?) (ty3 g c t u) -> (sn3 c t).
      Proof.
      Intros; XDecomPoseClear H '(ty3_arity ? ? ? ? H); XDEAuto 3.
      Qed.

   End ty3_arity_props.