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

Require app_defs.
Require ty3_props.
Require ty3_sred.
Require ty3_dec.
Require wf3_defs.

   Section wf3_props. (******************************************************)

      Lemma wf3_total: (g:?; c1:?) (EX c2 | (wf3 g c1 c2)).
      Proof.
      XElim c1; Intros.
(* case 1: CSort *)
      XDEAuto 2.
(* case 2: CHead *)
      XDecompose H; NewInduction k.
(* case 2.1: Bind *)
      XDecomPose '(ty3_inference g c t); XDEAuto 3.
(* case 2.2:Flat *)
      XDEAuto 3.
      Qed.

      Lemma getl_wf3_trans: (i:?; c1,d1:?) (getl i c1 d1) ->
                            (g:?; d2:?) (wf3 g d1 d2) ->
                            (EX c2 | (wf3 g c1 c2) & (getl i c2 d2)).
      Proof.
      XElim i.
(* case 1: i = 0 *)
      Intros; GetLGenBase.
      XDecomPose '(clear_wf3_trans ? ? H ? ? H0); Clear H H0; XDEAuto 3.
(* case 2: i > 0 *)
      XElim c1; Intros; GetLGenBase.
      NewInduction k; Simpl in H1.
(* case 2.1; Bind *)
      Clear H0; XDecomPoseClear H '(H ? ? H1 ? ? H2); Clear H1 H2.
      XDecomPose '(ty3_inference g c t); XDEAuto 4.
(* case 2.2; Flat *)
      Clear H; XDecomPoseClear H0 '(H0 ? H1 ? ? H2); Clear H1 H2; XDEAuto 3.
      Qed.

      Lemma ty3_shift1: (g:?; c:?) (wf3 g c c) ->
                        (t1,t2:?) (ty3 g c t1 t2) ->
                        (ty3 g (CSort (cbk c)) (app1 c t1) (app1 c t2)).
      Proof.
      Intros until 1; InsertEq H c; XElim H; Clear c y;
      Intros; XInv; Subst; Simpl.
(* case 1: wf3_sort *)
      XAuto.
(* case 2: wf3_bind *)
      Ty3Correct; XDEAuto 3.
(* case 3: wf3_void *)
      Ty3Correct; XDEAuto 3.
(* case 2: wf3_flat *)
      WF3GenBase.
      Qed.

   End wf3_props.

      Hints Resolve ty3_shift1 : ld.

      Tactic Definition WF3Props := (
         Match Context With
            | [ H1: (getl ? ? (CHead ?2 (Bind ?1) ?4)); H2: (wf3 ?0 ?2 ?3);
                H3: (ty3 ?0 ?2 ?4 ?) |- ? ] ->
               LApply (getl_wf3_trans ? ? ? H1 ?0 (CHead ?3 (Bind ?1) ?4));
               [ Clear H1 H2 H3; Intros H1; XDecompose H1 | XDEAuto 2 ]
            | [ |- ? ] -> WF3PropsBase
         ).

   Section wf3_ty3_conf. (***************************************************)

      Lemma wf3_pr2_conf: (g:?; c1:?; t1,t2:?) (pr2 c1 t1 t2) ->
                          (c2:?) (wf3 g c1 c2) -> (u:?) (ty3 g c1 t1 u) ->
                          (pr2 c2 t1 t2).
      Proof.
      Intros until 1; XElim H; Clear c1 t1 t2; Intros.
(* case 1: pr2_free *)
      XAuto.
(* case 2: pr2_delta *)
      Ty3SRed; Ty3GetLSubst0; WF3Props; XDEAuto 2.
      Qed.

      Hints Resolve pr3_sing wf3_pr2_conf ty3_sred_pr2 : ld.

      Lemma wf3_pr3_conf: (g:?; c1:?; t1,t2:?) (pr3 c1 t1 t2) ->
                          (c2:?) (wf3 g c1 c2) -> (u:?) (ty3 g c1 t1 u) ->
                          (pr3 c2 t1 t2).
      Proof.
      Intros until 1; XElim H; Clear t1 t2; XDEAuto 5.
      Qed.

      Hints Resolve wf3_pr3_conf : ld.

      Lemma wf3_pc3_conf: (g:?; c1:?; t1,t2:?) (pc3 c1 t1 t2) ->
                          (c2:?) (wf3 g c1 c2) ->
                          (u1:?) (ty3 g c1 t1 u1) ->
                          (u2:?) (ty3 g c1 t2 u2) ->
                          (pc3 c2 t1 t2).
      Proof.
      Intros; Pc3Unfold; XDEAuto 4.
      Qed.

      Hints Resolve ty3_conv wf3_pc3_conf : ld.

      Lemma wf3_ty3_conf: (g:?; c1:?; t1,t2:?) (ty3 g c1 t1 t2) ->
                          (c2:?) (wf3 g c1 c2) -> (ty3 g c2 t1 t2).
      Proof.
      Intros until 1; XElim H; Clear c1 t1 t2; Intros.
(* case 1: ty3_conv *)
      Ty3Correct; XDEAuto 5.
(* case 2: ty3_conv *)
      XAuto.
(* case 3: ty3_abbr *)
      WF3Props; XDEAuto 3.
(* case 4: ty3_abst *)
      WF3Props; XDEAuto 3.
(* case 5: ty3_bind *)
      XDEAuto 5.
(* case 6: ty3_appl *)
      XDEAuto 4.
(* case 7: ty3_cast *)
      XDEAuto 4.
      Qed.

   End wf3_ty3_conf.

   Section wf3_more_props. (*************************************************)

      Hints Resolve wf3_ty3_conf : ld.

      Lemma wf3_idem: (g:?; c1,c2:?) (wf3 g c1 c2) -> (wf3 g c2 c2).
      Proof.
      Intros until 1; XElim H; Clear c1 c2; XDEAuto 3.
      Qed.

      Lemma wf3_ty3: (g:?; c1:?; t,u:?) (ty3 g c1 t u) ->
                     (EX c2 | (wf3 g c1 c2) & (ty3 g c2 t u)).
      Proof.
      Intros; XDecomPose '(wf3_total g c1); XDEAuto 3.
      Qed.

   End wf3_more_props.