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

Require getl_props.
Require pc3_props.
Require pc3_gen.
Require ty3_defs.
Require ty3_gen.
Require ty3_lift.

   Section ty3_correct. (****************************************************)

      Hints Resolve getl_drop : ld.

      Lemma ty3_correct: (g:?; c:?; t1,t2:?)
                         (ty3 g c t1 t2) -> (EX t | (ty3 g c t2 t)).
      Proof.
      Intros; XElim H; Intros.
(* case 1: ty3_conv *)
      XDEAuto 2.
(* case 2: ty3_sort *)
      XDEAuto 2.
(* case 3: ty3_abbr *)
      XDecompose H1; XDEAuto 4.
(* case 4: ty3_abst *)
      XDEAuto 4.
(* case 5: ty3_bind *)
      XDecompose H2; XDEAuto 3.
(* case 6: ty3_appl *)
      XDecompose H0; XDecompose H2; Intros.
      Ty3GenBase; XDEAuto 4.
(* case 7 : ty3_cast *)
      XDecompose H2; XDEAuto 3.
      Qed.

   End ty3_correct.

      Tactic Definition Ty3Correct := (
         Match Context With
            | [ _: (ty3 ?1 ?2 ?3 ?4) |- ? ] ->
               LApply (ty3_correct ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
               XElim H_x; Intros until 1
         ).

   Section ty3_unique. (*****************************************************)

      Hints Resolve getl_drop pc3_s pc3_t : ld.

      Opaque pc3.

      Theorem ty3_unique: (g:?; c:?; u,t1:?) (ty3 g c u t1) ->
                          (t2:?) (ty3 g c u t2) -> (pc3 c t1 t2).
      Proof.
      Intros until 1; XElim H; Intros.
(* case 1: ty3_conv *)
      XDEAuto 4.
(* case 2: ty3_sort *)
      Ty3GenBase; XAuto.
(* case 3: ty3_abbr *)
      Ty3GenBase; GetLDis; XInv; Subst; XDEAuto 5.
(* case 4: ty3_abst *)
      Ty3GenBase; GetLDis; XInv; Subst; XDEAuto 5.
(* case 5: ty3_bind *)
      Ty3GenBase; XDEAuto 4.
(* case 6: ty3_appl *)
      Ty3GenBase; EApply pc3_t; [ Idtac | EApply H3 ]; XDEAuto 3.
(* case 7: ty3_cast *)
      Ty3GenBase; XDEAuto 4.
      Qed.

   End ty3_unique.

      Tactic Definition Ty3Dis := (
         Match Context With
            | [ H1: (ty3 ?0 ?1 ?2 ?); H2: (ty3 ?0 ?1 ?2 ?) |- ? ] ->
               XPoseClear H1 '(ty3_unique ? ? ? ? H1 ? H2); Clear H2
         ).

   Section ty3_xgen_base. (**************************************************)

      Hints Resolve ty3_conv : ld.

      Lemma ty3_gen_abst_abst: (g:?; c:?; u,t1,t2:?)
                               (ty3 g c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2)) ->
                               (EX w | (ty3 g c u w) &
                                       (ty3 g (CHead c (Bind Abst) u) t1 t2)
                                 ).
      Proof.
      Intros.
      Ty3Correct. Repeat Ty3GenBase. Pc3Gen; XDEAuto 3.
      Qed.

   End ty3_xgen_base.

      Tactic Definition Ty3XGenBase := (
         Match Context With
            | [ H: (ty3 ? ? (THead (Bind Abst) ?0 ?) (THead (Bind Abst) ?0 ?)) |- ? ] ->
               XDecomPoseClear H '(ty3_gen_abst_abst ? ? ? ? ? H)
            | [ |- ? ] -> Ty3GenBase
         ).

  Section ty3_typecheck. (***************************************************)

      Lemma ty3_typecheck: (g:?; c:?; t,v:?) (ty3 g c t v) ->
                           (EX u | (ty3 g c (THead (Flat Cast) v t) u)).
      Proof.
      Intros. Ty3Correct. XDEAuto 3.
      Qed.

   End ty3_typecheck.

   Section ty3_getl_subst0. (************************************************)

      Lemma ty3_getl_subst0: (g:?; c:?; t,u:?) (ty3 g c t u) ->
                             (v0,t0:?; i:?) (subst0 i v0 t t0) ->
                             (b:?; d:?; v:?)
                             (getl i c (CHead d (Bind b) v)) ->
                             (EX w | (ty3 g d v w)).
      Proof.
      Intros until 1; XElim H; Clear c t u; Intros.
(* case 1: ty3_conv *)
      XDEAuto 2.
(* case 2: ty3_sort *)
      Subst0GenBase.
(* case 3: ty3_abbr *)
      Subst0GenBase; Subst; GetLDis; XInv; Subst; XDEAuto 2.
(* case 4: ty3_abst *)
      Subst0GenBase; Subst; GetLDis; XInv; Subst; XDEAuto 2.
(* case 5: ty3_bind *)
      Subst0GenBase; Subst; [ Idtac | Simpl in H5 | Simpl in H6 ]; XDEAuto 3.
(* case 6: ty3_appl *)
      Subst0GenBase; Subst; XDEAuto 2.
(* case 7: ty3_cast *)
      Subst0GenBase; Subst; XDEAuto 2.
      Qed.

   End ty3_getl_subst0.

      Tactic Definition Ty3GetLSubst0 := (
         Match Context With
            | [ H1: (ty3 ? ?1 ?2 ?); H2: (subst0 ?3 ? ?2 ?);
                H3: (getl ?3 ?1 (CHead ? (Bind ?) ?)) |- ? ] ->
               XDecomPose '(ty3_getl_subst0 ? ? ? ? H1 ? ? ? H2 ? ? ? H3)
         ).