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

Require Export lift1_defs.
Require Export drop_defs.

      Inductive drop1: PList -> C -> C -> Prop :=
          | drop1_nil: (c:?) (drop1 PNil c c)
          | drop1_cons: (c1,c2:?; h,d:?) (drop h d c1 c2) ->
                        (c3:?; hds:?) (drop1 hds c2 c3) ->
                        (drop1 (PCons h d hds) c1 c3).

      Hint drop1 : ld := Constructors drop1.

      Fixpoint ptrans [hds:PList] : nat -> PList :=
         [i:?] Cases hds of
            | PNil            => PNil
            | (PCons h d hds) =>
                 let j = (trans hds i) in
                 let q = (ptrans hds i) in
                 if (blt j d) then (PCons h (minus d (S j)) q) else q
         end.

   Section drop1_gen_base. (*************************************************)

      Lemma drop1_gen_pnil: (c1,c2:?) (drop1 PNil c1 c2) -> c1 = c2.
      Proof.
      Intros; InsertEq H PNil; XElim H; Clear y c1 c2;
      Intros; XInv; Subst; XAuto.
      Qed.

      Lemma drop1_gen_pcons: (c1,c3:?; hds:?; h,d:?)
                             (drop1 (PCons h d hds) c1 c3) ->
                               (EX c2 | (drop h d c1 c2) &
                                        (drop1 hds c2 c3)
                               ).
      Proof.
      Intros; InsertEq H '(PCons h d hds); XElim H; Clear y c1 c3;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

   End drop1_gen_base.

      Tactic Definition Drop1GenBase := (
         Match Context With
            | [ H: (drop1 PNil ? ?) |- ? ] ->
               XPoseClear H '(drop1_gen_pnil ? ? H); Subst
            | [ H: (drop1 (PCons ? ? ?) ? ?) |- ? ] ->
               XDecomPoseClear H '(drop1_gen_pcons ? ? ? ? ? H)
         ).

   Section drop1_props. (****************************************************)

      Lemma drop1_skip_bind: (b:?; e:?; hds:?; c:?; u:?) (drop1 hds c e) ->
                             (drop1 (Ss hds) (CHead c (Bind b) (lift1 hds u)) (CHead e (Bind b) u)).
      Proof.
      XElim hds; Simpl; Intros;
      Drop1GenBase; XDEAuto 4.
      Qed.

      Lemma drop1_cons_tail: (c2,c3:?; h,d:?) (drop h d c2 c3) ->
                             (hds:?; c1:?) (drop1 hds c1 c2) ->
                             (drop1 (PConsTail hds h d) c1 c3).
      Proof.
      XElim hds; Simpl; Intros;
      Drop1GenBase; XDEAuto 3.
      Qed.

      Theorem drop1_trans: (is1:?; c1,c0:?) (drop1 is1 c1 c0) ->
                           (is2:?; c2:?) (drop1 is2 c0 c2) ->
                           (drop1 (papp is1 is2) c1 c2).
      Proof.
      XElim is1; Intros; Simpl; Drop1GenBase; XDEAuto 3.
      Qed.

   End drop1_props.

      Hints Resolve drop1_skip_bind drop1_cons_tail : ld.