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

Require drop1_defs.
Require getl_props.
Require aprem_defs.
Require arity_defs.
Require arity_gen.

   Section arity_props. (****************************************************)

      Hints Resolve le_S_n arity_repl : ld.

      Hint discr : ld := Extern 4 (drop ? ? ? ?) Simpl.

      Lemma arity_lift: (g:?; c2:?; t:?; a:?) (arity g c2 t a) ->
                        (c1:?; h,d:?) (drop h d c1 c2) ->
                        (arity g c1 (lift h d t) a).
      Proof.
      Intros until 1; XElim H; Clear c2 t a; Intros.
(* case 1: arity_sort *)
      Rewrite lift_sort; XAuto.
(* case 2: arity_abbr *)
      Apply (lt_le_e i d0); Intros.
(* case 2.1: i < d0 *)
      Rewrite lift_lref_lt; [ Intros | XAuto ].
      GetLDis; Rewrite minus_x_Sy in H2; [ Idtac | XAuto ].
      DropClear; XDEAuto 4.
(* case 2.2: i >= d0 *)
      GetLDis; Rewrite lift_lref_ge; XDEAuto 2.
(* case 3: arity_abst *)
      Apply (lt_le_e i d0); Intros.
(* case 3.1: i < d0 *)
      Rewrite lift_lref_lt; [ Intros | XAuto ].
      GetLDis; Rewrite minus_x_Sy in H2; [ Idtac | XAuto ].
      DropClear; XDEAuto 4.
(* case 3.2: i >= d0 *)
      GetLDis; Rewrite lift_lref_ge; XDEAuto 2.
(* case 4: arity_bind *)
      LiftHeadRw; XDEAuto 6.
(* case 5: arity_head *)
      LiftHeadRw; XAuto.
(* case 6: arity_appl *)
      LiftHeadRw; XDEAuto 4.
(* case 7: arity_flat *)
      LiftHeadRw; XDEAuto 4.
(* case 8: arity_repl *)
      XDEAuto 3.
      Qed.

      Hints Resolve arity_lift : ld.

      Lemma arity_lift1: (g:?; a:?; c2:?; hds:?; c1:?; t:?)
                         (drop1 hds c1 c2) -> (arity g c2 t a) ->
                         (arity g c1 (lift1 hds t) a).
      Proof.
      XElim hds; Simpl; Intros;
      Drop1GenBase; XDEAuto 3.
      Qed.

      Hints Resolve leq_sym leq_trans asucc_inj : ld.

      Theorem arity_mono: (g:?; c:?; t:?; a1:?) (arity g c t a1) ->
                          (a2:?) (arity g c t a2) -> (leq g a1 a2).
      Proof.
      Intros until 1; XElim H; Clear c t a1; Intros.
(* case 1: arity_sort *)
      ArityGenBase; XAuto.
(* case 2: arity_abbr *)
      ArityGenBase; GetLDis; XInv; Subst; XAuto.
(* case 3: arity_abst *)
      ArityGenBase; GetLDis; XInv; Subst; XDEAuto 5.
(* case 4: arity_bind *)
      ArityGenBase; XAuto.
(* case 5: arity_head *)
      ArityGenBase; XDEAuto 5.
(* case 6: arity_appl *)
      ArityGenBase; EApply ahead_inj_snd; XDEAuto 2.
(* case 7: arity_cast *)
      ArityGenBase; XDEAuto 4.
(* case 8: arity_repl *)
      XDEAuto 4.
      Qed.

      Lemma arity_cimp_conf: (g:?; c1:?; t:?; a:?) (arity g c1 t a) ->
                             (c2:?) (cimp c1 c2) -> (arity g c2 t a).
      Proof.
      Intros until 1; XElim H; Clear c1 t a; Intros.
(* case 1: arity_sort *)
      XAuto.
(* case 2: arity_abbr *)
      XDecomPose '(H2 ? ? ? ? H);
      GetLCImpDis; GetLDis; XInv; Subst; XDEAuto 3.
(* case 3: arity_abst *)
      XDecomPose '(H2 ? ? ? ? H);
      GetLCImpDis; GetLDis; XInv; Subst; XDEAuto 3.
(* case 4: arity_bind *)
      XDEAuto 5.
(* case 5: arity_head *)
      XDEAuto 5.
(* case 6: arity_appl *)
      XDEAuto 4.
(* case 7: arity_cast *)
      XDEAuto 4.
(* case 8: arity_repl *)
      XDEAuto 3.
      Qed.

      Hints Resolve arity_cimp_conf : ld.

      Lemma arity_aprem: (g:?; c:?; t:?; a:?) (arity g c t a) ->
                         (i:?; b:?) (aprem i a b) ->
                         (EX d u j | (drop (plus i j) (0) d c) &
                                     (arity g d u (asucc g b))
                         ).
      Proof.
      Intros until 1; XElim H; Clear c t a; Intros.
(* case 1: arity_sort *)
      APremGenBase.
(* case 2: arity_abbr *)
      XDecomPose '(H1 ? ? H2); Clear H0 H1 H2 a.
      GetLDis; Clear d u; XDEAuto 3.
