(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basic_2/notation/relations/degree_6.ma".
include "basic_2/grammar/genv.ma".
include "basic_2/substitution/drop.ma".
include "basic_2/static/sd.ma".

(* DEGREE ASSIGNMENT FOR TERMS **********************************************)

(* activate genv *)
inductive da (h:sh) (o:sd h): relation4 genv lenv term nat ≝
| da_sort: ∀G,L,s,d. deg h o s d → da h o G L (⋆s) d
| da_ldef: ∀G,L,K,V,i,d. ⬇[i] L ≡ K.ⓓV → da h o G K V d → da h o G L (#i) d
| da_ldec: ∀G,L,K,W,i,d. ⬇[i] L ≡ K.ⓛW → da h o G K W d → da h o G L (#i) (d+1)
| da_bind: ∀a,I,G,L,V,T,d. da h o G (L.ⓑ{I}V) T d → da h o G L (ⓑ{a,I}V.T) d
| da_flat: ∀I,G,L,V,T,d. da h o G L T d → da h o G L (ⓕ{I}V.T) d
.

interpretation "degree assignment (term)"
   'Degree h o G L T d = (da h o G L T d).

(* Basic inversion lemmas ***************************************************)

fact da_inv_sort_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d →
                      ∀s0. T = ⋆s0 → deg h o s0 d.
#h #o #G #L #T #d * -G -L -T -d
[ #G #L #s #d #Hkd #s0 #H destruct //
| #G #L #K #V #i #d #_ #_ #s0 #H destruct
| #G #L #K #W #i #d #_ #_ #s0 #H destruct
| #a #I #G #L #V #T #d #_ #s0 #H destruct
| #I #G #L #V #T #d #_ #s0 #H destruct
]
qed-.

lemma da_inv_sort: ∀h,o,G,L,s,d. ⦃G, L⦄ ⊢ ⋆s ▪[h, o] d → deg h o s d.
/2 width=5 by da_inv_sort_aux/ qed-.

fact da_inv_lref_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d → ∀j. T = #j →
                      (∃∃K,V. ⬇[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, o] d) ∨
                      (∃∃K,W,d0. ⬇[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, o] d0 &
                                 d = d0 + 1
                       ).
#h #o #G #L #T #d * -G -L -T -d
[ #G #L #s #d #_ #j #H destruct
| #G #L #K #V #i #d #HLK #HV #j #H destruct /3 width=4 by ex2_2_intro, or_introl/
| #G #L #K #W #i #d #HLK #HW #j #H destruct /3 width=6 by ex3_3_intro, or_intror/
| #a #I #G #L #V #T #d #_ #j #H destruct
| #I #G #L #V #T #d #_ #j #H destruct
]
qed-.

lemma da_inv_lref: ∀h,o,G,L,j,d. ⦃G, L⦄ ⊢ #j ▪[h, o] d →
                   (∃∃K,V. ⬇[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, o] d) ∨
                   (∃∃K,W,d0. ⬇[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, o] d0 & d = d0+1).
/2 width=3 by da_inv_lref_aux/ qed-.

fact da_inv_gref_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d → ∀p0. T = §p0 → ⊥.
#h #o #G #L #T #d * -G -L -T -d
[ #G #L #s #d #_ #p0 #H destruct
| #G #L #K #V #i #d #_ #_ #p0 #H destruct
| #G #L #K #W #i #d #_ #_ #p0 #H destruct
| #a #I #G #L #V #T #d #_ #p0 #H destruct
| #I #G #L #V #T #d #_ #p0 #H destruct
]
qed-.

lemma da_inv_gref: ∀h,o,G,L,p,d. ⦃G, L⦄ ⊢ §p ▪[h, o] d → ⊥.
/2 width=9 by da_inv_gref_aux/ qed-.

fact da_inv_bind_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d →
                      ∀b,J,X,Y. T = ⓑ{b,J}Y.X → ⦃G, L.ⓑ{J}Y⦄ ⊢ X ▪[h, o] d.
#h #o #G #L #T #d * -G -L -T -d
[ #G #L #s #d #_ #b #J #X #Y #H destruct
| #G #L #K #V #i #d #_ #_ #b #J #X #Y #H destruct
| #G #L #K #W #i #d #_ #_ #b #J #X #Y #H destruct
| #a #I #G #L #V #T #d #HT #b #J #X #Y #H destruct //
| #I #G #L #V #T #d #_ #b #J #X #Y #H destruct
]
qed-.

lemma da_inv_bind: ∀h,o,b,J,G,L,Y,X,d. ⦃G, L⦄ ⊢ ⓑ{b,J}Y.X ▪[h, o] d → ⦃G, L.ⓑ{J}Y⦄ ⊢ X ▪[h, o] d.
/2 width=4 by da_inv_bind_aux/ qed-.

fact da_inv_flat_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d →
                      ∀J,X,Y. T = ⓕ{J}Y.X → ⦃G, L⦄ ⊢ X ▪[h, o] d.
#h #o #G #L #T #d * -G -L -T -d
[ #G #L #s #d #_ #J #X #Y #H destruct
| #G #L #K #V #i #d #_ #_ #J #X #Y #H destruct
| #G #L #K #W #i #d #_ #_ #J #X #Y #H destruct
| #a #I #G #L #V #T #d #_ #J #X #Y #H destruct
| #I #G #L #V #T #d #HT #J #X #Y #H destruct //
]
qed-.

lemma da_inv_flat: ∀h,o,J,G,L,Y,X,d. ⦃G, L⦄ ⊢ ⓕ{J}Y.X ▪[h, o] d → ⦃G, L⦄ ⊢ X ▪[h, o] d.
/2 width=5 by da_inv_flat_aux/ qed-.