(****************************************************************************)
(*                                                                          *)
(*                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_defs.

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

      Tactic Definition IH := (
         Match Context With
            | [ H1: (drop ?1 ?2 c ?3); H2: (drop ?1 ?2 c ?4) |- ? ] ->
               LApply (H ?4 ?2 ?1); [ Clear H H2; Intros H | XAuto ];
               LApply (H ?3); [ Clear H H1; Intros | XAuto ]
         ).

      Hints Resolve sym_eq : ld.

      Theorem drop_mono: (c,x1:?; d,h:?) (drop h d c x1) ->
                         (x2:?) (drop h d c x2) -> x1 = x2.
      Proof.
      XElim c.
(* case 1: CSort *)
      Intros; Repeat DropGenBase; Subst; XAuto.
(* case 2: CHead k *)
      XElim d.
(* case 2.1: d = 0 *)
      XElim h; Intros; Repeat DropGenBase; Subst; XDEAuto 2.
(* case 2.2: d > 0 *)
      Intros; Repeat DropGenBase; Subst;
      LiftGen; Subst; IH; XAuto.
      Qed.

      Theorem drop_conf_lt: (k:?; i:?; u:?; c0,c:?)
                            (drop i (0) c (CHead c0 k u)) ->
                            (e:?; h,d:?) (drop h (S (plus i d)) c e) ->
                            (EX v e0 | u = (lift h (r k d) v) &
                                       (drop i (0) e (CHead e0 k v)) &
                                       (drop h (r k d) c0 e0)
                            ).
      Proof.
      XElim i.
(* case 1 : i = 0 *)
      Intros until 1; DropGenBase; Subst; DropGenBase; Subst; XDEAuto 2.
(* case 2 : i > 0 *)
     Intros i; XElim c.
(* case 2.1 : CSort *)
      Intros; DropGenBase; XInv.
(* case 2.2 : CHead k *)
      XElim k0; Intros; Repeat DropGenBase; Subst.
(* case 2.2.1 : Bind *)
      LApply (H u c0 c); [ Clear H H0 H1; Intros H | XAuto ].
      LApply (H x0 h d); [ Clear H H9; Intros H | XAuto ].
      XDecompose H; XDEAuto 3.
(* case 2.2.2 : Flat *)
      LApply H0; [ Clear H H0 H1; Intros H | XAuto ].
      LApply (H x0 h d); [ Clear H H9; Intros H | XAuto ].
      XElim H; XDEAuto 3.
      Qed.

      Hints Resolve le_S_n le_trans_plus_r : ld.

      Theorem drop_conf_ge: (i:?; a,c:?) (drop i (0) c a) ->
                            (e:?; h,d:?) (drop h d c e) -> (le (plus d h) i) ->
                            (drop (minus i h) (0) e a).
      Proof.
      XElim i.
(* case 1 : i = 0 *)
      Intros until 1.
      DropGenBase; Subst; LeLtGen; PlusO; Subst.
      DropGenBase; Subst; XAuto.
(* case 2 : i > 0 *)
      Intros i; XElim c.
(* case 2.1 : CSort *)
      Intros; Repeat DropGenBase; Subst; XInv; XInv.
(* case 2.2 : CHead k *)
      XElim k; Intros; DropGenBase;
      ( NewInduction d;
      [ NewInduction h; DropGenBase;
        [ Rewrite <- H2; Simpl; XAuto | Clear IHh ]
      | DropGenBase; Rewrite H2; Clear IHd H2 H4 e t ] ).
(* case 2.2.1 : Bind, d = 0, h > 0 *)
      LApply (H a c); [ Clear H H0 H1; Intros H | XAuto ].
      LApply (H e h (0)); XAuto.
(* case 2.2.2 : Bind, d > 0 *)
      LApply (H a c); [ Clear H H0 H1; Intros H | XAuto ].
      LApply (H x0 h d); [ Clear H H4; Intros H | XAuto ].
      LApply H; [ Clear H; Simpl in H3; Intros H | XAuto ].
      Rewrite <- minus_Sn_m; XDEAuto 3.
(* case 2.2.3 : Flat, d = 0, h > 0 *)
      LApply H0; [ Clear H H0 H1; Intros H | XAuto ].
      LApply (H e (S h) (0)); XAuto.
(* case 2.2.4 : Flat, d > 0 *)
      LApply H0; [ Clear H H0 H1; Intros H | XAuto ].
      LApply (H x0 h (S d)); [ Clear H H4; Intros H | XAuto ].
      LApply H; [ Clear H; Simpl in H3; Intros H | XAuto ].
      Rewrite <- minus_Sn_m in H; [ Idtac | XDEAuto 3 ].
      Rewrite <- minus_Sn_m; XDEAuto 3.
      Qed.

      Theorem drop_conf_rev: (j:?; e1,e2:?) (drop j (0) e1 e2) ->
                             (c2:?; i:?) (drop i (0) c2 e2) ->
                             (EX c1 | (drop j (0) c1 c2) & (drop i j c1 e1)).
      Proof.
      XElim j.
(* case 1: j = 0 *)
      Intros; DropGenBase; Subst; XDEAuto 2.
(* case 2: j > 0 *)
      Intros j IHj; XElim e1.
(* case 2.1: CSort *)
      Intros; DropGenBase; Subst; XInv; XInv.
(* case 2.2: CHead *)
      Intros e1 IHe1; Intros; DropGenBase; NewInduction k.
(* case 2.2.1: Bind *)
      XDecomPose '(IHj ? ? H ? ? H0); Clear IHj IHe1 H H0.
      EApply ex2_intro; [ Idtac | EApply drop_skip ]; XDEAuto 2.
(* case 2.2.2: Flat *)
      XDecomPose '(IHe1 ? H ? ? H0); Clear IHj IHe1 H H0.
      EApply ex2_intro; [ Idtac | EApply drop_skip ]; XDEAuto 2.
      Qed.

   End confluence.

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

      Hints Resolve le_S_n : ld.

      Theorem drop_trans_le: (i,d:?) (le i d) ->
                             (c1,c2:?; h:?) (drop h d c1 c2) ->
                             (e2:?) (drop i (0) c2 e2) ->
                             (EX e1 | (drop i (0) c1 e1) & (drop h (minus d i) e1 e2)).
      Proof.
      XElim i.
(* case 1 : i = 0 *)
      Intros; DropGenBase; Rewrite H1 in H0.
      Rewrite <- minus_n_O; XDEAuto 2.
(* case 2 : i > 0 *)
      Intros i IHi; XElim d.
(* case 2.1 : d = 0 *)
      Intros; LeLtGen; XInv.
(* case 2.2 : d > 0 *)
      Intros d IHd; XElim c1.
(* case 2.2.1 : CSort *)
      Intros.
      DropGenBase; Rewrite H0 in H1.
      DropGenBase; Rewrite H1; XInv; XInv.
(* case 2.2.2 : CHead k *)
      Intros c1 IHc; XElim k; Intros;
      DropGenBase; Rewrite H0 in H1; Rewrite H2; Clear IHd H0 H2 c2 t;
      DropGenBase.
(* case 2.2.2.1 : Bind *)
      LApply (IHi d); [ Clear IHi; Intros IHi | XAuto ].
      LApply (IHi c1 x0 h); [ Clear IHi H8; Intros IHi | XAuto ].
      LApply (IHi e2); [ Clear IHi H0; Intros IHi | XAuto ].
      XElim IHi; XDEAuto 3.
(* case 2.2.2.2 : Flat *)
      LApply (IHc x0 h); [ Clear IHc H8; Intros IHc | XAuto ].
      LApply (IHc e2); [ Clear IHc H0; Intros IHc | XAuto ].
      XElim IHc; XDEAuto 3.
      Qed.

      Theorem drop_trans_ge: (i:?; c1,c2:?; d,h:?) (drop h d c1 c2) ->
                             (e2:?) (drop i (0) c2 e2) -> (le d i) ->
                             (drop (plus i h) (0) c1 e2).
      Proof.
      XElim i.
(* case 1: i = 0 *)
      Intros; DropGenBase; Subst; LeLtGen; XAuto.
(* case 2 : i > 0 *)
      Intros i IHi; XElim c1; Simpl.
(* case 2.1: CSort *)
      Intros; DropGenBase; Subst; DropGenBase; Subst; XInv; XInv.
(* case 2.2: CHead *)
      Intros c1 IHc; XElim d.
(* case 2.2.1: d = 0 *)
      XElim h; Intros.
(* case 2.2.1.1: h = 0 *)
      DropGenBase; Subst; DropGenBase; Rewrite <- plus_n_O; XAuto.
(* case 2.2.1.2: h > 0 *)
      DropGenBase; Rewrite <- plus_n_Sm.
      Apply drop_drop; RRw; XDEAuto 2. (**) (* explicit constructor *)
(* case 2.2.2: d > 0 *)
      Intros d IHd; Intros.
      DropGenBase; Rewrite H in IHd; Rewrite H in H0; Rewrite H2 in IHd; Rewrite H2; Clear IHd H H2 c2 t;
      DropGenBase; Apply drop_drop; NewInduction k; Simpl; XDEAuto 3. (**) (* explicit constructor *)
      Qed.

   End transitivity.

      Tactic Definition DropDis := (
         Match Context With
            | [ H1: (drop ?1 ?2 ?3 ?4); H2: (drop ?1 ?2 ?3 ?5) |- ? ] ->
               LApply (drop_mono ?3 ?5 ?2 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?4); [ Clear H_x H1; Intros H1; Rewrite H1 in H2 | XAuto ]
            | [ H1: (drop ?0 (0) ?1 (CHead ?2 ?3 ?4));
                H2: (drop ?5 (S (plus ?0 ?6)) ?1 ?7) |- ? ] ->
               LApply (drop_conf_lt ?3 ?0 ?4 ?2 ?1); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?7 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
               XElim H1; Intros
            | [ _: (drop ?0 (0) ?1 ?2); _: (drop ?5 (0) ?1 ?7);
                _: (lt ?5 ?0) |- ? ] ->
               LApply (drop_conf_ge ?0 ?2 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?7 ?5 (0)); [ Clear H_x; Intros H_x | XAuto ];
               Simpl in H_x; LApply H_x; [ Clear H_x; Intros | XAuto ]
            | [ _: (drop ?1 (0) ?2 (CHead ?3 (Bind ?) ?));
                _: (drop (1) ?1 ?2 ?4) |- ? ] ->
               LApply (drop_conf_ge (S ?1) ?3 ?2); [ Intros H_x | XDEAuto 2 ];
               LApply (H_x ?4 (1) ?1); [ Clear H_x; Intros H_x | XAuto ];
               LApply H_x; [ Clear H_x; Intros | Rewrite plus_sym; XAuto ]; (
               Match Context With
                  | [ H: (drop (minus (S ?1) (1)) (0) ?4 ?3) |- ? ] ->
                     Simpl in H; Rewrite <- minus_n_O in H
               )
            | [ H0: (drop ?0 (0) ?1 ?2); H2: (lt ?6 ?0);
                H1: (drop (1) ?6 ?1 ?7) |- ? ] ->
               LApply (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: (drop ?0 (0) ?1 ?2);
                H1: (drop ?5 ?6 ?1 ?7) |- ? ] ->
               LApply (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: (drop ?1 (0) ?5 ?6) |- ? ] ->
               LApply (drop_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 ];
               XElim H_x; Intros
            | [ H1: (drop ?3 (0) ?4 ?5); H2: (drop ?2 (0) ?5 ?6) |- ? ] ->
               XPoseClear H1 '(drop_trans_ge ?2 ? ? ? ? H1 ? H2);
               LApply H1; [ Clear H1 H2; Intros | XAuto ]
            | [ H0: (le ?1 ?2);
                H1: (drop ?3 ?1 ?4 ?5); H2: (drop ?2 (0) ?5 ?6) |- ? ] ->
               LApply (drop_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 ]
            | [ H0: (le ?1 ?2);
                H1: (drop ?3 ?2 ?4 ?5); H2: (drop ?1 (0) ?5 ?6) |- ? ] ->
               LApply (drop_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
         ).