(****************************************************************************)
(*                                                                          *)
(*                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 getl_defs.
Require Export levels_defs.

      Inductive arity [g:G] : C -> T -> A -> Prop :=
         | arity_sort: (c:?; n:?) (arity g c (TSort n) (ASort (0) n))
         | arity_abbr: (c,d:?; u:?; i:?)
                       (getl i c (CHead d (Bind Abbr) u)) ->
                       (a:?) (arity g d u a) ->
                       (arity g c (TLRef i) a)
         | arity_abst: (c,d:?; u:?; i:?)
                       (getl i c (CHead d (Bind Abst) u)) ->
                       (a:?) (arity g d u (asucc g a)) ->
                       (arity g c (TLRef i) a)
         | arity_bind: (b:?) ~b=Abst ->
                       (c:?; u:?; a1:?) (arity g c u a1) ->
                       (t:?; a2:?) (arity g (CHead c (Bind b) u) t a2) ->
                       (arity g c (THead (Bind b) u t) a2)
         | arity_head: (c:?; u:?; a1:?) (arity g c u (asucc g a1)) ->
                       (t:?; a2:?) (arity g (CHead c (Bind Abst) u) t a2) ->
                       (arity g c (THead (Bind Abst) u t) (AHead a1 a2))
         | arity_appl: (c:?; u:?; a1:?) (arity g c u a1) ->
                       (t:?; a2:?) (arity g c t (AHead a1 a2)) ->
                       (arity g c (THead (Flat Appl) u t) a2)
         | arity_cast: (c:?; u:?; a:?) (arity g c u (asucc g a)) ->
                       (t:?) (arity g c t a) ->
                       (arity g c (THead (Flat Cast) u t) a)
         | arity_repl: (c:?; t:?; a1:?) (arity g c t a1) ->
                       (a2:?) (leq g a1 a2) -> (arity g c t a2).

      Hints Resolve arity_sort arity_abbr arity_abst arity_bind arity_head
                    arity_appl arity_cast : ld.

   Section arity_gen_base. (*************************************************)

      Hints Resolve leq_sym leq_trans : ld.

      Lemma arity_gen_sort: (g:?; c:?; n:?; a:?)
                            (arity g c (TSort n) a) -> (leq g a (ASort (0) n)).
      Proof.
      Intros; InsertEq H '(TSort n); XElim H; Intros;
      XInv; Subst; XDEAuto 4.
      Qed.

      Hints Resolve arity_repl : ld.

      Lemma arity_gen_lref: (g:?; c:?; i:?; a:?) (arity g c (TLRef i) a) ->
                            (EX d u | (getl i c (CHead d (Bind Abbr) u)) &
                                      (arity g d u a)
                            ) \/
                            (EX d u | (getl i c (CHead d (Bind Abst) u)) &
                                      (arity g d u (asucc g a))
                            ).
      Proof.
      Intros; InsertEq H '(TLRef i); XElim H; Intros;
      XInv; Subst.
(* case 2: arity_abbr *)
      XDEAuto 3.
(* case 3: arity_abst *)
      XDEAuto 3.
(* case 8: arity_repl *)
      LApply H0; [ Clear H0; Intros H0 | XAuto ].
      XDecompose H0; XDEAuto 5.
      Qed.

      Lemma arity_gen_bind: (b:?) ~b=Abst -> (g:?; c:?; u,t:?; a2:?)
                            (arity g c (THead (Bind b) u t) a2) ->
                            (EX a1 | (arity g c u a1) &
                                     (arity g (CHead c (Bind b) u) t a2)
                            ).
      Proof.
      Intros until 2; InsertEq H0 '(THead (Bind b) u t); XElim H0; Intros;
      XInv; Subst.
(* case 4: arity_bind *)
      XDEAuto 3.
(* case 5: arity_head *)
      EqFalse.
(* case 8: arity_repl *)
      LApply H1; [ Clear H1; Intros H1 | XAuto ].
      XDecompose H1; XDEAuto 3.
      Qed.

      Lemma arity_gen_abst: (g:?; c:?; u,t:?; a:?)
                            (arity g c (THead (Bind Abst) u t) a) ->
                            (EX a1 a2 | a = (AHead a1 a2) &
                                        (arity g c u (asucc g a1)) &
                                        (arity g (CHead c (Bind Abst) u) t a2)
                            ).
      Proof.
      Intros; InsertEq H '(THead (Bind Abst) u t); XElim H; Intros;
      XInv; Subst.
(* case 4: arity_bind *)
      EqFalse.
(* case 5: arity_head *)
      XDEAuto 2.
(* case 8: arity_repl *)
      LApply H0; [ Clear H0; Intros H0 | XAuto ].
      XDecompose H0; Subst; LEqGenBase; XDEAuto 5.
      Qed.

      Lemma arity_gen_appl: (g:?; c:?; u,t:?; a2:?)
                            (arity g c (THead (Flat Appl) u t) a2) ->
                            (EX a1 | (arity g c u a1) &
                                     (arity g c t (AHead a1 a2))
                            ).
      Proof.
      Intros; InsertEq H '(THead (Flat Appl) u t); XElim H; Intros;
      XInv; Subst.
(* case 6: arity_appl *)
      XDEAuto 2.
(* case 8: arity_repl *)
      LApply H0; [ Clear H0; Intros H0 | XAuto ].
      XDecompose H0; XDEAuto 4.
      Qed.

      Lemma arity_gen_cast: (g:?; c:?; u,t:?; a:?)
                            (arity g c (THead (Flat Cast) u t) a) ->
                            (arity g c u (asucc g a)) /\ (arity g c t a).
      Proof.
      Intros; InsertEq H '(THead (Flat Cast) u t); XElim H; Intros;
      XInv; Subst.
(* case 6: arity_appl *)
      XDEAuto 2.
(* case 8: arity_repl *)
      LApply H0; [ Clear H0; Intros H0 | XAuto ].
      XDecompose H0; XDEAuto 5.
      Qed.

   End arity_gen_base.

      Tactic Definition ArityGenBase := (
         Match Context With
            | [ H: (arity ?0 ?1 (TSort ?2) ?3) |- ? ] ->
               LApply (arity_gen_sort ?0 ?1 ?2 ?3); [ Clear H; Intros | XAuto ]
            | [ H: (arity ?0 ?1 (TLRef ?2) ?3) |- ? ] ->
               LApply (arity_gen_lref ?0 ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
               XDecompose H
            | [ H: (arity ?0 ?1 (THead (Bind Abbr) ?3 ?4) ?5) |- ? ] ->
               LApply (arity_gen_bind Abbr); [ Intros H_y | XAuto ];
               XDecomPose '(H_y ? ? ? ? ? H); Clear H H_y
            | [ H0: ~?2=Abst;
                H1: (arity ?0 ?1 (THead (Bind ?2) ?3 ?4) ?5) |- ? ] ->
               LApply (arity_gen_bind ?2); [ Intros H_x | XAuto ];
               LApply (H_x ?0 ?1 ?3 ?4 ?5); [ Clear H_x H1; Intros H1 | XAuto ];
               XDecompose H1
            | [ H: (arity ?0 ?1 (THead (Bind Abst) ?3 ?4) ?5) |- ? ] ->
               LApply (arity_gen_abst ?0 ?1 ?3 ?4 ?5); [ Clear H; Intros H | XAuto ];
               XDecompose H; Subst
            | [ H: (arity ?0 ?1 (THead (Flat Appl) ?3 ?4) ?5) |- ? ] ->
               LApply (arity_gen_appl ?0 ?1 ?3 ?4 ?5); [ Clear H; Intros H | XAuto ];
               XDecompose H
            | [ H: (arity ?0 ?1 (THead (Flat Cast) ?3 ?4) ?5) |- ? ] ->
               LApply (arity_gen_cast ?0 ?1 ?3 ?4 ?5); [ Clear H; Intros H | XAuto ];
               XDecompose H
         ).

   Section arities_gen_base. (***********************************************)

      Lemma arity_gen_appls: (g:?; c:?; t:?; vs:?; a2:?)
                             (arity g c (THeads (Flat Appl) vs t) a2) ->
                             (EX a | (arity g c t a)).
      Proof.
      XElim vs; Simpl; Intros.
(* case 1: TNil *)
      XDEAuto 2.
(* case 2: TCons *)
      ArityGenBase; XDecomPoseClear H '(H ? H2); Clear H2; XDEAuto 2.
      Qed.

   End arities_gen_base.

      Tactic Definition AritiesGenBase := (
         Match Context With
            | [ H: (arity ? ? (THeads (Flat Appl) ? ?) ?) |- ? ] ->
               XDecomPoseClear H '(arity_gen_appls ? ? ? ? ? H)
            | [ |- ? ] -> ArityGenBase
         ).

   Section arity_props_base. (***********************************************)

      Lemma node_inh: (g:?; n,k:?) (EX c t | (arity g c t (ASort k n))).
      Proof.
      XElim k; Intros.
(* case 1: k = 0 *)
      EApply ex_2_intro with x0:=(CSort (0)); XAuto.
(* case 2: k > 0 *)
      XDecompose H; XDEAuto 3.
      Qed.

   End arity_props_base.