(****************************************************************************)
(*                                                                          *)
(*                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 drop_props.
Require drop1_defs.
Require getl_defs.

   Section confluence. (*****************************************************)

      Hints Resolve clear_mono : ld.

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

      Theorem getl_mono: (c,x1:?; h:?) (getl h c x1) ->
                         (x2:?) (getl h c x2) -> x1 = x2.
      Proof.
      Intros; Repeat GetLGenBase.
      DropDis; Subst; XDEAuto 2.
      Qed.

      Hints Resolve clear_mono : ld.

      Lemma getl_clear_conf: (i:?; c1,c3:?) (getl i c1 c3) ->
                             (c2:?) (clear c1 c2) -> (getl i c2 c3).
      Proof.
      XElim i.
(* case 1: i = 0 *)
      Intros; GetLGenBase.
      Replace c2 with c3; [ Subst; Clear H0 | XDEAuto 2 ].
      ClearGenAll; XAuto.
(* case 2: i > 0 *)
      XElim c1; Intros;
      Try NewInduction k; GetLGenBase; ClearGenBase; XDEAuto 2.
      Qed.

      Lemma getl_drop_conf_lt: (b:?; c,c0:?; u:?; i:?)
                               (getl i c (CHead c0 (Bind b) u)) ->
                               (e:?; h,d:?) (drop h (S (plus i d)) c e) ->
                               (EX v e0 | u = (lift h d v) &
                                          (getl i e (CHead e0 (Bind b) v)) &
                                          (drop h d c0 e0)
                               ).
      Proof.
      XElim c; Intros; GetLGenBase.
      NewInduction x; Try NewInduction k0; ClearGenBase.
(* case 1: Bind *)
      XInv; Subst; DropDis; Subst; XDEAuto 3.
(* case 2: Flat *)
      NewInduction i; Repeat (DropGenBase; XInv; Subst).
(* case 2.1: i = 0 *)
      LApply (H c0 u (0)); [ Clear H H0; Intros H | XDEAuto 2 ].
      LApply (H x0 h d); [ Clear H H2; Intros H | XAuto ].
      XDecompose H; Subst; XDEAuto 3.
(* case 2.2.2.2: i > 0 *)
      Clear IHi; RRwIn H4.
      LApply (H c0 u (r k i)); [ Clear H H0; Intros H | XDEAuto 3 ].
      LApply (H x0 h d); [ Clear H H4; Intros H | XAuto ].
      XDecompose H; Subst; XDEAuto 4.
      Qed.

      Lemma getl_drop_conf_ge: (i:?; a,c:?) (getl i c a) ->
                               (e:?; h,d:?) (drop h d c e) ->
                               (le (plus d h) i) -> (getl (minus i h) e a).
      Proof.
      Intros; GetLGenBase; DropDis; XDEAuto 2.
      Qed.

      Lemma getl_conf_ge_drop: (b:?; c1,e:?; u:?; i:?) (getl i c1 (CHead e (Bind b) u)) ->
                               (c2:?) (drop (1) i c1 c2) -> (drop i (0) c2 e).
      Proof.
      Intros; GetLDrop; DropDis; [ Rewrite minus_Sx_SO in H2 | Rewrite plus_sym ]; XAuto.
      Qed.

      Hints Resolve getl_drop_conf_ge getl_clear_conf : ld.

      Lemma getl_conf_le: (i:?; a,c:?) (getl i c a) ->
                          (e:?; h:?) (getl h c e) -> (le h i) ->
                          (getl (minus i h) e a).
      Proof.
      Intros; GetLGenBase; XDEAuto 4.
      Qed.

      Hints Resolve drop_conf_rev : ld.

      Lemma getl_drop_conf_rev: (j:?; e1,e2:?) (drop j (0) e1 e2) ->
                                (b:?; c2:?; v2:?; i:?) (getl i c2 (CHead e2 (Bind b) v2)) ->
                                (EX c1 | (drop j (0) c1 c2) & (drop (S i) j c1 e1)).
      Proof.
      Intros; GetLDrop; XDEAuto 3.
      Qed.

   End confluence.

   Section transitivity. (***************************************************)

      Hints Resolve le_S_n : ld.

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

(* NOTE: This should replace drop_getl_trans_le *)
      Lemma drop_getl_trans_lt: (i,d:?) (lt i d) ->
                                (c1,c2:?; h:?) (drop h d c1 c2) ->
                                (b:?; e2:?; v:?) (getl i c2 (CHead e2 (Bind b) v)) ->
                                (EX e1 | (getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))) &
                                         (drop h (minus d (S i)) e1 e2)
                                ).
      Proof.
      Intros; GetLGenBase; DropDis.
      Rewrite minus_x_Sy in H1; [ DropClear | XAuto ].
      XDEAuto 3.
      Qed.

      Lemma drop_getl_trans_le: (i,d:?) (le i d) ->
                                (c1,c2:?; h:?) (drop h d c1 c2) ->
                                (e2:?) (getl i c2 e2) ->
                                (EX e0 e1 | (drop i (0) c1 e0) &
                                            (drop h (minus d i) e0 e1) &
                                            (clear e1 e2)
                                ).
      Proof.
      Intros; GetLGenBase; DropDis; XDEAuto 2.
      Qed.

      Lemma drop_getl_trans_ge: (i:?; c1,c2:?; d,h:?) (drop h d c1 c2) ->
                                (e2:?) (getl i c2 e2) -> (le d i) ->
                                (getl (plus i h) c1 e2).
      Proof.
      Intros; GetLGenBase; DropDis; XDEAuto 2.
      Qed.

      Lemma getl_drop_trans: (c1,c2:?; h:?) (getl h c1 c2) ->
                             (e2:?; i:?) (drop (S i) (0) c2 e2) ->
                             (drop (S (plus i h)) (0) c1 e2).
      Proof.
      XElim c1.
