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

Require pc3_props.
Require ty3_defs.

   Section ty3_gen_base. (***************************************************)

      Hints Resolve pc3_t : ld.

      Lemma ty3_gen_sort: (g:?; c:?; x:?; n:?)
                          (ty3 g c (TSort n) x) ->
                          (pc3 c (TSort (next g n)) x).
      Proof.
      Intros until 1; InsertEq H '(TSort n); XElim H; Intros;
      XInv; Subst; XDEAuto 3.
      Qed.

      Lemma ty3_gen_lref: (g:?; c:?; x:?; n:?) (ty3 g c (TLRef n) x) ->
                          (EX e u t | (pc3 c (lift (S n) (0) t) x) &
                                      (getl n c (CHead e (Bind Abbr) u)) &
                                      (ty3 g e u t)
                          ) \/
                          (EX e u t | (pc3 c (lift (S n) (0) u) x) &
                                      (getl n c (CHead e (Bind Abst) u)) &
                                      (ty3 g e u t)
                          ).
      Proof.
      Intros until 1; InsertEq H '(TLRef n); XElim H; Intros;
      XInv; Subst.
(* case 1: ty3_conv *)
      LApply H2; [ Clear H2; Intros H2 | XAuto ].
      XDecompose H2; XDEAuto 4.
(* case 3: ty3_abbr *)
      XDEAuto 3.
(* case 4: ty3_abst *)
      XDEAuto 3.
      Qed.

      Lemma ty3_gen_bind: (g:?; b:?; c:?; u,t1,x:?) (ty3 g c (THead (Bind b) u t1) x) ->
                          (EX t2 t | (pc3 c (THead (Bind b) u t2) x) &
                                     (ty3 g c u t) &
                                     (ty3 g (CHead c (Bind b) u) t1 t2)
                          ).
      Proof.
      Intros until 1; InsertEq H '(THead (Bind b) u t1); XElim H; Intros;
      XInv; Subst.
(* case 1: ty3_conv *)
      LApply H2; [ Clear H2; Intros H2 | XAuto ].
      XDecompose H2; XDEAuto 3.
(* case 5: ty3_bind *)
      XDEAuto 2.
      Qed.

      Lemma ty3_gen_appl: (g:?; c:?; w,v,x:?) (ty3 g c (THead (Flat Appl) w v) x) ->
                          (EX u t | (pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x) &
                                    (ty3 g c v (THead (Bind Abst) u t)) &
                                    (ty3 g c w u)
                          ).
      Proof.
      Intros until 1; InsertEq H '(THead (Flat Appl) w v); XElim H; Intros;
      XInv; Subst.
(* case 1: ty3_conv *)
      LApply H2; [ Clear H2; Intros H2 | XAuto ].
      XDecompose H2; XDEAuto 3.
(* case 6: ty3_appl *)
      XDEAuto 2.
      Qed.

      Lemma ty3_gen_cast: (g:?; c:?; t1,t2,x:?)
                          (ty3 g c (THead (Flat Cast) t2 t1) x) ->
                          (EX t0 | (pc3 c (THead (Flat Cast) t0 t2) x) &
                                   (ty3 g c t1 t2) & (ty3 g c t2 t0)
                          ).
      Proof.
      Intros until 1; InsertEq H '(THead (Flat Cast) t2 t1); XElim H; Intros;
      XInv; Subst.
(* case 1: ty3_conv *)
      LApply H2; [ Clear H2; Intros H2 | XAuto ].
      XDecompose H2; XDEAuto 3.
(* case 7: ty3_cast *)
      XDEAuto 2.
      Qed.

   End ty3_gen_base.

   Section tys3_gen_base. (**************************************************)

      Lemma tys3_gen_nil: (g:?; c:?; u:?) (tys3 g c TNil u) ->
                          (EX u0 | (ty3 g c u u0)).
      Proof.
      Intros; InsertEq H TNil; XElim H; Clear y u;
      Intros; XInv; XDEAuto 2.
      Qed.

      Lemma tys3_gen_cons: (g:?; c:?; ts:?; t,u:?)
                           (tys3 g c (TCons t ts) u) ->
                           (ty3 g c t u) /\ (tys3 g c ts u).
      Proof.
      Intros; InsertEq H '(TCons t ts); XElim H; Clear y u;
      Intros; XInv; Subst; XAuto.
      Qed.

   End tys3_gen_base.

      Tactic Definition Ty3GenBase := (
         Match Context With
            | [ H: (ty3 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
               LApply (ty3_gen_sort ?1 ?2 ?4 ?3); [ Clear H; Intros | XAuto ]
            | [ H: (ty3 ?1 ?2 (TLRef ?3) ?4) |- ? ] ->
               LApply (ty3_gen_lref ?1 ?2 ?4 ?3); [ Clear H; Intros H | XAuto ];
               XElim H; Intros H; XElim H; Intros
            | [ H: (ty3 ?1 ?2 (THead (Bind ?3) ?4 ?5) ?6) |- ? ] ->
               LApply (ty3_gen_bind ?1 ?3 ?2 ?4 ?5 ?6); [ Clear H; Intros H | XAuto ];
               XElim H; Intros
            | [ H: (ty3 ?1 ?2 (THead (Flat Appl) ?3 ?4) ?5) |- ? ] ->
               LApply (ty3_gen_appl ?1 ?2 ?3 ?4 ?5); [ Clear H; Intros H | XAuto ];
               XElim H; Intros
            | [ H: (ty3 ?1 ?2 (THead (Flat Cast) ?3 ?4) ?5) |- ? ] ->
               LApply (ty3_gen_cast ?1 ?2 ?4 ?3 ?5); [ Clear H; Intros H | XAuto ];
               XElim H; Intros
         ).

      Tactic Definition Tys3GenBase := (
         Match Context With
            | [ H: (tys3 ? ? TNil ?) |- ? ] ->
               XDecomPoseClear H '(tys3_gen_nil ? ? ? H)
            | [ H: (tys3 ? ? (TCons ? ?) ?) |- ? ] ->
               XDecomPoseClear H '(tys3_gen_cons ? ? ? ? ? H)
            | [ |- ? ] -> Ty3GenBase
         ).