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

Require lift1_props.
Require drop1_props.
Require getl_props.
Require aprem_defs.
Require arity_props.
Require csuba_props.
Require nf2_props.
Require sn3_props.
Require sn3_gen.
Require sc3_defs.

   Section sc3_lift. (*******************************************************)

      Lemma sc3_lift: (g:?; a:?; e:?; t:?) (sc3 g a e t) ->
                      (c:?; h,d:?) (drop h d c e) ->
                      (sc3 g a c (lift h d t)).
      Proof.
      XElim a; Simpl; Intros.
(* case 1: ASort *)
      XDecompose H; XDEAuto 4.
(* case 2: AHead *)
      XDecompose H1; Split; [ XDEAuto 2 | Clear H H0 H3; Intros ].
      XPoseClear H4 '(H4 ? ? H (PConsTail is h d)).
      Rewrite <- lift1_cons_tail; XDEAuto 3.
      Qed.

      Hints Resolve sc3_lift : ld.

      Lemma sc3_lift1: (g:?; e:?; a:?; hds:?; c:?; t:?) (sc3 g a e t) ->
                       (drop1 hds c e) -> (sc3 g a c (lift1 hds t)).
      Proof.
      XElim hds; Simpl; Intros;
      Drop1GenBase; XDEAuto 3.
      Qed.

   End sc3_lift.

      Hints Resolve sc3_lift sc3_lift1 : ld.

   Section sc3_props. (******************************************************)

      Hints Resolve arity_appls_abbr arity_appls_bind arity_appls_cast : ld.

      Lemma sc3_abbr: (g:?; a:?; vs:?; i:?; d:?; v:?; c:?)
                      (sc3 g a c (THeads (Flat Appl) vs (lift (S i) (0) v))) ->
                      (getl i c (CHead d (Bind Abbr) v)) ->
                      (sc3 g a c (THeads (Flat Appl) vs (TLRef i))).

      Proof.
      XElim a; Simpl; Intros.
(* case 1: ASort *)
      XDecompose H; XDEAuto 4.
(* case 2: AHead *)
      XDecompose H1; Clear H.
      Split; [ XDEAuto 2 | Clear H3; Intros; GetLXDis ].
      XPoseClear H0 '(H0 (TCons w (lifts1 is vs))); Simpl in H0.
      Rewrite lifts1_flat; Rewrite lift1_lref.
      EApply H0; [ Idtac | Idtac ].
(* case 2.1: first conclusion *)
      Rewrite <- lift1_free; Rewrite <- lifts1_flat; XAuto.
(* case 2.2: second conclusion *)
      XDEAuto 2.
      Qed.

      Theorem sc3_cast: (g:?; a:?; vs:?; c:?; u:?) (sc3 g (asucc g a) c (THeads (Flat Appl) vs u)) ->
                        (t:?) (sc3 g a c (THeads (Flat Appl) vs t)) ->
                        (sc3 g a c (THeads (Flat Appl) vs (THead (Flat Cast) u t))).
      Proof.
      XElim a; Simpl; Intros.
(* case 1: ASort *)
      NewInduction n; Simpl in H; XDecompose H; XDecompose H0; XAuto.
(* case 2: AHead *)
      XDecompose H1; XDecompose H2; Clear H.
      Split; [ XAuto | Clear H3 H1; Intros ].
      XPoseClear H0 '(H0 (TCons w (lifts1 is vs))); Simpl in H0.
      Rewrite lifts1_flat; Rewrite lift1_flat; Apply H0; Clear H0;
      Rewrite <- lifts1_flat; XAuto.
      Qed.

      Hints Resolve sn3_appls_lref sc3_arity_gen : ld.

      Remark sc3_sn3_abst: (g:?; a:?)
                           ((c:?; t:?) (sc3 g a c t) -> (sn3 c t)) /\
                           ((vs:?; i:?) let t = (THeads (Flat Appl) vs (TLRef i)) in
                            (c:?) (arity g c t a) -> (nf2 c (TLRef i)) -> (sns3 c vs) -> (sc3 g a c t)
                           ).
      Proof.
      XElim a; Simpl; Intros; Split; Intros.
(* case 1.1: ASort, first conclusion *)
      XDecompose H; XAuto.
(* case 1.2: ASort, second conclusion *)
      XAuto.
(* case 2.1: AHead, first conclusion *)
      XDecompose H; Clear H2; XDecompose H0; Clear H2; XDecompose H1.
