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

(* NOTE: this preorder should be swapped *)
      Inductive csubt [g:G] : C -> C -> Prop :=
         | csubt_sort: (n:?) (csubt g (CSort n) (CSort n))
         | csubt_head: (c1,c2:?) (csubt g c1 c2) -> (k,u:?)
                       (csubt g (CHead c1 k u) (CHead c2 k u))
         | csubt_void: (c1,c2:?) (csubt g c1 c2) -> (b:?) ~b=Void -> (u1,u2:?)
                       (csubt g (CHead c1 (Bind Void) u1) (CHead c2 (Bind b) u2))
         | csubt_abst: (c1,c2:?) (csubt g c1 c2) ->
                       (u,t:?) (ty3 g c1 u t) -> (ty3 g c2 u t) ->
                       (csubt g (CHead c1 (Bind Abst) t) (CHead c2 (Bind Abbr) u)).

      Hint csubt : ld := Constructors csubt.

   Section csubt_gen_base. (*************************************************)

      Lemma csubt_gen_abbr: (g:?; e1,c2:?; v:?) (csubt g (CHead e1 (Bind Abbr) v) c2) ->
                            (EX e2 | c2 = (CHead e2 (Bind Abbr) v) & (csubt g e1 e2)).
      Proof.
      Intros; InsertEq H '(CHead e1 (Bind Abbr) v); XElim H; Clear y c2;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

      Lemma csubt_gen_abst: (g:?; e1,c2:?; v1:?) (csubt g (CHead e1 (Bind Abst) v1) c2) ->
                            (EX e2 | c2 = (CHead e2 (Bind Abst) v1) & (csubt g e1 e2)) \/
                            (EX e2 v2 | c2 = (CHead e2 (Bind Abbr) v2) &
                                        (csubt g e1 e2) &
                                        (ty3 g e1 v2 v1) & (ty3 g e2 v2 v1)
                            ).
      Proof.
      Intros; InsertEq H '(CHead e1 (Bind Abst) v1); XElim H; Clear y c2;
      Intros; XInv; Subst; XDEAuto 3.
      Qed.

      Lemma csubt_gen_flat: (g:?; e1,c2:?; v:?; f:?) (csubt g (CHead e1 (Flat f) v) c2) ->
                            (EX e2 | c2 = (CHead e2 (Flat f) v) & (csubt g e1 e2)).
      Proof.
      Intros; InsertEq H '(CHead e1 (Flat f) v); XElim H; Clear y c2;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

      Lemma csubt_gen_bind: (g:?; b1:?; e1,c2:?; v1:?) (csubt g (CHead e1 (Bind b1) v1) c2) ->
                            (EX b2 e2 v2 | c2 = (CHead e2 (Bind b2) v2) & (csubt g e1 e2)).
      Proof.
      Intros; InsertEq H '(CHead e1 (Bind b1) v1); XElim H; Clear y c2;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

   End csubt_gen_base.

      Tactic Definition CSubTGenBase := (
         Match Context With
            | [ H: (csubt ?0 (CHead ?1 (Bind Abbr) ?3) ?4) |- ? ] ->
             LApply (csubt_gen_abbr ?0 ?1 ?4 ?3); [ Clear H; Intros H | XAuto ];
             XDecompose H
            | [ H: (csubt ?0 (CHead ?1 (Bind Abst) ?3) ?4) |- ? ] ->
             LApply (csubt_gen_abst ?0 ?1 ?4 ?3); [ Clear H; Intros H | XAuto ];
             XDecompose H
            | [ H: (csubt ?0 (CHead ?1 (Bind ?2) ?3) ?4) |- ? ] ->
             LApply (csubt_gen_bind ?0 ?2 ?1 ?4 ?3); [ Clear H; Intros H | XAuto ];
             XDecompose H
            | [ H: (csubt ?0 (CHead ? (Flat ?) ?) ?) |- ? ] ->
             XDecomPoseClear H '(csubt_gen_flat ? ? ? ? ? H)
         ).

   Section csubt_props. (****************************************************)

      Lemma csubt_refl: (g:?; c:?) (csubt g c c).
      Proof.
      XElim c; XAuto.
      Qed.

      Lemma csubt_clear_conf: (g:?; c1,c2:?) (csubt g c1 c2) ->
                              (e1:?) (clear c1 e1) ->
                              (EX e2 | (csubt g e1 e2) & (clear c2 e2)).
      Proof.
      Intros until 1; XElim H; Clear c1 c2; Intros;
      Try NewInduction k; ClearGenBase;
      Try (LApply (H0 e1); [ Clear H0 H1; Intros H0 | XAuto ]; XDecompose H0);
      XDEAuto 3.
      Qed.

   End csubt_props.

      Hints Resolve csubt_refl : ld.

      Tactic Definition CSubTClear := (
         Match Context With
            | [ H1: (csubt ?0 ?1 ?2); H2: (clear ?1 ?3) |- ? ] ->
               LApply (csubt_clear_conf ?0 ?1 ?2); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
               XDecompose H1
         ).

   Section csubt_drop. (*****************************************************)

      Lemma csubt_drop_flat: (g:?; f:?; n:?; c1,c2:?) (csubt g c1 c2) -> (d1,u:?)
                             (drop n (0) c1 (CHead d1 (Flat f) u)) ->
                             (EX d2 | (csubt g d1 d2) &
                                      (drop n (0) c2 (CHead d2 (Flat f) u))
                             ).
      Proof.
      XElim n.
