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

Require subst0_gen.
Require subst0_lift.
Require getl_props.
Require pr0_gen.
Require pr0_subst0.
Require pr2_defs.

   Section pr2_gen. (********************************************************)

      Lemma pr2_gen_appl: (c:?; u1,t1,x:?)
                          (pr2 c (THead (Flat Appl) u1 t1) x) -> (OR
                          (EX u2 t2 | x = (THead (Flat Appl) u2 t2) &
                                      (pr2 c u1 u2) & (pr2 c t1 t2)
                          ) |
                          (EX y1 z1 u2 t2 | t1 = (THead (Bind Abst) y1 z1) &
                                            x = (THead (Bind Abbr) u2 t2) &
                                            (pr2 c u1 u2) & (b:?; u:?)
                                            (pr2 (CHead c (Bind b) u) z1 t2)
                          ) |
                          (EX b y1 z1 z2 u2 y2 |
                              ~b=Abst &
                              t1 = (THead (Bind b) y1 z1) &
                              x = (THead (Bind b) y2 (THead (Flat Appl) (lift (1) (0) u2) z2)) &
                              (pr2 c u1 u2) & (pr2 c y1 y2) & (pr2 (CHead c (Bind b) y2) z1 z2))
                          ).
      Proof.
      Intros; InsertEq H '(THead (Flat Appl) u1 t1); XElim H; Clear c y x;
      Intros; Subst; Pr0GenBase; Subst.
(* case 1: pr2_free, pr0_cong *)
      Apply or3_intro0; EApply ex3_2_intro; XDEAuto 2.
(* case 2: pr2_free, pr0_beta *)
      Apply or3_intro1; EApply ex4_4_intro; XDEAuto 2.
(* case 3: pr2_free, pr0_upsilon *)
      Apply or3_intro2; EApply ex6_6_intro; XDEAuto 2.
(* case 4: pr2_delta, pr0_cong *)
      Subst0GenBase; Subst;
      Apply or3_intro0; EApply ex3_2_intro; XDEAuto 2.
(* case 5: pr2_delta, pr0_beta *)
      Subst0GenBase; Subst;
      Apply or3_intro1; EApply ex4_4_intro; XDEAuto 3.
(* case 6: pr2_delta, pr0_upsilon *)
      Subst0GenBase; Subst.
(* case 6.1: subst0_fst. *)
      Apply or3_intro2; EApply ex6_6_intro; XDEAuto 2.
(* case 6.2: subst0_snd. *)
      Subst0GenBase; Subst; Try Subst0Gen;
      Try Rewrite <- minus_n_O in H3; Try Rewrite <- minus_n_O in H7;
      XDEAuto 7.
(* case 6.3: subst0_both. *)
      Subst0GenBase; Subst; Try Subst0Gen;
      Try Rewrite <- minus_n_O in H7; Try Rewrite <- minus_n_O in H8;
      XDEAuto 7.
      Qed.

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

      Lemma pr2_gen_abbr: (c:?; u1,t1,x:?)
                          (pr2 c (THead (Bind Abbr) u1 t1) x) ->
                          (EX u2 t2 | x = (THead (Bind Abbr) u2 t2) &
                                      (pr2 c u1 u2) & (OR
                                      (b:?; u:?) (pr2 (CHead c (Bind b) u) t1 t2) |
                                      (EX u | (pr0 u1 u) & (pr2 (CHead c (Bind Abbr) u) t1 t2)) |
                                      (EX y z | (pr2 (CHead c (Bind Abbr) u1) t1 y) & (pr0 y z) & (pr2 (CHead c (Bind Abbr) u1) z t2))
                          )) \/ (b:?; u:?)
                          (pr2 (CHead c (Bind b) u) t1 (lift (1) (0) x)).
      Proof.
      Intros; InsertEq H '(THead (Bind Abbr) u1 t1); XElim H; Clear c y x;
      Intros; Subst; Pr0Gen; Subst; Try Subst0Gen; Try Pr0Subst0; XDEAuto 10.
      Qed.

      Lemma pr2_gen_void: (c:?; u1,t1,x:?)
                          (pr2 c (THead (Bind Void) u1 t1) x) ->
                          (EX u2 t2 | x = (THead (Bind Void) u2 t2) &
                                      (pr2 c u1 u2) & (b:?; u:?)
                                      (pr2 (CHead c (Bind b) u) t1 t2)
                          ) \/ (b:?; u:?)
                          (pr2 (CHead c (Bind b) u) t1 (lift (1) (0) x)).
      Proof.
      Intros; InsertEq H '(THead (Bind Void) u1 t1); XElim H; Clear c y x;
      Intros; Subst; Try Pr0Gen; Subst; Try Subst0Gen; XDEAuto 7.
      Qed.

      Lemma pr2_gen_lift: (c:?; t1,x:?; h,d:?) (pr2 c (lift h d t1) x) ->
                          (e:?) (drop h d c e) ->
                          (EX t2 | x = (lift h d t2) & (pr2 e t1 t2)).
      Proof.
      Intros until 1; InsertEq H '(lift h d t1); XElim H; Clear c y x;
      Intros; Subst; Pr0Gen; Subst.
(* case 1 : pr2_free *)
      XDEAuto 3.
(* case 2 : pr2_delta *)
      Apply (lt_le_e i d); Intros.
(* case 2.1 : i < d *)
      Rewrite (lt_plus_minus i d) in H1; [ Idtac | XAuto ].
      Rewrite (lt_plus_minus i d) in H3; [ Idtac | XAuto ].
      GetLDis; Subst; Subst0Gen; Rewrite <- lt_plus_minus in H; XDEAuto 3.
(* case 2.2 : i >= d *)
      Apply (lt_le_e i (plus d h)); Intros.
(* case 2.2.1 : i < d + h *)
      EApply subst0_gen_lift_false; [ Apply H0 | Apply H4 | XDEAuto 2 ].
(* case 2.2.2 : i >= d + h *)
      GetLDis; Subst0Gen; XDEAuto 3.
      Qed.

   End pr2_gen.

      Tactic Definition Pr2Gen := (
         Match Context With
            | [ H: (pr2 ?1 (THead (Bind Abbr) ?2 ?3) ?4) |- ? ] ->
               LApply (pr2_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
               XDecompose H
            | [ H: (pr2 ?1 (THead (Bind Void) ?2 ?3) ?4) |- ? ] ->
               LApply (pr2_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
               XDecompose H
            | [ H: (pr2 ?1 (THead (Flat Appl) ?2 ?3) ?4) |- ? ] ->
               LApply (pr2_gen_appl ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
               XDecompose H
            | [ H0: (pr2 ?1 (lift ?2 ?3 ?4) ?5);
                H1: (drop ?2 ?3 ?1 ?6) |- ? ] ->
               LApply (pr2_gen_lift ?1 ?4 ?5 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
               LApply (H0 ?6); [ Clear H0; Intros H0 | XAuto ];
               XDecompose H0
            | [ |- ? ] -> Pr2GenBase
         ).