(* case 1: CSort *)
      Intros; GetLGenBase.
(* case 2: CHead *)
      Intros c1 IHc; XElim k.
(* case 2.1: Bind *)
      XElim h; Intros; GetLGenBase.
(* case 2.1.1: h = 0 *)
      Clear IHc; ClearGenBase; DropGenBase.
      Rewrite <- plus_n_O; XAuto.
(* case 2.1.2: h > 0 *)
      Clear H; Rewrite <- plus_Snm_nSm; XDEAuto 4.
(* case 2.2: Bind *)
      XElim h; Intros; GetLGenBase.
(* case 2.2.1: h = 0 *)
      ClearGenBase; XDEAuto 5.
(* case 2.2.2: h > 0 *)
      Clear H; XDEAuto 4.
      Qed.

   End transitivity.

      Tactic Definition GetLDis := (
         Match Context With
            | [ H1: (getl ?1 ?3 ?4); H2: (getl ?1 ?3 ?5) |- ? ] ->
               LApply (getl_mono ?3 ?5 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?4); [ Clear H_x H1; Intros H1; Rewrite H1 in H2 | XAuto ]
            | [ H1: (getl ?0 ?1 (CHead ?2 (Bind ?3) ?4));
                H2: (drop ?5 (S (plus ?0 ?6)) ?1 ?7) |- ? ] ->
               LApply (getl_drop_conf_lt ?3 ?1 ?2 ?4 ?0); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?7 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
               XElim H1; Intros
            | [ H1: (getl ?0 ?1 ?); H2: (getl (S (plus ?2 ?0)) ?1 ?) |- ? ] ->
               XPoseClear H1 '(getl_conf_le ? ? ? H2 ? ? H1);
               LApply H1; [ Clear H1 H2; Intros H1 | XAuto ];
               Arith4In H1 ?2 ?0; Rewrite minus_plus_r in H1
            | [ _: (getl ?0 ?1 ?2); _: (getl ?5 ?1 ?7);
                _: (lt ?5 ?0) |- ? ] ->
               LApply (getl_conf_le ?0 ?2 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?7 ?5); [ Clear H_x; Intros H_x | XAuto ];
               LApply H_x; [ Clear H_x; Intros | XAuto ]
            | [ H1: (getl ?1 ?2 (CHead ?3 (Bind ?0) ?4));
                H2: (drop (1) ?1 ?2 ?5) |- ? ] ->
               LApply (getl_conf_ge_drop ?0 ?2 ?3 ?4 ?1); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?5); [ Clear H1 H2; Intros H1 | XAuto ]
            | [ H0: (getl ?0 ?1 ?2); H2: (lt ?6 ?0);
                H1: (drop (1) ?6 ?1 ?7) |- ? ] ->
               LApply (getl_drop_conf_ge ?0 ?2 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?7 (1) ?6); [ Clear H_x; Intros H_x | XAuto ];
               LApply H_x; [ Clear H_x; Intros | Rewrite plus_sym; XAuto ]
            | [ H0: (getl ?0 ?1 ?2);
                H1: (drop ?5 ?6 ?1 ?7) |- ? ] ->
               LApply (getl_drop_conf_ge ?0 ?2 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?7 ?5 ?6); [ Clear H_x; Intros H_x | XAuto ];
               LApply H_x; [ Clear H_x; Intros | XAuto ]
            | [ H0: (lt ?1 ?2);
                H1: (drop ?3 ?2 ?4 ?5); H2: (getl ?1 ?5 ?6) |- ? ] ->
               LApply (drop_getl_trans_le ?1 ?2); [ Intros H_x | XAuto ];
               LApply (H_x ?4 ?5 ?3); [ Clear H_x H1; Intros H_x | XAuto ];
               LApply (H_x ?6); [ Clear H_x H2; Intros H_x | XAuto ];
               XDecompose H_x
            | [ H0: (le ?1 ?2);
                H1: (drop ?3 ?1 ?4 ?5); H2: (getl ?2 ?5 ?6) |- ? ] ->
               LApply (drop_getl_trans_ge ?2 ?4 ?5 ?1 ?3); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
               LApply H1; [ Clear H1; Intros | XAuto ]
            | [ H1: (getl ? ? ?2); H2: (drop (S ?) (0) ?2 ?) |- ? ] ->
               XPoseClear H2 '(getl_drop_trans ? ? ? H1 ? ? H2)
            | [ H1: (drop ? (0) ? ?1); H2: (getl ? ? (CHead ?1 (Bind ?) ?)) |- ? ] ->
               XDecomPose '(getl_drop_conf_rev ? ? ? H1 ? ? ? ? H2); Clear H1 H2
            | [ H1: (drop ? (0) ? ?1); H2: (getl ? ?1 ?) |- ? ] ->
               XPoseClear H2 '(drop_getl_trans_ge ? ? ? ? ? H1 ? H2);
               LApply H2; [ Clear H2; Intros H2 | XAuto ]
            | [ H0: (lt ?2 ?1); H1: (drop ? ?1 ? ?0);
                H2: (getl ?2 ?0 (CHead ? (Bind ?) ?)) |- ? ] ->
               XDecomPose '(drop_getl_trans_lt ? ? H0 ? ? ? H1 ? ? ? H2);
               Clear H1 H2
         ).

   Section more_transitivity. (**********************************************)

      Hints Resolve getl_clear_trans : ld.

      Theorem getl_trans: (i:?; c1,c2:?; h:?) (getl h c1 c2) ->
                          (e2:?) (getl i c2 e2) -> (getl (plus i h) c1 e2).
      Proof.
      Intros; GetLGenBase; NewInduction i.