(* case 1 : n = 0 *)
      Intros; DropGenBase; Subst; CSubTGenBase; Subst; XDEAuto 2.
(* case 2 : n > 0 *)
      Intros until 2; XElim H0.
(* case 2.1 : csubt_sort *)
      Intros; DropGenBase; XInv; XInv.
(* case 2.2 : csubt_head *)
      XElim k; Intros; DropGenBase.
(* case 2.2.1 : Bind *)
      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
      LApply (H d1 u0); [ Clear H; Intros H | XAuto ].
      XElim H; XDEAuto 3.
(* case 2.2.2 : Flat *)
      LApply (H1 d1 u0); [ Clear H1; Intros H1 | XAuto ].
      XElim H1; XDEAuto 3.
(* case 2.3 : csubt_void *)
      Intros; DropGenBase.
      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
      LApply (H d1 u); [ Clear H; Intros H | XAuto ].
      XElim H; XDEAuto 3.
(* case 2.4 : csubt_abst *)
      Intros; DropGenBase.
      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
      LApply (H d1 u0); [ Clear H; Intros H | XAuto ].
      XElim H; XDEAuto 3.
      Qed.

      Lemma csubt_drop_abbr: (g:?; n:?; c1,c2:?) (csubt g c1 c2) -> (d1,u:?)
                             (drop n (0) c1 (CHead d1 (Bind Abbr) u)) ->
                             (EX d2 | (csubt g d1 d2) &
                                      (drop n (0) c2 (CHead d2 (Bind Abbr) u))
                             ).
      Proof.
      XElim n.
(* case 1 : n = 0 *)
      Intros; DropGenBase; Subst; CSubTGenBase; Subst; XDEAuto 2.
(* case 2 : n > 0 *)
      Intros until 2; XElim H0.
(* case 2.1 : csubt_sort *)
      Intros; DropGenBase; XInv; XInv.
(* case 2.2 : csubt_head *)
      XElim k; Intros; DropGenBase.
(* case 2.2.1 : Bind *)
      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
      LApply (H d1 u0); [ Clear H; Intros H | XAuto ].
      XElim H; XDEAuto 3.
(* case 2.2.2 : Flat *)
      LApply (H1 d1 u0); [ Clear H1; Intros H1 | XAuto ].
      XElim H1; XDEAuto 3.
(* case 2.3 : csubt_void *)
      Intros; DropGenBase.
      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
      LApply (H d1 u); [ Clear H; Intros H | XAuto ].
      XElim H; XDEAuto 3.
(* case 2.4 : csubt_abst *)
      Intros; DropGenBase.
      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
      LApply (H d1 u0); [ Clear H; Intros H | XAuto ].
      XElim H; XDEAuto 3.
      Qed.

      Lemma csubt_drop_abst: (g:?; n:?; c1,c2:?) (csubt g c1 c2) -> (d1,t:?)
                             (drop n (0) c1 (CHead d1 (Bind Abst) t)) ->
                             (EX d2 | (csubt g d1 d2) &
                                      (drop n (0) c2 (CHead d2 (Bind Abst) t))

                             ) \/
                             (EX d2 u | (csubt g d1 d2) &
                                        (drop n (0) c2 (CHead d2 (Bind Abbr) u)) &
                                        (ty3 g d1 u t) & (ty3 g d2 u t)
                             ).
      Proof.
      XElim n.
(* case 1 : n = 0 *)
      Intros; DropGenBase; Subst; CSubTGenBase; Subst; XDEAuto 3.
(* case 2 : n > 0 *)
      Intros until 2; XElim H0.
(* case 2.1 : csubt_sort *)
      Intros; DropGenBase; XInv; XInv.
(* case 2.2 : csubt_head *)
      XElim k; Intros; DropGenBase.
(* case 2.2.1 : Bind *)
      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
      LApply (H d1 t); [ Clear H; Intros H | XAuto ].
      XElim H; Intros; XElim H; XDEAuto 4.
(* case 2.2.2 : Flat *)
      LApply (H1 d1 t); [ Clear H1; Intros H1 | XAuto ].
      XElim H1; Intros; XElim H1; XDEAuto 4.
(* case 2.3 : csubt_void *)
      Intros; DropGenBase.
      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
      LApply (H d1 t); [ Clear H; Intros H | XAuto ].
      XElim H; Intros; XElim H; XDEAuto 4.
