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

   Section csubt_pc3. (*****************************************************)

      Lemma csubt_pr2: (g:?; c1:?; t1,t2:?) (pr2 c1 t1 t2) ->
                       (c2:?) (csubt g c1 c2) -> (pr2 c2 t1 t2).
      Proof.
      Intros until 1; XElim H; Clear c1 t1 t2; Intros.
(* case 1: pr2_free *)
      XAuto.
(* case 2: pr2_delta *)
      CSubTGetL; XDEAuto 2.
      Qed.

      Hints Resolve pc3_t ty3_conv csubt_pr2 : ld.

      Opaque pc3.

      Lemma csubt_pc3: (g:?; c1:?; t1,t2:?) (pc3 c1 t1 t2) ->
                       (c2:?) (csubt g c1 c2) -> (pc3 c2 t1 t2).
      Proof.
      Intros until 1; XElimUsing pc3_ind_left H; XDEAuto 5.
      Qed.

   End csubt_pc3.

   Section csubt_ty3. (*****************************************************)

      Hints Resolve csubt_pc3 : ld.

      Lemma csubt_ty3: (g:?; c1:?; t1,t2:?) (ty3 g c1 t1 t2) ->
                       (c2:?) (csubt g c1 c2) -> (ty3 g c2 t1 t2).
      Proof.
      Intros until 1; XElim H; Intros.
(* case 1: ty3_conv *)
      EApply ty3_conv; XDEAuto 2.
(* case 2: ty3_sort *)
      XDEAuto 2.
(* case 3: ty3_abbr *)
      CSubTGetL; EApply ty3_abbr; XDEAuto 2.
(* case 4: ty3_abst *)
      CSubTGetL; [ EApply ty3_abst | EApply ty3_abbr ]; XDEAuto 2.
(* case 5: ty3_bind *)
      EApply ty3_bind; XDEAuto 3.
(* case 6: ty3_appl *)
      EApply ty3_appl; XDEAuto 2.
(* case 7: ty3_cast *)
      EApply ty3_cast; XAuto.
      Qed.

      Lemma csubt_ty3_ld: (g:?; c:?; u,v:?) (ty3 g c u v) -> (t1,t2:?)
                          (ty3 g (CHead c (Bind Abst) v) t1 t2) ->
                          (ty3 g (CHead c (Bind Abbr) u) t1 t2).
      Proof.
      Intros; EApply csubt_ty3; XDEAuto 2.
      Qed.

   End csubt_ty3.

      Tactic Definition CSub0Ty3 := (
         Match Context With
            | [ _: (ty3 ?1 ?2 ?4 ?); _: (ty3 ?1 ?2 ?3 ?7); _: (pc3 ?2 ?4 ?7);
                H: (ty3 ?1 (CHead ?2 (Bind Abst) ?4) ?5 ?6) |- ? ] ->
               LApply (csubt_ty3_ld ?1 ?2 ?3 ?4); [ Intros H_x | EApply ty3_conv; XDEAuto 2 ];
               LApply (H_x ?5 ?6); [ Clear H_x H; Intros | XAuto ]
         ).