(* case 1: i = 0 *)
      DropGenBase; Subst; XDEAuto 2.
(* case 2: i > 0 *)
      Clear IHi; GetLDis; XDEAuto 2.
      Qed.

      Hints Resolve blt_lt bge_le : ld.

      Lemma drop1_getl_trans: (hds:?; c1,c2:?) (drop1 hds c2 c1) ->
                              (b:?; e1:?; v:?; i:?) (getl i c1 (CHead e1 (Bind b) v)) ->
                              (EX e2 | (drop1 (ptrans hds i) e2 e1) &
                                       (getl (trans hds i) c2 (CHead e2 (Bind b) (lift1 (ptrans hds i) v)))
                              ).
      Proof.
      XElim hds; Simpl.
(* case 1: PNil *)
      Intros; Drop1GenBase; XDEAuto 2.
(* case 2: PCons *)
      Intros h d hds; Intros; Drop1GenBase; XInduction '(blt (trans hds i) d).
(* case 2.1: (trans hds i) < d *)
      LApply (drop_getl_trans_lt (trans hds i) d); [ Clear H0; Intros H0 | XAuto ].
      XDecomPoseClear H '(H ? ? H3 ? ? ? ? H1); Clear H3 H1.
      XDecomPoseClear H0 '(H0 ? ? ? H2 ? ? ? H5); Clear H2 H5; XDEAuto 3.
(* case 2.2: (trans hds i) >= d *)
      XDecomPoseClear H '(H ? ? H3 ? ? ? ? H1); Clear H3 H1.
      XPose H '(drop_getl_trans_ge ? ? ? ? ? H2 ? H5); Clear H2 H5.
      XDEAuto 4.
      Qed.

   End more_transitivity.

      Tactic Definition GetLXDis := (
         Match Context With
            | [ H1: (getl ? ? (CHead ?1 (Bind ?) ?)); H2: (getl ?0 ?1 ?2) |- ? ] ->
               XPoseClear H1 '(getl_trans (S ?0) ? ? ? H1);
               LApply (H1 ?2); [ Clear H1; Intros | XAuto ]
            | [ H1: (drop1 ? ? ?1);
                H2: (getl ? ?1 (CHead ? (Bind ?) ?)) |- ?
              ] ->
               XDecomPoseClear H2 '(drop1_getl_trans ? ? ? H1 ? ? ? ? H2)
            | [ |- ? ] -> GetLDis
         ).

   Section more_confluence. (************************************************)

      Lemma cimp_getl_conf: (c1,c2:?) (cimp c1 c2) -> (b:?; d1:?; w:?; i:?)
                            (getl i c1 (CHead d1 (Bind b) w)) ->
                            (EX d2 | (cimp d1 d2) &
                                     (getl i c2 (CHead d2 (Bind b) w))
                            ).
      Proof.
      Unfold cimp; Intros.
      XDecomPose '(H ? ? ? ? H0).
      EApply ex2_intro; [ Intros | XDEAuto 2 ].
      GetLXDis; Clear H2.
      XDecomPose '(H ? ? ? ? H0); Clear H H0.
      GetLXDis; GetLGenBase; XDEAuto 2.
      Qed.

   End more_confluence.

      Tactic Definition GetLCImpDis := (
         Match Context With
            | [ H1: (cimp ?1 ?); H2: (getl ? ?1 (CHead ? (Bind ?) ?)) |- ? ] ->
               XDecomPose '(cimp_getl_conf ? ? H1 ? ? ? ? H2); Clear H1 H2
            | [ |- ? ] -> GetLXDis
         ).