(****************************************************************************)
(*                                                                          *)
(*                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 pr3_props.
Require sn3_defs.

   Section sn3_gen. (********************************************************)

      Lemma sn3_gen_lift: (c1:?; t:?; h,d:?) (sn3 c1 (lift h d t)) ->
                          (c2:?) (drop h d c1 c2) -> (sn3 c2 t).
      Proof.
      Intros until 1; InsertEq H '(lift h d t); UnIntro H t.
      XElim H; Clear y; Intros; Subst; Clear H.
      EApply sn3_sing; Intros; EApply H0;
      [ Idtac | Idtac | XAuto | XAuto ].
(* case 1: first premise *)
      Intros; LiftGen; Subst; Apply H; XAuto. (**)
(* case 2: second premise *)
      XDEAuto 2.
      Qed.

      Lemma sn3_gen_def: (c,d:?; v:?; i:?) (getl i c (CHead d (Bind Abbr) v)) ->
                         (sn3 c (TLRef i)) -> (sn3 d v).
      Proof.
      Intros; GetLDrop.
      EApply sn3_gen_lift; [ Idtac | XDEAuto 2 ].
      EApply sn3_pr3_trans; XDEAuto 3.
      Qed.

      Hints Resolve sn3_gen_def : ld.

      Lemma sn3_cdelta: (v,t:?; i:?) ((w:?) (EX u | (subst0 i w t u))) ->
                        (c,d:?) (getl i c (CHead d (Bind Abbr) v)) ->
                        (sn3 c t) -> (sn3 d v).
      Proof.
      Intros until 1; XDecomPoseClear H '(H v); Rename x into w.
      XElim H0; Clear t v w i; Intros; Subst.
(* case 1: subst0_lref *)
      XDEAuto 2.
(* case 2: subst0_fst *)
      SN3GenBase; XDEAuto 2.
(* case 3: subst0_snd *)
      NewInduction k; SN3GenBase; Simpl in H0; XDEAuto 3.
(* case 4: subst0_both *)
      SN3GenBase; XDEAuto 2.
      Qed.

   End sn3_gen.

      Tactic Definition SN3Gen := (
         Match Context With
            | [ H1: (sn3 ?3 (lift ?1 ?2 ?)); H2: (drop ?1 ?2 ?3 ?) |- ? ] ->
               XPoseClear H1 '(sn3_gen_lift ? ? ? ? H1 ? H2)
            | [ H: (sn3 (CHead ?0 (Bind ?) ?) (lift ? ? ?)) |- ? ] ->
               XPoseClear H '(sn3_gen_lift ? ? ? ? H ?0);
               LApply H; [ Clear H; Intros | XAuto ]
      ).