(****************************************************************************)
(*                                                                          *)
(*                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 csuba_defs.
Require Export sc3_defs.

(* NOTE: this preorder should be swapped *)
      Inductive csubc [g:G] : C -> C -> Prop :=
         | csubc_sort: (n:?) (csubc g (CSort n) (CSort n))
         | csubc_head: (c1,c2:?) (csubc g c1 c2) ->
                       (k:?; v:?) (csubc g (CHead c1 k v) (CHead c2 k v))
         | csubc_void: (c1,c2:?) (csubc g c1 c2) -> (b:?) ~b=Void -> (u1,u2:?)
                       (csubc g (CHead c1 (Bind Void) u1) (CHead c2 (Bind b) u2))
         | csubc_abst: (c1,c2:?) (csubc g c1 c2) ->
                       (v:?; a:?) (sc3 g (asucc g a) c1 v) ->
                       (w:?) (sc3 g a c2 w) ->
                       (csubc g (CHead c1 (Bind Abst) v) (CHead c2 (Bind Abbr) w)).

      Hint csubc : ld := Constructors csubc.

   Section csubc_gen_base. (*************************************************)

      Lemma csubc_gen_sort_l: (g:?; x:?; n:?) (csubc g (CSort n) x) ->
                              x = (CSort n).
      Proof.
      Intros; InsertEq H '(CSort n); XElim H; Clear y x;
      Intros; XInv; Subst; XAuto.
      Qed.

      Lemma csubc_gen_head_l: (g:?; c1,x:?; v:?; k:?)
                              (csubc g (CHead c1 k v) x) -> (OR
                              (EX c2 | x = (CHead c2 k v) &
                                       (csubc g c1 c2)
                                    ) |
                              (EX c2 w a | k = (Bind Abst) &
                                           x = (CHead c2 (Bind Abbr) w) &
                                           (csubc g c1 c2) &
                                           (sc3 g (asucc g a) c1 v) &
                                           (sc3 g a c2 w)
                              ) |
                              (EX b c2 v2 | x = (CHead c2 (Bind b) v2) &
                                              k = (Bind Void) & ~b=Void &
                                             (csubc g c1 c2)
                              )).
      Proof.
      Intros; InsertEq H '(CHead c1 k v); XElim H; Clear y x;
      Intros; XInv; Subst; XDEAuto 3.
      Qed.

      Lemma csubc_gen_sort_r: (g:?; x:?; n:?) (csubc g x (CSort n)) ->
                              x = (CSort n).
      Proof.
      Intros; InsertEq H '(CSort n); XElim H; Clear y x;
      Intros; XInv; Subst; XAuto.
      Qed.

      Lemma csubc_gen_head_r: (g:?; c2,x:?; w:?; k:?)
                              (csubc g x (CHead c2 k w)) -> (OR
                              (EX c1 | x = (CHead c1 k w) &
                                       (csubc g c1 c2)
                              ) |
                              (EX c1 v a | k = (Bind Abbr) &
                                           x = (CHead c1 (Bind Abst) v) &
                                           (csubc g c1 c2) &
                                           (sc3 g (asucc g a) c1 v) &
                                           (sc3 g a c2 w)
                              ) |
                              (EX b c1 v1 | x = (CHead c1 (Bind Void) v1) &
                                            k = (Bind b) & ~b=Void &
                                            (csubc g c1 c2)
                              )).
      Proof.
      Intros; InsertEq H '(CHead c2 k w); XElim H; Clear y x;
      Intros; XInv; Subst; XDEAuto 3.
      Qed.

   End csubc_gen_base.

      Tactic Definition CSubCGenBase := (
         Match Context With
            | [ H: (csubc ? (CSort ?) ?) |- ? ] ->
               XPoseClear H '(csubc_gen_sort_l ? ? ? H); Subst
            | [ H: (csubc ? (CHead ? ? ?) ?) |- ? ] ->
               XDecomPoseClear H '(csubc_gen_head_l ? ? ? ? ? H); Subst
            | [ H: (csubc ? ? (CSort ?)) |- ? ] ->
               XPoseClear H '(csubc_gen_sort_r ? ? ? H); Subst
            | [ H: (csubc ? ? (CHead ? ? ?)) |- ? ] ->
               XDecomPoseClear H '(csubc_gen_head_r ? ? ? ? ? H); Subst
         ).

   Section csubc_props_base. (***********************************************)

      Lemma csubc_refl: (g:?; c:?) (csubc g c c).
      Proof.
      XElim c; XAuto.
      Qed.

      Hints Resolve sc3_arity_gen : ld.

      Lemma csubc_csuba: (g:?; c1,c2:?) (csubc g c1 c2) -> (csuba g c1 c2).
      Proof.
      Intros until 1; XElim H; Clear c1 c2; Intros; XDEAuto 4.
      Qed.

   End csubc_props_base.

      Hints Resolve csubc_refl : ld.