(* case 3: arity_abst *)
      XPoseClear H1 '(H1 i0 b); XLApply H1; Clear H0 H2.
      XDecompose H1; GetLDis; Clear d u; XDEAuto 3.
(* case 4: arity_bind *)
      XDecomPose '(H3 ? ? H4); Clear H2 H3 H4 a2.
      DropS; Rewrite plus_n_Sm in H2; XDEAuto 2.
(* case 5: arity_head *)
      NewInduction i; Simpl in H3; APremGenBase.
(* case 5.1: i = 0 *)
      XDEAuto 3.
(* case 5.2: i > 0 *)
      Clear IHi; XDecomPose '(H2 ? ? H3); Clear H1 H2 H3 t a2.
      DropS; XDEAuto 3.
(* case 6: arity_appl *)
      Clear H H0 H1; Rename u into v.
      XPoseClear H2 '(H2 (S i) b); XLApply H2; Clear H3.
      XDecompose H2; Rename x0 into d; Rename x1 into u; Rename x2 into j.
      NewInduction d; DropGenBase.
(* case 6.1: CSort *)
      Do 2 XInv.
(* case 6.2: CHead k *)
      NewInduction k; Simpl in H.
(* case 6.2.1: Bind *)
      EApply ex2_3_intro;
         [ Rewrite <- plus_n_Sm; Apply drop_drop
         | Apply H0
         ]; XDEAuto 2.
(* case 6.2.2: Flat *)
      LApply (IHd H); [ Clear IHd H H0; Intros H | XDEAuto 2 ].
      XDecompose H; XDEAuto 2.
(* case 7: arity_cast *)
      XDecomPose '(H2 ? ? H3); Clear H2 H3; XDEAuto 2.
(* case 8: arity_repl *)
      XDecomPose '(aprem_repl ? ? ? H1 ? ? H2); Clear H1 H2.
      XDecomPose '(H0 ? ? H4); Clear H0 H4; XDEAuto 4.
      Qed.

   End arity_props.

      Hints Resolve arity_lift arity_lift1 : ld.

      Tactic Definition ArityDis := (
         Match Context With
            | [ H1: (arity ?0 ?1 ?2 ?3); H2: (arity ?0 ?1 ?2 ?4) |- ? ] ->
               LApply (arity_mono ?0 ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?4); [ Clear H1; Intros | XAuto ]
            | [ H1: (arity ? ? ? ?1); H2: (aprem ? ?1 ?) |- ? ] ->
               XDecomPose '(arity_aprem ? ? ? ? H1 ? ? H2); Clear H1
         ).

   Section more_arity_props. (***********************************************)

      Lemma arity_repellent: (g:?; c:?; w,t:?; a1:?)
                             (arity g (CHead c (Bind Abst) w) t a1) ->
                             (a2:?) (arity g c (THead (Bind Abst) w t) a2) ->
                             (leq g a1 a2) -> (P:Prop) P.
      Proof.
      Intros.
      XPoseClear H '(arity_repl ? ? ? ? H ? H1); Clear H1 a1.
      ArityGenBase; ArityDis; Clear H2 H3 c w t.
      EApply leq_ahead_false_2; XDEAuto 2.
      Qed.

   End more_arity_props.

   Section arity_heads_props. (**********************************************)

      Hints Resolve arity_repl : ld.

      Theorem arity_appls_cast: (g:?; c:?; u:?; t:?; vs:?; a:?)
                                (arity g c (THeads (Flat Appl) vs u) (asucc g a)) ->
                                (arity g c (THeads (Flat Appl) vs t) a) ->
                                (arity g c (THeads (Flat Appl) vs (THead (Flat Cast) u t)) a).
      Proof.
      XElim vs; Simpl; Intros.
(* case 1: nil *)
      XAuto.
(* case 2: cons *)
      Repeat ArityGenBase; ArityDis; XDEAuto 6.
      Qed.

      Hints Resolve arity_gen_lift : ld.

      Lemma arity_appls_abbr: (g:?; c,d:?; v:?; i:?) (getl i c (CHead d (Bind Abbr) v)) ->
                              (vs:?; a:?) (arity g c (THeads (Flat Appl) vs (lift (S i) (0) v)) a) ->
                              (arity g c (THeads (Flat Appl) vs (TLRef i)) a).
      Proof.
      XElim vs; Simpl; Intros.
(* case 1: nil *)
      GetLDrop; XDEAuto 3.
(* case 2: cons *)
      ArityGenBase; XDEAuto 3.
      Qed.

      Theorem arity_appls_bind: (g:?; b:?) ~b=Abst -> (c:?; v:?; a1:?)
                                (arity g c v a1) -> (t:?; vs:?; a2:?)
                                (arity g (CHead c (Bind b) v) (THeads (Flat Appl) (lifts (1) (0) vs) t) a2) ->
                                (arity g c (THeads (Flat Appl) vs (THead (Bind b) v t)) a2).
      Proof.
      XElim vs; Simpl; Intros.
(* case 1: nil *)
      XDEAuto 2.
(* case 2: cons *)
      ArityGenBase; XDEAuto 5.
      Qed.

   End arity_heads_props.