(* case 2.4 : csubt_abst *)
      Intros; DropGenBase.
      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
      LApply (H d1 t0); [ Clear H; Intros H | XAuto ].
      XElim H; Intros; XElim H; XDEAuto 4.
      Qed.

   End csubt_drop.

      Tactic Definition CSubTDrop := (
         Match Context With
            | [ H1: (csubt ?1 ?2 ?3);
                H2: (drop ?4 (0) ?2 (CHead ?5 (Flat ?0) ?6)) |- ? ] ->
               LApply (csubt_drop_flat ?1 ?0 ?4 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
               XElim H1; Intros
            | [ H1: (csubt ?1 ?2 ?3);
                H2: (drop ?4 (0) ?2 (CHead ?5 (Bind Abbr) ?6)) |- ? ] ->
               LApply (csubt_drop_abbr ?1 ?4 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
               XElim H1; Intros
            | [ H1: (csubt ?1 ?2 ?3);
                H2: (drop ?4 (0) ?2 (CHead ?5 (Bind Abst) ?6)) |- ? ] ->
               LApply (csubt_drop_abst ?1 ?4 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
               XElim H1; Intros H1; XElim H1; Intros
         ).

   Section csubt_getl. (*****************************************************)

      Lemma csubt_getl_abbr: (g:?; c1,d1:?; u:?; n:?) (getl n c1 (CHead d1 (Bind Abbr) u)) ->
                             (c2:?) (csubt g c1 c2) ->
                             (EX d2 | (csubt g d1 d2) &
                                      (getl n c2 (CHead d2 (Bind Abbr) u))
                             ).
      Proof.
      Intros until 1; GetLGenBase; NewInduction x;
      Try NewInduction k; ClearGenBase; Clear IHx.
(* case 1: Bind *)
      XInv; Subst; CSubTDrop; XDEAuto 3.
(* case 2: Flat *)
      Impl H1 H0; UnIntro H1 c1.
      XElim n; Intros; Rename x into c.
(* case 2.1: n = 0 *)
      DropGenBase; Subst.
      LApply (clear_flat c (CHead d1 (Bind Abbr) u)); [ Clear H1; Intros H1 | XAuto ].
      XPoseClear H1 '(H1 f t); CSubTClear; CSubTGenBase; Subst; XDEAuto 3.
(* case 2.2: n > 0 *)
      DropClear; CSubTClear; CSubTGenBase; Subst.
      LApply (H x2); [ Clear H H4; Intros H | XAuto ].
      LApply (H x5); [ Clear H H5; Intros H | XAuto ].
      XDecompose H; XDEAuto 3.
      Qed.

      Lemma csubt_getl_abst: (g:?; c1,d1:?; t:?; n:?) (getl n c1 (CHead d1 (Bind Abst) t)) ->
                             (c2:?) (csubt g c1 c2) ->
                             (EX d2 | (csubt g d1 d2) &
                                      (getl n c2 (CHead d2 (Bind Abst) t))
                             ) \/
                             (EX d2 u | (csubt g d1 d2) &
                                        (getl n c2 (CHead d2 (Bind Abbr) u)) &
                                        (ty3 g d1 u t) & (ty3 g d2 u t)
                             ).
      Proof.
      Intros until 1; GetLGenBase; NewInduction x;
      Try NewInduction k; ClearGenBase; Clear IHx.
(* case 1: Bind *)
      XInv; Subst; CSubTDrop; XDEAuto 4.
(* case 2: Flat *)
      Impl H1 H0; UnIntro H1 c1.
      XElim n; Intros; Rename x into c.
(* case 2.1: n = 0 *)
      DropGenBase; Subst.
      LApply (clear_flat c (CHead d1 (Bind Abst) t)); [ Clear H1; Intros H1 | XAuto ].
      XPoseClear H1 '(H1 f t0); CSubTClear; CSubTGenBase; Subst; XDEAuto 4.
(* case 2.2: n > 0 *)
      DropClear; CSubTClear; CSubTGenBase; Subst.
      LApply (H x2); [ Clear H H4; Intros H | XAuto ].
      LApply (H x5); [ Clear H H5; Intros H | XAuto ].
      XDecompose H; XDEAuto 4.
      Qed.

   End csubt_getl.

      Tactic Definition CSubTGetL := (
         Match Context With
            | [ H2: (csubt ?1 ?2 ?3);
                H1: (getl ?4 ?2 (CHead ?5 (Bind Abbr) ?6)) |- ? ] ->
               LApply (csubt_getl_abbr ?1 ?2 ?5 ?6 ?4); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
               XDecompose H1
            | [ H2: (csubt ?1 ?2 ?3);
                H1: (getl ?4 ?2 (CHead ?5 (Bind Abst) ?6)) |- ? ] ->
               LApply (csubt_getl_abst ?1 ?2 ?5 ?6 ?4); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
               XDecompose H1
         ).