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

Require csubv_defs.
Require sc3_props.
Require csuba_props.
Require csubc_defs.

   Section csubc_drop. (*****************************************************)

(* NOTE: The constant (0) can not be generalized *)
      Lemma csubc_drop_conf_O: (g:?; c1,e1:?; h:?) (drop h (0) c1 e1) ->
                               (c2:?) (csubc g c1 c2) ->
                               (EX e2 | (drop h (0) c2 e2) & (csubc g e1 e2)).
      Proof.
      XElim c1.
(* case 1: CSort *)
      Intros; DropGenBase; Subst; XDEAuto 2.
(* case 2: CHead *)
      XElim h; Intros; DropGenBase; Subst.
(* case 2.1: h = 0 *)
      XDEAuto 2.
(* case 2.2: h > 0 *)
      CSubCGenBase.
(* case 2.2.1: csubc_head *)
      XDecomPoseClear H '(H ? ? H1 ? H5); XDEAuto 3.
(* case 2.2.2: csubc_abst *)
      XDecomPoseClear H '(H ? ? H1 ? H6); XDEAuto 3.
(* case 2.2.3: csubc_void *)
      XDecomPoseClear H '(H ? ? H1 ? H7); XDEAuto 3.
      Qed.

      Lemma drop_csubc_trans: (g:?; c2,e2:?; d,h:?) (drop h d c2 e2) ->
                              (e1:?) (csubc g e2 e1) ->
                              (EX c1 | (drop h d c1 e1) & (csubc g c2 c1)).
      Proof.
      XElim c2.
(* case 1: CSort *)
      Intros; DropGenBase; Subst; XDEAuto 2.
(* case 2: CHead *)
      XElim d.
(* case 2.1: d = 0 *)
      XElim h; Intros; DropGenBase; Subst.
(* case 2.1.1: h = 0 *)
      XDEAuto 2.
(* case 2.1.2: h > 0 *)
      XDecomPoseClear H '(H ? ? ? H1 ? H2); XDEAuto 4.
(* case 2.2: d = 0 *)
      Intros; DropGenBase; Subst; CSubCGenBase.
(* case 2.2.1: csubc_head *)
      XDecomPoseClear H '(H ? ? ? H4 ? H5); XDEAuto 4.
(* case 2.2.2: csubc_abst *)
      XDecomPoseClear H '(H ? ? ? H4 ? H6); XDEAuto 6.
(* case 2.2.3: csubc_void *)
      XDecomPoseClear H '(H ? ? ? H4 ? H7); XDEAuto 4.
      Qed.

      Lemma csubc_drop_conf_rev: (g:?; c2,e2:?; d,h:?) (drop h d c2 e2) ->
                                 (e1:?) (csubc g e1 e2) ->
                                 (EX c1 | (drop h d c1 e1) &
                                          (csubc g c1 c2)
                                 ).
      Proof.
      XElim c2.
(* case 1: CSort *)
      Intros; DropGenBase; Subst; XDEAuto 2.
(* case 2: CHead *)
      XElim d.
(* case 2.1: d = 0 *)
      XElim h; Intros; DropGenBase; Subst.
(* case 2.1.1: h = 0 *)
      XDEAuto 2.
(* case 2.1.2: h > 0 *)
      XDecomPoseClear H '(H ? ? ? H1 ? H2); XDEAuto 4.
(* case 2.2: d = 0 *)
      Intros; DropGenBase; Subst; CSubCGenBase.
(* case 2.2.1: csubc_head *)
      XDecomPoseClear H '(H ? ? ? H4 ? H5); XDEAuto 4.
(* case 2.2.2: csubc_abst *)
      XDecomPoseClear H '(H ? ? ? H4 ? H6); XDEAuto 6.
(* case 2.2.3: csubc_void *)
      XDecomPoseClear H '(H ? ? ? H4 ? H7); XDEAuto 4.
      Qed.

   End csubc_drop.

      Tactic Definition CSubCDrop := (
         Match Context With
            | [ H1: (drop ? ? ? ?0); H2: (csubc ? ?0 ?) |- ? ] ->
               XDecomPoseClear H1 '(drop_csubc_trans ? ? ? ? ? H1 ? H2); Clear H2
            | [ H1: (drop ? ? ? ?0); H2: (csubc ? ? ?0) |- ? ] ->
               XDecomPoseClear H1 '(csubc_drop_conf_rev ? ? ? ? ? H1 ? H2); Clear H2
            | [ H1: (drop ? O ?0 ?); H2: (csubc ? ?0 ?) |- ? ] ->
               XDecomPoseClear H1 '(csubc_drop_conf_O ? ? ? ? H1 ? H2); Clear H1 H2
         ).

   Section csubc_drop1. (****************************************************)

      Lemma drop1_csubc_trans: (g:?; hds:?; c2,e2:?) (drop1 hds c2 e2) ->
                               (e1:?) (csubc g e2 e1) ->
                               (EX c1 | (drop1 hds c1 e1) &
                                        (csubc g c2 c1)
                               ).
      Proof.
      XElim hds; Intros; Drop1GenBase.
