(****************************************************************************)
(*                                                                          *)
(*                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 subst0_defs.
Require dnf_dec.
Require arity_defs.

   Section arity_gen. (******************************************************)

      Lemma arity_gen_cvoid_subst0: (g:?; c:?; t:?; a:?) (arity g c t a) ->
                                    (d:?; u:?; i:?) (getl i c (CHead d (Bind Void) u)) ->
                                    (w,v:?) (subst0 i w t v) -> (P:Prop) P.
      Proof.
      Intros until 1; XElim H; Clear c t a; Intros.
(* case 1: arity_sort *)
      Subst0GenBase.
(* case 2: arity_abbr *)
      Subst0GenBase; Subst; GetLDis; XInv.
(* case 3: arity_abst *)
      Subst0GenBase; Subst; GetLDis; XInv.
(* case 4: arity_bind *)
      Subst0GenBase; Subst;
      Solve [ (EApply H1; XDEAuto 1) | (EApply H3; XDEAuto 3) ].
(* case 5: arity_head *)
      Subst0GenBase; Subst;
      Solve [ (EApply H0; XDEAuto 1) | (EApply H2; XDEAuto 3) ].
(* case 6: arity_appl *)
      Subst0GenBase; Subst;
      Solve [ (EApply H0; XDEAuto 1) | (EApply H2; XDEAuto 3) ].
(* case 7: arity_cast *)
      Subst0GenBase; Subst;
      Solve [ (EApply H0; XDEAuto 1) | (EApply H2; XDEAuto 3) ].
(* case 8: arity_repl *)
      EApply H0; XDEAuto 2.
      Qed.

      Lemma arity_gen_cvoid: (g:?; c:?; t:?; a:?) (arity g c t a) ->
                             (d:?; u:?; i:?) (getl i c (CHead d (Bind Void) u)) ->
                             (EX v | t = (lift (1) i v)).
      Proof.
      Intros; XDecomPose '(dnf_dec u t i); Subst.
(* case 1: subst0 *)
      EApply arity_gen_cvoid_subst0; XDEAuto 1.
(* case 2: lift *)
      XDEAuto 2.
      Qed.

      Hints Resolve arity_repl : ld.

      Lemma arity_gen_lift: (g:?; c1:?; t:?; a:?; h,d:?)
                            (arity g c1 (lift h d t) a) ->
                            (c2:?) (drop h d c1 c2) ->
                            (arity g c2 t a).
      Proof.
      Intros until 1; InsertEq H '(lift h d t).
      UnIntro H t; UnIntro H d; XElim H; Clear c1 y a; Intros.
(* case 1: arity_sort *)
      LiftGenBase; Subst; XAuto.
(* case 2: arity_abbr *)
      LiftXGenBase; Subst.
(* case 2.1: i < d *)
      Rewrite (lt_plus_minus i x) in H3; [ Idtac | XAuto ].
      GetLDis; Subst; XDEAuto 3.
(* case 2.2: i >= d + h *)
      GetLDis; XDEAuto 2.
(* case 3: arity_abst *)
      LiftXGenBase; Subst.
(* case 3.1: i < d *)
      Rewrite (lt_plus_minus i x) in H3; [ Idtac | XAuto ].
      GetLDis; Subst; XDEAuto 3.
(* case 3.2: i >= d + h *)
      GetLDis; XDEAuto 2.
(* case 4: arity_bind *)
      LiftGenBase; Subst; XDEAuto 5.
(* case 5: arity_head *)
      LiftGenBase; Subst; XDEAuto 5.
(* case 6: arity_appl *)
      LiftGenBase; Subst; XDEAuto 4.
(* case 7: arity_cast *)
      LiftGenBase; Subst; XDEAuto 4.
(* case 8: arity_repl *)
      XDEAuto 3.
      Qed.

   End arity_gen.

      Tactic Definition ArityGen := (
         Match Context With
            | [ H: (arity ?0 (CHead ?1 (Bind Void) ?2) ?3 ?4) |- ? ] ->
               LApply (arity_gen_cvoid ?0 (CHead ?1 (Bind Void) ?2) ?3 ?4); [ Clear H; Intros H | XAuto ];
               LApply (H ?1 ?2 (0)); [ Clear H; Intros H | XAuto ];
               XDecompose H
            | [ H: (arity ? (CHead ?0 (Bind ?) ?) (lift (S O) O ?) ?) |- ? ] ->
               LApply (arity_gen_lift ? ? ? ? ? ? H ?0); [ Clear H; Intros | XAuto ]
            | [ H1: (arity ? ?0 (lift ?1 ?2 ?) ?); H2: (drop ?1 ?2 ?0 ?) |- ? ] ->
               XPoseClear H1 '(arity_gen_lift ? ? ? ? ? ? H1 ? H2)
            | [ |- ? ] -> ArityGenBase
         ).