(****************************************************************************)
(*                                                                          *)
(*                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 pr0_lift.
Require wcpr0_defs.
Require pr3_defs.
Require arity_defs.
Require arity_gen.
Require arity_props.
Require arity_subst0.
Require csuba_defs.
Require csuba_props.

   Section arity_sred_wcpr0_pr0. (*******************************************)

      Hints Resolve arity_appls_appl arity_subst0 csuba_arity
                    arity_repl : ld.

      Lemma arity_sred_wcpr0_pr0: (g:?; c1:?; t1:?; a:?) (arity g c1 t1 a) ->
                                  (c2:?) (wcpr0 c1 c2) ->
                                  (t2:?) (pr0 t1 t2) ->
                                  (arity g c2 t2 a).
      Proof.
      Intros until 1; XElim H; Clear c1 t1 a; Intros.
(* case 1: arity_sort *)
      Pr0GenBase; Subst; XAuto.
(* case 2: arity_abbr *)
      Pr0GenBase; Subst; WCpr0GetL; XDEAuto 3.
(* case 3: arity_abst *)
      Pr0GenBase; Subst; WCpr0GetL; XDEAuto 3.
(* case 4: arity_bind *)
      InsertEq H5 '(THead (Bind b) u t).
      XElim H5; Clear y t2; Intros; XInv; Subst.
(* case 4.1: pr0_refl *)
      EApply arity_bind; XDEAuto 3. (**)
(* case 4.2: pr0_comp *)
      EApply arity_bind; XDEAuto 3. (**)
(* case 4.5: pr0_delta *)
      EApply arity_bind; XDEAuto 4. (**)
(* case 4.6: pr0_zeta *)
      EApply arity_gen_lift.
(* case 4.6.1: first premise *)
      Apply H3; [ Apply wcpr0_comp; XDEAuto 2 | XAuto ].
(* case 4.6.2: second premise *)
      XAuto.
(* case 5: arity_head *)
      InsertEq H4 '(THead (Bind Abst) u t);
      XElim H4; Clear y t2; Intros; XInv; Subst; Try EqFalse.
(* case 5.1: pr0_refl *)
      XAuto.
(* case 5.2: pr0_comp *)
      XAuto.
(* case 6: arity_appl *)
      InsertEq H4 '(THead (Flat Appl) u t).
      XElim H4; Clear y t2; Intros; XInv; Subst.
(* case 6.1: pr0_refl *)
      EApply arity_appl; XDEAuto 2. (**)
(* case 6.2: pr0_comp *)
      EApply arity_appl; XDEAuto 2.
(* case 6.3: pr0_beta *)
      Cut (arity g c2 v2 a1); [ Clear H H0 H4 H5 H7 u; Intros | XAuto ].
      Cut (arity g c2 (THead (Bind Abst) u0 t2) (AHead a1 a2)); [ Clear H1 H2 H3 H6 c t1; Intros | XAuto ].
      ArityGenBase; Subst; XInv; Subst; XDEAuto 4.
(* case 6.4: pr0_upsilon *)
      Cut (arity g c2 v2 a1); [ Clear H H0; Intros | XAuto ].
      Cut (arity g c2 (THead (Bind b) u2 t2) (AHead a1 a2)); [ Clear H1 H2; Intros | XAuto ].
      ArityGenBase; EApply arity_bind; XDEAuto 4. (**)
(* case 7: arity_cast *)
      InsertEq H4 '(THead (Flat Cast) u t).
      XElim H4; Clear y t2; Intros; XInv; Subst.
(* case 7.1: pr0_refl *)
      EApply arity_cast; XAuto. (**)
(* case 7.2: pr0_comp *)
      EApply arity_cast; XAuto. (**)
(* case 7.7: pr0_tau *)
      XAuto.
(* case 7: arity_repl *)
      XDEAuto 3.
      Qed.

   End arity_sred_wcpr0_pr0.

   Section arity_sred_pr3.

      Hints Resolve arity_subst0 arity_sred_wcpr0_pr0 : ld.

      Lemma arity_sred_wcpr0_pr1: (t1,t2:?) (pr1 t1 t2) ->
                                  (g:?; c1:?; a:?) (arity g c1 t1 a) ->
                                  (c2:?) (wcpr0 c1 c2) -> (arity g c2 t2 a).
      Proof.
      Intros until 1; XElim H; Clear t1 t2; Intros.
(* case 1: pr1_refl *)
      XDEAuto 2.
(* case 2: pr1_sing *)
      XDEAuto 3.
      Qed.

      Lemma arity_sred_pr2: (c:?; t1,t2:?) (pr2 c t1 t2) ->
                            (g:?; a:?) (arity g c t1 a) ->
                            (arity g c t2 a).
      Proof.
      Intros until 1; XElim H; Clear c t1 t2; Intros.
(* case 1: pr2_free *)
      XDEAuto 2.
(* case 2: pr2_delta *)
      XDEAuto 3.
      Qed.

      Hints Resolve arity_sred_pr2 : ld.

      Lemma arity_sred_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) ->
                            (g:?; a:?) (arity g c t1 a) ->
                            (arity g c t2 a).
      Proof.
      Intros until 1; XElim H; Clear t1 t2; Intros.
(* case 1: pr3_refl *)
      XDEAuto 1.
(* case 2: pr3_sing *)
      XDEAuto 3.
      Qed.

   End arity_sred_pr3.

      Tactic Definition AritySRed := (
         Match Context With
            | [ H0: (pr3 ?1 ?2 ?3); H1: (arity ?0 ?1 ?2 ?4) |- ? ] ->
               LApply (arity_sred_pr3 ?1 ?2 ?3); [ Intros H_x | XAuto ];
               LApply (H_x ?0 ?4); [ Clear H_x H1; Intros | XAuto ]
         ).

      Tactic Definition AritySRedKeep := (
         Match Context With
            | [ H0: (pr3 ?1 ?2 ?3); H1: (arity ?0 ?1 ?2 ?4) |- ? ] ->
               LApply (arity_sred_pr3 ?1 ?2 ?3); [ Intros H_x | XAuto ];
               LApply (H_x ?0 ?4); [ Clear H_x H0; Intros | XAuto ]
         ).