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

Require lift_gen.
Require lift_props.
Require subst1_defs.
Require subst1_lift.
Require subst1_confluence.
Require getl_props.
Require csubst1_defs.
Require pc3_gen.
Require pc3_gen_context.
Require ty3_defs.
Require ty3_lift.

(* NOTE: these break the recursion between ty3_sred_cpr_pr0 and ty3_gen_lift *)

   Section ty3_gen_cabbr. (**************************************************)

      Hints Resolve le_S_n le_lt_trans lt_le_minus : ld.

      Tactic Definition IH d a0 a := (
         Match Context With
            | [ H: (e:?; u:?; d:?) ? -> (a0:?) ? -> (a:?) ? -> ? |- ? ] ->
               LApply (H e u0 d); [ Clear H; Intros H | XAuto ];
               LApply (H a0); [ Clear H; Intros H | XAuto ];
               LApply (H a); [ Clear H; Intros H | XDEAuto 2 ];
               XDecompose H
         ).

(* NOTE: This can be generalized removing the last two premises *)
      Lemma ty3_gen_cabbr: (g:?; c:?; t1,t2:?) (ty3 g c t1 t2) ->
                           (e:?; u:?; d:?) (getl d c (CHead e (Bind Abbr) u)) ->
                           (a0:?) (csubst1 d u c a0) ->
                           (a:?) (drop (1) d a0 a) ->
                           (EX y1 y2 | (subst1 d u t1 (lift (1) d y1)) &
                                       (subst1 d u t2 (lift (1) d y2)) &
                                       (ty3 g a y1 y2)
                           ).
      Proof.
      Intros until 1; XElim H; Clear c t1 t2; Intros.
(* case 1: ty3_conv *)
      Repeat IH d a0 a; EApply ex3_2_intro;
      [ XDEAuto 2 | XDEAuto 2 | EApply ty3_conv; Try EApply pc3_gen_cabbr; XDEAuto 2 ].
(* case 2: ty3_sort *)
      EApply ex3_2_intro; Try Rewrite lift_sort; XAuto.
(* case 3: ty3_abbr *)
      Apply (lt_eq_gt_e n d0); Intros.
(* case 3.1: n < d0 *)
      Clear H0; GetLDis; Rewrite minus_x_Sy in H0; [ GetLGenBase | XAuto ].
      CSubst1GetL; Rewrite minus_x_Sy in H; [ Idtac | XAuto ].
      CSubst1GenBase; Subst.
      Rewrite (lt_plus_minus n d0) in H4; [ Idtac | XAuto ].
      GetLDis; Subst; IH '(minus d0 (S n)) x1 x3.
      Subst1Confluence; Subst.
      Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
      Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
      EApply ex3_2_intro;
      [ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty3_abbr ]; XDEAuto 2.
(* case 3.2: n = d0 *)
      Subst; Clear H1.
      GetLDis; XInv; Subst; CSubst1GetL; GetLDis.
      EApply ex3_2_intro;
      [ EApply subst1_single; Rewrite lift_free; Simpl; XDEAuto 2
      | Rewrite lift_free; Simpl; XDEAuto 2
      | XDEAuto 2 ].
(* case 3.3: n > d0 *)
      Clear H1 H2 e; CSubst1GetL; GetLDis.
      Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XDEAuto 2 ].
      Arith4c '(0) '(minus n (1)).
      EApply ex3_2_intro;
      [ Rewrite lift_lref_ge
      | Rewrite lift_free; Simpl
      | Pattern 2 n; Rewrite (minus_x_SO n)
      ]; XDEAuto 3.
(* case 4: ty3_abst *)
      Apply (lt_eq_gt_e n d0); Intros.
(* case 4.1: n < d0 *)
      Clear H0; GetLDis; Rewrite minus_x_Sy in H0; [ GetLGenBase | XAuto ].
      CSubst1GetL; Rewrite minus_x_Sy in H; [ Idtac | XAuto ].
      CSubst1GenBase; Subst.
      Rewrite (lt_plus_minus n d0) in H4; [ Idtac | XAuto ].
      GetLDis; Subst; IH '(minus d0 (S n)) x1 x3.
      Subst1Confluence; Subst.
      Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
      Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
      EApply ex3_2_intro;
      [ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty3_abst ]; XDEAuto 2.
(* case 4.2: n = d0 *)
      Subst; GetLDis; XInv.
(* case 4.3: n > d0 *)
      Clear H1 H2 e; CSubst1GetL; GetLDis.
      Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XDEAuto 2 ].
      Arith4c '(0) '(minus n (1)).
      EApply ex3_2_intro;
      [ Rewrite lift_lref_ge
      | Rewrite lift_free; Simpl
      | Pattern 2 n; Rewrite (minus_x_SO n)
      ]; XDEAuto 3.
(* case 5: ty3_bind *)
      IH d a0 a; Clear H H1.
      IH '(S d) '(CHead a0 (Bind b) (lift (1) d x0)) '(CHead a (Bind b) x0).
      EApply ex3_2_intro; Try Rewrite lift_bind; XDEAuto 2.
(* case 6: ty3_appl *)
      Repeat IH d a0 a; Clear H H0 H1.
      Subst1GenBase; SymEqual; LiftGenBase; Subst.
      Subst1Confluence; Subst.
      EApply ex3_2_intro; Try Rewrite lift_flat;
      [ Idtac | EApply subst1_head; [ Idtac | Rewrite lift_bind ] | Idtac ]; XDEAuto 2.
