(****************************************************************************)
(*                                                                          *)
(*                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 contexts_defs.
Require Export lift_defs.

      Inductive subst0 : nat -> T -> T -> T -> Prop :=
         | subst0_lref: (v:?; i:?) (subst0 i v (TLRef i) (lift (S i) (0) v))
         | subst0_fst : (v,u2,u1:?; i:?) (subst0 i v u1 u2) ->
                        (t:?; k:?) (subst0 i v (THead k u1 t) (THead k u2 t))
         | subst0_snd : (k:?; v,t2,t1:?; i:?) (subst0 (s k i) v t1 t2) -> (u:?)
                        (subst0 i v (THead k u t1) (THead k u t2))
         | subst0_both: (v,u1,u2:?; i:?) (subst0 i v u1 u2) ->
                        (k:?; t1,t2:?) (subst0 (s k i) v t1 t2) ->
                        (subst0 i v (THead k u1 t1) (THead k u2 t2)).

      Hint subst0 : ld := Constructors subst0.

   Section subst0_gen_base. (************************************************)

      Lemma subst0_gen_sort: (v,x:?; i,n:?) (subst0 i v (TSort n) x) ->
                             (P:Prop) P.
      Proof.
      Intros; InsertEq H '(TSort n); XElim H; Clear i v y x; Intros; XInv.
      Qed.

      Lemma subst0_gen_lref: (v,x:?; i,n:?) (subst0 i v (TLRef n) x) ->
                             n = i /\ x = (lift (S n) (0) v).
      Proof.
      Intros; InsertEq H '(TLRef n); XElim H; Clear i v y x;
      Intros; XInv; Subst; XAuto.
      Qed.

      Lemma subst0_gen_head: (k:?; v,u1,t1,x:?; i:?)
                             (subst0 i v (THead k u1 t1) x) -> (OR
                             (EX u2 | x = (THead k u2 t1) &
                                      (subst0 i v u1 u2)) |
                             (EX t2 | x = (THead k u1 t2) &
                                      (subst0 (s k i) v t1 t2)) |
                             (EX u2 t2 | x = (THead k u2 t2) &
                                         (subst0 i v u1 u2) &
                                         (subst0 (s k i) v t1 t2))
                             ).

      Proof.
      Intros; InsertEq H '(THead k u1 t1); XElim H; Clear i v y x;
      Intros; XInv; Subst; XDEAuto 3.
      Qed.

   End subst0_gen_base.

      Tactic Definition Subst0GenBase := (
         Match Context With
            | [ H: (subst0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
               Apply (subst0_gen_sort ?2 ?4 ?1 ?3); Apply H
            | [ H: (subst0 ?1 ?2 (TLRef ?3) ?4) |- ? ] ->
               LApply (subst0_gen_lref ?2 ?4 ?1 ?3); [ Clear H; Intros H | XAuto ];
               XElim H; Intros
            | [ H: (subst0 ?1 ?2 (THead ?3 ?4 ?5) ?6) |- ? ] ->
               LApply (subst0_gen_head ?3 ?2 ?4 ?5 ?6 ?1); [ Clear H; Intros H | XAuto ];
               XElim H; Intros H; XElim H; Intros
         ).

   Section subst0_props. (***************************************************)

      Lemma subst0_refl: (u,t:?; d:?) (subst0 d u t t) -> (P:Prop) P.
      Proof.
      XElim t; Intros; Subst0GenBase; Subst.
(* case 2: TLRef *)
      LiftGenBase.
(* case 3.1: THead first operand *)
      XInv; Subst; EApply H; XDEAuto 1.
(* case 3.2: THead second operand *)
      XInv; Subst; EApply H0; XDEAuto 1.
(* case 3.3: THead second operand *)
      XInv; Subst; EApply H; XDEAuto 1.
      Qed.

   End subst0_props.

      Tactic Definition Subst0XGenBase := (
         Match Context With
            | [ _: (subst0 ? ? ?0 ?0) |- ? ] ->
               EApply subst0_refl; XDEAuto 2
            | [ |- ? ] -> Subst0GenBase
         ).