(****************************************************************************)
(*                                                                          *)
(*                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 getl_defs.
Require Export subst1_defs.
Require Export csubst0_defs.

      Inductive csubst1 [i:nat; v:T; c1:C] : C -> Prop :=
         | csubst1_refl: (csubst1 i v c1 c1)
         | csubst1_sing: (c2:?) (csubst0 i v c1 c2) -> (csubst1 i v c1 c2).

      Hint csubst1 : ld := Constructors csubst1.

   Section csubst1_props_base. (*********************************************)

      Theorem csubst1_head: (k:?; i:?; v,u1,u2:?) (subst1 i v u1 u2) ->
                            (c1,c2:?) (csubst1 i v c1 c2) ->
                            (csubst1 (s k i) v (CHead c1 k u1) (CHead c2 k u2)).
      Proof.
      Intros until 1; XElim H; Clear u2.
(* case 1: csubst1_refl *)
      Intros until 1; XElim H; Clear c2; XAuto.
(* case 2: csubst1_sing *)
      Intros until 2; XElim H0; Clear c2; XAuto.
      Qed.

      Hints Resolve csubst1_head : ld.

      Theorem csubst1_bind: (b:?; i:?; v,u1,u2:?) (subst1 i v u1 u2) ->
                            (c1,c2:?) (csubst1 i v c1 c2) ->
                            (csubst1 (S i) v (CHead c1 (Bind b) u1) (CHead c2 (Bind b) u2)).
      Proof.
      Intros; Replace (S i) with (s (Bind b) i); XAuto.
      Qed.

      Theorem csubst1_flat: (f:?; i:?; v,u1,u2:?) (subst1 i v u1 u2) ->
                            (c1,c2:?) (csubst1 i v c1 c2) ->
                            (csubst1 i v (CHead c1 (Flat f) u1) (CHead c2 (Flat f) u2)).
      Proof.
      Intros; Replace i with (s (Flat f) i); XAuto.
      Qed.

   End csubst1_props_base.

      Hints Resolve csubst1_head csubst1_bind csubst1_flat : ld.

   Section csubst1_gen_base. (***********************************************)

      Lemma csubst1_gen_head: (k:?; c1,x:?; u1,v:?; i:?)
                              (csubst1 (s k i) v (CHead c1 k u1) x) ->
                              (EX u2 c2 | x = (CHead c2 k u2) &
                                          (subst1 i v u1 u2) &
                                          (csubst1 i v c1 c2)
                              ).
      Proof.
      Intros; XElim H; Clear x; Intros.
(* case 1: csubst1_refl *)
      XDEAuto 2.
(* case 2: csubst1_sing *)
      CSubst0GenBase; Subst; SGen; XDEAuto 4.
      Qed.

   End csubst1_gen_base.

      Tactic Definition CSubst1GenBase := (
         Match Context With
            | [ H: (csubst1 (s ?4 ?1) ?2 (CHead ?3 ?4 ?5) ?6) |- ? ] ->
               LApply (csubst1_gen_head ?4 ?3 ?6 ?5 ?2 ?1); [ Clear H; Intros H | XAuto ];
               XDecompose H
            | [ H: (csubst1 (S ?1) ?2 (CHead ?3 (Bind ?4) ?5) ?6) |- ? ] ->
               LApply (csubst1_gen_head (Bind ?4) ?3 ?6 ?5 ?2 ?1); [ Clear H; Intros H | XAuto ];
               XDecompose H
         ).

   Section csubst1_getl. (***************************************************)

      Lemma csubst1_getl_ge: (i,n:?) (le i n) ->
                             (c1,c2:?; v:?) (csubst1 i v c1 c2) ->
                             (e:?) (getl n c1 e) -> (getl n c2 e).
      Proof.
      Intros until 2; XElim H0; Clear c2; Intros;
      Try CSubst0GetL; XAuto.
      Qed.

      Lemma csubst1_getl_lt: (i,n:?) (lt n i) ->
                             (c1,c2:?; v:?) (csubst1 i v c1 c2) ->
                             (e1:?) (getl n c1 e1) ->
                             (EX e2 | (csubst1 (minus i n) v e1 e2) &
                                      (getl n c2 e2)
                             ).
      Proof.
      Intros until 2; XElim H0; Clear c2; Intros;
      (Rewrite minus_x_Sy; [ Idtac | XAuto ]);
      Try CSubst0GetL; Subst; XDEAuto 4.
      Qed.

      Lemma csubst1_getl_ge_back : (i,n:?) (le i n) ->
                                   (c1,c2:?; v:?) (csubst1 i v c1 c2) ->
                                   (e:?) (getl n c2 e) -> (getl n c1 e).
      Proof.
      Intros until 2; XElim H0; Clear c2; Intros;
      Try CSubst0GetL; XAuto.
      Qed.

   End csubst1_getl.

      Tactic Definition CSubst1GetL := (
         Match Context With
            | [ H1: (lt ?2 ?1);
                H2: (csubst1 ?1 ?3 ?4 ?5); H3: (getl ?2 ?4 ?6) |- ? ] ->
               LApply (csubst1_getl_lt ?1 ?2); [ Intros H_x | XAuto ];
               LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
               LApply (H_x ?6); [ Clear H_x H3; Intros H3 | XAuto ];
               XElim H3; Intros
            | [H2: (csubst1 ?1 ?3 ?4 ?5); H3: (getl ?1 ?4 ?6) |- ? ] ->
               LApply (csubst1_getl_ge ?1 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
               LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ]
            | [ H2: (csubst1 ?1 ?3 ?4 ?5); H3: (getl ?2 ?4 ?6) |- ? ] ->
               LApply (csubst1_getl_ge ?1 ?2); [ Intros H_x | XAuto ];
               LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
               LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ]
         ).