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

      Inductive sty0 [g:G]: C -> T -> T -> Prop :=
         | sty0_sort: (c:?; n:?) (sty0 g c (TSort n) (TSort (next g n)))
         | sty0_abbr: (c,d:?; v:?; i:?) (getl i c (CHead d (Bind Abbr) v)) ->
                      (w:?) (sty0 g d v w) ->
                      (sty0 g c (TLRef i) (lift (S i) (0) w))
         | sty0_abst: (c,d:?; v:?; i:?) (getl i c (CHead d (Bind Abst) v)) ->
                      (w:?) (sty0 g d v w) ->
                      (sty0 g c (TLRef i) (lift (S i) (0) v))
         | sty0_bind: (b:?; c:?; v,t1,t2:?)
                      (sty0 g (CHead c (Bind b) v) t1 t2) ->
                      (sty0 g c (THead (Bind b) v t1) (THead (Bind b) v t2))
         | sty0_appl: (c:?; v,t1,t2:?) (sty0 g c t1 t2) ->
                      (sty0 g c (THead (Flat Appl) v t1) (THead (Flat Appl) v t2))
         | sty0_cast: (c:?; v1,v2:?) (sty0 g c v1 v2) ->
                      (t1,t2:?) (sty0 g c t1 t2) ->
                      (sty0 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v2 t2)).

      Hint sty0: ld := Constructors sty0.

   Section sty0_gen_base. (**************************************************)

      Lemma sty0_gen_sort: (g:?; c:?; x:?; n:?) (sty0 g c (TSort n) x) ->
                           x = (TSort (next g n)).
      Proof.
      Intros until 1; InsertEq H '(TSort n); XElim H; Clear c y x;
      Intros; XInv; Subst; XAuto.
      Qed.

      Lemma sty0_gen_lref: (g:?; c:?; x:?; n:?) (sty0 g c (TLRef n) x) ->
                           (EX e u t | (getl n c (CHead e (Bind Abbr) u)) &
                                       (sty0 g e u t) &
                                       x = (lift (S n) (0) t)
                           ) \/
                           (EX e u t | (getl n c (CHead e (Bind Abst) u)) &
                                       (sty0 g e u t) &
                                       x = (lift (S n) (0) u)
                           ).
      Proof.
      Intros until 1; InsertEq H '(TLRef n); XElim H; Clear c y x;
      Intros; XInv; Subst; XDEAuto 3.
      Qed.

      Lemma sty0_gen_bind: (g:?; b:?; c:?; u,t1,x:?) (sty0 g c (THead (Bind b) u t1) x) ->
                           (EX t2 | (sty0 g (CHead c (Bind b) u) t1 t2) &
                                     x = (THead (Bind b) u t2)
                           ).
      Proof.
      Intros until 1; InsertEq H '(THead (Bind b) u t1); XElim H; Clear c y x;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

      Lemma sty0_gen_appl: (g:?; c:?; u,t1,x:?) (sty0 g c (THead (Flat Appl) u t1) x) ->
                           (EX t2 | (sty0 g c t1 t2) &
                                           x = (THead (Flat Appl) u t2)
                           ).
      Proof.
      Intros until 1; InsertEq H '(THead (Flat Appl) u t1); XElim H; Clear c y x;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

      Lemma sty0_gen_cast: (g:?; c:?; v1,t1,x:?)
                           (sty0 g c (THead (Flat Cast) v1 t1) x) ->
                           (EX v2 t2 | (sty0 g c v1 v2) & (sty0 g c t1 t2) &
                                       x = (THead (Flat Cast) v2 t2)
                           ).
      Proof.
      Intros until 1; InsertEq H '(THead (Flat Cast) v1 t1); XElim H; Clear c y x;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

   End sty0_gen_base.

      Tactic Definition STy0GenBase := (
         Match Context With
            | [ H: (sty0 ? ? (TSort ?) ?) |- ? ] ->
               XPoseClear H '(sty0_gen_sort ? ? ? ? H); XInv; Subst
            | [ H: (sty0 ? ? (TLRef ?) ?) |- ? ] ->
               XDecomPoseClear H '(sty0_gen_lref ? ? ? ? H); XInv; Subst
            | [ H: (sty0 ? ? (THead (Bind ?) ? ?) ?) |- ? ] ->
               XDecomPoseClear H '(sty0_gen_bind ? ? ? ? ? ? H); XInv; Subst
            | [ H: (sty0 ? ? (THead (Flat Appl) ? ?) ?) |- ? ] ->
               XDecomPoseClear H '(sty0_gen_appl ? ? ? ? ? H); XInv; Subst
            | [ H: (sty0 ? ? (THead (Flat Cast) ? ?) ?) |- ? ] ->
               XDecomPoseClear H '(sty0_gen_cast ? ? ? ? ? H); XInv; Subst
         ).