(* case 1: PNil *)
      XDEAuto 2.
(* case 2: PCons *)
      XDecomPoseClear H '(H ? ? H3 ? H1); Clear H3 H1.
      CSubCDrop; XDEAuto 3.
      Qed.

      Lemma csubc_drop1_conf_rev: (g:?; hds:?; c2,e2:?) (drop1 hds c2 e2) ->
                                  (e1:?) (csubc g e1 e2) ->
                                  (EX c1 | (drop1 hds c1 e1) &
                                           (csubc g c1 c2)
                                  ).
      Proof.
      XElim hds; Intros; Drop1GenBase.
(* case 1: PNil *)
      XDEAuto 2.
(* case 2: PCons *)
      XDecomPoseClear H '(H ? ? H3 ? H1); Clear H3 H1.
      CSubCDrop; XDEAuto 3.
      Qed.

   End csubc_drop1.

      Tactic Definition CSubCDrop1 := (
         Match Context With
            | [ H1: (drop1 ? ? ?0); H2: (csubc ? ?0 ?) |- ? ] ->
               XDecomPoseClear H1 '(drop1_csubc_trans ? ? ? ? H1 ? H2); Clear H2
            | [ H1: (drop1 ? ? ?0); H2: (csubc ? ? ?0) |- ? ] ->
               XDecomPoseClear H1 '(csubc_drop1_conf_rev ? ? ? ? H1 ? H2); Clear H2
            | [ |- ? ] -> CSubCDrop
         ).

   Section csubc_clear. (****************************************************)

      Lemma csubc_clear_conf: (g:?; c1,e1:?) (clear c1 e1) ->
                              (c2:?) (csubc g c1 c2) ->
                              (EX e2 | (clear c2 e2) & (csubc g e1 e2)).
      Proof.
      Intros until 1; XElim H; Clear c1 e1; Intros;
      CSubCGenBase; XInv; Subst; Try XDecomPoseClear H0 '(H0 ? H4); XDEAuto 3.
      Qed.

   End csubc_clear.

      Tactic Definition CSubCClear := (
         Match Context With
            | [ H1: (clear ?0 ?); H2: (csubc ? ?0 ?) |- ? ] ->
               XDecomPoseClear H1 '(csubc_clear_conf ? ? ? H1 ? H2); Clear H2
         ).

   Section csubc_getl. (*****************************************************)

      Lemma csubc_getl_conf: (g:?; c1,e1:?; i:?) (getl i c1 e1) ->
                             (c2:?) (csubc g c1 c2) ->
                             (EX e2 | (getl i c2 e2) & (csubc g e1 e2)).
      Proof.
      Intros; GetLGenBase; CSubCDrop; CSubCClear; XDEAuto 3.
      Qed.

   End csubc_getl.

      Tactic Definition CSubCGetL := (
         Match Context With
            | [ H1: (getl ? ?0 ?); H2: (csubc ? ?0 ?) |- ? ] ->
               XDecomPoseClear H1 '(csubc_getl_conf ? ? ? ? H1 ? H2)
         ).

   Section csubc_arity. (****************************************************)

      Hints Resolve csubc_csuba csuba_arity csuba_arity_rev : ld.

      Lemma csubc_arity_conf: (g:?; c1,c2:?) (csubc g c1 c2) -> (t:?; a:?)
                              (arity g c1 t a) -> (arity g c2 t a).
      Proof.
      Intros; XDEAuto 3.
      Qed.

      Lemma csubc_arity_trans: (g:?; c1,c2:?) (csubc g c1 c2) ->
                               (csubv c1 c2) -> (t:?; a:?)
                               (arity g c2 t a) -> (arity g c1 t a).
      Proof.
      Intros; XDEAuto 3.
      Qed.

   End csubc_arity.