(* step 1 *)
      XPoseClear H0 '(arity_aprem ? ? ? ? H0 (0) a).
      LApply H0; [ Clear H0; Intros H0; XDecompose H0 | XAuto ].
      Rename x0 into d; Rename x1 into w; Rename x2 into i.
(* step 2 *)
      LApply (H3 TNil (0) (CHead d (Bind Abst) w)); Simpl; [ Clear H3 H4; Intros H3 | XDEAuto 2 ].
      LApply H3; [ Clear H3; Intros H3 | XDEAuto 2 ].
      LApply H3; [ Clear H3; Intros H3 | XAuto ].
(* step 3 *)
      XPoseClear H2 '(H2 ? ? H3 (PCons (S i) (0) PNil)); Simpl in H2; Clear H3.
      LApply H2; [ Clear H2; Intros H2 | XDEAuto 3 ].
(* step 4 *)
      XPoseClear H '(H ? ? H2); Clear H2.
      SN3GenBase; Clear H H0; EApply sn3_gen_lift; XDEAuto 2.
(* case 2.2: AHead, second conclusion *)
      Split; [ XAuto | Intros ].
      XDecompose H; XDecompose H0; Clear H H7.
      XPoseClear H8 '(H8 (TCons w (lifts1 is vs))); Simpl in H8.
      Rewrite lifts1_flat; Rewrite lift1_lref; Apply H8; Clear H8;
      Try Rewrite <- lift1_lref; Try Rewrite <- lifts1_flat; XDEAuto 4.
      Qed.

      Lemma sc3_sn3: (g:?; a:?; c:?; t:?) (sc3 g a c t) -> (sn3 c t).
      Proof.
      Intros; XDecomPose '(sc3_sn3_abst g a); XAuto.
      Qed.

      Lemma sc3_abst: (g:?; a:?; vs:?; c:?; i:?)
                      (arity g c (THeads (Flat Appl) vs (TLRef i)) a) ->
                      (nf2 c (TLRef i)) -> (sns3 c vs) ->
                      (sc3 g a c (THeads (Flat Appl) vs (TLRef i))).
      Proof.
      Intros; XDecomPose '(sc3_sn3_abst g a); XAuto.
      Qed.

      Hints Resolve sn3_appls_bind sc3_sn3 : ld.

      Theorem sc3_bind: (g:?; b:?) ~b=Abst ->
                        (a1,a2:?; vs:?; c:?; v,t:?)
                        (sc3 g a2 (CHead c (Bind b) v) (THeads (Flat Appl) (lifts (1) (0) vs) t)) ->
                        (sc3 g a1 c v) ->
                        (sc3 g a2 c (THeads (Flat Appl) vs (THead (Bind b) v t))).
      Proof.
      XElim a2; Simpl; Intros.
(* case 1: ASort *)
      XDecompose H0; XDEAuto 6.
(* case 2: AHead *)
      XDecompose H2; Clear H0.
      Split; [ XDEAuto 3 | Clear H4; Intros ].
      XPoseClear H1 '(H1 (TCons w (lifts1 is vs))); Simpl in H1.
      Rewrite lifts1_flat; Rewrite lift1_bind; Apply H1; Clear H1.
(* case 2.1: first conclusion *)
      Rewrite <- lifts1_xhg; Rewrite <- lifts1_flat; XDEAuto 5.
(* case 2.2: second conclusion *)
      XDEAuto 2.
      Qed.

      Hints Resolve arity_appls_appl : ld.

      Theorem sc3_appl: (g:?; a1,a2:?; vs:?; c:?; v,t:?)
                        (sc3 g a2 c (THeads (Flat Appl) vs (THead (Bind Abbr) v t))) ->
                        (sc3 g a1 c v) -> (w:?) (sc3 g (asucc g a1) c w) ->
                        (sc3 g a2 c (THeads (Flat Appl) vs (THead (Flat Appl) v (THead (Bind Abst) w t)))).
      Proof.
      XElim a2; Simpl; Intros.
(* case 1: ASort *)
      XDecompose H; XDEAuto 7.
(* case 2: AHead *)
      XDecompose H1; Clear H.
      Split; [ XDEAuto 4 | Clear H4; Intros ].
      Rewrite lifts1_flat; Rewrite lift1_flat; Rewrite lift1_bind.
      XPoseClear H0 '(H0 (TCons w0 (lifts1 is vs))); Simpl in H0.
      Apply H0; Clear H0; [ Idtac | XDEAuto 2 | XDEAuto 2 ].
      Rewrite <- lift1_bind; Rewrite <- lifts1_flat; XAuto.
      Qed.

   End sc3_props.