(* case 7: ty3_cast *)
      Rename u into u0; Repeat IH d a0 a; Clear H H1.
      Subst1Confluence; Subst.
      EApply ex3_2_intro; Try Rewrite lift_flat; XDEAuto 2.
      Qed.

   End ty3_gen_cabbr.

   Section ty3_gen_cvoid. (**************************************************)

      Hints Resolve sym_eq le_S_n le_lt_trans lt_le_minus : ld.

      Hints Resolve lift_bind ty3_conv : ld.

      Tactic Definition IH d a := (
         Match Context With
            | [ H: (e:?; u:?; d:?) ? -> (a:?) ? -> ? |- ? ] ->
               LApply (H e u0 d); [ Clear H; Intros H | XAuto ];
               LApply (H a); [ Clear H; Intros H | XDEAuto 2 ];
               XDecompose H; Subst
         ).

(* NOTE: This can be generalized removing the last premise *)
      Lemma ty3_gen_cvoid: (g:?; c:?; t1,t2:?) (ty3 g c t1 t2) ->
                           (e:?; u:?; d:?) (getl d c (CHead e (Bind Void) u)) ->
                           (a:?) (drop (1) d c a) ->
                           (EX y1 y2 | t1 = (lift (1) d y1) &
                                       t2 = (lift (1) d y2) &
                                       (ty3 g a y1 y2)
                           ).
      Proof.
      Intros until 1; XElim H; Clear c t1 t2; Intros.
(* case 1: ty3_conv *)
      Repeat IH d a; Subst; Pc3Gen; XDEAuto 3.
(* case 2: ty3_sort *)
      EApply ex3_2_intro; Try Rewrite lift_sort; XDEAuto 2.
(* case 3: ty3_abbr *)
      Apply (lt_eq_gt_e n d0); Intros.
(* case 3.1: n < d0 *)
      GetLDis; Rewrite minus_x_Sy in H5; [ GetLGenBase | XAuto ].
      Rewrite (lt_plus_minus n d0) in H3; [ Idtac | XAuto ].
      GetLDis; Subst; IH '(minus d0 (S n)) x1; LiftGen; Subst.
      Rewrite <- lift_d; [ Idtac | XAuto ].
      Rewrite <- le_plus_minus; [ Idtac | XAuto ].
      EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty3_abbr ]; XDEAuto 2.
(* case 3.2: n = d0 *)
      Subst; GetLDis; XInv.
(* case 3.3: n > d0 *)
      Clear H1 H2 e u0; GetLDis.
      Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XDEAuto 2 ].
      Arith4c '(0) '(minus n (1)).
      EApply ex3_2_intro;
      [ Rewrite lift_lref_ge
      | Rewrite lift_free; Simpl
      | Pattern 2 n; Rewrite (minus_x_SO n)
      ]; XDEAuto 3.
(* case 4: ty3_abst *)
      Apply (lt_eq_gt_e n d0); Intros.
(* case 4.1: n < d0 *)
      GetLDis; Rewrite minus_x_Sy in H5; [ GetLGenBase | XAuto ].
      Rewrite (lt_plus_minus n d0) in H3; [ Idtac | XAuto ].
      GetLDis; Subst; IH '(minus d0 (S n)) x1; LiftGen; Subst.
      Rewrite <- lift_d; [ Idtac | XAuto ].
      Rewrite <- le_plus_minus; [ Idtac | XAuto ].
      EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty3_abst ]; XDEAuto 2.
(* case 4.2: n = d0 *)
      Subst; GetLDis; XInv.
(* case 4.3: n > d0 *)
      Clear H1 H2 e u0; GetLDis.
      Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XDEAuto 2 ].
      Arith4c '(0) '(minus n (1)).
      EApply ex3_2_intro;
      [ Rewrite lift_lref_ge
      | Rewrite lift_free; [ Simpl | Simpl | Idtac ]
      | Pattern 2 n; Rewrite (minus_x_SO n)
      ]; XDEAuto 3.
(* case 5: ty3_bind *)
      IH d a; Clear H H1.
      IH '(S d) '(CHead a (Bind b) x0).
      XDEAuto 5.
(* case 6: ty3_appl *)
      IH d a; Subst; Clear H H1.
      LiftGenBase; Subst; IH d a.
      LiftGen; Subst; LiftHeadRwBack; XDEAuto 3.
(* case 7: ty3_cast *)
      Rename u into u0.
      IH d a; IH d a; Clear H H1.
      LiftGen; Subst; LiftHeadRwBack; XDEAuto 3.
      Qed.

   End ty3_gen_cvoid.

      Tactic Definition Ty3GenContext := (
         Match Context With
            | [ H: (ty3 ?1 (CHead ?2 (Bind Abbr) ?3) ?4 ?5) |- ? ] ->
               LApply (ty3_gen_cabbr ?1 (CHead ?2 (Bind Abbr) ?3) ?4 ?5); [ Clear H; Intros H | XAuto ];
               LApply (H ?2 ?3 (0)); [ Clear H; Intros H | XAuto ];
               LApply (H (CHead ?2 (Bind Abbr) ?3)); [ Clear H; Intros H | XAuto ];
               LApply (H ?2); [ Clear H; Intros H | XAuto ];
               XDecompose H
            | [ H: (ty3 ?1 (CHead ?2 (Bind Void) ?3) ?4 ?5) |- ? ] ->
               LApply (ty3_gen_cvoid ?1 (CHead ?2 (Bind Void) ?3) ?4 ?5); [ Clear H; Intros H | XAuto ];
               LApply (H ?2 ?3 (0)); [ Clear H; Intros H | XAuto ];
               LApply (H ?2); [ Clear H; Intros H | XAuto ];
               XDecompose H
            | [ |- ? ] -> Ty3GenBase
         ).